CLI Usage

Installing py-mcmas makes the CLIs for mcmas and ispl available.

  • The mcmas CLI basically wraps the dockerized entrypoint1 for the official engine, proxying commands to the container.
  • The ispl CLI adds lots of additional functionality that's more specific to py-mcmas, including support for JSON I/O, support for pure-python specifications, etc.

ISPL CLI

The ispl CLI does most of what mcmas does, but also provides various helpers for ISPL/JSON conversion, and optionally allows for things like simulating the input spec, evaluating a command, or dropping into a REPL with the context.

Without other instructions, the default action is to handle conversion between supported formats.

# Load JSON-based ISPL, converting to raw ISPL
$ ispl --json file.json

# Load raw ISPL, converting to JSON
$ ispl --ispl file.ispl

# Load pythonic ISPL, converting to raw ISPL
$ ispl --python file.py

Explicit flags for input-format are usually optional, but required in case of nonstandard file extensions or in case of using piped input with stdin.

Given a specification in any format, typical actions are to actually run that specification, or validate it, or analyze it. All actions return JSON.

# Simulate the specification
$ ispl --sim file.ispl

# Verbose output, including raw text from `mcmas` stdout
$ ispl --verbose --sim file.ispl

# Return witnesses (implying --sim)
$ ispl --witness file.ispl

# Static analysis and extracting metadata
$ ispl --analyze file.ispl

See the analysis & witnesses demo for more details.

$ ispl --help

Usage: ispl [OPTIONS] [FNAME]

  Helper for interacting with ISPL files.

Options:
  -j, --json              Load ISPL spec from JSON file.  (Implied if filename
                          ends in .json)
  -i, --ispl              Load ISPL spec from the given ISPL  (Implied if
                          filename ends in .ispl)
  -r, --repl              Start a REPL with this context
  -c, --command TEXT      Command to execute
  -s, --sim               Simulate the specification after loading one.
                          Returns JSON
  -a, --analyze           Analyze specification after loading one.  (Cannot be
                          used with --sim)
  -p, --python            Load ISPL specification from python.  (Implied if
                          filename ends in .py)
  -W, --witness           Generate witnesses (implies --sim).\Returns counter-
                          examples only (witnesses for false formulae)
  -w, --counter-example   Generate ALL witnesses (implies --sim)
  -q, --quiet             Generate ALL witnesses (implies --sim)
  --list-pydantic-models  List available pydantic models
  --schema                Return JSON schema for named model
  --validate              Validate specification
  -v, --verbose           Do not include raw output from engine (used with
                          --sim)
  --help                  Show this message and exit.

Typically you want to pass enough information to load a specification.

For example you can convert between JSON / raw ISPL source:

# Convert ISPL source to JSON
$ ispl --ispl tests/data/muddy_children.ispl | jq . 
$ ispl --ispl tests/data/muddy_children.ispl > tests/data/muddy_children.json

# Convert JSON to ISPL
$ ispl --json tests/data/muddy_children.json

Passing --sim actually runs the specification.

This always returns JSON, and unless you pass --quiet, the JSON includes raw data from the engine.

# Run JSON, quiet output
$ ispl -q --sim --json tests/data/muddy_children.json

{
  "metadata": {
    "file": ".tmp.asgka12",
    "deadlock": false,
    "validates": true,
    "parsed": true,
    "exit_code": 0
  },
  "time": {
    "generate_time": 0.0,
    "execution_time": 0.006,
    "encoding_time": 0.001
  },
  "state_space": {
    "reachable_states": 32,
    "memory": {
      "bdd": 9065680
    }
  },
  "formulae": {
    "true": [
      "(AG ((saysknows1 -> (K(Child1, muddy1) || K(Child1, (! muddy1)))) && ((K(Child1, muddy1) || K(Child1, (! muddy1))) -> saysknows1)))",
      "(AG ((saysknows2 -> (K(Child2, muddy2) || K(Child2, (! muddy2)))) && ((K(Child2, muddy2) || K(Child2, (! muddy2))) -> saysknows2)))",
      "(AG ((saysknows3 -> (K(Child3, muddy3) || K(Child3, (! muddy3)))) && ((K(Child3, muddy3) || K(Child3, (! muddy3))) -> saysknows3)))"
    ],
    "false": []
  }
}

MCMAS CLI

# Proxies commands to container
$ mcmas ..arguments..

# Equivalently, 
$ python -m mcmas ..arguments..

# Run specification file
$ mcmas tests/data/card_games.ispl
...

See the full CLI help here.

Besides the default interface for mcmas, for convenience you can request output in JSON, via the Simulation schema, without using the ispl CLI

# One additional argument: asking for JSON output
$ mcmas --json tests/data/card_games.ispl
...


$ mcmas -h

************************************************************************
                       MCMAS v1.3.0 

 This software comes with ABSOLUTELY NO WARRANTY, to the extent
 permitted by applicable law. 

 Please check http://vas.doc.ic.ac.uk/tools/mcmas/ for the latest release.
 Please send any feedback to <mcmas@imperial.ac.uk>
************************************************************************

Usage: mcmas [OPTIONS] FILE 
Example: mcmas -v 3 -u myfile.ispl

Options: 
  -s         Interactive execution

  -v Number      verbosity level ( 1 -- 5 )
  -u         Print BDD statistics 

  -e Number      Choose the way to generate reachable state space (1 -- 3, default 2)
  -o Number      Choose the way to order BDD variables (1 -- 4, default 2)
  -g Number      Choose the way to group BDD variables (1 -- 3, default 3)
  -d Number      Choose the point to disable dynamic BDD reordering (0 -- 3, default 3)
  -nobddcache    Disable internal BDD cache

  -k         Check deadlock in the model
  -a         Check arithmetic overflow in the model

  -c Number      Choose the way to display counterexamples/witness executions (1 -- 3)
  -p Path    Choose the path to store files for counterexamples
  -exportmodel   Export model (states and transition relation) to a file in dot format

  -f Number      Choose the level of generating ATL strategies (1 -- 4)
  -l Number      Choose the level of generating ATL counterexamples (1 -- 2)
  -w         Try to choose new states when generating ATL strategies
  -atlk Number   Choose ATL semantics when generating ATL strategies (0 -- 2, default 0)
  -uc Number     Choose the interval to display the number of uniform strategies processed
  -uniform   Use uniform semantics for model checking
  -ufgroup Name  Specify the name of the group to generate uniform strategies

  -n         Disable comparison between an enumeration type and its strict subset

  -h         This screen

When this is used to run a .ispl file, a docker-volume is used to ensure the container can access it.

References

  1. See docker-mcmas.git for the default container, see environment variables for control over default image. ↩