ReCon framework 1.1.0

bench/cardano-recon-framework/CHANGELOG.md

@@ -1,5 +1,11 @@
 # Revision history for cardano-trace-ltl
 
+## 1.1.0 -- April 2026
+
+* Support configurable timeunits in formulas via a CLI option.
+* Support existential quantification over properties (both finite and infinite domain)
+* Support Presburger arithmetic (over ℤ)
+
 ## 1.0.0 -- Feb 2026
 
 * First version.

bench/cardano-recon-framework/app/Cardano/ReCon.hs

@@ -7,8 +7,8 @@ import           Cardano.Logging
 import           Cardano.Logging.Prometheus.TCPServer (TracePrometheusSimple (..),
                    runPrometheusSimple)
 import           Cardano.Logging.Types.TraceMessage (TraceMessage (..))
-import           Cardano.ReCon.Cli (CliOptions (..), Mode (..), opts)
-import           Cardano.ReCon.Common (extractProps)
+import           Cardano.ReCon.Cli (CliOptions (..), Mode (..), opts, timeunitToMicrosecond)
+import           Cardano.ReCon.Common (extractIntProps, extractTextProps)
 import           Cardano.ReCon.LTL.Check (checkFormula, prettyError)
 import           Cardano.ReCon.LTL.Lang.Formula
 import           Cardano.ReCon.LTL.Lang.Formula.Parser (Context (..))
@@ -37,23 +37,27 @@ import           Data.Maybe (fromMaybe, isJust, listToMaybe)
 import           Data.Text (Text, unpack)
 import qualified Data.Text as Text
 import           Data.Traversable (for)
+import           GHC.IO.Encoding (setLocaleEncoding, utf8)
 import           Network.HostName (HostName)
 import           Network.Socket (PortNumber)
 import           Options.Applicative hiding (Success)
 import           System.Exit (die)
 import qualified System.Metrics as EKG
 
-import           GHC.IO.Encoding (setLocaleEncoding, utf8)
 import           Streaming
 
 
 instance Event TemporalEvent Text where
   ofTy (TemporalEvent _ msgs) c = isJust $ find (\msg -> msg.tmsgNS == c) msgs
-  props (TemporalEvent _ msgs) c =
+  intProps (TemporalEvent _ msgs) c =
     case find (\msg -> msg.tmsgNS == c) msgs of
-      Just x  -> Map.insert "host" (TextValue x.tmsgHost)       $
-                   Map.insert "thread" (TextValue x.tmsgThread) $
-                     extractProps x.tmsgData
+      Just x  -> extractIntProps x.tmsgData
+      Nothing -> error ("Not an event of type " <> unpack c)
+  textProps (TemporalEvent _ msgs) c =
+    case find (\msg -> msg.tmsgNS == c) msgs of
+      Just x  -> Map.insert "host"   x.tmsgHost   $
+                   Map.insert "thread" x.tmsgThread $
+                     extractTextProps x.tmsgData
       Nothing -> error ("Not an event of type " <> unpack c)
   beg (TemporalEvent t _) = t
 
@@ -107,10 +111,6 @@ checkOffline tr eventDuration file phis = do
     check idx tr phi events
   threadDelay 200_000 -- Give the tracer a grace period to output the logs to whatever backend
 
--- | Convert time unit used in the yaml (currently second) input to μs.
-unitToMicrosecond :: Word -> Word
-unitToMicrosecond = (1_000_000 *)
-
 setupTraceDispatcher :: Maybe FilePath -> IO (Trace IO App.TraceMessage)
 setupTraceDispatcher optTraceDispatcherConfigFile = do
   stdTr <- standardTracer
@@ -155,7 +155,7 @@ main = do
   ctx <- Map.toList . fromMaybe Map.empty <$> for options.context (readPropValues >=> dieOnYamlException)
   putStrLn "Context:"
   print ctx
-  formulas <- readFormulas options.formulas (Context ctx) Parser.text >>= dieOnYamlException
+  formulas <- readFormulas options.formulas (Context { interpDomain = ctx, varKinds = Map.empty }) Parser.text >>= dieOnYamlException
   for_ (fmap (\phi -> (phi, checkFormula mempty phi)) formulas) $ \case
     (phi, e : es) -> die $
       Text.unpack $
@@ -164,7 +164,7 @@ main = do
         <> " is syntactically invalid:\n"
         <> Text.unlines (fmap (("— " <>) . prettyError) (e : es))
     (_, []) -> pure ()
-  let formulas' = fmap (interpTimeunit (\u -> unitToMicrosecond u `div` fromIntegral options.duration)) formulas
+  let formulas' = fmap (interpTimeunit (\u -> timeunitToMicrosecond options.timeunit u `div` fromIntegral options.duration)) formulas
   tr <- setupTraceDispatcher options.traceDispatcherCfg
   case options.mode of
     Offline -> do

bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs

@@ -1,4 +1,4 @@
-module Cardano.ReCon.Cli(Mode(..), CliOptions(..), opts) where
+module Cardano.ReCon.Cli(Timeunit(..), timeunitToMicrosecond, Mode(..), CliOptions(..), opts) where
 
 
 import           Control.Arrow ((>>>))
@@ -20,6 +20,7 @@ readMode = eitherReader $ \case
   "online"  -> Right Online
   _         -> Left "Expected either of: 'offline' or 'online'"
 
+
 readBool :: ReadM Bool
 readBool = eitherReader $ fmap toLower >>> \case
   "true"   -> Right True
@@ -31,6 +32,51 @@ readBool = eitherReader $ fmap toLower >>> \case
 parseMode :: Parser Mode
 parseMode = option readMode (long "mode" <> metavar "<offline|online>" <> help "mode")
 
+data Timeunit = Hour | Minute | Second | Millisecond | Microsecond deriving (Ord, Eq)
+
+-- | Convert `Timeunit` to μs.
+timeunitToMicrosecond :: Timeunit -> Word -> Word
+timeunitToMicrosecond Hour        = (3_600_000_000 *)
+timeunitToMicrosecond Minute      = (60_000_000 *)
+timeunitToMicrosecond Second      = (1_000_000 *)
+timeunitToMicrosecond Millisecond = (1_000 *)
+timeunitToMicrosecond Microsecond = id
+
+instance Show Timeunit where
+  show Hour        = "hour"
+  show Minute      = "minute"
+  show Second      = "second"
+  show Millisecond = "millisecond"
+  show Microsecond = "microsecond"
+
+readTimeunit :: ReadM Timeunit
+readTimeunit = eitherReader $ fmap toLower >>> \case
+  "hour"         -> Right Hour
+  "h"            -> Right Hour
+  "minute"       -> Right Minute
+  "min"          -> Right Minute
+  "m"            -> Right Minute
+  "second"       -> Right Second
+  "sec"          -> Right Second
+  "s"            -> Right Second
+  "millisecond"  -> Right Millisecond
+  "millisec"     -> Right Millisecond
+  "millis"       -> Right Millisecond
+  "ms"           -> Right Millisecond
+  "microsecond"  -> Right Microsecond
+  "microsec"     -> Right Microsecond
+  "micros"       -> Right Microsecond
+  "μs"           -> Right Microsecond
+  _              -> Left "Can't read a Timeunit"
+
+parseTimeunit :: Parser Timeunit
+parseTimeunit = option readTimeunit $
+     long "timeunit"
+  <> metavar "<hour|minute|second|millisecond|microsecond>"
+  <> showDefault
+  <> value Second
+  <> help "timeunit"
+
 parseEventDuration :: Parser Word
 parseEventDuration = option auto (long "duration" <> metavar "INT" <> help "temporal event duration (μs)")
 
@@ -82,6 +128,7 @@ data CliOptions = CliOptions
   , context             :: Maybe FilePath
   , enableProgressDumps :: Bool
   , enableSeekToEnd     :: Bool
+  , timeunit            :: Timeunit
   }
 
 parseCliOptions :: Parser CliOptions
@@ -95,6 +142,7 @@ parseCliOptions = CliOptions
               <*> parseContext
               <*> parseDumpMetrics
               <*> parseSeekToEnd
+              <*> parseTimeunit
 
 opts :: ParserInfo CliOptions
 opts = info (parseCliOptions <**> helper)

bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs

@@ -1,17 +1,31 @@
 module Cardano.ReCon.Common where
 import           Cardano.ReCon.LTL.Lang.Formula
 
-import           Data.Aeson
+import           Data.Aeson (Object, Value (..))
 import           Data.Aeson.Key (toText)
 import qualified Data.Aeson.KeyMap as KeyMap
 import qualified Data.Map as Map
 import           Data.Map.Strict (Map)
+import           Data.Text (Text)
 
--- | Extract all accessible properties (fields) from the json object, non-recursively.
---   Accessible fields are all fields of one of the following types: number, string.
-extractProps :: Object -> Map PropVarIdentifier PropValue
-extractProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
+-- | Extract integer properties from a JSON object.
+extractIntProps :: Object -> Map VariableIdentifier IntValue
+extractIntProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
   where
-    f (Number v)  = Just $ IntValue (truncate v)
-    f (String v)  = Just $ TextValue v
-    f _           = Nothing
+    f (Number v) = Just (truncate v)
+    f _          = Nothing
+
+-- | Extract text properties from a JSON object.
+extractTextProps :: Object -> Map VariableIdentifier Text
+extractTextProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
+  where
+    f (String v) = Just v
+    f _          = Nothing
+
+-- | Extract scalar properties from a JSON object as Aeson Values, for display.
+extractJsonProps :: Object -> Map Text Value
+extractJsonProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
+  where
+    f v@(Number _) = Just v
+    f v@(String _) = Just v
+    f _            = Nothing

bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs

@@ -5,8 +5,8 @@ module Cardano.ReCon.TraceMessage where
 import           Cardano.Logging
 import           Cardano.Logging.Prometheus.TCPServer (TracePrometheusSimple (..))
 import qualified Cardano.Logging.Types.TraceMessage as Envelop
-import           Cardano.ReCon.Common (extractProps)
-import           Cardano.ReCon.LTL.Lang.Formula (Formula, PropValue (..), Relevance)
+import           Cardano.ReCon.Common (extractJsonProps)
+import           Cardano.ReCon.LTL.Lang.Formula (Formula, Relevance)
 import qualified Cardano.ReCon.LTL.Lang.Formula.Prec as Prec
 import           Cardano.ReCon.LTL.Pretty (prettyFormula)
 import           Cardano.ReCon.LTL.Satisfy (SatisfactionResult (..))
@@ -61,11 +61,11 @@ red text = "\x001b[31m" <> text <> "\x001b[0m"
 prettyTraceMessage :: Envelop.TraceMessage -> Text
 prettyTraceMessage Envelop.TraceMessage{..} =
   toStrict $ toLazyText $ encodePrettyToTextBuilder  $
-    Map.insert "at" (TextValue (showT tmsgAt))       $
-      Map.insert "namespace" (TextValue tmsgNS)      $
-        Map.insert "host" (TextValue tmsgHost)       $
-          Map.insert "thread" (TextValue tmsgThread) $
-            extractProps tmsgData
+    Map.insert "at" (String (showT tmsgAt))        $
+      Map.insert "namespace" (String tmsgNS)       $
+        Map.insert "host" (String tmsgHost)        $
+          Map.insert "thread" (String tmsgThread)  $
+            extractJsonProps tmsgData
 
 prettyTemporalEvent :: TemporalEvent -> Text -> Text
 prettyTemporalEvent (TemporalEvent _ msgs) ns =

bench/cardano-recon-framework/cardano-recon-framework.cabal

@@ -4,7 +4,7 @@ description:        Cardano Re(altime) Con(formance) Framework based on Linear T
 category:           Cardano
                     Testing
 copyright:          2026 Intersect.
-version:            1.0.0
+version:            1.1.0
 license:            Apache-2.0
 license-files:      LICENSE
                     NOTICE
@@ -62,15 +62,13 @@ common common
 library
     import:           common
     exposed-modules:
-                      Cardano.ReCon.LTL.Check
+                      Cardano.ReCon.Common.BinRel
+                    , Cardano.ReCon.Common.Types
+                    , Cardano.ReCon.LTL.Check
                     , Cardano.ReCon.LTL.Lang.Formula
                     , Cardano.ReCon.LTL.Lang.Formula.Parser
                     , Cardano.ReCon.LTL.Lang.Formula.Prec
                     , Cardano.ReCon.LTL.Lang.Formula.Yaml
-                    , Cardano.ReCon.LTL.Lang.Fragment
-                    , Cardano.ReCon.LTL.Lang.Fragment.Fragment0
-                    , Cardano.ReCon.LTL.Lang.Fragment.Fragment1
-                    , Cardano.ReCon.LTL.Lang.Fragment.Fragment2
                     , Cardano.ReCon.LTL.Lang.HomogeneousFormula
                     , Cardano.ReCon.LTL.Occurs
                     , Cardano.ReCon.LTL.Pretty
@@ -79,10 +77,28 @@ library
                     , Cardano.ReCon.LTL.Satisfy
                     , Cardano.ReCon.LTL.Subst
 
+                    , Cardano.ReCon.Integer.Polynomial.Parser
+                    , Cardano.ReCon.Integer.Polynomial.Term
+                    , Cardano.ReCon.Integer.Polynomial.Value
+
+                    , Cardano.ReCon.Presburger.Decide
+                    , Cardano.ReCon.Presburger.Formula
+                    , Cardano.ReCon.Presburger.Parser
+
                     , Cardano.ReCon.Trace.Feed
                     , Cardano.ReCon.Trace.Ingest
 
     other-modules:
+                      Cardano.ReCon.LTL.Lang.HomogeneousFormula.IR.FinFree
+                    , Cardano.ReCon.LTL.Lang.HomogeneousFormula.IR.TextFree
+                    , Cardano.ReCon.Presburger.Internal.CooperQE
+                    , Cardano.ReCon.Presburger.Internal.IR.AffineDNF
+                    , Cardano.ReCon.Presburger.Internal.IR.CompNF
+                    , Cardano.ReCon.Presburger.Internal.IR.DNF
+                    , Cardano.ReCon.Presburger.Internal.IR.ForallFree
+                    , Cardano.ReCon.Presburger.Internal.IR.NegNF
+                    , Cardano.ReCon.Presburger.Internal.IR.NormAffineDNF
+                    , Cardano.ReCon.Presburger.Internal.IR.QuantifierFree
     other-extensions:
 
     build-depends:    base
@@ -147,6 +163,13 @@ test-suite cardano-recon-test
   type: exitcode-stdio-1.0
   hs-source-dirs: test
   main-is: Cardano/ReCon/Unit.hs
+  other-modules:
+      Cardano.ReCon.Integer.Polynomial.Semantics.Suite
+    , Cardano.ReCon.Integer.Polynomial.Syntax.Suite
+    , Cardano.ReCon.LTL.Semantics.Suite
+    , Cardano.ReCon.LTL.Syntax.Suite
+    , Cardano.ReCon.Presburger.Semantics.Suite
+    , Cardano.ReCon.Presburger.Syntax.Suite
   build-depends:
       base
     , cardano-recon-framework

bench/cardano-recon-framework/docs/ltl-formula-syntax.txt

@@ -1,11 +1,18 @@
-s ::= "..."        where ... stands for a list of arbitrary unicode characters such that each is:
-                      — not a control
-                      — if whitespace, then simple ' '
-                      — not a double quote
+<string> stands for a list of arbitrary unicode characters in double-quotes such that each is:
+            — not a control
+            — if whitespace, then simple ' '
+            — not a double quote
+<int> stands for an integer // examples: 0, -1, 42
+
 x ::= [_a-zA-Z][_a-zA-Z0-9]*
-v ::= <int> | s               // property value, examples:
-                              //   — 42
-                              //   — "hello"
+
+// integer (ℤ) terms
+i{atom} ::= <int> | (v{≥universe}) | x
+i{universe} ::= v{≥atom} + v{≥universe}
+
+// string terms
+s ::= <string>
+
 v̄ ::= {v, ..., v}             // set of property values, examples:
                               //   — {42, "hello"}
                               //   — {}
@@ -28,12 +35,13 @@ ns ::= s                      // namespace, examples:
                               //   — "Forge.Loop.NodeIsLeader"
 
 φ{atom} ::= ⊤ | ⊥ | ns c̄ | (φ{≥universe})
-φ{eq} ::= t = v
+φ{eq} ::= i = i | i < i | i > i | i ≤ i | i ≥ i | <int> \| i
 φ{prefix} ::= ◯ φ{≥atom} | ◯ᵏ φ{≥atom} | ♢ᵏ φ{≥atom} | ☐ ᪲ₖ φ{≥atom} | ☐ᵏ φ{≥atom} | ¬ φ{≥atom}
 φ{and} ::= φ{>and} ∧ φ{≥and}
 φ{or} ::= φ{>or} ∨ φ{≥or}
 φ{implies} ::= φ{>implies} ⇒ φ{≥implies}
-φ{universe} ::= ∀(x ∈ v̄). φ{≥universe}
-              | ∀x. φ{≥universe} | φ{≥implies} \|ᵏ φ{≥implies}
+φ{universe} ::= ∀x ∈ v̄. φ{≥universe} | ∀x : Int. φ{≥universe} | ∀x : Text. φ{≥universe}
+              | ∃x ∈ v̄. φ{≥universe} | ∃x : Int. φ{≥universe} | ∃x : Text. φ{≥universe}
+              | φ{≥implies} \|ᵏ φ{≥implies}
 
 atom < eq = prefix < and < or < implies < universe