SemanticDLTL — a DLTL model checker

SemanticDLTL checks the traces of an event log against DLTL formulas: linear temporal logic over finite words, extended with freeze operators that bind the data attributes of an event to a variable, so that properties can relate the attributes of different events of the same trace. The log is given in the tool's own text format (.mod) or as a standard XES event log (.xes).

The semantic part is what the data attributes can point to: an attribute can hold the identifier of an event in a knowledge graph, and propositions written in Python can query that graph (with SPARQL, or any other means) while the formula is checked. The repository includes a complete example of this kind, built on synthetic clinical histories generated with Synthea and annotated with SNOMED CT concepts: see A semantic example below and examples/synthea/README.md.

It implements the algorithm described in

J. M. Couvreur, J. Ezpeleta. A Linear Temporal Logic Model Checking Method over Finite Words with Correlated Transition Attributes. Data-Driven Process Discovery and Analysis (SIMPDA 2017), Lecture Notes in Business Information Processing, vol. 340, Springer, 2019.

Installation

Python 3.10 or later, no dependencies. From PyPI:

pip install semanticdltl             # the checker
pip install "semanticdltl[synthea]"  # plus pyoxigraph, for the semantic example

or from a checkout of this repository:

pip install .              # the checker
pip install -e ".[dev]"    # editable, with the test tools (pytest, ruff, build, twine)
pip install ".[synthea]"   # with pyoxigraph, for the semantic example

Either way this installs the dltl package and the dltl-mc command. The examples and the test-suite are in the repository, not in the PyPI package.

For development on macOS or Linux, make venv creates a virtual environment in .venv/ with the package installed in editable mode and the development tools; make test, make lint and make sample run the test-suite, the linter and the checker on the sample model. The virtual environment is local to each machine and is not part of the repository. On Windows use the manual commands of the Test suite section instead of the Makefile.

This installs the dltl package and the dltl-mc command. The checker can also be run without installing, from the repository root, with python MC.py or python -m dltl (with PYTHONPATH=src).

Usage

dltl-mc --log-file <model> [--init-file FILE] [--formula-file FILE]
        [--no-interactive] [--multi-line] [--propositions FILE.py]
        [--xes-schema FILE.xml] [--xes-trace-id-key KEY] [--xes-ignore]

Option	Description	Default
--log-file MODEL	the trace model, with or without the .mod suffix, or an XES event log (.xes); gzipped files (.mod.gz, .xes.gz) are accepted	required
--init-file FILE	commands executed before reading formulas (typically macro definitions)	none
--formula-file FILE	file with the formulas/commands to check	standard input
--interactive / --no-interactive	show the DLTL -> prompt when reading from standard input	interactive
--multi-line	formulas may span several lines and are terminated by $	off
--propositions FILE.py	Python file whose functions are available as PROP.<name> in data expressions	dltl.propositions
--xes-schema FILE.xml	XES logs: XML file that gives a type and a name to the attributes of the events (see XES event logs)	concept:name is an atomic proposition
--xes-trace-id-key KEY	XES logs: trace attribute used as trace identifier	concept:name
--xes-ignore	XES logs: load only the attributes that appear in the schema	off: every attribute is loaded

The syntax of the original prototype is still accepted:

python MC.py log-file=<model> init-file=FILE formula-file=FILE interactive=false multi-line=true

Each checked formula prints one line

<satisfying traces>,<non-satisfying traces>,<% satisfying>,<seconds>

Running the sample model

examples/sample.mod is a tiny model with three traces (id0, id1, id2) and one attribute of each kind: the atomic proposition E, the number V, the set att and the dictionary p:

aE,nV,@att,$p
id0,a&4&a;1&a=1;b=2
id0,a&1&a;1&a=1;b=3
id1,a&4&a;1&a=1;b=2
id1,a&1&a;1&a=1;b=2
id1,b&1&a;2&a=1;b=2
...
id2,b&10&z;input=kkkkkkk;99;Mundo&a=1;b=2

Interactive session

Start the checker on the model and type formulas or commands at the prompt:

$ dltl-mc --log-file examples/sample
----------------------------------------
file:      examples/sample.mod
#traces:   3
#events:   17
#atomics:  3
att. desc: ['aE', 'nV', '@att', '$p']
----------------------------------------
DLTL -> F x.("(x)x[V] == 10")
2,1,66.67,0.0
DLTL -> _WHO
id1 id2
DLTL -> G (a | b)
2,1,66.67,0.0
DLTL -> _WHO_NOT
id2
DLTL -> F ((a | b) & z.((X false) & "(z)z[#] == 2"))
1,2,33.33,0.0
DLTL -> _SET ?v 4,10
DLTL -> F x.("(x)x[V] == ?v")
2,1,66.67,0.0
2,1,66.67,0.0
DLTL -> _WRITE
DLTL -> _BYE

Reading the session: some event has V = 10 in two of the three traces (_WHO lists them); every event is a or b except in id2, which contains c and z events; only id0 has exactly two events; the macro ?v makes the last formula be checked twice, once per value. _WRITE saves the results next to the model (examples/sample.res, .norm, .forms) and _BYE (or _AGUR) ends the session (Ctrl-D also does).

Batch run

The same can be done non-interactively with an init file, which usually defines macros, and a formula file:

$ dltl-mc --log-file examples/sample --init-file examples/sample.init \
          --formula-file examples/formulas.txt --no-interactive
----------------------------------------
file:      examples/sample.mod
#traces:   3
#events:   17
#atomics:  3
att. desc: ['aE', 'nV', '@att', '$p']
----------------------------------------
0,3,0.0,0.0
1,2,33.33,0.0
3,0,100.0,0.0
...
1,2,33.33,0.0

examples/formulas.txt contains fourteen formulas (two of them generated by the macro ?vals), ends with _WRITE and _BYE, and therefore leaves in examples/:

$ cat examples/sample.res           # one column per formula: holds at the first event?
id0,0,0,1,0,0,0,1,0,1,1,0,0,0,0
id1,0,0,1,0,0,0,1,1,0,0,0,0,0,0
id2,0,1,1,1,1,1,1,0,0,0,1,1,1,1
$ head -2 examples/sample.norm      # fraction of events where each formula holds
id0,0.0,0.0,1.0,0.0,0.0,0.0,1.0,0.0,1.0,1.0,0.0,0.0,0.0,0.0
id1,0.125,0.0,1.0,0.0,0.0,0.0,0.625,0.75,0.0,0.0,0.0,0.0,0.0,0.0
$ head -2 examples/sample.forms     # the formulas, in column order
F a & x.("(x)x[V]==10")
F x.("(x)x[p]['b']==22")

With the legacy syntax the batch run reads

python MC.py log-file=examples/sample init-file=examples/sample.init formula-file=examples/formulas.txt interactive=false

This run is exactly what the regression tests reproduce (see Test suite).

A semantic example: Synthea and SNOMED CT

examples/synthea/ contains twenty event logs (50 to 100 000 traces) that simulate patients going through ten Synthea disease modules (asthma, allergies, breast and colorectal cancer, COPD, epilepsy, ...). Each event of a log has, besides its attributes, its own named graph in an RDF knowledge graph (N-Quads) describing the clinical state it executes: SNOMED CT, LOINC and RxNorm codes with their labels, state type, category, remarks and observation ranges. The propositions of the example load the graph into an embedded RDF store (Oxigraph) and ask SPARQL questions inside the graph of the frozen event, so a formula can say things like "every allergic disposition is eventually followed by an allergy screening test":

G x.("(x)PROP.Allergic_disposition(x[Event])" -> X F y.("(y)PROP.Allergy_screening_test(y[Event])"))
48,2,96.0,0.08

The example needs the optional dependency pyoxigraph (pip install "semanticdltl[synthea]"). Its README explains the data, the propositions, a full session step by step, and how to generate new logs: examples/synthea/README.md.

Trace model format (.mod)

A .mod file is a comma-separated text file with one header line describing the attributes and then one event per line:

aE,nV,@att,$p
id0,a&4&a;1&a=1;b=2
id0,a&1&a;1&a=1;b=3
id1,a&4&a;1&a=1;b=5
id1,b&1&h;2&a=1;b=2

Header. The first character of each field is the attribute type, the rest its name:

Type	Attribute
a	atomic proposition: the value is a proposition that holds in the event
s	string
n	number (stored as a float)
b	boolean
@	set of strings, item1;item2
$	dictionary of key=value pairs, name=John;age=34 (values are cast to bool, float or string)

Missing values default to 0, False and '' respectively.

Events. trace_id,value_1&value_2&..., one value per header field, in order. Events of the same trace need not be contiguous; traces are sorted by id.

XES event logs

--log-file also accepts an event log in XES (eXtensible Event Stream, IEEE 1849), the interchange format of process mining tools. A file ending in .xes (or a gzipped .xes.gz) is read directly into memory: no .mod file is written.

examples/sample.xes is the sample model as an XES log, with a timestamp and a resource added to each event:

<trace>
    <string key="concept:name" value="id0"/>
    <event>
        <string key="concept:name" value="a"/>
        <int key="V" value="4"/>
        <list key="att">
            <values>
                <string key="item" value="a"/>
                <int key="item" value="1"/>
            </values>
        </list>
        <container key="p">
            <int key="a" value="1"/>
            <int key="b" value="2"/>
        </container>
        <date key="time:timestamp" value="2024-03-04T09:00:00.000+01:00"/>
        <string key="org:resource" value="Ana"/>
    </event>
    ...

$ dltl-mc --log-file examples/sample.xes
----------------------------------------
file:      examples/sample.xes
#traces:   3
#events:   17
#atomics:  4
att. desc: ['aconcept:name', 'nV', '@att', '$p', 'ntime:timestamp', 'sorg:resource']
----------------------------------------
DLTL -> F x.("(x)x[V] == 10")
2,1,66.67,0.0
DLTL -> F x.(b & "(x)x[COL['org:resource']] == 'Marta'")
2,1,66.67,0.0

Default mapping. The trace identifier is the attribute concept:name of the trace (trace_<n>, counting from 0, for a trace without it; another attribute can be chosen with --xes-trace-id-key). The concept:name of an event, its activity, is an atomic proposition. Every other attribute of the events keeps its name and gets a type from its XES type, in the order in which the attributes first appear in the log:

XES type	Type in the model
string	s string
int, float	n number
date	n number: milliseconds since 1970-01-01 00:00:00 UTC
boolean	b boolean
id	a atomic proposition
list	@ set of strings
container	$ dictionary

An XES name such as org:resource is not a Python identifier, so in a data expression it is read as x[COL['org:resource']] rather than x[Resource]. A mapping schema gives it a better name.

Mapping schema. --xes-schema FILE.xml names an XML file that gives a type and a name to the attributes you choose (examples/sample.schema.xml):

<container key="mod:schema">
    <string key="concept:name" value="aE"/>
    <string key="V" value="nV"/>
    <string key="att" value="@att"/>
    <string key="p" value="$p"/>
    <string key="time:timestamp" value="nTime"/>
    <string key="org:resource" value="sResource"/>
</container>

key is the name of the attribute in the XES file; the first character of value is its type in the model and the rest its name, exactly as in the header of a .mod file. Without a schema only concept:name is mapped (to an atomic proposition).

By default every attribute of the events is loaded: those that appear in the schema with the type and the name it gives them, in its order, and then the rest with the name they have in the XES file and the type of the default mapping. With --xes-ignore only the attributes that appear in the schema are loaded:

$ dltl-mc --log-file examples/sample.xes --xes-schema examples/sample.schema.xml --xes-ignore

$ dltl-mc --log-file examples/sample.xes --xes-schema examples/sample.schema.xml
----------------------------------------
file:      examples/sample.xes
#traces:   3
#events:   17
#atomics:  4
att. desc: ['aE', 'nV', '@att', '$p', 'nTime', 'sResource']
----------------------------------------
DLTL -> F x.(a & X F y.(b & "(x,y)y[Time] - x[Time] <= 60000"))
1,2,33.33,0.0
DLTL -> _WHO
id1

(an a event followed, within a minute, by a b event). _WRITE saves the results next to the log, as examples/sample.res, .norm and .forms.

Values. The model loaded from an XES log is one that a .mod file can express. That format has no quoting, so some values are adapted:

• the value of an atomic attribute, and the trace identifier, become identifiers: every character that cannot be part of one is replaced by _, repeated _ are collapsed and a leading digit gets a _ in front (Hand washing → Hand_washing, event-7 → event_7, 123-test → _123_test), so that they can be written in formulas;
• in strings, and in the items of sets and dictionaries, only the separators of the .mod format (&, ,, ;, =, tabs and line breaks) are replaced by _: John Doe - Manager is kept, A&B becomes A_B;
• an attribute that an event does not have gets the atomic proposition _, the string '', the number 0, False or an empty collection;
• a value that does not fit the type the schema asks for (a non-numeric string for n) stops the load with an error.

Only the attributes of the events are loaded (not those of the traces or of the log), nested attributes are ignored and a list or container cannot contain another one.

examples/xes-example/ applies all this to a real log, that of the Conformance Checking Challenge 2019 (recorded procedures of central venous catheter installation), with a schema and a session explained step by step: see examples/xes-example/README.md.

Formulas

Propositions

• Atomic propositions are the values of the a columns (e.g. a, b, ac_Start). They must be identifiers and cannot be U, S, X, Y, G, H, F, O.
• Data expressions "(x,y)<python expression>" are Python boolean expressions over the events frozen in the listed variables (see below).
• true, false.

Operators

From the loosest to the tightest binding (see docs/grammar.md):

Syntax	Meaning
f -> g, f <-> g	implication, equivalence
f | g	or
f & g	and
f U g	f holds until g holds
f S g	f holds since g held
F f, O f	eventually / once: f holds at some future / past event (including the current one)
Fn f, On f	f holds at the current and the next / previous n-1 events (F3 f)
G f, H f	globally / historically: f holds at every future / past event
X f, Y f	f holds at the next / previous event; false at the last / first event
Xn f, Yn f	X / Y applied n times (X2 f is X X f)
! f	not
z.(f)	freeze: bind the current event to variable z inside f

Parentheses group sub-formulas. Useful idioms: X false holds only at the last event of a trace and Y false only at the first one.

Freeze operator and data expressions

z.(f) binds the current event to the variable z (any single lowercase letter) so that data expressions inside f can read its attributes:

F x.("(x)x[V] <= 34+7")                       some event has V <= 41
F x.("(x)x[p]['b'] == 22")                    ... has b = 22 in dictionary p
F x.("(x)'z' in x[att]")                      ... contains z in set att
F b & x.(F y.(a & "(x,y)x[V] == y[V]"))       a b-event followed by an a-event with the same V
F ((a | b) & z.((X false) & "(z)z[#] == 2"))  the last event is the 2nd one and is a or b
F x.(b & "(x)PROP.IN_DIC(x[p], 'b', 22)")     using a user-defined proposition

Inside a data expression:

• x[<attr>] is the value of the non-atomic attribute <attr> of the event frozen in x; <attr> is written bare (x[V], not x['V']);
• x[#] is the position of the event in its trace, starting at 1;
• an event is a tuple (position, atoms, attr1, attr2, ...): x[I_POS] is its position (the same value as x[#]), x[I_ATOM] the set of its atomic propositions, and COL['<attr>'] the position of <attr> in the tuple;
• PROP.<name>(...) calls a function of the propositions module, and <mod>.<name>(...) one of a module loaded with _LOAD (see below);
• any Python expression is allowed (and, or, int(...), .get(...)); only numeric attributes can be used in numeric comparisons.

Do not use the name of a freeze variable inside string literals of its expression ('x' in x[att] would be rewritten; use another variable name).

Security note. Data expressions are executed with Python's eval, files given to _LOAD are imported, and @ lines are run in the shell. A formula or init file is therefore as trusted as a Python script: only check files you would be willing to run.

User-defined propositions

src/dltl/propositions.py is loaded by default as PROP. To use your own, write a Python file and pass it with --propositions my_props.py:

COLUMNS = {}   # filled in by the checker: attribute name -> position in the event

def same_actor(x, y):
    return x[COLUMNS['Actor']] == y[COLUMNS['Actor']]

F x.(X F y.("(x,y)PROP.same_actor(x, y)"))

Loading propositions during a session

Functions can also be added at any moment of a session, without restarting the checker, with _LOAD name file.py; the file becomes available under the name you choose. examples/extra_props.py defines f(x) (twice x) and has_V(event, value):

DLTL -> F x.("(x)x[V] == 10")
2,1,66.67,0.0
DLTL -> _LOAD mp examples/extra_props.py
DLTL -> F x.("(x)mp.f(x[V]) == 20")
2,1,66.67,0.0
DLTL -> F x.("(x)mp.has_V(x, 4)")
2,1,66.67,0.0

Several files can be loaded under different names, and _LOAD can go in an init file so that the functions are available from the start. Loading a name again replaces the module: edit the file, run _LOAD again and the new definitions are used by the next formula. If the file declares a COLUMNS dictionary it is filled with the attribute positions, as for PROP.

The default module provides, among others, IN_DIC, SAME_KEY_VALUE, check_patt (regular expression on a string attribute), diff_pos (distance between two events) and has_f_value (float comparison with tolerance); see src/dltl/propositions.py.

For propositions that query a knowledge graph with SPARQL, see the Synthea example in examples/synthea/: each event of the log has its own named graph in an RDF store, and the propositions ask questions inside the graph of the frozen event.

Commands and macros

Lines starting with _ are commands, lines starting with ; are comments, and a line starting with @ runs the rest of the line as an operating-system command (@ls examples).

Command	Effect
_INFO	show information about the loaded model
_SET ?name v1, v2, ...	define macro ?name with the given values
_RE ?name <regex>	define macro ?name with the atomic propositions matching the regular expression
_RANGE ?name from,to[,step]	define macro ?name with a range of integers (inclusive)
_LOAD name file.py	load a Python file; its functions are used in formulas as name.<function>
_WHO / _WHO_NOT	ids of the traces that satisfy / do not satisfy the last checked formula
_WRITE	save the results (see below)
_WRITE_LENGTHS	save <model>_trace_lengths.csv with the length of each trace
_CLEAR_DATA (or _CLEAR_CHECKED)	forget the checked formulas and their results
_AGUR or _BYE	end the session (_AGUR is the historical name, agur is also accepted)

A formula containing macros is checked once per value; with several macros, once per combination:

_SET ?acts ac_Start, ac_End
_RANGE ?n 1,3
F (?acts & X?n ac_Activity)     -> 6 formulas

A macro value may itself contain macros, and the resulting formulas keep the order in which the values were written:

DLTL -> _SET ?a a,b
DLTL -> _SET ?b ?a,c
DLTL -> F ?b                     -> F a, F b, F c
2,1,66.67,0.0
2,1,66.67,0.0
1,2,33.33,0.0

Macros are expanded only inside formulas: _SET does not accept commands. Commands are recognised before macros are expanded, so _SET ?bye _AGUR followed by ?bye does not end the session; it checks the formula _AGUR (an atomic proposition that never holds).

_WRITE produces, next to the model:

File	Content
<model>.res	per trace: id,1,0,1,..., whether each checked formula holds at its first event
<model>.norm	per trace: id,0.5,0.0,..., the fraction of events where each formula holds
<model>.forms	the checked formulas, one per line, in the same order as the columns above

Using it as a library

from dltl import Log, Session

log = Log.load("examples/sample")
session = Session(log)
for summary in session.check_formula('F x.("(x)x[V] == ?v")'):
    print(summary.formula, summary.yes, summary.no, summary.pct)
session.execute("_WRITE")

Log.load reads an XES log too when the path ends in .xes or .xes.gz; load_xes takes the options of the command line:

from dltl import Session, load_xes

log = load_xes("examples/sample.xes", schema="examples/sample.schema.xml")
#     also: trace_id_key="concept:name", ignore=False
session = Session(log)

Lower level, dltl.parser.parse_formula builds the formula and dltl.evaluator.Evaluator(log.column_index).eval_formula(node, trace) returns the value of the formula at every event of a trace.

Repository layout

MC.py               legacy entry point (python MC.py log-file=...)
src/dltl/           the package
  formula.py          formula node constructors
  parser.py           lexer and parser
  evaluator.py        evaluation of formulas over a trace
  log.py              loading of .mod models, saving of results
  xes.py              loading of XES event logs
  macros.py           macro expansion
  session.py          session: results, macros, commands
  propositions.py     default user propositions (PROP)
  cli.py              command line
tests/              pytest suite (tests/golden holds the reference output)
examples/           example models and formulas; examples/synthea is a semantic
                    example with SPARQL-backed propositions (needs pyoxigraph);
                    examples/xes-example is a real XES event log
docs/grammar.md     formal grammar and operator precedence
docs/architecture.md  technical description of the design and implementation

Run the tests with pytest and the linter with ruff check src tests (see Test suite below).

Contributing

Bug reports, questions and pull requests are welcome: see CONTRIBUTING.md for how to report a problem usefully and the rules for code changes.

Authors and license

SemanticDLTL is developed by Joaquín Ezpeleta and Javier Fabra (Universidad de Zaragoza, Spain) and María José Ibáñez (Universidad de La Rioja, Spain). Contact: semanticdltl@unizar.es.

GPL-3.0-or-later. See LICENSE.

The software is archived on Zenodo: DOI 10.5281/zenodo.22777412 always resolves to the latest version, and each release has its own DOI (1.2.0: 10.5281/zenodo.23991412; 1.1.0: 10.5281/zenodo.22777413). To cite the tool, use CITATION.cff (GitHub shows a "Cite this repository" button with APA and BibTeX); to cite the method, use the SIMPDA 2017 paper referenced above.

Test suite

The tests/ directory contains a pytest suite of 116 test cases, organised in ten modules. The tests need pytest and ruff, which are not part of the standard library, so they are run inside a virtual environment created from the repository root:

python3 -m venv .venv                 # 1. create the environment (once)
source .venv/bin/activate             # 2. activate it (Windows: .venv\Scripts\activate)
pip install -e ".[dev]"               # 3. install the package and the dev tools (once)
pytest                                # 4. run the suite
ruff check src tests                  #    and the linter

Once the environment exists, only steps 2 and 4 are needed in later sessions. The same can be done without activating the environment, by calling the tools through their path:

.venv/bin/pytest
.venv/bin/ruff check src tests

or through the Makefile, which creates the environment on first use:

make test          # pytest
make lint          # ruff
make check         # both

Useful pytest options are -v (list every test), tests/test_parser.py (one module only) and -k <expr> (tests whose name matches an expression).

The suite serves two purposes: it guarantees that the packaged implementation reproduces the results of the original prototype, and it specifies the intended behaviour of every component in isolation.

Regression against the original prototype. The directory tests/golden/ stores the output obtained from the original, unrefactored implementation on the model examples/sample.mod with the init file examples/sample.init and the formulas in examples/formulas.txt. Two tests reproduce that session and compare the summary lines printed for each formula, as well as the files .res, .norm and .forms produced by _WRITE, with the stored reference: test_regression_cli.py invokes the command-line tool with the legacy key=value syntax in a subprocess, whereas test_regression_api.py drives the same session through the Log and Session classes of the library. A second, smaller fixture (examples/sample2.mod with examples/formulas2.txt, two formulas combining nested freezes with U and H) is checked the same way. The API module additionally exercises every session command (_INFO, _SET, _RE, _RANGE, _LOAD, _WHO, _WHO_NOT, _CLEAR_DATA, _WRITE_LENGTHS, _AGUR/_BYE, @ system calls) and verifies that a malformed macro name, a missing file in _LOAD or a syntactically incorrect formula is reported without terminating the session. The reference output was updated deliberately, and only where documented in CHANGELOG.md, for the changes in behaviour introduced in version 1.0.0 (operator precedence and the removal of the quote escaping in .forms).

Parser (test_parser.py, 13 cases). Construction of atomic propositions and constants; sharing of a single node among all the occurrences of an atomic proposition; every unary and binary operator, including implication and equivalence; expansion of the bounded operators Xn, Yn, Fn and On into nested nodes; operator precedence, in particular that & binds tighter than |; left associativity; the freeze operator and data expressions with one, two or no variables, including the unescaping of quoted characters; the treatment of the $ terminator; and the detection of syntax errors.

Evaluator (test_evaluator.py, 17 cases). On a hand-built trace of four events with numeric, set-valued and dictionary-valued attributes, the tests check the truth value of formulas at every event for each temporal operator (X, Y, F, G, O, H, U, S and their bounded versions), the idioms X false and Y false identifying the last and first events, the freeze operator over each attribute type, the event position x[#], the COL map, properties relating two frozen events, the default propositions module and a user-supplied one relying on COLUMNS, the summary statistics of a trace, the fact that a run-time error inside a data expression is reported and evaluates to false, the early termination of F, G, O and H once their value is known, and the registration of extra modules for _LOAD.

Model loading (test_log.py, 11 cases). Loading of the sample model (number of traces and events, sorted identifiers, atomic propositions, column index and event tuples); tolerance to the .mod suffix; every attribute type together with its default value when missing; column numbering when atomic and non-atomic attributes are interleaved; independence of two models loaded in the same process; rejection of unknown attribute types, of lines with a wrong number of values and of missing files; the value casting functions; and the generation of the information text, the _WHO/_WHO_NOT answers and the result files.

XES event logs (test_xes.py, 42 cases). The conversion rules (identifiers, separators, timestamps); the default mapping of every XES type and the values of missing attributes; attributes that first appear late in the log; the mapping schema (types, names, order, ignore, the trace identifier) and the rejection of invalid schemas, values and files; gzipped logs and Log.load; and, on examples/sample.xes, that the model loaded from XES is the model of examples/sample.mod and reproduces the reference session and its result files. The command-line options for XES are tested through main, and the formulas of examples/xes-example are checked against tests/golden/xes-example.stdout.

Macro expansion (test_macros.py, 7 cases). Formulas without macros, with a single macro, with several macros (Cartesian product, in order), nested macros keeping the order of their values, the preference for the longest matching macro name, and the bounded expansion of cyclic definitions.

Command line (test_cli_args.py, 8 cases). Translation of the legacy key=value arguments into options, default values, the exit codes returned when the model is not given (2) or when an input file does not exist (1), single-line and multi-line ($-terminated) reading of formulas, and the display of the prompt only in interactive mode.