bench: cardano-recon-framework configurable timeunits in formulas

bench/cardano-recon-framework/CHANGELOG.md

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

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

@@ -7,7 +7,7 @@ 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.Cli (CliOptions (..), Mode (..), opts, timeunitToMicrosecond)
 import           Cardano.ReCon.Common (extractProps)
 import           Cardano.ReCon.LTL.Check (checkFormula, prettyError)
 import           Cardano.ReCon.LTL.Lang.Formula
@@ -37,13 +37,13 @@ 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
 
 
@@ -107,10 +107,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
@@ -164,7 +160,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/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

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

@@ -33,7 +33,8 @@ ns ::= s                      // namespace, examples:
 φ{and} ::= φ{>and} ∧ φ{≥and}
 φ{or} ::= φ{>or} ∨ φ{≥or}
 φ{implies} ::= φ{>implies} ⇒ φ{≥implies}
-φ{universe} ::= ∀(x ∈ v̄). φ{≥universe}
-              | ∀x. φ{≥universe} | φ{≥implies} \|ᵏ φ{≥implies}
+φ{universe} ::= ∀(x ∈ v̄). φ{≥universe} | ∀x. φ{≥universe}
+              | ∃(x ∈ v̄). φ{≥universe} | ∃x. φ{≥universe}
+              | φ{≥implies} \|ᵏ φ{≥implies}
 
 atom < eq = prefix < and < or < implies < universe

bench/cardano-recon-framework/docs/satisfiability-semantics.txt

@@ -35,6 +35,8 @@
  t̄ ⊧ φ     // connective & event property fragments
 (t̄ ⊧ ∀x. φ)         ⇔ (∀x. (t̄ ⊧ φ))
 (t̄ ⊧ ∀(x ∈ v̄). φ)   ⇔ (∀(x ∈ v̄). (t̄ ⊧ φ))
+(t̄ ⊧ ∃x. φ)         ⇔ (∃x. (t̄ ⊧ φ))
+(t̄ ⊧ ∃(x ∈ v̄). φ)   ⇔ (∃(x ∈ v̄). (t̄ ⊧ φ))
 (t̄ ⊧ φ ∨ ψ)         ⇔ ((t̄ ⊧ φ) ∨ (t̄ ⊧ ψ))
 (t̄ ⊧ φ ∧ ψ)         ⇔ ((t̄ ⊧ φ) ∧ (t̄ ⊧ ψ))
 (t̄ ⊧ φ ⇒ ψ)         ⇔ ((t̄ ⊧ φ) ⇒ (t̄ ⊧ ψ))

bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Check.hs

@@ -54,5 +54,7 @@ checkFormula bound (Implies phi psi) = checkFormula bound phi ++ checkFormula bo
 checkFormula bound (UntilN _ phi psi) = checkFormula bound phi ++ checkFormula bound psi
 checkFormula bound (PropForall x phi) = checkFormula (insert x bound) phi
 checkFormula bound (PropForallN x _ phi) = checkFormula (insert x bound) phi
+checkFormula bound (PropExists x phi) = checkFormula (insert x bound) phi
+checkFormula bound (PropExistsN x _ phi) = checkFormula (insert x bound) phi
 checkFormula bound (PropEq _ t _) = checkParamTerm bound t
 checkFormula bound (Atom _ cs) = foldl' (++) [] (fmap (checkParamConstraint bound) (Set.toList cs))

bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula.hs

@@ -111,6 +111,11 @@ data Formula event ty =
      -- | ∀(x ∈ v̄). φ
      --   `x` ranges over values in `v̄`
    | PropForallN PropVarIdentifier (Set PropValue) (Formula event ty)
+     -- | ∃x. φ
+   | PropExists PropVarIdentifier (Formula event ty)
+     -- | ∃(x ∈ v̄). φ
+     --   `x` ranges over values in `v̄`
+   | PropExistsN PropVarIdentifier (Set PropValue) (Formula event ty)
      -- | i = v
    | PropEq (Relevance event ty) PropTerm PropValue deriving (Show, Eq, Ord)
    -------------------------------------
@@ -135,6 +140,8 @@ relevance = go mempty where
   go acc (Atom {})             = acc
   go acc (PropForall _ phi)    = go acc phi
   go acc (PropForallN _ _ phi) = go acc phi
+  go acc (PropExists _ phi)    = go acc phi
+  go acc (PropExistsN _ _ phi) = go acc phi
   go acc (PropEq rel _ _)      = rel `union` acc
 
 unfoldForall :: Word -> Formula event ty -> Formula event ty
@@ -189,6 +196,8 @@ interpTimeunit _ phi@Atom{} = phi
 interpTimeunit _ phi@PropEq{} = phi
 interpTimeunit f (PropForall x phi) = PropForall x (interpTimeunit f phi)
 interpTimeunit f (PropForallN x dom phi) = PropForallN x dom (interpTimeunit f phi)
+interpTimeunit f (PropExists x phi) = PropExists x (interpTimeunit f phi)
+interpTimeunit f (PropExistsN x dom phi) = PropExistsN x dom (interpTimeunit f phi)
 
 -- | A constraint signifying that `a` is an `Event` over base `ty`:
 --    — Given an element of `ty`, `ofTy` shall name whether the event is of the given type.

bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula/Parser.hs

@@ -196,6 +196,20 @@ formulaPropForall ctx ty = do
   phi <- formulaUniverse ctx ty
   pure (maybe (PropForall x phi) (\dom -> PropForallN x dom phi) optDom)
 
+formulaPropExists :: Context -> Parser ty -> Parser (Formula event ty)
+formulaPropExists ctx ty = do
+  void $ string "∃"
+  space
+  x <- variableIdentifier
+  space
+  optDom <- optional $ do
+    void $ string "∈"
+    space *> setPropValue ctx <* space
+  void $ string "."
+  space
+  phi <- formulaUniverse ctx ty
+  pure (maybe (PropExists x phi) (\dom -> PropExistsN x dom phi) optDom)
+
 formulaPropForallN :: Context -> Parser ty -> Parser (Formula event ty)
 formulaPropForallN ctx ty = do
   void $ try (string "∀" *> space *> string "(" *> space)
@@ -212,6 +226,22 @@ formulaPropForallN ctx ty = do
   phi <- formulaUniverse ctx ty
   pure (PropForallN x vs phi)
 
+formulaPropExistsN :: Context -> Parser ty -> Parser (Formula event ty)
+formulaPropExistsN ctx ty = do
+  void $ try (string "∃" *> space *> string "(" *> space)
+  x <- variableIdentifier
+  space
+  void $ string "∈"
+  space
+  vs <- setPropValue ctx
+  space
+  void $ string ")"
+  space
+  void $ string "."
+  space
+  phi <- formulaUniverse ctx ty
+  pure (PropExistsN x vs phi)
+
 formulaUntilN :: Context -> Parser ty -> Parser (Formula event ty)
 formulaUntilN ctx ty = apply <$> (formulaImplies ctx ty <* space) <*> optional (do
      void $ string "|"
@@ -224,7 +254,11 @@ formulaUntilN ctx ty = apply <$> (formulaImplies ctx ty <* space) <*> optional (
   apply phi (Just (!k, !psi)) = UntilN k phi psi
 
 formulaUniverse :: Context -> Parser ty -> Parser (Formula event ty)
-formulaUniverse ctx ty = formulaPropForallN ctx ty <|> formulaPropForall ctx ty <|> formulaUntilN ctx ty
+formulaUniverse ctx ty = formulaPropForallN ctx ty
+                     <|> formulaPropForall ctx ty
+                     <|> formulaPropExistsN ctx ty
+                     <|> formulaPropExists ctx ty
+                     <|> formulaUntilN ctx ty
 
 formula :: Context -> Parser ty -> Parser (Formula event ty)
 formula = formulaUniverse

bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Fragment.hs

@@ -28,7 +28,9 @@ retract abs (F.Not a)        = F0.Not <$> retract abs a
 retract _ F.Top              = Just F0.Top
 retract _ F.Bottom           = Just F0.Bottom
 retract _ (F.PropForall {})  = Nothing
+retract _ (F.PropExists {})  = Nothing
 retract _ (F.PropForallN {}) = Nothing
+retract _ (F.PropExistsN {}) = Nothing
 retract (!x, !v) (F.PropEq rel (Var x') v') | x == x' && v == v'
                              = Just (F0.Atom rel)
 retract _ (F.PropEq {})      = Nothing
@@ -77,7 +79,9 @@ findAtoms F.Top set                   = set
 findAtoms (F.PropEq _ (Var x) v) set  = Set.insert (x, v) set
 findAtoms (F.PropEq {}) set           = set
 findAtoms (F.PropForall _ phi) set    = findAtoms phi set
+findAtoms (F.PropExists _ phi) set    = findAtoms phi set
 findAtoms (F.PropForallN _ _ phi) set = findAtoms phi set
+findAtoms (F.PropExistsN _ _ phi) set = findAtoms phi set
 
 -- | Given a set of propositional equalities {xᵢ = vᵢ}ᵢ and a formula, if the formula can be retracted into
 --   `Fragment0` where the atom is taken to be one of the equalities (xᵢ = vᵢ), computes normal form in `Fragment0` and

bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/HomogeneousFormula.hs

@@ -1,4 +1,6 @@
 {- HLINT ignore "Use all" -}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Use any" #-}
 module Cardano.ReCon.LTL.Lang.HomogeneousFormula (
     HomogeneousFormula(..)
   , toFormula
@@ -37,6 +39,8 @@ data HomogeneousFormula event ty =
    ----------- Event property ----------
    | PropForall PropVarIdentifier (HomogeneousFormula event ty)
    | PropForallN PropVarIdentifier (Set PropValue) (HomogeneousFormula event ty)
+   | PropExists PropVarIdentifier (HomogeneousFormula event ty)
+   | PropExistsN PropVarIdentifier (Set PropValue) (HomogeneousFormula event ty)
    | PropEq (Relevance event ty) PropTerm PropValue deriving (Show, Eq, Ord)
    -------------------------------------
 
@@ -50,6 +54,8 @@ toFormula Top                     = F.Top
 toFormula (PropEq e a b)          = F.PropEq e a b
 toFormula (PropForall x phi)      = F.PropForall x (toFormula phi)
 toFormula (PropForallN x dom phi) = F.PropForallN x dom (toFormula phi)
+toFormula (PropExists x phi)      = F.PropExists x (toFormula phi)
+toFormula (PropExistsN x dom phi) = F.PropExistsN x dom (toFormula phi)
 
 valuesAccum :: Set PropValue -> PropVarIdentifier -> HomogeneousFormula event ty -> Set PropValue
 valuesAccum acc x (Or phi psi) = valuesAccum (valuesAccum acc x phi) x psi
@@ -65,6 +71,10 @@ valuesAccum acc x (PropForall x' phi) | x /= x' = valuesAccum acc x phi
 valuesAccum acc _ (PropForall _ _) = acc
 valuesAccum acc x (PropForallN x' _ phi) | x /= x' = valuesAccum acc x phi
 valuesAccum acc _ (PropForallN {}) = acc
+valuesAccum acc x (PropExists x' phi) | x /= x' = valuesAccum acc x phi
+valuesAccum acc _ (PropExists _ _) = acc
+valuesAccum acc x (PropExistsN x' _ phi) | x /= x' = valuesAccum acc x phi
+valuesAccum acc _ (PropExistsN {}) = acc
 
 -- | Set of values the given prop var can take in the formula.
 values :: PropVarIdentifier -> HomogeneousFormula event ty -> Set PropValue
@@ -88,6 +98,10 @@ substHomogeneousFormula v x (PropForall x' phi) | x /= x' = PropForall x' (subst
 substHomogeneousFormula _ _ (PropForall x' phi) = PropForall x' phi
 substHomogeneousFormula v x (PropForallN x' dom phi) | x /= x' = PropForallN x' dom (substHomogeneousFormula v x phi)
 substHomogeneousFormula _ _ (PropForallN x' dom phi) = PropForallN x' dom phi
+substHomogeneousFormula v x (PropExists x' phi) | x /= x' = PropExists x' (substHomogeneousFormula v x phi)
+substHomogeneousFormula _ _ (PropExists x' phi) = PropExists x' phi
+substHomogeneousFormula v x (PropExistsN x' dom phi) | x /= x' = PropExistsN x' dom (substHomogeneousFormula v x phi)
+substHomogeneousFormula _ _ (PropExistsN x' dom phi) = PropExistsN x' dom phi
 
 -- | Evaluate the `HomogeneousFormula` onto `Bool`.
 --   This is the "interesting" part of the iso: `HomogeneousFormula` ≅ `Bool`
@@ -112,6 +126,18 @@ eval (PropForallN x dom phi) =
     Set.toList dom <&> \v ->
       eval (substHomogeneousFormula (Val v) x phi)
   )
+-- ⟦∃x. φ⟧ <=> φ[☐/x] ∨ φ[v₁ / x] ∨ ... ∨ φ[vₖ / x] where v₁...vₖ is the set of values in φ which x can take.
+eval (PropExists x phi) = eval (substHomogeneousFormula Placeholder x phi) ||
+  Prelude.or (
+    Set.toList (values x phi) <&> \v ->
+      eval (substHomogeneousFormula (Val v) x phi)
+  )
+-- ⟦∃(x ∈ v₁...vₖ). φ⟧ <=> φ[v₁ / x] ∨ ... ∨ φ[vₖ / x]
+eval (PropExistsN x dom phi) =
+  Prelude.or (
+    Set.toList dom <&> \v ->
+      eval (substHomogeneousFormula (Val v) x phi)
+  )
 
 -- | This is the "easy" part of the iso: `HomogeneousFormula` ≅ `Bool`
 quote :: Bool -> HomogeneousFormula event ty
@@ -144,6 +170,8 @@ retract = go Set.empty where
   go _     (F.PropEq _ (Var _) _)        = Nothing
   go bound (F.PropForall x phi)          = PropForall x <$> go (Set.insert x bound) phi
   go bound (F.PropForallN x dom phi)     = PropForallN x dom <$> go (Set.insert x bound) phi
+  go bound (F.PropExists x phi)          = PropExists x <$> go (Set.insert x bound) phi
+  go bound (F.PropExistsN x dom phi)     = PropExistsN x dom <$> go (Set.insert x bound) phi
 
 normaliseHomogeneous :: Formula event ty -> Maybe (Formula event ty)
 normaliseHomogeneous phi =

bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Occurs.hs

@@ -39,5 +39,9 @@ occursFormula x (PropForall x' _) | x == x' = False
 occursFormula x (PropForall _ phi) = occursFormula x phi
 occursFormula x (PropForallN x' _ _) | x == x' = False
 occursFormula x (PropForallN _ _ phi) = occursFormula x phi
+occursFormula x (PropExists x' _) | x == x' = False
+occursFormula x (PropExists _ phi) = occursFormula x phi
+occursFormula x (PropExistsN x' _ _) | x == x' = False
+occursFormula x (PropExistsN _ _ phi) = occursFormula x phi
 occursFormula x (Atom _ is) = foldl' (\acc phi -> acc || occursPropConstraint x phi) False is
 occursFormula x (PropEq _ t _) = occursPropTerm x t

bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Pretty.hs

@@ -114,6 +114,12 @@ prettyFormula (PropForallN x dom phi) lvl = surround lvl Prec.Universe $
   "∀" <> "(" <> x <> " ∈ "
       <> "{" <> intercalate ", " (fmap prettyPropValue (Set.toList dom)) <> "}"
       <> ")" <> ". " <> prettyFormula phi Prec.Universe
+prettyFormula (PropExistsN x dom phi) lvl = surround lvl Prec.Universe $
+  "∃" <> "(" <> x <> " ∈ "
+      <> "{" <> intercalate ", " (fmap prettyPropValue (Set.toList dom)) <> "}"
+      <> ")" <> ". " <> prettyFormula phi Prec.Universe
+prettyFormula (PropExists x phi) lvl = surround lvl Prec.Universe $
+  "∃" <> x <> ". " <> prettyFormula phi Prec.Universe
 prettyFormula (Atom c is) lvl = surround lvl Prec.Atom $
   showT c <> "(" <> prettyPropConstraints (Set.toList is) <> ")"
 prettyFormula (PropEq _ t v) lvl = surround lvl Prec.Eq $