Library Usage

This is a quick, tutorial-style introduction to some important parts of the py-mcmas codebase.

See the full API here.

Engine

Low-level access to the MCMAS model-checker is via api://mcmas.engine.

Supported inputs include raw ISPL source, pythonic ISPL (aka Specification objects), or file that have ISPL source. Regardless of input-format.. you'll probably want to learn about the ISPL primitives, which you can read about here.

Supported outputs include Simulation objects, python-dictionaries, and JSON.

Check out the tests below for more usage hints.

Summary 
import mcmas
from mcmas import engine
from mcmas.sim import Simulation


def test_run_filename_return_dict():
    out: dict = mcmas.engine(fname="tests/data/muddy_children.ispl")
    assert isinstance(out, (dict,)), "returns dictionary by default"
    assert "metadata" in out, "dictionary-output includes key for `model`"
    assert "facts" in out, "dictionary-output includes key for `facts`"
    assert out["metadata"]["parsed"], "parsed? => legal ISPL"
    assert out["metadata"][
        "validates"
    ], "validates? => parsed and all formulae confirmed"


def test_run_filename_return_text():
    out: str = mcmas.engine(
        fname="tests/data/muddy_children.ispl", output_format="text"
    )
    assert isinstance(out, (str,))
    assert out.startswith("Command line: mcmas ")


def test_run_text_return_model():
    with open("tests/data/muddy_children.ispl") as fhandle:
        text = fhandle.read()
    out = mcmas.engine(text=text, output_format="model")
    assert isinstance(out, (Simulation,)), "requested a model? => Simulation"
    assert not out.error, "successful run => no error"
    assert out.text, "model encapsulates raw output"
    assert out.metadata, "model has metadata"


def test_run_bad_program_returns_error():
    out = mcmas.engine(text="ILLEGAL PROGRAM", output_format="model")
    assert isinstance(out, (Simulation,)), "requested a model? => Simulation"
    assert not out.metadata.validates, "bad program => marked as not valid"
    assert not out.metadata.parsed, "bad program => marked as not parsed"
    assert not out.text, "bad program => `text` not set"
    assert out.error, "expected error but error is not set!"


def test_bad_filename():
    try:
        engine(fname="does/not/exist.ispl")
    except (SystemExit,) as exc:
        pass
    else:
        raise ValueError("non existant file should exit 1")


def test_run_partial():
    ispl = mcmas.ISPL(agents={})
    out = mcmas.engine(model=ispl, strict=False, output_format="model")
    assert not out.metadata.parsed, "bad data should not parse!"
    assert not out.metadata.validates, "bad data should not validate!"

Specifications & Simulations

api://mcmas.ISPL is an input to an api://mcmas.engine, and returns api://Simulation.

Partial specifications are supported so that you can build specifications up in pieces. For each case.. py-mcmas uses pydantic models for datastructures and typing.

Pydantic models are easily extended from python, or easily exported as JSON-schema in case that helps to pass data downstream to other tools, or to MCP.

Check out the test suite below for some example usage.

Summary 
import mcmas
from mcmas import ISPL, Simulation


def test_empty_simulation():
    """empty simulations are allowed so they can be built incrementally"""
    sim = Simulation()


def test_run_text_return_model():
    with open("tests/data/muddy_children.ispl") as fhandle:
        text = fhandle.read()
    out = mcmas.engine(text=text, output_format="model")
    assert isinstance(out, (Simulation,)), "requested a model? => Simulation"
    data = out.model_dump()
    for k in ["deadlock", "exit_code", "parsed", "validates"]:
        assert k in data["metadata"]


def test_run_model_return_model():
    spec = ISPL.load_from_ispl_file("tests/data/muddy_children.ispl")
    out = mcmas.engine(model=spec, output_format="model")
    assert isinstance(out, (Simulation,)), "requested a model? => Simulation"


def test_run_model_return_json():
    spec = ISPL.load_from_ispl_file("tests/data/muddy_children.ispl")
    out = mcmas.engine(model=spec, output_format="json")
    assert isinstance(out, str), "JSON request should return a string"


def test_run_model_return_data():
    spec = ISPL.load_from_ispl_file("tests/data/muddy_children.ispl")
    out = mcmas.engine(model=spec, output_format="data")
    assert isinstance(out, dict), "data request should return dict"

Logical Expressions

The mcmas.logic module provides some helpers for generating ISPL fragments, including formulae statements that use modal logic operators. See the test suite for some examples:

Summary 
from mcmas import logic, util
from mcmas.ispl import ISPL
from mcmas.logic import Environment, false, symbols, true

LOGGER = util.get_logger(__name__)
ask = symbols.ask
othersayknow = symbols.othersayknow
know = symbols.know


def test_multiple_symbols():
    a, b, c = symbols["a b c"]
    assert str(a + b + c) == "a+b+c"


def test_basic_symbols():
    # create a symbol just by naming it
    x, y = symbols.x, symbols.y
    assert str(x) == "x", "symbol evaluates to itself"
    assert str(y) == "y", "symbol evaluates to itself"
    z = symbols.z
    expr1 = logic.Equal(z, x + y)
    assert str(expr1) == "z=x+y", "addition and equality works"
    expr2 = z(x + y)
    assert str(expr2) == "z(x+y)", "symbols are callable"


def test_logical_if():
    label = 'working if-as-syntax ( i.e. ">>" )'
    actual = str(symbols.aaa >> symbols.bbb)
    expected = "aaa if bbb"
    assert actual == expected, label
    label = "working if-as-function, i.e. rshift"
    actual = str(logic.If(symbols.aaa, symbols.bbb))
    assert actual == expected, label


def test_logical_and():
    label = 'working and-as-syntax ( i.e. "&" )'
    expected = "aaa and bbb"
    actual = symbols.aaa & symbols.bbb
    assert actual == expected, label
    # ==str(logic.And(symbols.aaa, symbols.bbb))


def test_symbol_or():
    expected = "aaa or bbb"
    label = "working or-as-function"
    actual = str(logic.Or(symbols.aaa, symbols.bbb))
    assert actual == expected, label
    label = 'working or-as-syntax ( i.e. "|" )'
    actual = str(symbols.aaa | symbols.bbb)
    assert actual == expected, label


def test_fragment4():
    actual = symbols.muddy1 >> logic.Eq(Environment.child1, 1)
    expected = "muddy1 if Environment.child1=1"
    label = ""
    assert actual == expected, label
    ispl = ISPL(evaluation=[symbols.muddy1 + " if Environment.child1=1;"])
    label = "instantiated model with combined strings/symbols"
    assert ispl, label


def test_logic_fragment1():
    expected = "othersayknow=true"
    actual = str(logic.Eq(othersayknow, true))
    # assert frag1 == str(expr)
    label = "fragment1"
    assert actual == expected, label


def test_logic_fragment2():
    expected = "Environment.Action=ask and Environment.mem<Environment.child1+Environment.child3"
    actual = str(
        logic.And(
            logic.Eq(Environment.Action, ask),
            Environment.mem < Environment.child1 + Environment.child3,
        )
    )
    label = "fragment2"
    assert actual == expected, label
    # frag2 == str(expr2)


def test_logic_fragment3():
    frag3 = "othersayknow=true if Environment.Action=ask and Environment.mem<Environment.child1+Environment.child3 and othersayknow=false and (Child1.Action=know or Child3.Action=know)"
    expr = logic.If(
        logic.Eq(othersayknow, true),
        logic.And(
            logic.Eq(Environment.Action, ask),
            Environment.mem < Environment.child1 + Environment.child3,
            logic.Eq(othersayknow, false),
            logic.Grouping(
                logic.Or(
                    logic.Equal(symbols.Child1.Action, know),
                    logic.Equal(symbols.Child3.Action, know),
                )
            ),
        ),
    )
    assert frag3 == str(expr)

Validation

See also the demos for witnesses and analysis

References