ADR-009: Apalache Outputs
|Jure Kukovec, Shon Feder||2021-12-14|
This ADR documents the various files produced by Apalache, and where they get written to.
1. Categories of outputs
Files produced by Apalache belong to one of the following categories:
- Log files
- Intermediate state outputs
- Run analysis files
Counterexamples (if there are any) and basic logs should always be produced, but the remaining outputs are considered optional.
Each optional category is associated with a flag:
--write-intermediate for intermediate state outputs and an individual flag for each kind of analysis. At the time of writing, the only analysis is governed by
--profiling, for profiling results.
All such optional flags should default to
2. Output directory and run directories
Apalache should define an
out-dir parameter, which defines the location of all outputs produced by Apalache. If unspecified, this value should default to the working directory, during each run, but it should be possible to designate a fixed location, e.g.
Each run looks for a subdirectory inside of the
out-dir with the same name as
the principle file provided as input (or, for commands that do not read input
from a file, named after the executed subcommand). This subdirectory is called
the specification's (resp. command's) namespace within the
outputs originating from that input file (resp. command) will be written to this
Each run produces a subdirectory in its namespace, with the following name:
based on the ISO 8601 standard.
<DATE> is the date in
<TIME> is the local time in
Example file structure for a run executed on a file
_apalache-out/ └── test.tla ├── 2021-11-05T22-54-55_810261790529975561
Custom run directories
--run-dir flag can be used to specify an output directory into which
outputs are written directly. When the
--run-dir flag is specified, all
content included in the run directory specified above will also be written
into the directories specified by this argument.
3. Structure of a run directory
Each run directory outlined in the previous section, should contain the following:
- A file
run.txt, containing the command issued for this run, with all implicit parameters filled in, so it can be replicated exactly
- 0 or more counterexample files
- a pre-filled bug report file
BugReport.md, if the tool exited with a
--write-intermediateis set, a subdirectory
intermediate, containing outputs associated with each of the passes in Apalache
- an Apalache log file
- an SMT log file
- Files associated with enabled analyses, e.g.
4. Global Configuration File
Apalache should define a global configuration file
apalache.cfg, e.g. in the
<HOME>/.tlaplus directory, in which users can define the default values of all parameters, including all flags listed in section 1, as well as
out-dir. The format of the configuration file is an implementation detail and will not be specified here.
Apalache should also look for a local configuration file
current working directory or its parents. If it finds such file, any configured
parameters therein will override the parameters from the global config file.
If a parameter is specified in the configuration file, it replaces the default value, but specifying a parameter manually always overrides config defaults. In other words, parameter values are determined in the following way, by order of priority:
--<flag>=<value>is given, use
- if a local
.apalache.cfgfile is found (or is specified with the
<flag>: <value>, then use
- if the global
- Use the defaults specified in the