diff --git a/src/ldfi2/src/Ldfi.hs b/src/ldfi2/src/Ldfi.hs index 9373e298..03bfd887 100644 --- a/src/ldfi2/src/Ldfi.hs +++ b/src/ldfi2/src/Ldfi.hs @@ -4,6 +4,8 @@ module Ldfi where +import Data.IntMap (IntMap) +import qualified Data.IntMap as IntMap import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set @@ -57,7 +59,8 @@ failureSemantic events failures = And [ Var (EventVar event) :+ Or [ Var (FaultVar failure) | failure <- Set.toList failures , failure `affects` event] - | event <- Set.toList events] + | event <- Set.toList events + ] -- failureSpecConstraint is the formula that makes sure we are following the -- Failure Specification. Although we will never generate any faults that occur @@ -67,7 +70,7 @@ failureSpecConstraint fs faults | null crashes = TT | otherwise = AtMost crashes (Nat.naturalToInt $ maxCrashes fs) where - crashes = [ FaultVar c | c@(Crash _ _) <- Set.toList faults] + crashes = [ FaultVar c | c@(Crash _ _) <- Set.toList faults ] -- enumerateAllFaults will generate the interesting faults that could affect the -- set of events. But since it is pointless to generate a fault that is later @@ -82,11 +85,26 @@ failureSpecConstraint fs faults enumerateAllFaults :: Set Event -> FailureSpec -> Set Fault enumerateAllFaults events fs = Set.unions (Set.map possibleFailure events) where + eff :: Time eff = endOfFiniteFailures fs + + activeNodesAt :: IntMap (Set Node) + activeNodesAt = IntMap.fromListWith (<>) + [ (fromEnum at, Set.singleton from) + | Event from _to at <- Set.toList events + ] + + beenActive :: Node -> Time -> Bool + beenActive n t = case IntMap.lookup (fromEnum t) activeNodesAt of + Nothing -> False + Just ns -> Set.member n ns + possibleFailure :: Event -> Set Fault possibleFailure (Event f t a) - | eff < a = Set.singleton (Crash t eff) - | otherwise = Set.fromList [Omission (f,t) a, Crash t a] + | eff < a = Set.singleton (Crash t eff) + | otherwise = Set.fromList ([Omission (f, t) a] ++ + -- Only crash nodes that have sent something. + if beenActive t a then [Crash t a] else []) -- ldfi will produce a formula that if solved will give you: -- * Which faults to introduce diff --git a/src/ldfi2/test/LdfiTest.hs b/src/ldfi2/test/LdfiTest.hs index a9bde58e..73ddd113 100644 --- a/src/ldfi2/test/LdfiTest.hs +++ b/src/ldfi2/test/LdfiTest.hs @@ -113,21 +113,17 @@ broadcastFailureSpec = FailureSpec , endOfTime = 5 } --- TODO(stevan): this seems wrong, B hasn't sent anything. Should be `Omission --- "A" "B" 1` or `Omission "A" "C" 1`, can we make a variant of run that returns --- all possible models? +-- TODO(stevan): This seems wrong, should be `Omission "A" "B" 1` or `Omission +-- "A" "C" 1`, can we make a variant of run that returns all possible models? unit_broadcast1Run1 :: Assertion unit_broadcast1Run1 = do fs <- run (mockStorage (take 1 broadcast1Traces)) z3Solver dummyTestId broadcastFailureSpec - fs @?= [ Crash "B" 1 ] + fs @?= [] --- TODO(stevan): Lets assume this fault gets picked rather than omission between --- A and B, so that we need another concrete run. Can we force this selection somehow? unit_broadcast1Run2 :: Assertion unit_broadcast1Run2 = do fs <- run (mockStorage (take 2 broadcast1Traces)) z3Solver dummyTestId broadcastFailureSpec - fs @?= [ Crash "B" 1 ] -- XXX: should be: - -- [ Omission ("A", "B") 1 ] -- Minimal counterexample. + fs @?= [ Omission ("A", "B") 1 ] -- Minimal counterexample. ------------------------------------------------------------------------ @@ -144,10 +140,7 @@ broadcast2Traces = [ [Event "A" "B" 1, Event "A" "C" 1] unit_broadcast2Run3 :: Assertion unit_broadcast2Run3 = do fs <- run (mockStorage (take 3 broadcast2Traces)) z3Solver dummyTestId broadcastFailureSpec - fs @?= - [ Omission ("A", "B") 1 - , Omission ("A", "B") 2 - ] + fs @?= [Omission ("A", "C") 1] unit_broadcast2Run4 :: Assertion unit_broadcast2Run4 = do