smcplaus 1.1.5

A symbolic model checker for the single-agent plausibility models of dynamic epistemic logic

smcplaus

Owner : David Alvarez Lombardi

Repository : https://gitlab.com/dqalombardi/smcplaus

PyPI : https://pypi.org/project/smcplaus/

Description

A symbolic model checker for the single-agent plausibility models of dynamic epistemic logic.

References

• SEP : Plausibility models and belief change (Baltag & Renne 2016)
• A qualitative theory of dynamic interactive belief revision (Baltag & Smets 2008)
• Dynamic logic for belief revision (van Benthem 2007)
• Dynamic interactive epistemology (Board 2004)
• Two modellings for theory change (Grove 1988)

Installation

To install using pip, run the following.

$ python3 -m pip install smcplaus

Usage

Specifying formulas

Specify propositional variables.

p = PropositionalVariable(letter="p")
q0 = PropositionalVariable(letter="q", index=0)
q1 = PropositionalVariable(letter="q", index=1)

Specify complex formulas.

form_p = Formula(node=p, subformulas=None)
form_q0 = Formula(node=q0, subformulas=None)
form0 = Formula(node=Connectives.DIAMOND, subformulas=(form_q0,))  # <>q0
form1 = Formula(node=Connectives.RADICAL_UPGRADE, subformulas=(form_q0, form0))  # [$q0]<>q0

Specifying models

Specify plausibility frames by specifying a domain and a state-to-appearance map.

state0 = State(index=0)
state1 = State(index=1)
state2 = State(index=2)

my_frame = PlausibilityFrame(
    domain={state0, state1, state2},
    state_to_appearance={
        state0: {state1},
        state1: {state2},
        state2: {state2},
    },
    force_s4=True,
)

Specify plausibility models by specifying a frame and a state-to-facts map.

my_model = PlausibilityModel(
    frame=my_frame,
    state_to_facts={
        state0: {p, q0},
        state1: {q1},
        state2: {p, q1},
    },
)

Specify pointed plausibility models by specifying a model and a point.

my_pointed_model = PointedPlausibilityModel(
    model=my_model,
    point=state1,
)

Checking (pointed) models against formulas

Check if a pointed model satisfies a formula.

my_pointed_model_satisfies_form0 = my_pointed_model.satisfies(form0)  # False
my_pointed_model_satisfies_form1 = my_pointed_model.satisfies(form1)  # True

Check where a model satisfies a formula.

form_p_truthset = my_model.truthset(form_p)  # {State(s2), State(s0)}

Modifying models with formulas

Upgrade a model with a formula.

my_new_model = my_model.radical_upgrade(form_q0)

Loading and dumping structures with JSON files

Specify and load a structure from a JSON file.

my_other_model_json_str = """
{
    "frame": {
        "domain": ["s0", "s1", "s2"],
        "state_to_appearance": {
            "s0": ["s1"],
            "s1": ["s2"],
            "s2": ["s2"]
        }
    },
    "state_to_facts": {
        "s0": ["p", "q0"],
        "s1": ["q1"],
        "s2": ["p", "q1"]
    }
}
"""

my_other_model = PlausibilityModel.from_json(my_other_model_json_str, force_s4=True)

Dump a structure to a JSON file.

output_json = my_other_model.to_json()

Generating digraphs from structures

Generate the digraph of a structure.

my_model_digraph = my_model.generate_digraph()

Dump the digraph of a structure to a file.

my_model.dump_digraph(filepath=Path("my_model.dot"))

The file my_model.dot will then have the following contents.

digraph {
	s0 [label="s0 || p, q0"]
	s1 [label="s1 || q1"]
	s2 [label="s2 || p, q1"]
	s0 -> s1
	s1 -> s2
}

This can be converted to an image via dot in the command-line.

$ dot my_model.dot -Tsvg -omy_model.svg

The file my_model.svg will then have the following contents.

Examples

See ./examples/ for functional example usage.

Contributing

Before submitting a merge request, run the command tox, which will run formatters, linters, static type-checkers, and unit tests respectively.