Skip to content

Command line

Here is a description of ProVeLines’ command-line options. Remember that if Multi-features are enabled then the following command must be executed first:

export DYLD_LIBRARY_PATH=./lib/z3:$DYLD_LIBRARY_PATH

ProVeLines’ command line follows the following pattern: ./provelines [options] model.pml

Options for model checking:

  • (none) Does nothing.
  • -check Verifies the model. When a problem (assert, deadlock or property violation) is found, an error trace (counterexample) is printed and execution stops.
  • -exhaustive Determines also which products have no problems. The normal check will stop at the first problem, and does not determine whether there are products that have no problems (e.g. those that satisfy a property).
  • -fdlc Search for trivially invalid end states (more costly).
  • -ltl Checks whether the specified property is satisfied (when used with -check). Never claims can be specified manually, too.
  • -sim Checks whether the specified model refines the input model according to the specified properties.
  • -stutter Executes non stutter steps. When combined with -sim, checks stutter simulation instead of standard simulation.
  • -props Parses the file containing the relevant properties. Required by -sim and -stutter.

Options for output control:

  • (none) Prints a full trace for every counterexample.
  • -st Only prints states when there are no changed variables.
  • -nt Does not print any traces, only information about violating (or satisfying) products.

Options for features and feature model:

  • (none) Will attempt to load a TVL feature model that is named as the .pml file but with extension .tvl
  • -fm Load the specified TVL file (only used in verification). This parameter can be omitted if the TVL file is named as the .pml file but with extension .tvl.
  • -fmdimacs As before, but load the dimacs of the feature model directly.
  • -filter Limit the verification to a subset of the products specified in the TVL file. The TVL syntax has to be used for this.
  • -spin Treat features like normal variables (as SPIN would do).
  • -ospin Similar to -spin, but statements with a bad guard are removed from the model before model checking. The input is thus interpreted as fPromela (not exactly as SPIN would do). This is normally more efficient than -spin.

Options for debugging:

  • -exec Execute the model (does not print states, only model output).
  • -l Stop when the given number of states were explored. (This option can also be used for model checking.
  • -s Parse and print static info (symbol table, FSMs, MTypes, ..).
  • -t Do not delete the generated temporary files.