From 06fc91f0bd8be482ea97ad22dfe3870d5ff617ca Mon Sep 17 00:00:00 2001 From: Russoul Date: Fri, 13 Mar 2026 15:14:59 +0300 Subject: [PATCH 1/2] bench: cardano-recon-framework configurable timeunits in formulas --- bench/cardano-recon-framework/CHANGELOG.md | 4 ++ .../app/Cardano/ReCon.hs | 10 ++-- .../app/Cardano/ReCon/Cli.hs | 50 ++++++++++++++++++- .../cardano-recon-framework.cabal | 2 +- 4 files changed, 57 insertions(+), 9 deletions(-) diff --git a/bench/cardano-recon-framework/CHANGELOG.md b/bench/cardano-recon-framework/CHANGELOG.md index d8a905440ba..b8e29f7b0e7 100644 --- a/bench/cardano-recon-framework/CHANGELOG.md +++ b/bench/cardano-recon-framework/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for cardano-trace-ltl +## 1.1.0 -- March 2026 + +* Support configurable timeunits in formulas via a CLI option. + ## 1.0.0 -- Feb 2026 * First version. diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon.hs b/bench/cardano-recon-framework/app/Cardano/ReCon.hs index a3d10111ba2..fc0244334de 100644 --- a/bench/cardano-recon-framework/app/Cardano/ReCon.hs +++ b/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 diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs index 86e725b31ea..4f68f2becd2 100644 --- a/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs +++ b/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 "" <> 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 "" + <> 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) diff --git a/bench/cardano-recon-framework/cardano-recon-framework.cabal b/bench/cardano-recon-framework/cardano-recon-framework.cabal index 6c729ec13d2..9090f66e306 100644 --- a/bench/cardano-recon-framework/cardano-recon-framework.cabal +++ b/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 From 352fe4d53c74e2c2cf29baef7e56eb6c70f6990c Mon Sep 17 00:00:00 2001 From: Russoul Date: Tue, 24 Mar 2026 16:11:52 +0400 Subject: [PATCH 2/2] Support existential quantification over properties --- bench/cardano-recon-framework/CHANGELOG.md | 1 + .../docs/ltl-formula-syntax.txt | 5 +- .../docs/satisfiability-semantics.txt | 2 + .../src/Cardano/ReCon/LTL/Check.hs | 2 + .../src/Cardano/ReCon/LTL/Lang/Formula.hs | 9 +++ .../Cardano/ReCon/LTL/Lang/Formula/Parser.hs | 36 ++++++++- .../src/Cardano/ReCon/LTL/Lang/Fragment.hs | 4 + .../ReCon/LTL/Lang/HomogeneousFormula.hs | 28 +++++++ .../src/Cardano/ReCon/LTL/Occurs.hs | 4 + .../src/Cardano/ReCon/LTL/Pretty.hs | 6 ++ .../src/Cardano/ReCon/LTL/Progress.hs | 6 ++ .../src/Cardano/ReCon/LTL/Rewrite.hs | 18 +++++ .../src/Cardano/ReCon/LTL/Subst.hs | 4 + .../test/Cardano/ReCon/Unit.hs | 74 ++++++++++++++++++- 14 files changed, 195 insertions(+), 4 deletions(-) diff --git a/bench/cardano-recon-framework/CHANGELOG.md b/bench/cardano-recon-framework/CHANGELOG.md index b8e29f7b0e7..f9bc34cc2c4 100644 --- a/bench/cardano-recon-framework/CHANGELOG.md +++ b/bench/cardano-recon-framework/CHANGELOG.md @@ -3,6 +3,7 @@ ## 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 diff --git a/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt b/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt index acc805aaf75..bbed42545ef 100644 --- a/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt +++ b/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 diff --git a/bench/cardano-recon-framework/docs/satisfiability-semantics.txt b/bench/cardano-recon-framework/docs/satisfiability-semantics.txt index 0936d6515b0..91f92548adf 100644 --- a/bench/cardano-recon-framework/docs/satisfiability-semantics.txt +++ b/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̄ ⊧ ψ)) diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Check.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Check.hs index 91fc5225ab2..141b0db1de5 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Check.hs +++ b/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)) diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula.hs index 83e82d28aa3..53d97c88075 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula.hs +++ b/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. diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula/Parser.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula/Parser.hs index 45d7394053d..67f31530848 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula/Parser.hs +++ b/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 diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Fragment.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Fragment.hs index deaa16b0ad6..fcc28955b87 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Fragment.hs +++ b/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 diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/HomogeneousFormula.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/HomogeneousFormula.hs index 8a5579f9afc..05d571a6599 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/HomogeneousFormula.hs +++ b/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 = diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Occurs.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Occurs.hs index 6d85b78afc6..223625cebf8 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Occurs.hs +++ b/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 diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Pretty.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Pretty.hs index a76bca380da..d15c89efc32 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Pretty.hs +++ b/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 $ diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Progress.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Progress.hs index 7d2e06c3d4b..82507e6d04b 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Progress.hs +++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Progress.hs @@ -49,6 +49,8 @@ next (Atom c is) s | ofTy s c = next (Atom {}) _ = Bottom next (PropForall x phi) s = PropForall x (next phi s) next (PropForallN x dom phi) s = PropForallN x dom (next phi s) +next (PropExists x phi) s = PropExists x (next phi s) +next (PropExistsN x dom phi) s = PropExistsN x dom (next phi s) next (PropEq rel a b) _ = PropEq rel a b -- | This is an algorithm for (∅ ⊧ ◯ φ) @@ -61,6 +63,8 @@ terminateNext (Implies phi psi) = terminateNext phi `H.Implies` terminateNext ps terminateNext (Not phi) = H.Not (terminateNext phi) terminateNext (PropForall x phi) = H.PropForall x (terminateNext phi) terminateNext (PropForallN x dom phi) = H.PropForallN x dom (terminateNext phi) +terminateNext (PropExists x phi) = H.PropExists x (terminateNext phi) +terminateNext (PropExistsN x dom phi) = H.PropExistsN x dom (terminateNext phi) terminateNext (PropEq rel t v) = H.PropEq rel t v terminateNext (NextN _ phi) = terminateNext phi terminateNext (Atom ty cs) = terminate (Atom ty cs) @@ -86,5 +90,7 @@ terminate (Not phi) = H.Not (terminate phi) terminate Bottom = H.Bottom terminate Top = H.Top terminate (PropForall x phi) = H.PropForall x (terminate phi) +terminate (PropExists x phi) = H.PropExists x (terminate phi) terminate (PropForallN x dom phi) = H.PropForallN x dom (terminate phi) +terminate (PropExistsN x dom phi) = H.PropExistsN x dom (terminate phi) terminate (PropEq rel a b) = H.PropEq rel a b diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Rewrite.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Rewrite.hs index 3e58b6dc4c4..509128cc54a 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Rewrite.hs +++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Rewrite.hs @@ -37,6 +37,8 @@ recurseHomogeneous f self@Top = fromMaybe self (f self) recurseHomogeneous f self@(PropEq {}) = fromMaybe self (f self) recurseHomogeneous f self@(PropForall x phi) = fromMaybe (PropForall x (recurseHomogeneous f phi)) (f self) recurseHomogeneous f self@(PropForallN x dom phi) = fromMaybe (PropForallN x dom (recurseHomogeneous f phi)) (f self) +recurseHomogeneous f self@(PropExists x phi) = fromMaybe (PropExists x (recurseHomogeneous f phi)) (f self) +recurseHomogeneous f self@(PropExistsN x dom phi) = fromMaybe (PropExistsN x dom (recurseHomogeneous f phi)) (f self) -- | Rewrite the formula by applying the fragment retraction & normalisation recursively. rewriteFragment :: (Ord event, Ord ty) => Formula event ty -> Formula event ty @@ -70,9 +72,14 @@ rewriteHomogeneous = recurseHomogeneous normaliseHomogeneous -- (v = v') = ⊥ where v ≠ v' -- ∀x. ⊤ = ⊤ -- ∀x. ⊥ = ⊥ +-- ∃x. ⊤ = ⊤ +-- ∃x. ⊥ = ⊥ -- ∀(x ∈ ∅). φ = ⊤ -- ∀(x ∈ {v} ⊔ v̄). ⊥ = ⊥ -- ∀(x ∈ {v} ⊔ v̄). ⊤ = ⊤ +-- ∃(x ∈ ∅). φ = ⊥ +-- ∃(x ∈ {v} ⊔ v̄). ⊥ = ⊥ +-- ∃(x ∈ {v} ⊔ v̄). ⊤ = ⊤ -- Additionally, unfolds base-cases of finite temporal operators. rewriteIdentity :: Eq ty => Formula event ty -> Formula event ty rewriteIdentity (Forall k phi) = @@ -135,9 +142,20 @@ rewriteIdentity (PropForall x phi) = Top -> Top Bottom -> Bottom phi' -> PropForall x phi' +rewriteIdentity (PropExists x phi) = + case rewriteIdentity phi of + Top -> Top + Bottom -> Bottom + phi' -> PropExists x phi' rewriteIdentity (PropForallN _ dom _) | Set.null dom = Top rewriteIdentity (PropForallN x dom phi) = case rewriteIdentity phi of Top -> Top Bottom -> Bottom phi' -> PropForallN x dom phi' +rewriteIdentity (PropExistsN _ dom _) | Set.null dom = Bottom +rewriteIdentity (PropExistsN x dom phi) = + case rewriteIdentity phi of + Top -> Top + Bottom -> Bottom + phi' -> PropExistsN x dom phi' diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Subst.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Subst.hs index 2fe9b1ccc21..8547c19b0fa 100644 --- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Subst.hs +++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Subst.hs @@ -36,6 +36,10 @@ substFormula _ _ Bottom = Bottom substFormula _ _ Top = Top substFormula _ x (PropForall x' e) | x == x' = PropForall x' e substFormula v x (PropForall x' e) = PropForall x' (substFormula v x e) +substFormula _ x (PropExists x' e) | x == x' = PropExists x' e +substFormula v x (PropExists x' e) = PropExists x' (substFormula v x e) substFormula _ x (PropForallN x' dom e) | x == x' = PropForallN x' dom e substFormula v x (PropForallN x' dom e) = PropForallN x' dom (substFormula v x e) +substFormula _ x (PropExistsN x' dom e) | x == x' = PropExistsN x' dom e +substFormula v x (PropExistsN x' dom e) = PropExistsN x' dom (substFormula v x e) substFormula v x (PropEq rel t rhs) = PropEq rel (substPropTerm v x t) rhs diff --git a/bench/cardano-recon-framework/test/Cardano/ReCon/Unit.hs b/bench/cardano-recon-framework/test/Cardano/ReCon/Unit.hs index f3d4ac09bfc..53d24d2c799 100644 --- a/bench/cardano-recon-framework/test/Cardano/ReCon/Unit.hs +++ b/bench/cardano-recon-framework/test/Cardano/ReCon/Unit.hs @@ -106,6 +106,27 @@ log11 = , Msg Success 2 ] +log12 :: [Msg] +log12 = + [ + Msg Start 1 + , Placeholder + , Msg Success 1 + , Msg Start 2 + , Placeholder + ] + +log13 :: [Msg] +log13 = + [ + Msg Start 1 + , Placeholder + , Msg Success 0 + , Msg Start 2 + , Msg Success 2 + , Placeholder + ] + logEmpty :: [Msg] logEmpty = [] @@ -134,13 +155,32 @@ prop2 = PropForall "i" $ UntilN ) (Atom Start (fromList [PropConstraint "idx" (Var "i")])) +-- ☐ (∃i. i = 1 ∧ (Start("idx" = i) ⇒ ♢³ Success("idx" = i))) +prop3 :: Formula Msg Ty +prop3 = Forall 0 $ PropExists "i" $ And + (PropEq mempty (Var "i") (IntValue 1)) + ( + Implies + (Atom Start (fromList [PropConstraint "idx" (Var "i")])) + ( + ExistsN 3 + (Atom Success (fromList [PropConstraint "idx" (Var "i")])) + ) + ) + main :: IO () main = do setLocaleEncoding utf8 defaultMain tests tests :: TestTree -tests = testGroup "Unit tests" [syntacticTests, prop1SatisfiabilityTests, prop2SatisfiabilityTests, parserTests] +tests = testGroup "Unit tests" + [ syntacticTests + , prop1SatisfiabilityTests + , prop2SatisfiabilityTests + , prop3SatisfiabilityTests + , parserTests + ] syn1 :: Formula event () syn1 = PropForall "i" (Atom () (fromList [PropConstraint "idx" (Var "i")])) @@ -148,6 +188,12 @@ syn1 = PropForall "i" (Atom () (fromList [PropConstraint "idx" (Var "i")])) syn2 :: Formula event () syn2 = PropForall "i" (Atom () (fromList [PropConstraint "idx" (Var "j")])) +syn3 :: Formula event () +syn3 = PropExists "i" (Atom () (fromList [PropConstraint "idx" (Var "i")])) + +syn4 :: Formula event () +syn4 = PropExists "i" (Atom () (fromList [PropConstraint "idx" (Var "j")])) + syntacticTests :: TestTree syntacticTests = testGroup "Syntanctic checks" [ @@ -156,6 +202,11 @@ syntacticTests = testGroup "Syntanctic checks" , testCase (unpack $ prettyFormula syn2 Prec.Universe <> " is syntactically invalid") $ [UnboundPropVarIdentifier "j"] @?= checkFormula mempty syn2 + , testCase (unpack $ prettyFormula syn3 Prec.Universe <> " is syntactically valid") $ + [] @?= checkFormula mempty syn3 + , + testCase (unpack $ prettyFormula syn4 Prec.Universe <> " is syntactically invalid") $ + [UnboundPropVarIdentifier "j"] @?= checkFormula mempty syn4 ] prop1SatisfiabilityTests :: TestTree @@ -203,6 +254,15 @@ prop2SatisfiabilityTests = testGroup ("Satisfiability of: " <> unpack (prettyFor ] +prop3SatisfiabilityTests :: TestTree +prop3SatisfiabilityTests = testGroup ("Satisfiability of: " <> unpack (prettyFormula prop3 Prec.Universe)) + [ + testCase (show log12 <> " satisfies the formula") $ + satisfies prop3 log12 @?= Satisfied + , testCase (show log13 <> " does not satisfy the formula") $ + satisfies prop3 log13 @?= Unsatisfied (fromList [(Msg Start 1,Start),(Msg Success 0,Success)]) + ] + formula0 :: Text formula0 = "☐ ᪲ (∀x. \"Forge.Loop.StartLeadershipCheck\"{\"slot\" = x} ⇒ \ \♢³⁰⁰⁰ (\"Forge.Loop.NodeIsLeader\"{\"slot\" = x} ∨ \"Forge.Loop.NodeNotLeader\"{\"slot\" = x}))" @@ -224,6 +284,9 @@ formula4 = "∀(x ∈ {1, 2, 3}). x = 1 ∨ x = 2 ∨ x = 3" formula5 :: Text formula5 = "∀x ∈ {1, 2, 3}. x = 1 ∨ x = 2 ∨ x = 3" +formula6 :: Text +formula6 = "∃x ∈ {1, 2, 3}. x = 1" + emptyCtx :: Context emptyCtx = Context [] @@ -291,4 +354,13 @@ parserTests = testGroup "Parsing" (Or (PropEq (fromList []) (Var "x") (IntValue 2)) (PropEq (fromList []) (Var "x") (IntValue 3))))) + , + testCase (Text.unpack formula6) $ + parse (Parser.formula @Text @() emptyCtx Parser.text) "input" formula6 @?= + Right + (PropExistsN + "x" + (fromList [IntValue 1,IntValue 2,IntValue 3]) + (PropEq (fromList []) (Var "x") (IntValue 1)) + ) ]