Skip to content

Commit 0d31e25

Browse files
Russoulmgmeier
Russoul
and
mgmeier
authored
Accommodate recon-framework from cardano-node (#11)
* Accommodate recon-framework from cardano-node * Rename recon-framework to hermod-recon-framework Renames the directory, cabal package (cardano-recon-framework → hermod-recon-framework), and all internal references. Also drops the Cardano category from the cabal file. * Update recon-language-overview.md to reflect actual semantics and syntax - Mention Presburger arithmetic support in section 1 - Rename "Derivative Perspective" to "Formula Progression" and rewrite to describe the satisfiability-based rewriting approach (no Brzozowski reference) - Update "Simplification & Verdicts" to describe the actual two-pass rewrite (rewriteHomogeneous + rewriteIdentity) and terminate behaviour - Remove "Automata & Offline Monitoring" section - Rewrite worked examples using actual formula syntax (☐ ᪲, ♢ᵏ, ∀i ∈ ℤ, Forge.Loop.X{prop = val}) * nix: hermod-recon-framework flake outputs --------- Co-authored-by: Michael Karg <michael.karg@iohk.io>
1 parent 86368ed commit 0d31e25

74 files changed

Lines changed: 6021 additions & 4 deletions

Some content is hidden

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

‎CHANGELOG.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
# Changelog for the Hermod Tracing Project
22

3+
## June 2026
4+
5+
* Import `hermod-recon-framework` (was: `cardano-recon-framework`).
6+
37
## March 2026
48

59
* Release `trace-dispatcher-2.12.0`.

‎cabal.project‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ index-state:
1515

1616
packages:
1717
trace-dispatcher
18+
hermod-recon-framework
1819

1920
program-options
2021
ghc-options: -Werror

‎hermod-recon-framework/CHANGELOG.md‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
# Revision history for hermod-recon-framework
2+
3+
## 1.3.0 -- June 2026
4+
5+
* Rename module namespace from `Cardano.ReCon.*` to `Hermod.ReCon.*`.
6+
* Rename executables: `cardano-recon` → `hermod-recon`, `cardano-recon-grep` → `hermod-recon-grep`.
7+
8+
## 1.2.1 -- May 2026
9+
10+
* Replace positional `FILE` and `FILES` arguments in `cardano-recon` with named `--formulas` and `--traces` options.
11+
12+
## 1.2.0 -- May 2026
13+
14+
* Add `ContinuousFormula` — the temporal-operator-free fragment of `Formula`, with `retract` for
15+
converting a `Formula` and `eval` for deciding it against a single event.
16+
* Add `cardano-recon-grep` executable — filters a JSON array of `TraceMessage`s by a list of
17+
continuous formulas, emitting only the messages that satisfy all of them.
18+
* Add `--grep` flag to `cardano-recon` — on a negative formula outcome prints only the JSON array
19+
of relevant events to stdout (bypassing trace-dispatcher); prints nothing on a positive outcome.
20+
* Replace the raw context printout with a `ContextDump` trace message at `Debug` severity.
21+
22+
## 1.1.1 -- April 2026
23+
* Support atoms that refer to property keys at arbitrary depth
24+
* Replace the `crash-on-missing-key` build flag with a runtime CLI option `--on-missing-key <crash|bottom>` (default: `bottom`)
25+
26+
## 1.1.0 -- April 2026
27+
28+
* Support configurable timeunits in formulas via a CLI option.
29+
* Support existential quantification over properties (both finite and infinite domain)
30+
* Support Presburger arithmetic (over ℤ)
31+
32+
## 1.0.0 -- Feb 2026
33+
34+
* First version.

‎hermod-recon-framework/LICENSE‎

Lines changed: 177 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,177 @@
1+
2+
Apache License
3+
Version 2.0, January 2004
4+
http://www.apache.org/licenses/
5+
6+
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
7+
8+
1. Definitions.
9+
10+
"License" shall mean the terms and conditions for use, reproduction,
11+
and distribution as defined by Sections 1 through 9 of this document.
12+
13+
"Licensor" shall mean the copyright owner or entity authorized by
14+
the copyright owner that is granting the License.
15+
16+
"Legal Entity" shall mean the union of the acting entity and all
17+
other entities that control, are controlled by, or are under common
18+
control with that entity. For the purposes of this definition,
19+
"control" means (i) the power, direct or indirect, to cause the
20+
direction or management of such entity, whether by contract or
21+
otherwise, or (ii) ownership of fifty percent (50%) or more of the
22+
outstanding shares, or (iii) beneficial ownership of such entity.
23+
24+
"You" (or "Your") shall mean an individual or Legal Entity
25+
exercising permissions granted by this License.
26+
27+
"Source" form shall mean the preferred form for making modifications,
28+
including but not limited to software source code, documentation
29+
source, and configuration files.
30+
31+
"Object" form shall mean any form resulting from mechanical
32+
transformation or translation of a Source form, including but
33+
not limited to compiled object code, generated documentation,
34+
and conversions to other media types.
35+
36+
"Work" shall mean the work of authorship, whether in Source or
37+
Object form, made available under the License, as indicated by a
38+
copyright notice that is included in or attached to the work
39+
(an example is provided in the Appendix below).
40+
41+
"Derivative Works" shall mean any work, whether in Source or Object
42+
form, that is based on (or derived from) the Work and for which the
43+
editorial revisions, annotations, elaborations, or other modifications
44+
represent, as a whole, an original work of authorship. For the purposes
45+
of this License, Derivative Works shall not include works that remain
46+
separable from, or merely link (or bind by name) to the interfaces of,
47+
the Work and Derivative Works thereof.
48+
49+
"Contribution" shall mean any work of authorship, including
50+
the original version of the Work and any modifications or additions
51+
to that Work or Derivative Works thereof, that is intentionally
52+
submitted to Licensor for inclusion in the Work by the copyright owner
53+
or by an individual or Legal Entity authorized to submit on behalf of
54+
the copyright owner. For the purposes of this definition, "submitted"
55+
means any form of electronic, verbal, or written communication sent
56+
to the Licensor or its representatives, including but not limited to
57+
communication on electronic mailing lists, source code control systems,
58+
and issue tracking systems that are managed by, or on behalf of, the
59+
Licensor for the purpose of discussing and improving the Work, but
60+
excluding communication that is conspicuously marked or otherwise
61+
designated in writing by the copyright owner as "Not a Contribution."
62+
63+
"Contributor" shall mean Licensor and any individual or Legal Entity
64+
on behalf of whom a Contribution has been received by Licensor and
65+
subsequently incorporated within the Work.
66+
67+
2. Grant of Copyright License. Subject to the terms and conditions of
68+
this License, each Contributor hereby grants to You a perpetual,
69+
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
70+
copyright license to reproduce, prepare Derivative Works of,
71+
publicly display, publicly perform, sublicense, and distribute the
72+
Work and such Derivative Works in Source or Object form.
73+
74+
3. Grant of Patent License. Subject to the terms and conditions of
75+
this License, each Contributor hereby grants to You a perpetual,
76+
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
77+
(except as stated in this section) patent license to make, have made,
78+
use, offer to sell, sell, import, and otherwise transfer the Work,
79+
where such license applies only to those patent claims licensable
80+
by such Contributor that are necessarily infringed by their
81+
Contribution(s) alone or by combination of their Contribution(s)
82+
with the Work to which such Contribution(s) was submitted. If You
83+
institute patent litigation against any entity (including a
84+
cross-claim or counterclaim in a lawsuit) alleging that the Work
85+
or a Contribution incorporated within the Work constitutes direct
86+
or contributory patent infringement, then any patent licenses
87+
granted to You under this License for that Work shall terminate
88+
as of the date such litigation is filed.
89+
90+
4. Redistribution. You may reproduce and distribute copies of the
91+
Work or Derivative Works thereof in any medium, with or without
92+
modifications, and in Source or Object form, provided that You
93+
meet the following conditions:
94+
95+
(a) You must give any other recipients of the Work or
96+
Derivative Works a copy of this License; and
97+
98+
(b) You must cause any modified files to carry prominent notices
99+
stating that You changed the files; and
100+
101+
(c) You must retain, in the Source form of any Derivative Works
102+
that You distribute, all copyright, patent, trademark, and
103+
attribution notices from the Source form of the Work,
104+
excluding those notices that do not pertain to any part of
105+
the Derivative Works; and
106+
107+
(d) If the Work includes a "NOTICE" text file as part of its
108+
distribution, then any Derivative Works that You distribute must
109+
include a readable copy of the attribution notices contained
110+
within such NOTICE file, excluding those notices that do not
111+
pertain to any part of the Derivative Works, in at least one
112+
of the following places: within a NOTICE text file distributed
113+
as part of the Derivative Works; within the Source form or
114+
documentation, if provided along with the Derivative Works; or,
115+
within a display generated by the Derivative Works, if and
116+
wherever such third-party notices normally appear. The contents
117+
of the NOTICE file are for informational purposes only and
118+
do not modify the License. You may add Your own attribution
119+
notices within Derivative Works that You distribute, alongside
120+
or as an addendum to the NOTICE text from the Work, provided
121+
that such additional attribution notices cannot be construed
122+
as modifying the License.
123+
124+
You may add Your own copyright statement to Your modifications and
125+
may provide additional or different license terms and conditions
126+
for use, reproduction, or distribution of Your modifications, or
127+
for any such Derivative Works as a whole, provided Your use,
128+
reproduction, and distribution of the Work otherwise complies with
129+
the conditions stated in this License.
130+
131+
5. Submission of Contributions. Unless You explicitly state otherwise,
132+
any Contribution intentionally submitted for inclusion in the Work
133+
by You to the Licensor shall be under the terms and conditions of
134+
this License, without any additional terms or conditions.
135+
Notwithstanding the above, nothing herein shall supersede or modify
136+
the terms of any separate license agreement you may have executed
137+
with Licensor regarding such Contributions.
138+
139+
6. Trademarks. This License does not grant permission to use the trade
140+
names, trademarks, service marks, or product names of the Licensor,
141+
except as required for reasonable and customary use in describing the
142+
origin of the Work and reproducing the content of the NOTICE file.
143+
144+
7. Disclaimer of Warranty. Unless required by applicable law or
145+
agreed to in writing, Licensor provides the Work (and each
146+
Contributor provides its Contributions) on an "AS IS" BASIS,
147+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
148+
implied, including, without limitation, any warranties or conditions
149+
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
150+
PARTICULAR PURPOSE. You are solely responsible for determining the
151+
appropriateness of using or redistributing the Work and assume any
152+
risks associated with Your exercise of permissions under this License.
153+
154+
8. Limitation of Liability. In no event and under no legal theory,
155+
whether in tort (including negligence), contract, or otherwise,
156+
unless required by applicable law (such as deliberate and grossly
157+
negligent acts) or agreed to in writing, shall any Contributor be
158+
liable to You for damages, including any direct, indirect, special,
159+
incidental, or consequential damages of any character arising as a
160+
result of this License or out of the use or inability to use the
161+
Work (including but not limited to damages for loss of goodwill,
162+
work stoppage, computer failure or malfunction, or any and all
163+
other commercial damages or losses), even if such Contributor
164+
has been advised of the possibility of such damages.
165+
166+
9. Accepting Warranty or Additional Liability. While redistributing
167+
the Work or Derivative Works thereof, You may choose to offer,
168+
and charge a fee for, acceptance of support, warranty, indemnity,
169+
or other liability obligations and/or rights consistent with this
170+
License. However, in accepting such obligations, You may act only
171+
on Your own behalf and on Your sole responsibility, not on behalf
172+
of any other Contributor, and only if You agree to indemnify,
173+
defend, and hold each Contributor harmless for any liability
174+
incurred by, or claims asserted against, such Contributor by reason
175+
of your accepting any such warranty or additional liability.
176+
177+
END OF TERMS AND CONDITIONS

‎hermod-recon-framework/NOTICE‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
Copyright 2023 Input Output Global Inc (IOG), 2023-2026 Intersect.
2+
3+
Licensed under the Apache License, Version 2.0 (the "License");
4+
you may not use this file except in compliance with the License.
5+
You may obtain a copy of the License at
6+
7+
http://www.apache.org/licenses/LICENSE-2.0
8+
9+
Unless required by applicable law or agreed to in writing, software
10+
distributed under the License is distributed on an "AS IS" BASIS,
11+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12+
See the License for the specific language governing permissions and
13+
limitations under the License.

‎hermod-recon-framework/README.md‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
# Re(altime) Con(formance) Framework
2+
3+
## Applications
4+
5+
### `hermod-recon` — LTL conformance checker
6+
7+
The application CLI takes as input:
8+
- A yaml list of strings, where each string is a parseable Linear Temporal Logic formula.
9+
For further details about the formula language, consult the syntax [reference](docs/ltl-formula-syntax.txt).
10+
For an example, see [this](examples/cfgs/formulas.yaml).
11+
- A list of files which contain machine-readable traces. For an example, see [this](examples/extracts/ok-1.txt).
12+
- An operation _mode_, which can be either _online_ or _offline_. For realtime conformance testing of multiple
13+
ever-growing log files, run in online mode. For testing on one read-only file run in offline mode.
14+
- Other configuration options (see `$ --help` for a comprehensive list).
15+
16+
The application traverses the events from the given log files and checks if each given formula is satisfied by them.
17+
If negative, reports as such and lists the events that have been relevant to the formula.
18+
19+
Pass `--grep` for machine-readable output: on a negative outcome only the JSON array of relevant events is written
20+
to stdout (bypassing trace-dispatcher), and nothing is printed on a positive outcome. This makes it straightforward
21+
to pipe results directly into `hermod-recon-grep`.
22+
23+
#### CLI Syntax
24+
25+
```
26+
Usage: hermod-recon FILE --mode <offline|online> --duration INT FILES
27+
[--retention INT] [--trace-dispatcher-cfg FILE]
28+
[--context FILE] [--dump-metrics BOOL] [--seek-to-end BOOL]
29+
[--timeunit <hour|minute|second|millisecond|microsecond>]
30+
[--on-missing-key <crash|bottom>] [--grep]
31+
32+
Check formula satisfiability against a log of trace messages
33+
34+
Available options:
35+
--mode <offline|online> mode
36+
--duration INT temporal event duration (μs)
37+
--retention INT temporal event retention period (ms) (default: 200)
38+
--trace-dispatcher-cfg FILE
39+
trace dispatcher configuration file
40+
--context FILE context variables
41+
--dump-metrics BOOL enable periodic metric dumps to stdout
42+
(default: False)
43+
--seek-to-end BOOL seek to the end of the trace file before ingesting it
44+
(default: True)
45+
--timeunit <hour|minute|second|millisecond|microsecond>
46+
unit in which numeric arguments of temporal
47+
operators in input formulas are measured
48+
(default: second)
49+
--on-missing-key <crash|bottom>
50+
behaviour when a formula atom references a missing
51+
event property key (default: bottom)
52+
--grep on formula violation print only the JSON array of
53+
relevant events; print nothing on satisfaction
54+
-h,--help Show this help text
55+
```
56+
57+
### `hermod-recon-grep` — Global Realisation Print
58+
59+
A stateless utility that filters a JSON array of trace messages by interpreting a list of
60+
_continuous_ (temporal-operator-free) formulas against each message individually.
61+
Only messages that satisfy **all** given formulas are written to stdout as a pretty-printed
62+
JSON array.
63+
64+
Inputs:
65+
- A YAML list of continuous formula strings (same syntax as `hermod-recon`, but temporal
66+
operators such as `□`, `◇`, `○`, and `|` are not permitted).
67+
For further details about the formula language, consult the [language overview](docs/formula-languages.txt).
68+
- A JSON array of `TraceMessage` objects, read from a file (`--traces FILE`) or from stdin
69+
if `--traces` is omitted (e.g. piped from `hermod-recon` on a negative formula outcome).
70+
- An optional context variables YAML file for variable substitution in formulas.
71+
- An `--on-missing-key` policy (default: `bottom`) controlling behaviour when a formula
72+
references a property absent from a message.
73+
74+
#### CLI Syntax
75+
76+
```
77+
Usage: hermod-recon-grep --formulas FILE [--traces FILE]
78+
[--context FILE]
79+
[--on-missing-key <crash|bottom>]
80+
81+
Print log events that realise all given continuous formulas (Global Realisation Print)
82+
83+
Available options:
84+
--formulas FILE YAML file with a list of ContinuousFormulas
85+
--traces FILE JSON array of TraceMessages to filter (default: stdin)
86+
--context FILE context variables YAML file
87+
--on-missing-key <crash|bottom>
88+
behaviour when a formula atom references a missing
89+
event property key (default: bottom)
90+
-h,--help Show this help text
91+
```
92+
93+
## Build flags
94+
- _debug_ for enabling verbose tracing of formulas as they evolve (multiple traces per each temporal event).

0 commit comments

Comments
 (0)