feat(ltl): Introduce proof terms in ltl

This would give us better error messages in some cases.

fixes #194

src/ltl/app/Main.hs

@@ -14,6 +14,7 @@ import Options.Generic
 
 import Ltl
 import Ltl.Json
+import qualified Ltl.Proof as Proof
 import Ltl.Prop.Parser (parse)
 import qualified Ltl.Storage as Storage
 
@@ -46,6 +47,14 @@ data Config
 
 instance ParseRecord Config
 
+data Result = Result
+  { result :: Bool
+  , reason :: String
+  } deriving (Generic)
+
+instance Aeson.FromJSON Result
+instance Aeson.ToJSON Result
+
 main :: IO ()
 main = do
   (cfg, help) <- getWithHelp "LTL checker"
@@ -56,13 +65,10 @@ main = do
       testFormula <- case parse (unHelpful formula) of
         Left s  -> error s
         Right x -> pure x
-      let r = Result $ check testFormula trace
+      let
+        dec = check testFormula trace
+        result = case dec of
+          Proof.No{} -> False
+          Proof.Yes{} -> True
+        r = Result result (Proof.reason dec)
       TextIO.putStrLn $ AesonText.encodeToLazyText r
-
-
-data Result = Result
-  { result :: Bool
-  } deriving (Generic)
-
-instance Aeson.FromJSON Result
-instance Aeson.ToJSON Result

src/ltl/ltl.cabal

@@ -21,6 +21,7 @@ library
   exposed-modules:
       Ltl
     , Ltl.Json
+    , Ltl.Proof
     , Ltl.Prop
     , Ltl.Prop.Parser
     , Ltl.Storage

src/ltl/src/Ltl.hs

@@ -14,7 +14,7 @@ import qualified Data.HashMap.Strict as H
 import Ltl.Json
 import Ltl.Prop
 import Ltl.Traces
-
+import Ltl.Proof
 
 --------------------------------------------------------------------------------
 
@@ -29,9 +29,12 @@ evalExpr state sb (Variable (Var t n e)) =
   in jq e (fromMaybe Aeson.Null $ Map.lookup (evalNode (nodeEnv state) n) s)
 evalExpr state _ (IntLang e) = Aeson.Number $ fromInteger $ evalInt (intEnv state) e
 
-checkPredicate :: CheckState -> Predicate -> StateBehaviour -> Bool
+checkPredicate :: CheckState -> Predicate -> StateBehaviour -> Dec
 checkPredicate state p sb = case p of
-  Eq e e' -> evalExpr state sb e == evalExpr state sb e'
+  Eq e e' ->
+    let lhs = evalExpr state sb e
+        rhs = evalExpr state sb e'
+    in if lhs == rhs then Yes (PP (PEq lhs)) else No (RP (REq lhs rhs))
 
 
 --------------------------------------------------------------------------------
@@ -57,42 +60,46 @@ updateIenv b i (CheckState nenv ienv ns) = CheckState nenv (Map.insert b i ienv)
 updateNenv :: NodeVar -> Node -> CheckState -> CheckState
 updateNenv b n (CheckState nenv ienv ns) = CheckState (Map.insert b n nenv) ienv ns
 
-check' :: CheckState -> Formula -> Trace -> Bool
+check' :: CheckState -> Formula -> Trace -> Dec
 check' state formula ts = case formula of
   P pred -> checkPredicate state pred (NE.head ts)
-  Always f -> all (check' state f) (futures ts)
-  Eventually f -> any (check' state f) (futures ts)
-  ForallNode b f -> all (\n -> check' (updateNenv b n state) f ts) (nodes state)
-  ExistsNode b f -> any (\n -> check' (updateNenv b n state) f ts) (nodes state)
-  ForallInt is b f -> all (\i -> check' (updateIenv b i state) f ts) is
-  ExistsInt is b f -> any (\i -> check' (updateIenv b i state) f ts) is
-  Imp f g -> not (check' state f ts) || check' state g ts
-  And f g -> check' state f ts && check' state g ts
-  Or  f g -> check' state f ts || check' state g ts
-  Neg f -> not (check' state f ts) -- strong negation trick?
-  TT -> True
-  FF -> False
-
-
-check :: Formula -> Trace -> Bool
+  Always f ->
+    allDec (check' state f) (futures ts) (RAlways . worldTime . NE.head) PAlways
+  Eventually f ->
+    anyDec (check' state f) (futures ts) (PEventually . worldTime . NE.head) REventually
+  ForallNode b f ->
+    allDec (\n -> check' (updateNenv b n state) f ts) (nodes state) RForallNode PForallNode
+  ExistsNode b f ->
+    anyDec (\n -> check' (updateNenv b n state) f ts) (nodes state) PExistsNode RExistsNode
+  ForallInt is b f ->
+    allDec (\i -> check' (updateIenv b i state) f ts) is RForallInt PForallInt
+  ExistsInt is b f ->
+    anyDec (\i -> check' (updateIenv b i state) f ts) is PExistsInt RExistsInt
+  Imp f g -> (check' state f ts) `impDec` check' state g ts
+  And f g -> check' state f ts `andDec` check' state g ts
+  Or  f g -> check' state f ts `orDec` check' state g ts
+  Neg f -> notDec (check' state f ts)
+  TT -> Yes PTT
+  FF -> No RFF
+
+check :: Formula -> Trace -> Dec
 check f t = check' state (concreteNodes (nodesFromTrace t) f) t
   where
     state = CheckState Map.empty Map.empty (nodesFromTrace t)
-    nodesFromTrace (StateBehaviour (State x) _ _ :| _) = Map.keys x
-
+    nodesFromTrace (StateBehaviour (State x) _ _ _ :| _) = Map.keys x
 --------------------------------------------------------------------------------
 
 exampleTrace :: Trace
 exampleTrace =
-  sb [(a, sa1), (b, sb1)] [(a,sa2), (b,sb2)] :| [
-  sb [(a, sa2), (b, sb2)] [(a,sa3), (b,sb3)],
-  sb [(a, sa3), (b, sb3)] [(a,sa4), (b,sb4)]]
+  sb 0 [(a, sa1), (b, sb1)] [(a,sa2), (b,sb2)] :| [
+  sb 1 [(a, sa2), (b, sb2)] [(a,sa3), (b,sb3)],
+  sb 2 [(a, sa3), (b, sb3)] [(a,sa4), (b,sb4)]]
   where
-    sb x y = StateBehaviour (State (Map.fromList x)) Event (State (Map.fromList y))
+    sb i x y = StateBehaviour (State (Map.fromList x)) i Event (State (Map.fromList y))
     a = "NodeA"
     b = "NodeB"
     sa1 = Aeson.object [("state", Aeson.Bool True)]
     (sa2:sa3:sa4:_) = repeat sa1
-    sb1 = Aeson.object [("b-state", Aeson.Bool True)]
+    sb1 = Aeson.object [("bstate", Aeson.Bool True)]
     (sb2:sb3:_) = repeat sb1
-    sb4 = Aeson.object [("b-state", Aeson.Bool False)]
+    sb4 = Aeson.object [("bstate", Aeson.Bool False)]

src/ltl/src/Ltl/Proof.hs

@@ -0,0 +1,86 @@
+module Ltl.Proof where
+
+import Ltl.Json
+import Ltl.Traces
+
+{-
+We might want to store more information in the predicates but this is a start
+-}
+data PredicateProof = PEq Json -- the value both were equal to
+  deriving (Eq, Show)
+
+data PredicateRefutation = REq Json Json -- the two different values
+  deriving (Eq, Show)
+
+data Proof
+  = PP PredicateProof
+  | PAlways -- we intentionally don't have proof for all the subterms
+  | PEventually Int Proof -- the world it was true in, and proof it was true
+  | PForallNode -- intentionally empty
+  | PExistsNode Node Proof -- node, and proof this is true for this node
+  | PForallInt -- intentionally empty
+  | PExistsInt Integer Proof -- Int and proof that the int satisfy the formula
+  | PImp (Either Refutation Proof) -- Proof (p -> q) = Refutation p + Proof q
+  | PAnd Proof Proof -- Proof (p /\ q) = Proof p * Proof q
+  | POr (Either Proof Proof) -- Proof (p \/ q) = Proof p + Proof q
+  | PNeg Refutation -- Proof (~ p) = Refutation p
+  | PTT -- P tt = {}
+  deriving (Eq, Show)
+
+data Refutation
+  = RP PredicateRefutation
+  | RAlways Int Refutation -- R ([] p) =  w * R p @ w
+  | REventually -- R (<> p) = {}
+  | RForallNode Node Refutation -- R (\forall n. p) = N * R (p[n:=N])
+  | RExistsNode -- R (\exists n. p) = {}
+  | RForallInt Integer Refutation -- R (\forall x. p) = i * R (p [x:=i])
+  | RExistsInt -- R (\exists x. p) = {}
+  | RImp Proof Refutation -- R (p -> q) = P p * R q
+  | RAnd (Either Refutation Refutation) -- R (p /\ q) = R p + R q
+  | ROr Refutation Refutation -- R (p \/ q) = R p * R q
+  | RNeg Proof -- R (~ p) = P p
+  | RFF -- R ff = {}
+  deriving (Eq, Show)
+
+data Dec
+  = Yes Proof
+  | No Refutation
+  deriving (Eq, Show)
+
+notDec :: Dec -> Dec
+notDec (Yes p) = No (RNeg p)
+notDec (No r) = Yes (PNeg r)
+
+andDec :: Dec -> Dec -> Dec
+andDec (No r) _ = No (RAnd (Left r))
+andDec _ (No r) = No (RAnd (Right r))
+andDec (Yes p) (Yes p') = Yes (PAnd p p')
+
+orDec :: Dec -> Dec -> Dec
+orDec (Yes p) _ = Yes (POr (Left p))
+orDec _ (Yes p) = Yes (POr (Right p))
+orDec (No r) (No r') = No (ROr r r')
+
+impDec :: Dec -> Dec -> Dec
+impDec _ (Yes p) = Yes (PImp (Right p))
+impDec (No r) _ = Yes (PImp (Left r))
+impDec (Yes p) (No r) = No (RImp p r)
+
+allDec :: (r -> Dec) -> [r] -> (r -> Refutation -> Refutation) -> Proof -> Dec
+allDec pred xs ref pro = go xs
+  where
+    go [] = Yes pro
+    go (x:xs) = case pred x of
+      Yes _ -> go xs
+      No r -> No $ ref x r
+
+anyDec :: (r -> Dec) -> [r] -> (r -> Proof -> Proof) -> Refutation -> Dec
+anyDec pred xs pro ref = go xs
+  where
+    go [] = No ref
+    go (x:xs) = case pred x of
+      Yes p -> Yes $ pro x p
+      No _ -> go xs
+
+reason :: Dec -> String
+reason = show

src/ltl/src/Ltl/Storage.hs

@@ -96,7 +96,16 @@ mkTrace es s = case go es s of
   where
     updateState es = Map.adjust (\v -> mergePatch v (Maybe.fromMaybe ("Can't decode heap") $ Aeson.decode $ TextEncoding.encodeUtf8 $ esHeapDiff es)) (esReactor es)
     go [] _ = []
-    go (es:ess) state = let state' = updateState es state in StateBehaviour (State state) Event (State state') : go ess state'
+    go (es:ess) state =
+      let
+        state' = updateState es state
+        sb = StateBehaviour
+          { before = State state
+          , worldTime = esLogicalTime es
+          , action = Event
+          , after = State state'
+          }
+      in sb : go ess state'
 
 sqliteLoad :: TestId -> RunId -> IO Trace
 sqliteLoad testId runId = do

src/ltl/src/Ltl/Traces.hs

@@ -14,6 +14,7 @@ data Event = Event -- we will extend this later
 
 data StateBehaviour = StateBehaviour
   { before :: State
+  , worldTime :: Int
   , action :: Event
   , after  :: State
   } deriving (Show)