Merge pull request #131 from symbiont-io/ldfi-runnable

fix(ldfi2): marshalling of events and replace partial foldl1

src/ldfi2/app/Main.hs

@@ -10,7 +10,6 @@ import qualified Ldfi
 import Ldfi.FailureSpec (FailureSpec(FailureSpec))
 import qualified Ldfi.GitHash as Git
 import Ldfi.Sat (z3Solver)
-import Ldfi.Solver
 import Ldfi.Storage
 
 ------------------------------------------------------------------------

src/ldfi2/src/Ldfi.hs

@@ -31,10 +31,10 @@ type LDFIFormula = FormulaF LDFIVar
 
 lineage :: [Trace] -> LDFIFormula
 lineage ts =
-  -- Or [ makeVars t | t <- map nodes ts]
+  -- Or [ makeVars t | t <- map nodes ts ]
   let
-    vs = map (foldMap $ Set.singleton . EventVar) ts
-    is  = foldl1 Set.intersection vs
+    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
@@ -63,7 +63,9 @@ failureSemantic events failures = And
 -- Failure Specification. Although we will never generate any faults that occur
 -- later than eff, so we don't have to check that here
 failureSpecConstraint :: FailureSpec -> Set Fault -> LDFIFormula
-failureSpecConstraint fs faults = AtMost crashes (Nat.naturalToInt $ maxCrashes fs)
+failureSpecConstraint fs faults
+  | null crashes = TT
+  | otherwise    = AtMost crashes (Nat.naturalToInt $ maxCrashes fs)
   where
     crashes = [ FaultVar c | c@(Crash _ _) <- Set.toList faults]
 
@@ -118,10 +120,17 @@ makeFaults (Solution assign) =
   ]
 
 marshalFaults :: [Fault] -> Text
-marshalFaults  fs = "{\"faults\":" <> marshalList (map show fs) <> "}"
+marshalFaults  fs = "{\"faults\":" <> marshalList (map marshalFault fs) <> "}"
   where
-    marshalList :: [String] -> Text
-    marshalList = T.pack . show
+    marshalList :: [Text] -> Text
+    marshalList ts = "[" <> T.intercalate "," ts <> "]"
+
+    marshalFault :: Fault -> Text
+    marshalFault (Crash from at) =
+      "{\"kind\":\"crash\",\"from\":" <> T.pack (show from) <> ",\"at\":" <> T.pack (show at) <> "}"
+    marshalFault (Omission (from, to) at) =
+      "{\"kind\":\"omission\",\"from\":" <> T.pack (show from) <> ",\"to\":" <> T.pack (show to) <>
+      ",\"at\":" <> T.pack (show at) <> "}"
 
 run :: Monad m => Storage m -> Solver m -> TestId -> FailureSpec -> m [Fault]
 run Storage{load} Solver{solve} testId failureSpec = do

src/ldfi2/src/Ldfi/Prop.hs

@@ -53,32 +53,24 @@ getVars :: Ord var => FormulaF var -> Set var
 getVars = foldMap Set.singleton
 
 simplify1 :: FormulaF var -> FormulaF var
-simplify1 (TT :&& r)  = simplify1 r
-simplify1 (l  :&& r)  = simplify1 l :&& simplify1 r
-simplify1 (FF :|| r)  = simplify1 r
-simplify1 (_l :|| TT) = TT
-simplify1 (l  :|| r)  = simplify1 l :|| simplify1 r
-simplify1 (And [])    = TT
-simplify1 (And [f])   = f
-simplify1 (And fs)    = And (map simplify1 fs)
-simplify1 (Neg f)     = Neg (simplify1 f)
-simplify1 (l :<-> r)  = simplify1 l :<-> simplify1 r
-simplify1 (l :+ r)    = simplify1 l :+ simplify1 r
-simplify1 f           = f
-
--- simplify (TT :&& r)     = simplify r
--- simplify (And xs :&& y) = And (map simplify xs ++ [simplify y])
--- simplify (x :&& And ys) = And (simplify x : map simplify ys)
--- simplify (FF :|| r)     = simplify r
--- simplify (l  :|| r)     = simplify l :|| simplify r
--- simplify (And fs)       = case filter (/= TT) . (>>= expandAnd) $ map simplify fs of
---   [] -> TT
---   [f] -> f
---   fs' -> And fs'
---   where
---     expandAnd (And xs) = xs
---     expandAnd (l :&& r) = [l, r]
---     expandAnd f = [f]
+simplify1 (TT :&& r)    = simplify1 r
+simplify1 (l  :&& r)    = simplify1 l :&& simplify1 r
+simplify1 (FF :|| r)    = simplify1 r
+simplify1 (_l :|| TT)   = TT
+simplify1 (l  :|| r)    = simplify1 l :|| simplify1 r
+simplify1 (And [])      = TT
+simplify1 (And [f])     = f
+simplify1 (And fs)      = And (map simplify1 fs)
+simplify1 (Or [])       = FF
+simplify1 (Or [f])      = f
+simplify1 (Or fs)       = Or (map simplify1 fs)
+simplify1 (Neg f)       = Neg (simplify1 f)
+simplify1 (l :<-> r)    = simplify1 l :<-> simplify1 r
+simplify1 (l :+ r)      = simplify1 l :+ simplify1 r
+simplify1 f@(AtMost {}) = f
+simplify1 f@TT          = f
+simplify1 f@FF          = f
+simplify1 f@(Var _)     = f
 
 fixpoint :: Eq a => (a -> a) -> a -> a
 fixpoint f x | f x == x  = x