Command Line
The semantifyr command lists, compiles, measures and verifies the verification cases of OXSTS models. semantifyr-sysml for SysML v2 models and semantifyr-gamma for Gamma models share its verification options, output and exit codes. Each launcher comes in a release zip of its own with the Theta backend (Getting Started), or builds from source with ./gradlew :semantifyr-cli:installDist, :sysml-cli:installDist or :gamma-cli:installDist; semantifyr is then subprojects/semantifyr-cli/build/install/semantifyr/bin/semantifyr. They need a Java 25 runtime and at least one verification backend.
Usage: semantifyr [<options>] <command> [<args>]...
Semantifyr for OXSTS models.
Options:
--log-level=(ERROR|WARN|INFO|DEBUG|TRACE) Root log level. (default: WARN)
--version Show the version and exit
-h, --help Show this message and exit
Commands:
verify Verify the cases of an OXSTS model.
compile Compile cases to inlined OXSTS.
list List the cases of an OXSTS model.
metrics Print the model sizes of cases.
portfolios List the portfolios.
A model or library path is an .oxsts file or a directory, which is searched recursively for .oxsts files. --log-level before the command sets the level of the log on standard error, WARN by default.
--case-name selects cases by qualified name and overrides the tag filters. Without it, a command takes the cases that carry one of the --include-tag tags, or every case when none is given, except those that carry an --exclude-tag tag. --artifacts debug, or --enable-artifact CompilationStep, also writes the model after every compiler pass into pipeline/steps, which is slow and meant for bisecting compiler regressions. The artifacts of a case go to a directory named after the model file and the qualified name of the case, with :: written as . and every character other than letters, digits, ., _ and - as _, shortened with a hash when longer than 64 characters. An artifact directory that cannot be created or written stops the command before it compiles anything.
verify
Usage: semantifyr verify [<options>] <model path>
Verify the cases of an OXSTS model.
Verification case specification:
--case-name=<text> Qualified name of a case, repeatable.
--include-tag=<text> Select the cases with this tag, repeatable.
--exclude-tag=<text> Skip the cases with this tag, repeatable.
Backend options:
--portfolio=<text> Portfolio id. (default: smart-full)
--theta-executor=(Auto|Shell|Docker)
How to run Theta. (default: Auto)
--theta-docker-image=<text> Theta Docker image. (default:
ftsrg/theta-xsts-cli:8.6.0)
-t, --timeout-seconds=<int> Timeout per case, in seconds. (default: 300)
Compilation options:
--optimization=(None|All) Optimization preset. (default: All)
--enable-optimization=
(ExpressionSimplification|OperationFlattening|RedundantOperationRemoval|AssumeFalsePropagation|ConstantVariableSubstitution|CopyPropagation|DeadStoreElimination|DeadCodeRemoval|VariableLiveness)
Optimization pass to run, repeatable.
--disable-optimization=
(ExpressionSimplification|OperationFlattening|RedundantOperationRemoval|AssumeFalsePropagation|ConstantVariableSubstitution|CopyPropagation|DeadStoreElimination|DeadCodeRemoval|VariableLiveness)
Optimization pass to skip, repeatable.
Artifact options:
-d, --artifact-directory=<path> Directory of the artifacts.
--artifacts=(None|All|Debug) Artifact preset. (default: All)
--enable-artifact=
(InstantiatedModel|InlinedModel|FlattenedModel|CompilationStep|Mapping)
Artifact kind to write, repeatable.
--disable-artifact=
(InstantiatedModel|InlinedModel|FlattenedModel|CompilationStep|Mapping)
Artifact kind to skip, repeatable.
Options:
-l, --library=<path> OXSTS library file or directory, repeatable.
-q, --quiet Only the verdict of each case.
--json One JSON object per case, one per line.
-h, --help Show this message and exit
Arguments:
<model path> OXSTS model file or directory.
--timeout-seconds bounds each case as a whole: its compilation, every backend run of the portfolio and the back-annotation of the witness. --theta-executor runs Theta from PATH (shell), in Docker (docker), or from PATH when it is there and in Docker otherwise (auto); --theta-docker-image is the image Docker runs, a repository:tag or @digest reference.
For each case, verify prints Verifying <case> ..., then the verdict with the time it took, compilation included, then the path of the report.json it wrote for the case. A case that does not compile gets COMPILATION_ERROR in place of the verdict and no report, and the compiler's message goes to standard error; a case whose witness cannot be back-annotated gets BACK_ANNOTATION_ERROR the same way. With --quiet it prints only the verdict of each case, one per line: PASSED, FAILED, INCONCLUSIVE, NOT_SUPPORTED, TIMEOUT, ERRORED, COMPILATION_ERROR or BACK_ANNOTATION_ERROR.
With --json it prints one JSON object per case and line, as each case finishes:
{"case":"semantifyr::verification::smoke::CounterReachesThree","exitCode":0,"report":"/tmp/semantifyr-123/smoke.semantifyr.verification.smoke.CounterReachesThree/report.json","compilationDuration":"PT0.158S","verificationDuration":"PT1.204S"}
case is the qualified name of the case, exitCode its exit code, report the absolute path of its report.json, compilationDuration the time the compilation took and verificationDuration the time from the compiled model to the verdict, both ISO 8601 durations. A case that does not compile or whose witness cannot be back-annotated has phase, compilation or back-annotation, and error, the message, instead of report and the durations:
{"case":"semantifyr::verification::smoke::CounterReachesThree","exitCode":4,"phase":"compilation","error":"Property body must have a temporal operator (`AG` or `EF`) at the top level."}
report.json holds the rest: verificationCase, portfolioId, optimization, timeout and result, whose verdict is Passed, Failed, Inconclusive, NotSupported, Timeout or Errored, with the message of the backend, metadata.backendId, the backend configuration that answered, and metrics: the durations of the run, of the backend and of the compiler's phases, the optimizer's statistics and the model sizes.
Verdicts
A case is Passed when its property holds and Failed when it does not. Otherwise it is Inconclusive when the backends finished without a verdict the portfolio trusts (see soundness directions), Timeout when the time limit ran out before a backend decided, NotSupported when the chosen backend refuses a construct of the model (the pages of Theta, nuXmv, Spin and Uppaal list what each refuses and why) or a value leaves the range Uppaal declared for its variable (the message names each construct or variable and its source line), or Errored when a backend run failed, an engine rejected the model it was given (the message carries the engine's text) or trusted backends disagreed.
compile
Usage: semantifyr compile [<options>] <model path>
Compile cases to inlined OXSTS.
Verification case specification:
--case-name=<text> Qualified name of a case, repeatable.
--include-tag=<text> Select the cases with this tag, repeatable.
--exclude-tag=<text> Skip the cases with this tag, repeatable.
Compilation options:
--optimization=(None|All) Optimization preset. (default: All)
--enable-optimization=
(ExpressionSimplification|OperationFlattening|RedundantOperationRemoval|AssumeFalsePropagation|ConstantVariableSubstitution|CopyPropagation|DeadStoreElimination|DeadCodeRemoval|VariableLiveness)
Optimization pass to run, repeatable.
--disable-optimization=
(ExpressionSimplification|OperationFlattening|RedundantOperationRemoval|AssumeFalsePropagation|ConstantVariableSubstitution|CopyPropagation|DeadStoreElimination|DeadCodeRemoval|VariableLiveness)
Optimization pass to skip, repeatable.
Artifact options:
-d, --artifact-directory=<path> Directory of the artifacts.
--artifacts=(None|All|Debug) Artifact preset. (default: All)
--enable-artifact=
(InstantiatedModel|InlinedModel|FlattenedModel|CompilationStep|Mapping)
Artifact kind to write, repeatable.
--disable-artifact=
(InstantiatedModel|InlinedModel|FlattenedModel|CompilationStep|Mapping)
Artifact kind to skip, repeatable.
Options:
-l, --library=<path> OXSTS library file or directory, repeatable.
-o, --output=<path> Output file, or directory for several cases.
-h, --help Show this message and exit
Arguments:
<model path> OXSTS model file or directory.
For each case, compile prints Compiling <case> to <file>, writes the inlined model to the file, and prints the directory holding the artifacts of the case, a temporary directory unless --artifact-directory names one. With one selected case, --output is the file, <model>.inlined.oxsts next to the model by default; with several, it is a directory, <model>.inlined next to the model by default, holding a file for each case named as its artifact directory, with .oxsts appended.
list
Usage: semantifyr list [<options>] <model path>
List the cases of an OXSTS model.
Verification case specification:
--case-name=<text> Qualified name of a case, repeatable.
--include-tag=<text> Select the cases with this tag, repeatable.
--exclude-tag=<text> Skip the cases with this tag, repeatable.
Options:
-l, --library=<path> OXSTS library file or directory, repeatable.
-h, --help Show this message and exit
Arguments:
<model path> OXSTS model file or directory.
metrics
Usage: semantifyr metrics [<options>] <model path>
Print the model sizes of cases.
Verification case specification:
--case-name=<text> Qualified name of a case, repeatable.
--include-tag=<text> Select the cases with this tag, repeatable.
--exclude-tag=<text> Skip the cases with this tag, repeatable.
Compilation options:
--optimization=(None|All) Optimization preset. (default: All)
--enable-optimization=
(ExpressionSimplification|OperationFlattening|RedundantOperationRemoval|AssumeFalsePropagation|ConstantVariableSubstitution|CopyPropagation|DeadStoreElimination|DeadCodeRemoval|VariableLiveness)
Optimization pass to run, repeatable.
--disable-optimization=
(ExpressionSimplification|OperationFlattening|RedundantOperationRemoval|AssumeFalsePropagation|ConstantVariableSubstitution|CopyPropagation|DeadStoreElimination|DeadCodeRemoval|VariableLiveness)
Optimization pass to skip, repeatable.
Options:
-l, --library=<path> OXSTS library file or directory, repeatable.
--json One JSON object per case, one per line.
-h, --help Show this message and exit
Arguments:
<model path> OXSTS model file or directory.
For each case, metrics prints the size of the input model, of the inlined model and of the flattened model a backend receives, each as its number of variables, operations and expressions. With --json it prints one JSON object per case and line, with case and the sizes under the keys report.json has under result.metrics.verifier.compilation:
{"case":"semantifyr::verification::smoke::CounterReachesThree","inputSize":{"variables":1,"operations":4,"expressions":13},"inlinedSize":{"variables":1,"operations":5,"expressions":15},"flattenedSize":{"variables":1,"operations":5,"expressions":12}}
metrics and verify report the same sizes for the same case and compilation options.
portfolios
Usage: semantifyr portfolios [<options>]
List the portfolios.
Options:
-h, --help Show this message and exit
The portfolio ids are listed under Portfolios.
Exit codes
| Code | Meaning |
|---|---|
| 0 | Every selected case passed, or the command completed. |
| 1 | Internal error: an unexpected exception, or the launcher could not start Java. |
| 2 | Usage error: an unknown command or option, a missing or invalid value, conflicting options, an unknown portfolio. |
| 3 | Input error: a model or library path does not exist, is not readable, or is not a model file of the launcher (.oxsts, .sysml or .gamma) or, where a directory is allowed, a directory holding one, or the case selection names or matches no case. |
| 4 | Compilation error: the model does not parse, validate or translate, or a case does not compile. |
| 5 | Failed: a property does not hold. |
| 6 | Inconclusive or NotSupported: a backend could not decide a case. |
| 7 | Timeout. |
| 8 | Errored: a backend failed, or the portfolio has no available backend. |
| 9 | Back-annotation error: a backend returned a witness that could not be back-annotated. |
| 10 | Output error: the artifact directory cannot be created or written. |
Codes 2 to 4, code 10 and an unavailable portfolio stop the command before it verifies anything, or, in compile and metrics, at the case that does not compile. Every launcher's verify runs every case, including those after a case that does not compile, and exits with the highest of their codes: 0 means every case passed, 4 that some case did not compile and the rest passed, 5 that some case failed and the rest passed, failed or did not compile.