Skip to content

Commit 51b6046

Browse files
mgmeiermgmeier
authored
Merge pull request #6531 from IntersectMBO/russoul/bench-recon-1.1.0
ReCon framework 1.1.0
2 parents 5fb5c54 + abb8bd9 commit 51b6046

67 files changed

Lines changed: 3550 additions & 1259 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎bench/cardano-recon-framework/CHANGELOG.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,11 @@
11
# Revision history for cardano-trace-ltl
22

3+
## 1.1.0 -- April 2026
4+
5+
* Support configurable timeunits in formulas via a CLI option.
6+
* Support existential quantification over properties (both finite and infinite domain)
7+
* Support Presburger arithmetic (over ℤ)
8+
39
## 1.0.0 -- Feb 2026
410

511
* First version.

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

Lines changed: 14 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,20 @@
1-
{-# OPTIONS_GHC -Wno-orphans #-}
21
{-# LANGUAGE PackageImports #-}
32

43
module Main(main) where
54

65
import Cardano.Logging
76
import Cardano.Logging.Prometheus.TCPServer (TracePrometheusSimple (..),
87
runPrometheusSimple)
9-
import Cardano.Logging.Types.TraceMessage (TraceMessage (..))
10-
import Cardano.ReCon.Cli (CliOptions (..), Mode (..), opts)
11-
import Cardano.ReCon.Common (extractProps)
8+
import Cardano.Logging.Types.TraceMessage ()
9+
import Cardano.ReCon.Cli (CliOptions (..), Mode (..), opts, timeunitToMicrosecond)
10+
import Cardano.ReCon.Trace.Event ()
1211
import Cardano.ReCon.LTL.Check (checkFormula, prettyError)
13-
import Cardano.ReCon.LTL.Lang.Formula
14-
import Cardano.ReCon.LTL.Lang.Formula.Parser (Context (..))
15-
import qualified Cardano.ReCon.LTL.Lang.Formula.Parser as Parser
16-
import Cardano.ReCon.LTL.Lang.Formula.Yaml
17-
import Cardano.ReCon.LTL.Pretty (prettyFormula)
18-
import qualified Cardano.ReCon.LTL.Pretty as Prec
12+
import Cardano.ReCon.LTL.Formula
13+
import Cardano.ReCon.LTL.Formula.Parser (Context (..))
14+
import qualified Cardano.ReCon.LTL.Formula.Parser as Parser
15+
import Cardano.ReCon.LTL.Formula.Yaml
16+
import Cardano.ReCon.LTL.Formula.Pretty (prettyFormula)
17+
import qualified Cardano.ReCon.LTL.Formula.Pretty as Prec
1918
import Cardano.ReCon.LTL.Satisfy
2019
import Cardano.ReCon.Trace.Feed (TemporalEvent (..), TemporalEventDurationMicrosec, read,
2120
readS)
@@ -31,32 +30,21 @@ import Control.Monad (forever, when, (>=>))
3130
import "contra-tracer" Control.Tracer (Tracer (..))
3231
import Data.Foldable (for_)
3332
import Data.IORef (IORef, newIORef, readIORef)
34-
import Data.List (find)
3533
import qualified Data.Map as Map
36-
import Data.Maybe (fromMaybe, isJust, listToMaybe)
37-
import Data.Text (Text, unpack)
34+
import Data.Maybe (fromMaybe, listToMaybe)
35+
import Data.Text (Text)
3836
import qualified Data.Text as Text
3937
import Data.Traversable (for)
38+
import GHC.IO.Encoding (setLocaleEncoding, utf8)
4039
import Network.HostName (HostName)
4140
import Network.Socket (PortNumber)
4241
import Options.Applicative hiding (Success)
4342
import System.Exit (die)
4443
import qualified System.Metrics as EKG
4544

46-
import GHC.IO.Encoding (setLocaleEncoding, utf8)
4745
import Streaming
4846

4947

50-
instance Event TemporalEvent Text where
51-
ofTy (TemporalEvent _ msgs) c = isJust $ find (\msg -> msg.tmsgNS == c) msgs
52-
props (TemporalEvent _ msgs) c =
53-
case find (\msg -> msg.tmsgNS == c) msgs of
54-
Just x -> Map.insert "host" (TextValue x.tmsgHost) $
55-
Map.insert "thread" (TextValue x.tmsgThread) $
56-
extractProps x.tmsgData
57-
Nothing -> error ("Not an event of type " <> unpack c)
58-
beg (TemporalEvent t _) = t
59-
6048
check :: Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> [TemporalEvent] -> IO ()
6149
check idx {- Formula index -} tr phi events =
6250
let result = satisfies phi events in
@@ -107,10 +95,6 @@ checkOffline tr eventDuration file phis = do
10795
check idx tr phi events
10896
threadDelay 200_000 -- Give the tracer a grace period to output the logs to whatever backend
10997

110-
-- | Convert time unit used in the yaml (currently second) input to μs.
111-
unitToMicrosecond :: Word -> Word
112-
unitToMicrosecond = (1_000_000 *)
113-
11498
setupTraceDispatcher :: Maybe FilePath -> IO (Trace IO App.TraceMessage)
11599
setupTraceDispatcher optTraceDispatcherConfigFile = do
116100
stdTr <- standardTracer
@@ -155,7 +139,7 @@ main = do
155139
ctx <- Map.toList . fromMaybe Map.empty <$> for options.context (readPropValues >=> dieOnYamlException)
156140
putStrLn "Context:"
157141
print ctx
158-
formulas <- readFormulas options.formulas (Context ctx) Parser.text >>= dieOnYamlException
142+
formulas <- readFormulas options.formulas (Context { interpDomain = ctx, varKinds = Map.empty }) Parser.name >>= dieOnYamlException
159143
for_ (fmap (\phi -> (phi, checkFormula mempty phi)) formulas) $ \case
160144
(phi, e : es) -> die $
161145
Text.unpack $
@@ -164,7 +148,7 @@ main = do
164148
<> " is syntactically invalid:\n"
165149
<> Text.unlines (fmap (("— " <>) . prettyError) (e : es))
166150
(_, []) -> pure ()
167-
let formulas' = fmap (interpTimeunit (\u -> unitToMicrosecond u `div` fromIntegral options.duration)) formulas
151+
let formulas' = fmap (interpTimeunit (\u -> timeunitToMicrosecond options.timeunit u `div` fromIntegral options.duration)) formulas
168152
tr <- setupTraceDispatcher options.traceDispatcherCfg
169153
case options.mode of
170154
Offline -> do

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

Lines changed: 49 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
module Cardano.ReCon.Cli(Mode(..), CliOptions(..), opts) where
1+
module Cardano.ReCon.Cli(Timeunit(..), timeunitToMicrosecond, Mode(..), CliOptions(..), opts) where
22

33

44
import Control.Arrow ((>>>))
@@ -20,6 +20,7 @@ readMode = eitherReader $ \case
2020
"online" -> Right Online
2121
_ -> Left "Expected either of: 'offline' or 'online'"
2222

23+
2324
readBool :: ReadM Bool
2425
readBool = eitherReader $ fmap toLower >>> \case
2526
"true" -> Right True
@@ -31,6 +32,51 @@ readBool = eitherReader $ fmap toLower >>> \case
3132
parseMode :: Parser Mode
3233
parseMode = option readMode (long "mode" <> metavar "<offline|online>" <> help "mode")
3334

35+
data Timeunit = Hour | Minute | Second | Millisecond | Microsecond deriving (Ord, Eq)
36+
37+
-- | Convert `Timeunit` to μs.
38+
timeunitToMicrosecond :: Timeunit -> Word -> Word
39+
timeunitToMicrosecond Hour = (3_600_000_000 *)
40+
timeunitToMicrosecond Minute = (60_000_000 *)
41+
timeunitToMicrosecond Second = (1_000_000 *)
42+
timeunitToMicrosecond Millisecond = (1_000 *)
43+
timeunitToMicrosecond Microsecond = id
44+
45+
instance Show Timeunit where
46+
show Hour = "hour"
47+
show Minute = "minute"
48+
show Second = "second"
49+
show Millisecond = "millisecond"
50+
show Microsecond = "microsecond"
51+
52+
readTimeunit :: ReadM Timeunit
53+
readTimeunit = eitherReader $ fmap toLower >>> \case
54+
"hour" -> Right Hour
55+
"h" -> Right Hour
56+
"minute" -> Right Minute
57+
"min" -> Right Minute
58+
"m" -> Right Minute
59+
"second" -> Right Second
60+
"sec" -> Right Second
61+
"s" -> Right Second
62+
"millisecond" -> Right Millisecond
63+
"millisec" -> Right Millisecond
64+
"millis" -> Right Millisecond
65+
"ms" -> Right Millisecond
66+
"microsecond" -> Right Microsecond
67+
"microsec" -> Right Microsecond
68+
"micros" -> Right Microsecond
69+
"μs" -> Right Microsecond
70+
_ -> Left "Can't read a Timeunit"
71+
72+
parseTimeunit :: Parser Timeunit
73+
parseTimeunit = option readTimeunit $
74+
long "timeunit"
75+
<> metavar "<hour|minute|second|millisecond|microsecond>"
76+
<> showDefault
77+
<> value Second
78+
<> help "timeunit"
79+
3480
parseEventDuration :: Parser Word
3581
parseEventDuration = option auto (long "duration" <> metavar "INT" <> help "temporal event duration (μs)")
3682

@@ -82,6 +128,7 @@ data CliOptions = CliOptions
82128
, context :: Maybe FilePath
83129
, enableProgressDumps :: Bool
84130
, enableSeekToEnd :: Bool
131+
, timeunit :: Timeunit
85132
}
86133

87134
parseCliOptions :: Parser CliOptions
@@ -95,6 +142,7 @@ parseCliOptions = CliOptions
95142
<*> parseContext
96143
<*> parseDumpMetrics
97144
<*> parseSeekToEnd
145+
<*> parseTimeunit
98146

99147
opts :: ParserInfo CliOptions
100148
opts = info (parseCliOptions <**> helper)

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

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,16 @@
11
module Cardano.ReCon.Common where
2-
import Cardano.ReCon.LTL.Lang.Formula
32

4-
import Data.Aeson
3+
import Data.Aeson (Object, Value (..))
54
import Data.Aeson.Key (toText)
65
import qualified Data.Aeson.KeyMap as KeyMap
76
import qualified Data.Map as Map
87
import Data.Map.Strict (Map)
8+
import Data.Text (Text)
99

10-
-- | Extract all accessible properties (fields) from the json object, non-recursively.
11-
-- Accessible fields are all fields of one of the following types: number, string.
12-
extractProps :: Object -> Map PropVarIdentifier PropValue
13-
extractProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
10+
-- | Extract scalar properties from a JSON object as Aeson Values, for display.
11+
extractJsonProps :: Object -> Map Text Value
12+
extractJsonProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
1413
where
15-
f (Number v) = Just $ IntValue (truncate v)
16-
f (String v) = Just $ TextValue v
17-
f _ = Nothing
14+
f v@(Number _) = Just v
15+
f v@(String _) = Just v
16+
f _ = Nothing

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@ module Cardano.ReCon.TraceMessage where
55
import Cardano.Logging
66
import Cardano.Logging.Prometheus.TCPServer (TracePrometheusSimple (..))
77
import qualified Cardano.Logging.Types.TraceMessage as Envelop
8-
import Cardano.ReCon.Common (extractProps)
9-
import Cardano.ReCon.LTL.Lang.Formula (Formula, PropValue (..), Relevance)
10-
import qualified Cardano.ReCon.LTL.Lang.Formula.Prec as Prec
11-
import Cardano.ReCon.LTL.Pretty (prettyFormula)
8+
import Cardano.ReCon.Common (extractJsonProps)
9+
import Cardano.ReCon.LTL.Formula (Formula, Relevance)
10+
import qualified Cardano.ReCon.LTL.Formula.Prec as Prec
11+
import Cardano.ReCon.LTL.Formula.Pretty (prettyFormula)
1212
import Cardano.ReCon.LTL.Satisfy (SatisfactionResult (..))
1313
import Cardano.ReCon.Trace.Feed (TemporalEvent (..))
1414

@@ -61,11 +61,11 @@ red text = "\x001b[31m" <> text <> "\x001b[0m"
6161
prettyTraceMessage :: Envelop.TraceMessage -> Text
6262
prettyTraceMessage Envelop.TraceMessage{..} =
6363
toStrict $ toLazyText $ encodePrettyToTextBuilder $
64-
Map.insert "at" (TextValue (showT tmsgAt)) $
65-
Map.insert "namespace" (TextValue tmsgNS) $
66-
Map.insert "host" (TextValue tmsgHost) $
67-
Map.insert "thread" (TextValue tmsgThread) $
68-
extractProps tmsgData
64+
Map.insert "at" (String (showT tmsgAt)) $
65+
Map.insert "namespace" (String tmsgNS) $
66+
Map.insert "host" (String tmsgHost) $
67+
Map.insert "thread" (String tmsgThread) $
68+
extractJsonProps tmsgData
6969

7070
prettyTemporalEvent :: TemporalEvent -> Text -> Text
7171
prettyTemporalEvent (TemporalEvent _ msgs) ns =

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

Lines changed: 74 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ description: Cardano Re(altime) Con(formance) Framework based on Linear T
44
category: Cardano
55
Testing
66
copyright: 2026 Intersect.
7-
version: 1.0.0
7+
version: 1.1.0
88
license: Apache-2.0
99
license-files: LICENSE
1010
NOTICE
@@ -13,6 +13,20 @@ maintainer: ruslan.feizerakhmanov@iohk.io
1313

1414
build-type: Simple
1515
extra-doc-files: CHANGELOG.md
16+
data-files:
17+
examples/cfgs/context.yaml
18+
examples/cfgs/formulas.yaml
19+
examples/extracts/ok-1.txt
20+
examples/extracts/ok-2.txt
21+
examples/extracts/ok-3.txt
22+
examples/extracts/ok-4.txt
23+
examples/extracts/ok-5.txt
24+
examples/extracts/fail-1.txt
25+
examples/extracts/fail-2.txt
26+
examples/extracts/fail-3.txt
27+
examples/extracts/fail-4.txt
28+
examples/extracts/fail-5.txt
29+
examples/extracts/fail-6.txt
1630
README.md
1731
recon-language-overview.md
1832
docs/*.txt
@@ -62,27 +76,45 @@ common common
6276
library
6377
import: common
6478
exposed-modules:
65-
Cardano.ReCon.LTL.Check
66-
, Cardano.ReCon.LTL.Lang.Formula
67-
, Cardano.ReCon.LTL.Lang.Formula.Parser
68-
, Cardano.ReCon.LTL.Lang.Formula.Prec
69-
, Cardano.ReCon.LTL.Lang.Formula.Yaml
70-
, Cardano.ReCon.LTL.Lang.Fragment
71-
, Cardano.ReCon.LTL.Lang.Fragment.Fragment0
72-
, Cardano.ReCon.LTL.Lang.Fragment.Fragment1
73-
, Cardano.ReCon.LTL.Lang.Fragment.Fragment2
74-
, Cardano.ReCon.LTL.Lang.HomogeneousFormula
75-
, Cardano.ReCon.LTL.Occurs
76-
, Cardano.ReCon.LTL.Pretty
77-
, Cardano.ReCon.LTL.Progress
78-
, Cardano.ReCon.LTL.Rewrite
79+
Cardano.ReCon.Common.Types
80+
, Cardano.ReCon.Common.Parser
81+
82+
, Cardano.ReCon.LTL.Check
83+
, Cardano.ReCon.LTL.Formula
84+
, Cardano.ReCon.LTL.Formula.Parser
85+
, Cardano.ReCon.LTL.Formula.Prec
86+
, Cardano.ReCon.LTL.Formula.Yaml
87+
, Cardano.ReCon.LTL.Formula.Pretty
7988
, Cardano.ReCon.LTL.Satisfy
80-
, Cardano.ReCon.LTL.Subst
8189

90+
, Cardano.ReCon.Integer.Polynomial.Parser
91+
, Cardano.ReCon.Integer.Polynomial.Term
92+
, Cardano.ReCon.Integer.Polynomial.Value
93+
94+
, Cardano.ReCon.Presburger.Decide
95+
, Cardano.ReCon.Presburger.Formula
96+
, Cardano.ReCon.Presburger.Parser
97+
98+
, Cardano.ReCon.Trace.Event
8299
, Cardano.ReCon.Trace.Feed
83100
, Cardano.ReCon.Trace.Ingest
84101

85102
other-modules:
103+
Cardano.ReCon.LTL.Internal.Occurs
104+
, Cardano.ReCon.LTL.Internal.Progress
105+
, Cardano.ReCon.LTL.Internal.Rewrite
106+
, Cardano.ReCon.LTL.Internal.Subst
107+
, Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula
108+
, Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree
109+
, Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree
110+
, Cardano.ReCon.Presburger.Internal.CooperQE
111+
, Cardano.ReCon.Presburger.Internal.IR.AffineDNF
112+
, Cardano.ReCon.Presburger.Internal.IR.CompNF
113+
, Cardano.ReCon.Presburger.Internal.IR.DNF
114+
, Cardano.ReCon.Presburger.Internal.IR.ForallFree
115+
, Cardano.ReCon.Presburger.Internal.IR.NegNF
116+
, Cardano.ReCon.Presburger.Internal.IR.NormAffineDNF
117+
, Cardano.ReCon.Presburger.Internal.IR.QuantifierFree
86118
other-extensions:
87119

88120
build-depends: base
@@ -147,6 +179,13 @@ test-suite cardano-recon-test
147179
type: exitcode-stdio-1.0
148180
hs-source-dirs: test
149181
main-is: Cardano/ReCon/Unit.hs
182+
other-modules:
183+
Cardano.ReCon.Integer.Polynomial.Semantics.Suite
184+
, Cardano.ReCon.Integer.Polynomial.Syntax.Suite
185+
, Cardano.ReCon.LTL.Semantics.Suite
186+
, Cardano.ReCon.LTL.Syntax.Suite
187+
, Cardano.ReCon.Presburger.Semantics.Suite
188+
, Cardano.ReCon.Presburger.Syntax.Suite
150189
build-depends:
151190
base
152191
, cardano-recon-framework
@@ -155,3 +194,22 @@ test-suite cardano-recon-test
155194
, tasty-hunit
156195
, text
157196
, megaparsec
197+
198+
test-suite cardano-recon-integration-test
199+
import: common
200+
type: exitcode-stdio-1.0
201+
hs-source-dirs: test
202+
main-is: Cardano/ReCon/Integration.hs
203+
other-modules:
204+
Cardano.ReCon.Integration.Suite
205+
, Paths_cardano_recon_framework
206+
autogen-modules:
207+
Paths_cardano_recon_framework
208+
build-depends:
209+
base
210+
, cardano-recon-framework
211+
, containers
212+
, filepath
213+
, tasty
214+
, tasty-hunit
215+
, text

0 commit comments

Comments
 (0)