fix(ldfi2): don't crash nodes until after they have sent something

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

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