bug(ldfi2): Fix lineage, don't try to be too clever

src/ldfi2/src/Ldfi.hs

@@ -33,18 +33,7 @@ type LDFIFormula = FormulaF LDFIVar
 
 lineage :: [Trace] -> LDFIFormula
 lineage ts =
-  -- Or [ makeVars t | t <- map nodes ts ]
-  let
-    vs  = map (foldMap $ Set.singleton . EventVar) ts
-    is  = foldl Set.intersection Set.empty vs
-    c   = \i j -> (i `Set.intersection` j) Set.\\ is
-    len = length vs `div` 2
-  in
-    makeVars is :&&
-    And [ makeVars (c i j) :&& (makeVars (i Set.\\ j) :|| makeVars (j Set.\\ i))
-        | i <- take len vs
-        , j <- drop len vs
-        ]
+  Or [ makeVars t | t <- map (foldMap $ Set.singleton . EventVar) ts ]
 
 affects :: Fault -> Event -> Bool
 affects (Omission (f, t) a) (Event f' t' a') = f == f' && t == t' && a == a'

src/ldfi2/test/LdfiTest.hs

@@ -118,7 +118,7 @@ broadcastFailureSpec = FailureSpec
 unit_broadcast1Run1 :: Assertion
 unit_broadcast1Run1 = do
   fs <- run (mockStorage (take 1 broadcast1Traces)) z3Solver dummyTestId broadcastFailureSpec
-  fs @?= []
+  fs @?= [ Omission ("A", "B") 1 ]
 
 unit_broadcast1Run2 :: Assertion
 unit_broadcast1Run2 = do
@@ -133,21 +133,22 @@ broadcast2Traces :: [Trace]
 broadcast2Traces = [ [Event "A" "B" 1, Event "A" "C" 1]
                    , [Event "A" "B" 1]
                    , [Event "A" "B" 2, Event "A" "C" 1]
-                   , [Event "A" "B" 1, Event "A" "C" 1]
+                   , [Event "A" "B" 4]
                    ]
 
 -- Lets assume that run 1 and 2 were the same as in broadcast1.
 unit_broadcast2Run3 :: Assertion
 unit_broadcast2Run3 = do
   fs <- run (mockStorage (take 3 broadcast2Traces)) z3Solver dummyTestId broadcastFailureSpec
-  fs @?= [Omission ("A", "C") 1]
+  fs @?= [Omission ("A", "B") 1, Omission ("A", "B") 2]
 
 unit_broadcast2Run4 :: Assertion
 unit_broadcast2Run4 = do
   fs <- run (mockStorage (take 4 broadcast2Traces)) z3Solver dummyTestId broadcastFailureSpec
   fs @?=
-    [ Omission ("A", "B") 1
-    , Crash "A" 2
+    [ Crash "B" 3
+    , Omission ("A", "B") 1
+    , Omission ("A", "B") 2
     ] -- Minimal counterexample.
 
 ------------------------------------------------------------------------