Merge pull request #6560 from IntersectMBO/russoul/recon-grep

cardano-recon-framework: Add cardano-recon-grep and ContinuousFormula (v1.2.0)

Author: mgmeier

bench/cardano-recon-framework/CHANGELOG.md

@@ -1,5 +1,15 @@
 # Revision history for cardano-trace-ltl
 
+## 1.2.0 -- May 2026
+
+* Add `ContinuousFormula` — the temporal-operator-free fragment of `Formula`, with `retract` for
+  converting a `Formula` and `eval` for deciding it against a single event.
+* Add `cardano-recon-grep` executable — filters a JSON array of `TraceMessage`s by a list of
+  continuous formulas, emitting only the messages that satisfy all of them.
+* Add `--grep` flag to `cardano-recon` — on a negative formula outcome prints only the JSON array
+  of relevant events to stdout (bypassing trace-dispatcher); prints nothing on a positive outcome.
+* Replace the raw context printout with a `ContextDump` trace message at `Debug` severity.
+
 ## 1.1.1 -- April 2026
 * Support atoms that refer to property keys at arbitrary depth
 * Replace the `crash-on-missing-key` build flag with a runtime CLI option `--on-missing-key <crash|bottom>` (default: `bottom`)

bench/cardano-recon-framework/README.md

@@ -1,6 +1,8 @@
 # Cardano Re(altime) Con(formance) Framework
 
-## What it does
+## Applications
+
+### `cardano-recon` — LTL conformance checker
 
 The application CLI takes as input:
   - A yaml list of strings, where each string is a parseable Linear Temporal Logic formula.
@@ -14,14 +16,18 @@ The application CLI takes as input:
 The application traverses the events from the given log files and checks if each given formula is satisfied by them.
 If negative, reports as such and lists the events that have been relevant to the formula.
 
-## CLI Syntax
+Pass `--grep` for machine-readable output: on a negative outcome only the JSON array of relevant events is written
+to stdout (bypassing trace-dispatcher), and nothing is printed on a positive outcome. This makes it straightforward
+to pipe results directly into `cardano-recon-grep`.
+
+#### CLI Syntax
 
 ```
 Usage: cardano-recon FILE --mode <offline|online> --duration INT FILES
                      [--retention INT] [--trace-dispatcher-cfg FILE]
                      [--context FILE] [--dump-metrics BOOL] [--seek-to-end BOOL]
                      [--timeunit <hour|minute|second|millisecond|microsecond>]
-                     [--on-missing-key <crash|bottom>]
+                     [--on-missing-key <crash|bottom>] [--grep]
 
   Check formula satisfiability against a log of trace messages
 
@@ -38,6 +44,44 @@ Available options:
                            (default: True)
   --timeunit <hour|minute|second|millisecond|microsecond>
                            timeunit (default: second)
+  --on-missing-key <crash|bottom>
+                           behaviour when a formula atom references a missing
+                           event property key (default: bottom)
+  --grep                   on formula violation print only the JSON array of
+                           relevant events; print nothing on satisfaction
+  -h,--help                Show this help text
+```
+
+### `cardano-recon-grep` — Global Realisation Print
+
+A stateless utility that filters a JSON array of trace messages by interpreting a list of
+_continuous_ (temporal-operator-free) formulas against each message individually.
+Only messages that satisfy **all** given formulas are written to stdout as a pretty-printed
+JSON array.
+
+Inputs:
+  - A YAML list of continuous formula strings (same syntax as `cardano-recon`, but temporal
+    operators such as `□`, `◇`, `○`, and `|` are not permitted).
+    For further details about the formula language, consult the [language overview](docs/formula-languages.txt).
+  - A JSON array of `TraceMessage` objects, read from a file (`--traces FILE`) or from stdin
+    if `--traces` is omitted (e.g. piped from `cardano-recon` on a negative formula outcome).
+  - An optional context variables YAML file for variable substitution in formulas.
+  - An `--on-missing-key` policy (default: `bottom`) controlling behaviour when a formula
+    references a property absent from a message.
+
+#### CLI Syntax
+
+```
+Usage: cardano-recon-grep --formulas FILE [--traces FILE]
+                            [--context FILE]
+                            [--on-missing-key <crash|bottom>]
+
+  Print log events that realise all given continuous formulas (Global Realisation Print)
+
+Available options:
+  --formulas FILE          YAML file with a list of ContinuousFormulas
+  --traces FILE            JSON array of TraceMessages to filter (default: stdin)
+  --context FILE           context variables YAML file
   --on-missing-key <crash|bottom>
                            behaviour when a formula atom references a missing
                            event property key (default: bottom)

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

@@ -34,6 +34,7 @@ import qualified Data.Map as Map
 import           Data.Maybe (fromMaybe, listToMaybe)
 import           Data.Text (Text)
 import qualified Data.Text as Text
+import qualified Data.Text.IO as TIO
 import           Data.Traversable (for)
 import           GHC.IO.Encoding (setLocaleEncoding, utf8)
 import           Network.HostName (HostName)
@@ -45,18 +46,26 @@ import qualified System.Metrics as EKG
 import           Streaming
 
 
-check :: OnMissingKey -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> [TemporalEvent] -> IO ()
-check omk idx {- Formula index -} tr phi events =
+check :: OnMissingKey -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> [TemporalEvent] -> IO ()
+check omk greppable idx {- Formula index -} tr phi events =
   let result = satisfies omk phi events in
-  traceWith tr $ formulaOutcome phi result idx
-
-checkS' :: OnMissingKey -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> Stream (Of TemporalEvent) IO () -> IO ()
-checkS' omk enableProgressDumps idx {- Formula index -} tr phi events = do
+  if greppable
+    then case result of
+      Satisfied       -> pure ()
+      Unsatisfied rel -> TIO.putStrLn (App.prettyRelevanceArray rel)
+    else traceWith tr $ formulaOutcome phi result idx
+
+checkS' :: OnMissingKey -> Bool -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> Stream (Of TemporalEvent) IO () -> IO ()
+checkS' omk greppable enableProgressDumps idx {- Formula index -} tr phi events = do
   let initial = SatisfyMetrics 0 phi 0
   metrics <- newIORef initial
   withAsync (when enableProgressDumps $ runDisplayProgressDump initial metrics) $ \counterDisplayThread -> do
     r <- satisfiesS omk phi events metrics
-    traceWith tr $ formulaOutcome phi r idx
+    if greppable
+      then case r of
+        Satisfied       -> pure ()
+        Unsatisfied rel -> TIO.putStrLn (App.prettyRelevanceArray rel)
+      else traceWith tr $ formulaOutcome phi r idx
     cancel counterDisplayThread
   where
     runDisplayProgressDump :: SatisfyMetrics TemporalEvent Text -> IORef (SatisfyMetrics TemporalEvent Text) -> IO ()
@@ -69,6 +78,7 @@ checkS' omk enableProgressDumps idx {- Formula index -} tr phi events = do
       runDisplayProgressDump next counter
 
 checkOnline :: OnMissingKey
+            -> Bool
             -> Bool
             -> Trace IO App.TraceMessage
             -> TemporalEventDurationMicrosec
@@ -78,23 +88,24 @@ checkOnline :: OnMissingKey
             -> [FilePath]
             -> [Formula TemporalEvent Text]
             -> IO ()
-checkOnline omk enableProgressDumps tr eventDuration retentionMs failureMode ingestMode files phis = do
+checkOnline omk greppable enableProgressDumps tr eventDuration retentionMs failureMode ingestMode files phis = do
   ing <- mkIngestor (fromIntegral retentionMs)
   for_ files (ingestFileThreaded ing failureMode ingestMode)
   forConcurrently_ (zip [0..] phis) $ \(idx, phi) -> mkIngestorReader ing >>= \reader -> forever $ do
     traceWith tr $ FormulaStartCheck phi idx
-    checkS' omk enableProgressDumps idx tr phi (readS reader eventDuration)
+    checkS' omk greppable enableProgressDumps idx tr phi (readS reader eventDuration)
 
 checkOffline :: OnMissingKey
+             -> Bool
              -> Trace IO App.TraceMessage
              -> TemporalEventDurationMicrosec
              -> FilePath
              -> [Formula TemporalEvent Text]
              -> IO ()
-checkOffline omk tr eventDuration file phis = do
+checkOffline omk greppable tr eventDuration file phis = do
   events <- read file eventDuration
   forConcurrently_ (zip [0..] phis) $ \(idx, phi) ->
-    check omk idx tr phi events
+    check omk greppable idx tr phi events
   threadDelay 200_000 -- Give the tracer a grace period to output the logs to whatever backend
 
 setupTraceDispatcher :: Maybe FilePath -> IO (Trace IO App.TraceMessage)
@@ -139,8 +150,6 @@ main = do
   setLocaleEncoding utf8
   options <- execParser opts
   ctx <- Map.toList . fromMaybe Map.empty <$> for options.context (readPropValues >=> dieOnYamlException)
-  putStrLn "Context:"
-  print ctx
   formulas <- readFormulas options.formulas (Context { interpDomain = ctx, varKinds = Map.empty }) Parser.name >>= dieOnYamlException
   for_ (fmap (\phi -> (phi, checkFormula mempty phi)) formulas) $ \case
     (phi, e : es) -> die $
@@ -152,15 +161,17 @@ main = do
     (_, []) -> pure ()
   let formulas' = fmap (interpTimeunit (\u -> timeunitToMicrosecond options.timeunit u `div` fromIntegral options.duration)) formulas
   tr <- setupTraceDispatcher options.traceDispatcherCfg
+  traceWith tr $ ContextDump (map (second showT) ctx)
   case options.mode of
     Offline -> do
       file <- case options.traces of
         [x] -> pure x
         _   -> die "Only exactly one trace file is supported in 'offline' mode"
-      checkOffline options.onMissingKey tr options.duration file formulas'
+      checkOffline options.onMissingKey options.greppable tr options.duration file formulas'
     Online -> do
       checkOnline
         options.onMissingKey
+        options.greppable
         options.enableProgressDumps
         tr
         options.duration

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

@@ -134,6 +134,11 @@ parseOnMissingKey = option readOnMissingKey $
   <> value BottomOnMissingKey
   <> help "behaviour when a formula atom references a missing event property key"
 
+parseGreppable :: Parser Bool
+parseGreppable = switch $
+     long "grep"
+  <> help "on formula violation print only the JSON array of relevant events; print nothing on satisfaction"
+
 data CliOptions = CliOptions
   { formulas            :: FilePath
   , mode                :: Mode
@@ -146,6 +151,7 @@ data CliOptions = CliOptions
   , enableSeekToEnd     :: Bool
   , timeunit            :: Timeunit
   , onMissingKey        :: OnMissingKey
+  , greppable           :: Bool
   }
 
 parseCliOptions :: Parser CliOptions
@@ -161,6 +167,7 @@ parseCliOptions = CliOptions
               <*> parseSeekToEnd
               <*> parseTimeunit
               <*> parseOnMissingKey
+              <*> parseGreppable
 
 opts :: ParserInfo CliOptions
 opts = info (parseCliOptions <**> helper)

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

@@ -5,17 +5,15 @@ 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 (extractJsonProps)
 import           Cardano.ReCon.LTL.Formula (Formula, Relevance)
 import qualified Cardano.ReCon.LTL.Formula.Prec as Prec
 import           Cardano.ReCon.LTL.Formula.Pretty (prettyFormula)
 import           Cardano.ReCon.LTL.Satisfy (SatisfactionResult (..))
 import           Cardano.ReCon.Trace.Feed (TemporalEvent (..))
 
-import           Data.Aeson (Value (..), (.=))
+import           Data.Aeson ((.=))
 import           Data.Aeson.Encode.Pretty
 import           Data.List (find)
-import qualified Data.Map as Map
 import qualified Data.Set as Set
 import           Data.Text (Text)
 import qualified Data.Text as Text
@@ -44,13 +42,14 @@ data TraceMessage = FormulaStartCheck {
                   | FormulaNegativeOutcome {
                       formula   :: Formula TemporalEvent Text,
                       relevance :: Relevance TemporalEvent Text,
-                      index :: Word
+                      index     :: Word
                   }
+                  | ContextDump { context :: [(Text, Text)] }
 
 -- | Smart constructor.
 formulaOutcome :: Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Word -> TraceMessage
-formulaOutcome formula Satisfied         idx = FormulaPositiveOutcome formula idx
-formulaOutcome formula (Unsatisfied rel) idx = FormulaNegativeOutcome formula rel idx
+formulaOutcome formula Satisfied         idx = FormulaPositiveOutcome { formula, index = idx }
+formulaOutcome formula (Unsatisfied rel) idx = FormulaNegativeOutcome { formula, relevance = rel, index = idx }
 
 green :: Text -> Text
 green text = "\x001b[32m" <> text <> "\x001b[0m"
@@ -59,51 +58,49 @@ red :: Text -> Text
 red text = "\x001b[31m" <> text <> "\x001b[0m"
 
 prettyTraceMessage :: Envelop.TraceMessage -> Text
-prettyTraceMessage Envelop.TraceMessage{..} =
-  toStrict $ toLazyText $ encodePrettyToTextBuilder  $
-    Map.insert "at" (String (showT tmsgAt))        $
-      Map.insert "namespace" (String tmsgNS)       $
-        Map.insert "host" (String tmsgHost)        $
-          Map.insert "thread" (String tmsgThread)  $
-            extractJsonProps tmsgData
+prettyTraceMessage = toStrict . toLazyText . encodePrettyToTextBuilder
 
 prettyTemporalEvent :: TemporalEvent -> Text -> Text
 prettyTemporalEvent (TemporalEvent _ msgs) ns =
   maybe ("<<Unexpected namespace " <> ns <> ">>") prettyTraceMessage (find (\ x -> x.tmsgNS == ns) msgs)
 
+prettyRelevanceArray :: Relevance TemporalEvent Text -> Text
+prettyRelevanceArray rel =
+  Text.unlines $ "[" : fmap (uncurry prettyTemporalEvent) (Set.toList rel) ++ ["]"]
+
 prettySatisfactionResult :: Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Text
 prettySatisfactionResult initial Satisfied = prettyFormula initial Prec.Universe <> " " <> green "(✔)"
 prettySatisfactionResult initial (Unsatisfied rel) =
   prettyFormula initial Prec.Universe <> red " (✗)" <> "\n"
-    <> Text.intercalate
-         "\n----------------------------------------------\n"
-         (fmap (uncurry prettyTemporalEvent) (Set.toList rel))
+  <> prettyRelevanceArray rel
 
 instance LogFormatting TraceMessage where
   forMachine _ FormulaStartCheck{..} = mconcat
     [
-      "formula" .= String (prettyFormula formula Prec.Universe),
+      "formula" .= prettyFormula formula Prec.Universe,
       "index" .= index
     ]
   forMachine _ FormulaProgressDump{..} = mconcat
     [
-      "events_per_second" .= Number (fromIntegral eventsPerSecond),
-      "catch_up_ratio" .= Number (realToFrac catchupRatio),
+      "eventsPerSecond" .= (fromIntegral eventsPerSecond :: Int),
+      "catchUpRatio" .= (realToFrac catchupRatio :: Double),
       "index" .= index
     ]
   forMachine _ FormulaPositiveOutcome{..} = mconcat
     [
-      "formula" .= String (prettyFormula formula Prec.Universe),
+      "formula" .= prettyFormula formula Prec.Universe,
       "index" .= index
     ]
   forMachine _ FormulaNegativeOutcome{..} = mconcat
     [
-      "formula" .= String (prettyFormula formula Prec.Universe)
+      "formula" .= prettyFormula formula Prec.Universe
     ,
-      "relevance" .= String (showT relevance)
+      "relevance" .= showT relevance
     ,
       "index" .= index
     ]
+  forMachine _ ContextDump{..} = mconcat
+    [ "context" .= context ]
 
   forHuman FormulaStartCheck{..} =
     "Starting satisfiability check on formula #" <> showT index <> ": " <> prettyFormula formula Prec.Universe
@@ -119,28 +116,35 @@ instance LogFormatting TraceMessage where
     prettySatisfactionResult formula Satisfied
   forHuman FormulaNegativeOutcome{..} =
     prettySatisfactionResult formula (Unsatisfied relevance)
+  forHuman ContextDump{..} =
+    Text.unlines $ "Context:" : map (\(k, v) -> "  " <> k <> " = " <> v) context
 
   asMetrics FormulaStartCheck{} = []
   asMetrics (FormulaProgressDump {catchupRatio, index}) = [DoubleM ("catchup_ratio_" <> showT index) catchupRatio]
   asMetrics FormulaPositiveOutcome{} = []
   asMetrics FormulaNegativeOutcome{} = []
+  asMetrics ContextDump{} = []
 
 
 instance MetaTrace TraceMessage where
   allNamespaces =
     [
+      Namespace [] ["ContextDump"]
+    ,
       Namespace [] ["FormulaStartCheck"]
     ,
       Namespace [] ["FormulaProgressDump"]
     ,
       Namespace [] ["FormulaOutcome"]
     ]
 
+  namespaceFor ContextDump{}            = Namespace [] ["ContextDump"]
   namespaceFor FormulaStartCheck{}      = Namespace [] ["FormulaStartCheck"]
   namespaceFor FormulaProgressDump{}    = Namespace [] ["FormulaProgressDump"]
   namespaceFor FormulaPositiveOutcome{} = Namespace [] ["FormulaPositiveOutcome"]
   namespaceFor FormulaNegativeOutcome{} = Namespace [] ["FormulaNegativeOutcome"]
 
+  severityFor (Namespace [] ["ContextDump"])            _ = Just Debug
   severityFor (Namespace [] ["FormulaStartCheck"])       _ = Just Info
   severityFor (Namespace [] ["FormulaProgressDump"])     _ = Just Debug
   severityFor (Namespace [] ["FormulaPositiveOutcome"])  _ = Just Info
@@ -149,6 +153,8 @@ instance MetaTrace TraceMessage where
 
   detailsFor _ _ =  Just DNormal
 
+  documentFor (Namespace [] ["ContextDump"]) =
+    Just "Dump of the context variables supplied to the formula parser."
   documentFor (Namespace [] ["FormulaStartCheck"]) =
     Just "Formula satisfiability check has started."
   documentFor (Namespace [] ["FormulaProgressDump"]) =