Merge pull request #171 from symbiont-io/ldfi/limit-faults

feat(ldfi): Add optional limit of number of faults.

src/ldfi2/app/Main.hs

@@ -7,7 +7,7 @@ module Main where
 
 import qualified Data.Text.IO as T
 import qualified Ldfi
-import Ldfi.FailureSpec (FailureSpec(FailureSpec))
+import Ldfi.FailureSpec (FailureSpec (FailureSpec))
 import qualified Ldfi.GitHash as Git
 import Ldfi.Sat (z3Solver)
 import Ldfi.Storage
@@ -23,6 +23,7 @@ data Config = Config
     endOfFiniteFailures :: Maybe Int <?> "The logical time after which we can't generate faults",
     maxCrashes :: Maybe Int <?> "The number of crashes we are allowed to generate",
     endOfTime :: Maybe Int <?> "NOT USED",
+    limitNumberOfFaults :: Maybe Int <?> "Set a limit to the number of faults generated",
     version :: Bool <?> "Print the git commit this binary was built from"
   }
   deriving (Generic, Show)
@@ -38,15 +39,15 @@ go :: Config -> IO () -> IO ()
 go cfg help
   | unHelpful $ version cfg = putStrLn Git.version
   | otherwise =
-    let mFailSpec = makeFailureSpec (unHelpful $ endOfFiniteFailures cfg) (unHelpful $ maxCrashes cfg) (unHelpful $ endOfTime cfg)
+    let mFailSpec = makeFailureSpec (unHelpful $ endOfFiniteFailures cfg) (unHelpful $ maxCrashes cfg) (unHelpful $ endOfTime cfg) (unHelpful $ limitNumberOfFaults cfg)
      in case (unHelpful $ testId cfg, mFailSpec) of
           (Just tid, Just failSpec) -> do
             let testInformation = TestInformation tid (unHelpful $ failedRunId cfg)
             json <- Ldfi.run' sqliteStorage z3Solver testInformation failSpec
             T.putStrLn json
           (_, _) -> help
 
-makeFailureSpec :: Maybe Int -> Maybe Int -> Maybe Int -> Maybe FailureSpec
-makeFailureSpec (Just eof) (Just crashes) (Just eot) =
-  Just (FailureSpec (toEnum eof) (toEnum crashes) (toEnum eot))
-makeFailureSpec _ _ _ = Nothing
+makeFailureSpec :: Maybe Int -> Maybe Int -> Maybe Int -> Maybe Int -> Maybe FailureSpec
+makeFailureSpec (Just eof) (Just crashes) (Just eot) limitFailures =
+  Just (FailureSpec (toEnum eof) (toEnum crashes) (toEnum eot) limitFailures)
+makeFailureSpec _ _ _ _ = Nothing

src/ldfi2/src/Ldfi.hs

@@ -6,6 +6,7 @@ module Ldfi where
 
 import qualified Data.Aeson as Aeson
 import qualified Data.ByteString.Lazy as BSL
+import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
@@ -43,12 +44,12 @@ affects (Crash n a) (Event s sa r ra) =
 -- failureSemantic computes a formula s.t for each event either (xor) the event
 -- is true or one of the failures that affect it is true
 failureSemantic :: Set Event -> Set Fault -> LDFIFormula
-failureSemantic events failures =
+failureSemantic events faults =
   And
     [ Var (EventVar event)
         :+ Or
           [ Var (FaultVar failure)
-            | failure <- Set.toList failures,
+            | failure <- Set.toList faults,
               failure `affects` event
           ]
       | event <- Set.toList events
@@ -102,22 +103,27 @@ enumerateAllFaults events fs = Set.unions (Set.map possibleFailure events)
 --     * If we introduce faults the corresponding events are false (`failureSemantic`)
 --     * We don't intruduce faults that violates the failure spec (`failureSpecConstaint`)
 --     * The lineage graph from traces are not satisfied (`Neg lineage`)
-ldfi :: FailureSpec -> [Trace] -> [Failures] -> FormulaF String
-ldfi fs ts failures =
+ldfi :: FailureSpec -> Map RunId Trace -> Failures -> FormulaF String
+ldfi failureSpec tracesByRuns failures =
   fmap show $
     simplify $
-      And
-        [ failureSemantic allEvents allFaults,
-          failureSpecConstraint fs allEvents allFaults,
-          Neg (lineage ts),
-          And
-            [ Neg $ And $ map (Var . FaultVar) faults
-              | faults <- failures
-            ]
-        ]
+      And $
+        addLimit
+          [ failureSemantic allEvents allFaults,
+            failureSpecConstraint failureSpec allEvents allFaults,
+            Neg (lineage traces),
+            And
+              [ Neg $ And $ map (Var . FaultVar) faults
+                | faults <- fFaultsFromFailedRuns failures
+              ]
+          ]
   where
-    allEvents = Set.unions (map Set.fromList ts)
-    allFaults = enumerateAllFaults allEvents fs
+    addLimit xs = case numberOfFaultLimit failureSpec of
+      Nothing -> xs
+      Just l -> AtMost [FaultVar $ f | f <- Set.toList allFaults] l : xs
+    traces = Map.elems tracesByRuns
+    allEvents = Set.unions (map Set.fromList traces)
+    allFaults = enumerateAllFaults allEvents failureSpec
 
 ------------------------------------------------------------------------
 
@@ -136,7 +142,7 @@ marshalFaults = TE.decodeUtf8 . BSL.toStrict . Aeson.encode . MF.Faults . map co
   where
     convert :: Fault -> MF.Fault
     convert (Crash f a) = MF.Crash f a
-    convert (Omission (f,t) a) = MF.Omission f t a
+    convert (Omission (f, t) a) = MF.Omission f t a
 
 run :: Monad m => Storage m -> Solver m -> TestInformation -> FailureSpec -> m [Fault]
 run Storage {load, loadFailures} Solver {solve} testInformation failureSpec = do

src/ldfi2/src/Ldfi/FailureSpec.hs

@@ -13,5 +13,7 @@ data FailureSpec = FailureSpec
     -- | The maximum amount of crashes allowed.
     maxCrashes :: Natural,
     -- | When the test stops (a.k.a. EOT).
-    endOfTime :: Time
+    endOfTime :: Time,
+    -- | Potential max limit of number of faults
+    numberOfFaultLimit :: Maybe Int
   }

src/ldfi2/src/Ldfi/Marshal/Faults.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveGeneric #-}
+
 module Ldfi.Marshal.Faults where
 
 import Data.Aeson
@@ -8,21 +9,23 @@ import GHC.Natural (Natural)
 
 data Fault
   = Omission
-    { from :: String,
-      to :: String,
-      at :: Natural
-    }
+      { from :: String,
+        to :: String,
+        at :: Natural
+      }
   | Crash
-    { from :: String,
-      at :: Natural
-    }
+      { from :: String,
+        at :: Natural
+      }
   deriving (Generic, Show)
 
 customOptions :: Options
-customOptions = defaultOptions
-  { sumEncoding = defaultTaggedObject { tagFieldName = "kind"},
-    constructorTagModifier = map toLower
-  }
+customOptions =
+  defaultOptions
+    { sumEncoding = defaultTaggedObject {tagFieldName = "kind"},
+      constructorTagModifier = map toLower
+    }
+
 instance FromJSON Fault where
   parseJSON = genericParseJSON customOptions
 
@@ -31,7 +34,7 @@ instance ToJSON Fault where
   toEncoding = genericToEncoding customOptions
 
 data Faults = Faults
-  { faults :: [Fault]}
+  {faults :: [Fault]}
   deriving (Generic, Show)
 
 instance ToJSON Faults

src/ldfi2/src/Ldfi/Prop.hs

@@ -20,10 +20,10 @@ data FormulaF var
   | FormulaF var :|| FormulaF var
   | FormulaF var :+ FormulaF var
   | FormulaF var :-> FormulaF var
+  | FormulaF var :<-> FormulaF var
   | And [FormulaF var]
   | Or [FormulaF var]
   | Neg (FormulaF var)
-  | FormulaF var :<-> FormulaF var
   | AtMost [var] Int
   | TT
   | FF
@@ -37,13 +37,14 @@ genFormula env 0 =
   QC.oneof
     [ pure TT,
       pure FF,
-      Var <$> QC.elements env
+      Var <$> QC.elements env,
+      AtMost <$> QC.listOf1 (QC.elements env) <*> QC.arbitrarySizedNatural
     ]
 genFormula env size =
   QC.oneof
     [ genFormula env 0,
       Neg <$> genFormula env (size - 1),
-      QC.elements [(:&&), (:||), (:+), (:<->)] <*> genFormula env (size `div` 2) <*> genFormula env (size `div` 2),
+      QC.elements [(:&&), (:||), (:+), (:<->), (:->)] <*> genFormula env (size `div` 2) <*> genFormula env (size `div` 2),
       do
         n <- QC.choose (0, size `div` 2)
         QC.elements [And, Or] <*> QC.vectorOf n (genFormula env (size `div` 4))
@@ -57,6 +58,14 @@ instance QC.Arbitrary v => QC.Arbitrary (FormulaF v) where
 getVars :: Ord var => FormulaF var -> Set var
 getVars = foldMap Set.singleton
 
+isTT :: FormulaF var -> Bool
+isTT TT = True
+isTT _ = False
+
+isFF :: FormulaF var -> Bool
+isFF FF = True
+isFF _ = False
+
 simplify1 :: FormulaF var -> FormulaF var
 simplify1 (TT :&& r) = simplify1 r
 simplify1 (l :&& r) = simplify1 l :&& simplify1 r
@@ -65,12 +74,23 @@ 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 (And fs)
+  | not (null [() | FF <- fs]) = FF
+  | otherwise = And (map simplify1 $ filter (not . isTT) fs)
 simplify1 (Or []) = FF
 simplify1 (Or [f]) = f
-simplify1 (Or fs) = Or (map simplify1 fs)
+simplify1 (Or fs)
+  | not (null [()| TT <- fs]) = TT
+  | otherwise = Or (map simplify1 $ filter (not . isFF) fs)
+simplify1 (Neg FF) = TT
+simplify1 (Neg TT) = FF
+simplify1 (Neg (Neg f)) = f
 simplify1 (Neg f) = Neg (simplify1 f)
 simplify1 (l :<-> r) = simplify1 l :<-> simplify1 r
+simplify1 (TT :-> f) = simplify1 f
+simplify1 (FF :-> _) = TT
+simplify1 (f :-> FF) = Neg $ simplify1 f
+simplify1 (_ :-> TT) = TT
 simplify1 (l :-> r) = simplify1 l :-> simplify1 r
 simplify1 (l :+ r) = simplify1 l :+ simplify1 r
 simplify1 f@(AtMost {}) = f

src/ldfi2/src/Ldfi/Sat.hs

@@ -58,31 +58,31 @@ z3SolveAll limit f = do
     a <- translate env f
     assert a
     go 0 [] vs vs'
-    where
-      limitReached :: Int -> Bool
-      limitReached n = case limit of
-        Nothing -> False
-        Just k -> n >= k
+  where
+    limitReached :: Int -> Bool
+    limitReached n = case limit of
+      Nothing -> False
+      Just k -> n >= k
 
-      go :: MonadZ3 z3 => Int -> [Solution] -> [String] -> [AST] -> z3 [Solution]
-      go n acc vs vs'
-        | limitReached n = return (reverse acc)
-        | otherwise = do
-          (result, mModel) <- getModel
-          case result of
-            Undef -> error "impossible"
-            Unsat -> return (reverse acc)
-            Sat -> case mModel of
-              Nothing -> error "impossible" -- TODO(stevan): steal Agda's __IMPOSSIBLE__?
-              Just model -> do
-                mbs <- mapM (evalBool model) vs'
-                let bs = map (maybe (error "impossible") id) mbs
-                bs' <-
-                  mapM
-                    (\(ix, b) -> mkNot =<< mkEq (vs' !! ix) =<< mkBool b)
-                    (zip [0 .. length bs - 1] bs)
-                assert =<< mkOr bs'
-                go (succ n) (Solution (Map.fromList (zip vs bs)) : acc) vs vs'
+    go :: MonadZ3 z3 => Int -> [Solution] -> [String] -> [AST] -> z3 [Solution]
+    go n acc vs vs'
+      | limitReached n = return (reverse acc)
+      | otherwise = do
+        (result, mModel) <- getModel
+        case result of
+          Undef -> error "impossible"
+          Unsat -> return (reverse acc)
+          Sat -> case mModel of
+            Nothing -> error "impossible" -- TODO(stevan): steal Agda's __IMPOSSIBLE__?
+            Just model -> do
+              mbs <- mapM (evalBool model) vs'
+              let bs = map (maybe (error "impossible") id) mbs
+              bs' <-
+                mapM
+                  (\(ix, b) -> mkNot =<< mkEq (vs' !! ix) =<< mkBool b)
+                  (zip [0 .. length bs - 1] bs)
+              assert =<< mkOr bs'
+              go (succ n) (Solution (Map.fromList (zip vs bs)) : acc) vs vs'
 
 z3Solver :: Solver IO
 z3Solver = Solver z3Solve