feat(ltl): Add events as atoms

src/ltl/cabal.project

@@ -1,6 +1,6 @@
 packages: .
 
-with-compiler: ghc-8.10.3
+with-compiler: ghc-8.10.4
 
 reject-unconstrained-dependencies: all
 

src/ltl/ltl.cabal

@@ -14,7 +14,7 @@ copyright:          Copyright (c) 2021 Symbiont Inc
 category:           Testing, Distributed Systems
 build-type:         Simple
 extra-source-files: CHANGELOG.md
-tested-with:        GHC ==8.10.3
+tested-with:        GHC ==8.10.4
 
 library
   hs-source-dirs:   src/
@@ -57,9 +57,12 @@ test-suite test
     , HUnit
     , ltl
     , QuickCheck
+    , scientific
     , tasty
     , tasty-hunit
     , text
+    , unordered-containers
+    , vector
 
   build-depends:
       aeson

src/ltl/src/Ltl.hs

@@ -28,6 +28,9 @@ evalExpr state sb (Variable (Var t n e)) =
         After  -> after sb
   in jq e (fromMaybe Aeson.Null $ Map.lookup (evalNode (nodeEnv state) n) s)
 evalExpr state _ (IntLang e) = Aeson.Number $ fromInteger $ evalInt (intEnv state) e
+evalExpr state sb (EEvent e) =
+  let Event js = action sb
+  in jq e js
 
 checkPredicate :: CheckState -> Predicate -> StateBehaviour -> Dec
 checkPredicate state p sb = case p of
@@ -95,7 +98,7 @@ exampleTrace =
   sb 1 [(a, sa2), (b, sb2)] [(a,sa3), (b,sb3)],
   sb 2 [(a, sa3), (b, sb3)] [(a,sa4), (b,sb4)]]
   where
-    sb i x y = StateBehaviour (State (Map.fromList x)) i Event (State (Map.fromList y))
+    sb i x y = StateBehaviour (State (Map.fromList x)) i (Event Aeson.Null) (State (Map.fromList y))
     a = "NodeA"
     b = "NodeB"
     sa1 = Aeson.object [("state", Aeson.Bool True)]

src/ltl/src/Ltl/Json.hs

@@ -22,7 +22,8 @@ jq :: JQ -> Json -> Json
 jq This js = js
 jq (Lookup f k) js = case js of
   Aeson.Object hm -> case HashMap.lookup k hm of
-    Nothing -> error $ "Unknown key " ++ show k-- Aeson.Null
+    --Nothing -> error $ "Unknown key " ++ show k ++ " of possible keys: "  ++ show (HashMap.keys hm)
+    Nothing -> Aeson.Null
     Just js' -> jq f js'
   _ -> Aeson.Null -- or fail?
 jq (Index f i) js = case js of

src/ltl/src/Ltl/Prop.hs

@@ -49,7 +49,7 @@ data Expr
   = Variable Var
   | Constant Json
   | IntLang IntExpr
-  -- This will also have somethin to look at the event
+  | EEvent JQ
   deriving (Eq, Show)
 
 data Predicate
@@ -82,6 +82,7 @@ concreteE :: [Node] -> Expr -> Expr
 concreteE nodes (Variable (Var t n jq)) = Variable (Var t (concreteN nodes n) jq)
 concreteE nodes j@(Constant{}) = j
 concreteE nodes i@(IntLang{}) = i
+concreteE nodes e@(EEvent{}) = e
 
 concreteP :: [Node] -> Predicate -> Predicate
 concreteP nodes (Eq l r) = Eq (concreteE nodes l) (concreteE nodes r)

src/ltl/src/Ltl/Prop/Parser.hs

@@ -35,14 +35,16 @@ pVar = f <$ (P.satisfy (== '@')) <*> stringVar <*> PL.lexeme space (P.option Bef
   where
     f x temp = Var temp (VariableNode x)
 
+pEvent = PL.symbol space "$" *> PL.lexeme space pJQ
+
 pInt = P.choice
   [ IConst <$> decimal,
     IVarAdd <$> PL.lexeme space stringVar <*> (PL.symbol space "+" *> decimal <|> pure 0)
   ]
 
 pConst :: Parser Json
 pConst = do
-   t <- P.char '`' *> P.takeWhileP (Just "json") (/= '`') <* P.char '`'
+   t <- P.char '`' *> P.takeWhileP (Just "json") (/= '`') <* PL.symbol space "`"
    case Json.decode t of
      Left reason -> fail reason
      Right x -> pure x
@@ -51,7 +53,8 @@ pExpr :: Parser Expr
 pExpr = P.choice
   [ Variable <$> pVar,
     Constant <$> pConst,
-    IntLang <$> pInt
+    IntLang <$> pInt,
+    EEvent <$> pEvent
   ]
 
 pPredicate :: Parser Formula

src/ltl/src/Ltl/Storage.hs

@@ -2,15 +2,16 @@
 {-# LANGUAGE OverloadedStrings #-}
 module Ltl.Storage where
 
--- import Data.Aeson (FromJSON(..))
+import Database.SQLite.Simple
 import qualified Data.Aeson as Aeson
 import Data.ByteString.Lazy (ByteString)
-import Database.SQLite.Simple
+import qualified Data.HashMap.Strict as HashMap
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Maybe as Maybe
 import Data.Text.Lazy (Text)
+import qualified Data.Text.Lazy as Text
 import qualified Data.Text.Lazy.Encoding as TextEncoding
 
 import Control.Exception (throwIO)
@@ -47,22 +48,34 @@ getDbPath = do
 data ExecutionStep = ExecutionStep
   { esReactor :: String,
     esLogicalTime :: Int,
-    esHeapDiff :: Text
+    esHeapDiff :: Text,
+    esMessage :: Text,
+    esEvent :: Text
   }
 
 instance FromRow ExecutionStep where
-  fromRow = ExecutionStep <$> field <*> field <*> field
+  fromRow = ExecutionStep <$> field <*> field <*> field <*> field <*> field
 
 sqliteLoadExecutionSteps:: TestId -> RunId -> IO [ExecutionStep]
 sqliteLoadExecutionSteps testId runId = do
   path <- getDbPath
   conn <- open path
   queryNamed conn
-       "SELECT reactor, logical_time, heap_diff FROM execution_step \
-       \ WHERE test_id = :testId \
-       \ AND run_id = :runId \
-       \ ORDER BY logical_time ASC"
-       [":testId" := testId, ":runId" := runId]
+    "SELECT execution_step.reactor, \
+    \       execution_step.logical_time, \
+    \       execution_step.heap_diff, \
+    \       network_trace.message, \
+    \       network_trace.args \
+    \FROM execution_step \
+    \INNER JOIN network_trace \
+    \ON (execution_step.test_id=network_trace.test_id \
+    \   AND execution_step.run_id = network_trace.run_id \
+    \   AND execution_step.logical_time=network_trace.recv_logical_time) \
+    \WHERE \
+    \  execution_step.test_id=:testId \
+    \  AND execution_step.run_id=:runId \
+    \ORDER BY execution_step.logical_time ASC"
+    [":testId" := testId, ":runId" := runId]
 
 data DeploymentInfo = DeploymentInfo
   { diReactor :: String,
@@ -102,7 +115,9 @@ mkTrace es s = case go es s of
         sb = StateBehaviour
           { before = State state
           , worldTime = esLogicalTime es
-          , action = Event
+          , action = Event $ Aeson.Object (HashMap.fromList [
+                                              ("message", Aeson.String $ Text.toStrict $ esMessage es),
+                                              ("event", Maybe.fromMaybe "(Can't decode event)" $ Aeson.decode $ TextEncoding.encodeUtf8 $ esEvent es)])
           , after = State state'
           }
       in sb : go ess state'

src/ltl/src/Ltl/Traces.hs

@@ -9,7 +9,7 @@ type Node = String
 
 data State = State (Map Node Json) deriving (Show)
 
-data Event = Event -- we will extend this later
+data Event = Event Json
   deriving (Show)
 
 data StateBehaviour = StateBehaviour

src/ltl/test/Ltl/Prop/ParserTest.hs

@@ -2,10 +2,18 @@
 module Ltl.Prop.ParserTest where
 
 import Data.Text (Text)
+import qualified Data.Aeson as Aeson
+import qualified Data.Aeson.Text as AesonText
+import qualified Data.HashMap.Strict as Hashmap
+import Data.Scientific (Scientific)
+import qualified Data.Scientific as Scientific
 import qualified Data.Text as Text
-import qualified Test.QuickCheck as QC
+import qualified Data.Text.Lazy as LazyText
+import qualified Data.Vector as Vector
 import Test.HUnit
+import qualified Test.QuickCheck as QC
 
+import Ltl.Json
 import Ltl.Prop
 import Ltl.Prop.Parser
 
@@ -17,9 +25,22 @@ ppI (IVarAdd v 0) = QC.elements
 ppI (IVarAdd v k) = pure $ Text.pack v <> "+" <> Text.pack (show k)
 ppI (IConst k) = pure $ Text.pack (show k)
 
+ppJq :: JQ -> QC.Gen Text
+ppJq This = pure $ ""
+ppJq (Lookup jq t) = do
+  r <- ppJq jq
+  pure $ "." <> t <> r
+ppJq (Index jq i) = do
+  r <- ppJq jq
+  pure $ "[" <> Text.pack (show i) <> "]" <> r
 
 ppE :: Expr -> QC.Gen Text
 ppE (IntLang ie) = ppI ie
+ppE (EEvent jq) = do
+  r <- ppJq jq
+  pure $ "$" <> r
+ppE (Constant json) =
+  pure $ "`" <> LazyText.toStrict (AesonText.encodeToLazyText json) <> "`"
 
 ppP :: Predicate -> QC.Gen Text
 ppP (Eq l r) = do
@@ -81,6 +102,9 @@ pp f = maybeParens $ case f of
 stringVar :: QC.Gen String
 stringVar = QC.elements ["x", "y", "z"] -- do better
 
+jsonKey :: QC.Gen Text
+jsonKey = Text.pack <$> stringVar -- do better
+
 -- TODO we should have no spaces in the var
 genI :: QC.Gen IntExpr
 genI = QC.oneof
@@ -89,9 +113,44 @@ genI = QC.oneof
     IConst <$> QC.arbitrary
   ]
 
+genJq :: QC.Gen JQ
+genJq = QC.sized $ go
+  where
+    go 0 = return This
+    go n = QC.oneof
+      [ go 0
+      , Lookup <$> go (n `div` 2) <*> jsonKey
+      , Index <$> go (n `div` 2) <*> QC.arbitrary]
+
+genText :: QC.Gen Text
+genText = pure "h " -- Text.pack <$> QC.arbitrary
+
+genNumber :: QC.Gen Scientific
+genNumber = Scientific.scientific <$> QC.arbitrary <*> QC.arbitrary
+
+genJson :: QC.Gen Json
+genJson = QC.sized $ go
+  where
+    go 0 = QC.oneof
+      [ pure $ Aeson.Null
+      , Aeson.Bool <$> QC.arbitrary
+      , Aeson.Number <$> genNumber
+      , Aeson.String <$> genText]
+    go n = QC.oneof
+      [ go 0
+      , do
+          a <- QC.listOf (go $ n `div` 10)
+          pure $ Aeson.Array (Vector.fromList a)
+      , do
+          m <- QC.listOf (QC.liftArbitrary2 jsonKey (go $ n `div` 10))
+          pure $ Aeson.Object (Hashmap.fromList m)
+      ]
+
 genE :: QC.Gen Expr
 genE = QC.oneof
   [ IntLang <$> genI
+  , Constant <$> genJson
+  , EEvent <$> genJq
   ]
 
 genP :: QC.Gen Predicate