Gamma on the Command Line

semantifyr-gamma verifies Gamma models (.gamma files, the language of the in-tree Gamma frontend, a simplified Gamma): statecharts, their composition and their verification cases. It compiles a model to OXSTS on top of the bundled Gamma semantic library. Its distribution, semantifyr-gamma-<version>.zip, carries Theta, the library in libraries/gamma and the example model models/smoke/Simple.gamma.

Usage: semantifyr-gamma [<options>] <command> [<args>]...

  Semantifyr for Gamma 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 a Gamma model.
  compile  Compile a Gamma model to OXSTS.

verify

Usage: semantifyr-gamma verify [<options>] <model path>

  Verify the cases of a Gamma model.

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:
  --case-name=<text>  Qualified name of a case, 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>  Gamma model file.

verify compiles the model and verifies its cases with the options, output and exit codes of semantifyr verify. A case is named by its Gamma qualified name, such as Simple.WorkerStatechartIdleReachable; without --case-name, verify verifies every case of the model. Under the artifact directory, each case gets a directory named after it, holding the compiled model model.oxsts and the verification artifacts under verification/. For each case with a witness, verify writes the witness as a Gamma execution trace, trace.gamma, next to the case's report.json (Gamma traces).

compile

Usage: semantifyr-gamma compile [<options>] <model path>

  Compile a Gamma model to OXSTS.

Options:
  -o, --output=<path>  Output file.
  -h, --help           Show this message and exit

Arguments:
  <model path>  Gamma model file.

compile writes the OXSTS model of a Gamma model to --output, by default next to the model with the .oxsts extension. semantifyr verifies it together with that library: semantifyr verify -l <semantifyr-gamma distribution>/libraries/gamma Simple.oxsts.