SysML v2 on the Command Line

semantifyr-sysml verifies SysML v2 models. Its distribution, semantifyr-sysml-<version>.zip, carries Theta, the SysML v2 semantic library in libraries/sysmlv2 and the tutorial model as models/smoke/room.sysml. It translates a model to OXSTS with the bundled SysIDE fork, which runs on Node.js, so it needs node (22 or newer) on PATH; without it, translating fails with exit code 4 and a message naming node. The translator reads every .sysml and .kerml file below the model's directory as the model's workspace, so keep other models and the artifact directory out of that directory. Translations are cached under ~/.semantifyr/sysml-cache, keyed by the model and its workspace. The SysML v2 tutorial walks through a run.

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

  Semantifyr for SysML v2 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 SysML v2 model.
  compile  Translate a SysML v2 model to OXSTS.

`verify`

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

  Verify the cases of a SysML v2 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>  SysML v2 model file.

verify translates the model and verifies its cases with the options, output and exit codes of semantifyr verify. The case names start with semantifyr::sysml::model, the package the translator gives every model. The translated model stays in compiled/default/<model>.oxsts under the artifact directory, with its name map, <model>.names.json, beside it. For each case with a witness, verify runs the translator's trace command on the case's witness.json and trace.json and the name map, which writes the witness as a SysML v2 model, trace.sysml, next to the case's report.json (SysML v2 traces); a witness the generator cannot express keeps its verdict, gets no trace.sysml and a warning in the log.

The translation is verified on top of the bundled SysML v2 semantic library, the state-level library in libraries/sysmlv2. --library loads OXSTS files in addition to it and does not replace it.

`compile`

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

  Translate a SysML v2 model to OXSTS.

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

Arguments:
  <model path>  SysML v2 model file.

compile writes the OXSTS translation of the model to --output, by default next to the model with the .oxsts extension, and the name map from the model's elements to the OXSTS beside it with the .names.json extension. A construct the translator refuses is an error at its line and no OXSTS is written; a warning is printed and the translation written (SysML v2 subset). semantifyr verifies it together with that library: semantifyr verify -l <semantifyr-sysml distribution>/libraries/sysmlv2 room.oxsts.

verify​

compile​

`verify`

`compile`