# smcplaus
Owner : [David Alvarez Lombardi](https://linktr.ee/dqalombardi)
Repository : [https://gitlab.com/dqalombardi/smcplaus](https://gitlab.com/dqalombardi/smcplaus)
PyPI : [https://pypi.org/project/smcplaus/](https://pypi.org/project/smcplaus/)
## Description
A symbolic model checker for the single-agent plausibility models of [dynamic epistemic logic](https://plato.stanford.edu/entries/dynamic-epistemic/).
## References
- [SEP : *Plausibility models and belief change* (Baltag & Renne 2016)](https://plato.stanford.edu/entries/dynamic-epistemic/#PlauModeBeliChan)
- [*A qualitative theory of dynamic interactive belief revision* (Baltag & Smets 2008)](https://doi.org/10.1007/978-3-319-20451-2_39)
- [*Dynamic logic for belief revision* (van Benthem 2007)](https://doi.org/10.3166/jancl.17.129-155)
- [*Dynamic interactive epistemology* (Board 2004)](https://doi.org/10.1016/j.geb.2003.10.006)
- [*Two modellings for theory change* (Grove 1988)](https://doi.org/10.1007/BF00247909)
## Installation
To install using `pip`, run the following.
```shell
$ python3 -m pip install smcplaus
```
## Usage
### Specifying formulas
Specify propositional variables.
```python
p = PropositionalVariable(letter="p")
q0 = PropositionalVariable(letter="q", index=0)
q1 = PropositionalVariable(letter="q", index=1)
```
Specify complex formulas.
```python
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.
```python
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.
```python
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.
```python
my_pointed_model = PointedPlausibilityModel(
model=my_model,
point=state1,
)
```
### Checking (pointed) models against formulas
Check if a pointed model satisfies a formula.
```python
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.
```python
form_p_truthset = my_model.truthset(form_p) # {State(s2), State(s0)}
```
### Modifying models with formulas
Upgrade a model with a formula.
```python
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.
```python
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.
```python
output_json = my_other_model.to_json()
```
### Generating digraphs from structures
Generate the digraph of a structure.
```python
my_model_digraph = my_model.generate_digraph()
```
Dump the digraph of a structure to a file.
```python
my_model.dump_digraph(filepath=Path("my_model.dot"))
```
The file `my_model.dot` will then have the following contents.
```dot
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.
```shell
$ 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.
Raw data
{
"_id": null,
"home_page": "https://gitlab.com/dqalombardi/smcplaus",
"name": "smcplaus",
"maintainer": "David Alvarez Lombardi",
"docs_url": null,
"requires_python": ">=3.11,<4.0",
"maintainer_email": "dqalombardi@proton.me",
"keywords": "belief revision,dynamic epistemic logic,logic,plausibility,symbolic model checking",
"author": "David Alvarez Lombardi",
"author_email": "dqalombardi@proton.me",
"download_url": "https://files.pythonhosted.org/packages/24/47/e724156ebef866fda6f55faa4c6ee0dc76bf721343e14d7aa1c0dfdb244b/smcplaus-1.1.5.tar.gz",
"platform": null,
"description": "# smcplaus\n\nOwner : [David Alvarez Lombardi](https://linktr.ee/dqalombardi)\n\nRepository : [https://gitlab.com/dqalombardi/smcplaus](https://gitlab.com/dqalombardi/smcplaus)\n\nPyPI : [https://pypi.org/project/smcplaus/](https://pypi.org/project/smcplaus/)\n\n## Description\n\nA symbolic model checker for the single-agent plausibility models of [dynamic epistemic logic](https://plato.stanford.edu/entries/dynamic-epistemic/).\n\n## References\n\n- [SEP : *Plausibility models and belief change* (Baltag & Renne 2016)](https://plato.stanford.edu/entries/dynamic-epistemic/#PlauModeBeliChan)\n- [*A qualitative theory of dynamic interactive belief revision* (Baltag & Smets 2008)](https://doi.org/10.1007/978-3-319-20451-2_39)\n- [*Dynamic logic for belief revision* (van Benthem 2007)](https://doi.org/10.3166/jancl.17.129-155)\n- [*Dynamic interactive epistemology* (Board 2004)](https://doi.org/10.1016/j.geb.2003.10.006)\n- [*Two modellings for theory change* (Grove 1988)](https://doi.org/10.1007/BF00247909)\n\n## Installation\n\nTo install using `pip`, run the following.\n\n```shell\n$ python3 -m pip install smcplaus\n```\n\n## Usage\n\n### Specifying formulas\n\nSpecify propositional variables.\n```python\np = PropositionalVariable(letter=\"p\")\nq0 = PropositionalVariable(letter=\"q\", index=0)\nq1 = PropositionalVariable(letter=\"q\", index=1)\n```\n\nSpecify complex formulas.\n\n```python\nform_p = Formula(node=p, subformulas=None)\nform_q0 = Formula(node=q0, subformulas=None)\nform0 = Formula(node=Connectives.DIAMOND, subformulas=(form_q0,)) # <>q0\nform1 = Formula(node=Connectives.RADICAL_UPGRADE, subformulas=(form_q0, form0)) # [$q0]<>q0\n```\n\n### Specifying models\n\nSpecify plausibility frames by specifying a domain and a state-to-appearance map.\n\n```python\nstate0 = State(index=0)\nstate1 = State(index=1)\nstate2 = State(index=2)\n\nmy_frame = PlausibilityFrame(\n domain={state0, state1, state2},\n state_to_appearance={\n state0: {state1},\n state1: {state2},\n state2: {state2},\n },\n force_s4=True,\n)\n```\n\n\nSpecify plausibility models by specifying a frame and a state-to-facts map.\n\n```python\nmy_model = PlausibilityModel(\n frame=my_frame,\n state_to_facts={\n state0: {p, q0},\n state1: {q1},\n state2: {p, q1},\n },\n)\n```\n\n\nSpecify pointed plausibility models by specifying a model and a point.\n\n```python\nmy_pointed_model = PointedPlausibilityModel(\n model=my_model,\n point=state1,\n)\n```\n\n### Checking (pointed) models against formulas\n\nCheck if a pointed model satisfies a formula.\n\n```python\nmy_pointed_model_satisfies_form0 = my_pointed_model.satisfies(form0) # False\nmy_pointed_model_satisfies_form1 = my_pointed_model.satisfies(form1) # True\n```\n\nCheck where a model satisfies a formula.\n\n```python\nform_p_truthset = my_model.truthset(form_p) # {State(s2), State(s0)}\n```\n\n### Modifying models with formulas\n\nUpgrade a model with a formula.\n\n```python\nmy_new_model = my_model.radical_upgrade(form_q0)\n```\n\n### Loading and dumping structures with JSON files\n\nSpecify and load a structure from a JSON file.\n\n```python\nmy_other_model_json_str = \"\"\"\n{\n \"frame\": {\n \"domain\": [\"s0\", \"s1\", \"s2\"],\n \"state_to_appearance\": {\n \"s0\": [\"s1\"],\n \"s1\": [\"s2\"],\n \"s2\": [\"s2\"]\n }\n },\n \"state_to_facts\": {\n \"s0\": [\"p\", \"q0\"],\n \"s1\": [\"q1\"],\n \"s2\": [\"p\", \"q1\"]\n }\n}\n\"\"\"\n\nmy_other_model = PlausibilityModel.from_json(my_other_model_json_str, force_s4=True)\n```\n\nDump a structure to a JSON file.\n\n```python\noutput_json = my_other_model.to_json()\n```\n\n### Generating digraphs from structures\n\nGenerate the digraph of a structure.\n\n```python\nmy_model_digraph = my_model.generate_digraph()\n```\n\nDump the digraph of a structure to a file.\n\n```python\nmy_model.dump_digraph(filepath=Path(\"my_model.dot\"))\n```\n\nThe file `my_model.dot` will then have the following contents.\n\n```dot\ndigraph {\n\ts0 [label=\"s0 || p, q0\"]\n\ts1 [label=\"s1 || q1\"]\n\ts2 [label=\"s2 || p, q1\"]\n\ts0 -> s1\n\ts1 -> s2\n}\n```\n\nThis can be converted to an image via `dot` in the command-line.\n\n```shell\n$ dot my_model.dot -Tsvg -omy_model.svg\n```\n\nThe file `my_model.svg` will then have the following contents.\n\n\n\n### Examples\n\nSee `./examples/` for functional example usage.\n\n\n## Contributing\n\nBefore submitting a merge request, run the command `tox`, which will run formatters, linters, static type-checkers, and unit tests respectively.\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "A symbolic model checker for the single-agent plausibility models of dynamic epistemic logic",
"version": "1.1.5",
"project_urls": {
"Homepage": "https://gitlab.com/dqalombardi/smcplaus",
"Repository": "https://gitlab.com/dqalombardi/smcplaus"
},
"split_keywords": [
"belief revision",
"dynamic epistemic logic",
"logic",
"plausibility",
"symbolic model checking"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "2c14b8fc7b9b97b4770be521878b21df7bd0255b17c87344069cda6c7f13e137",
"md5": "0d85ed74dfa20ce237da7b601a98a7c1",
"sha256": "ed9da10f21d87c56f5c4cff5ef9a1443e227907222d6a9cf1517508ea6288ef7"
},
"downloads": -1,
"filename": "smcplaus-1.1.5-py3-none-any.whl",
"has_sig": false,
"md5_digest": "0d85ed74dfa20ce237da7b601a98a7c1",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.11,<4.0",
"size": 16305,
"upload_time": "2024-01-08T15:26:53",
"upload_time_iso_8601": "2024-01-08T15:26:53.606501Z",
"url": "https://files.pythonhosted.org/packages/2c/14/b8fc7b9b97b4770be521878b21df7bd0255b17c87344069cda6c7f13e137/smcplaus-1.1.5-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "2447e724156ebef866fda6f55faa4c6ee0dc76bf721343e14d7aa1c0dfdb244b",
"md5": "05662447a6d1208e1628544307019160",
"sha256": "4cb1313f5182b51a08b23fe6d935e998b2e0b56096f4ac8fba2a1d245b7cdab0"
},
"downloads": -1,
"filename": "smcplaus-1.1.5.tar.gz",
"has_sig": false,
"md5_digest": "05662447a6d1208e1628544307019160",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.11,<4.0",
"size": 13264,
"upload_time": "2024-01-08T15:26:59",
"upload_time_iso_8601": "2024-01-08T15:26:59.730915Z",
"url": "https://files.pythonhosted.org/packages/24/47/e724156ebef866fda6f55faa4c6ee0dc76bf721343e14d7aa1c0dfdb244b/smcplaus-1.1.5.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-01-08 15:26:59",
"github": false,
"gitlab": true,
"bitbucket": false,
"codeberg": false,
"gitlab_user": "dqalombardi",
"gitlab_project": "smcplaus",
"lcname": "smcplaus"
}
JSON