# pyModelChecking
*pyModelChecking* is a small Python model checking package. Currently, it is
able to represent [Kripke structures][Kripke], [CTL][CTL], [LTL][LTL], and
[CTL*][CTLS] formulas and it provides [model checking][modelchecking] methods
for LTL, CTL, and CTL*. In future, it will hopefully support symbolic model
checking.
[Kripke]: https://en.wikipedia.org/wiki/Kripke_structure_%28model_checking%29
[CTL]: https://en.wikipedia.org/wiki/Computation_tree_logic
[modelchecking]: https://en.wikipedia.org/wiki/Model_checking
[LTL]: https://en.wikipedia.org/wiki/Linear_temporal_logic
[CTLS]: https://en.wikipedia.org/wiki/CTL*
### Documentation
[Here][last_doc] you can find the *pyModelChecking* documenation. It contains:
* a brief introduction to Kripke structures, temporal logics and model checking
* the user manual and some examples
* the API manual
[last_doc]: https://pymodelchecking.readthedocs.io/
### Examples
First of all, import all the functions and all the classes in the package.
```python
>>> from pyModelChecking import *
```
In order to represent a Kripke structure use the `Kripke` class.
```
>>> K=Kripke(R=[(0,0),(0,1),(1,2),(2,2),(3,3)],
... L={0: set(['p']), 1:set(['p','q']),3:set(['p'])})
```
CTL can be represented by importing the `CTL` module.
```python
>>> from pyModelChecking.CTL import *
>>> phi=AU(True,Or('q',Not(EX('p'))))
>>> print(phi)
A(True U (q or not (EX p)))
```
Whenever a non-CTL formula is built, an exception is thrown.
```python
>>> psi=A(F(G('p')))
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "pyModelChecking/CTL/language.py", line 42, in __init__
self.wrap_subformulas(phi,StateFormula)
File "pyModelChecking/CTLS/language.py", line 59, in wrap_subformulas
phi.__desc__,phi))
TypeError: expected a CTL state formula, got the CTL path formula G p
```
It is also possible to parse a string representing a CTL formula by using
the `Parser` class in the module `CTL`.
```python
>>> parser = Parser()
>>> psi = parser("A(true U (q or not E X p))")
>>> print(psi)
A(True U (q or not EX p))
>>> print(psi.__class__)
<class 'pyModelChecking.CTL.language.A'>
```
The function `modelcheck` in the module `CTL` finds the states of Kripke
structure that model a given CTL formula.
```python
>>> modelcheck(K,phi)
set([1, 2])
```
The formula `AFG p`, which we tried to build above, is a LTL formula. The
`LTL` module can be used to represent and model check it on any Kripke
structure.
```python
>>> from pyModelChecking.LTL import *
>>> psi=A(F(G('p')))
>>> print(psi)
A(G(F(p))
>>> modelcheck(K,psi)
set([3])
```
Strings representing formulas in the opportune language can be used as a
parameter of the model checking function too.
```python
>>> modelcheck(K,'A G F p')
set([3])
```
The module `CTLS` is meant to deal with CTL* formulas. It can also combine and
model checks CTL and LTL formulas.
```python
>>> from pyModelChecking.CTLS import *
>>> eta=A(F(E(U(True,Imply('p',Not('q'))))))
>>> print(eta,eta.__class__)
(A(F(E((True U (p --> not q))))), <class 'pyModelChecking.CTLS.language.A'>)
>>> rho=A(G(And(X('p'),'p')))
>>> print(rho,rho.__class__)
(A(G((X(p) and p))), <class 'pyModelChecking.CTLS.language.A'>)
>>> gamma=And(phi, psi)
>>> print(gamma,gamma.__class__)
(A(True U (q or not (EX p))) and A(G(F(p)))), <class 'pyModelChecking.CTLS.language.And'>)
>>> modelcheck(K,eta)
set([0, 1, 2, 3])
>>> modelcheck(K, psi)
set([3])
>>> modelcheck(K, gamma)
set([])
```
Whenever a CTL* formula is a CTL formula (LTL formula), CTL (LTL) model
checking can be applied to it.
```python
>>> import pyModelChecking.CTL as CTL
>>> CTL.modelcheck(K,eta)
set([0, 1, 2, 3])
>>> CTL.modelcheck(K,rho)
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "pyModelChecking/CTL/model_checking.py", line 183, in modelcheck
raise RuntimeError('%s is not a CTL formula' % (formula))
RuntimeError: A(G((X(p) and p))) is not a CTL formula
>>> import pyModelChecking.LTL as LTL
>>> LTL.modelcheck(K,rho)
set([3])
```
### Copyright and license
pyModelChecking
Copyright (C) 2015-2020 Alberto Casagrande <acasagrande@units.it>
pyModelChecking is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
Raw data
{
"_id": null,
"home_page": "https://github.com/albertocasagrande/pyModelChecking",
"name": "pyModelChecking",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.6",
"maintainer_email": null,
"keywords": "model checking temporal logics kripke structure",
"author": "Alberto Casagrande",
"author_email": "acasagrande@units.it",
"download_url": "https://files.pythonhosted.org/packages/af/db/20e709d417b971d45dbc32cf88f90ec134ba83f6ab795ccbb9f907912976/pymodelchecking-1.3.4.tar.gz",
"platform": null,
"description": "# pyModelChecking\n*pyModelChecking* is a small Python model checking package. Currently, it is \nable to represent [Kripke structures][Kripke], [CTL][CTL], [LTL][LTL], and \n[CTL*][CTLS] formulas and it provides [model checking][modelchecking] methods \nfor LTL, CTL, and CTL*. In future, it will hopefully support symbolic model \nchecking.\n\n[Kripke]: https://en.wikipedia.org/wiki/Kripke_structure_%28model_checking%29\n[CTL]: https://en.wikipedia.org/wiki/Computation_tree_logic\n[modelchecking]: https://en.wikipedia.org/wiki/Model_checking\n[LTL]: https://en.wikipedia.org/wiki/Linear_temporal_logic\n[CTLS]: https://en.wikipedia.org/wiki/CTL*\n\n### Documentation\n\n[Here][last_doc] you can find the *pyModelChecking* documenation. It contains:\n* a brief introduction to Kripke structures, temporal logics and model checking\n* the user manual and some examples\n* the API manual \n\n[last_doc]: https://pymodelchecking.readthedocs.io/\n\n### Examples\n\nFirst of all, import all the functions and all the classes in the package.\n\n```python\n>>> from pyModelChecking import *\n```\n\nIn order to represent a Kripke structure use the `Kripke` class.\n\n```\n>>> K=Kripke(R=[(0,0),(0,1),(1,2),(2,2),(3,3)],\n... L={0: set(['p']), 1:set(['p','q']),3:set(['p'])})\n```\n\nCTL can be represented by importing the `CTL` module.\n\n```python\n>>> from pyModelChecking.CTL import *\n\n>>> phi=AU(True,Or('q',Not(EX('p'))))\n\n>>> print(phi)\n\nA(True U (q or not (EX p)))\n```\n\nWhenever a non-CTL formula is built, an exception is thrown.\n\n```python\n>>> psi=A(F(G('p')))\nTraceback (most recent call last):\n File \"<stdin>\", line 1, in <module>\n File \"pyModelChecking/CTL/language.py\", line 42, in __init__\n self.wrap_subformulas(phi,StateFormula)\n File \"pyModelChecking/CTLS/language.py\", line 59, in wrap_subformulas\n phi.__desc__,phi))\nTypeError: expected a CTL state formula, got the CTL path formula G p\n```\n\nIt is also possible to parse a string representing a CTL formula by using \nthe `Parser` class in the module `CTL`.\n\n```python\n>>> parser = Parser()\n\n>>> psi = parser(\"A(true U (q or not E X p))\")\n\n>>> print(psi)\n\nA(True U (q or not EX p))\n\n>>> print(psi.__class__)\n\n<class 'pyModelChecking.CTL.language.A'>\n```\n\nThe function `modelcheck` in the module `CTL` finds the states of Kripke \nstructure that model a given CTL formula.\n\n```python\n>>> modelcheck(K,phi)\n\nset([1, 2])\n```\n\nThe formula `AFG p`, which we tried to build above, is a LTL formula. The \n`LTL` module can be used to represent and model check it on any Kripke \nstructure.\n\n```python\n>>> from pyModelChecking.LTL import *\n\n>>> psi=A(F(G('p')))\n\n>>> print(psi)\n\nA(G(F(p))\n\n>>> modelcheck(K,psi)\n\nset([3])\n```\n\nStrings representing formulas in the opportune language can be used as a \nparameter of the model checking function too.\n\n```python\n>>> modelcheck(K,'A G F p')\n\nset([3])\n```\n\nThe module `CTLS` is meant to deal with CTL* formulas. It can also combine and \nmodel checks CTL and LTL formulas.\n\n```python\n>>> from pyModelChecking.CTLS import *\n\n>>> eta=A(F(E(U(True,Imply('p',Not('q'))))))\n\n>>> print(eta,eta.__class__)\n\n(A(F(E((True U (p --> not q))))), <class 'pyModelChecking.CTLS.language.A'>)\n\n>>> rho=A(G(And(X('p'),'p')))\n\n>>> print(rho,rho.__class__)\n\n(A(G((X(p) and p))), <class 'pyModelChecking.CTLS.language.A'>)\n\n>>> gamma=And(phi, psi)\n\n>>> print(gamma,gamma.__class__)\n\n(A(True U (q or not (EX p))) and A(G(F(p)))), <class 'pyModelChecking.CTLS.language.And'>)\n\n>>> modelcheck(K,eta)\n\nset([0, 1, 2, 3])\n\n>>> modelcheck(K, psi)\n\nset([3])\n\n>>> modelcheck(K, gamma)\n\nset([])\n\n```\n\nWhenever a CTL* formula is a CTL formula (LTL formula), CTL (LTL) model \nchecking can be applied to it.\n\n```python\n>>> import pyModelChecking.CTL as CTL\n\n>>> CTL.modelcheck(K,eta)\n\nset([0, 1, 2, 3])\n\n>>> CTL.modelcheck(K,rho)\nTraceback (most recent call last):\n File \"<stdin>\", line 1, in <module>\n File \"pyModelChecking/CTL/model_checking.py\", line 183, in modelcheck\n raise RuntimeError('%s is not a CTL formula' % (formula))\nRuntimeError: A(G((X(p) and p))) is not a CTL formula\n\n>>> import pyModelChecking.LTL as LTL\n\n>>> LTL.modelcheck(K,rho)\n\nset([3])\n```\n\n### Copyright and license\n\npyModelChecking\nCopyright (C) 2015-2020 Alberto Casagrande <acasagrande@units.it>\n\npyModelChecking is free software; you can redistribute it and/or\nmodify it under the terms of the GNU General Public License\nas published by the Free Software Foundation; either version 2\nof the License, or (at your option) any later version.\n\nThis program is distributed in the hope that it will be useful,\nbut WITHOUT ANY WARRANTY; without even the implied warranty of\nMERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the\nGNU General Public License for more details.\n\nYou should have received a copy of the GNU General Public License\nalong with this program; if not, write to the Free Software\nFoundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.\n",
"bugtrack_url": null,
"license": "GNU General Public License, version 2",
"summary": "A simple Python model checking package",
"version": "1.3.4",
"project_urls": {
"Documentation": "https://readthedocs.org/projects/pymodelchecking/",
"Homepage": "https://github.com/albertocasagrande/pyModelChecking",
"Source Code": "https://github.com/albertocasagrande/pyModelChecking"
},
"split_keywords": [
"model",
"checking",
"temporal",
"logics",
"kripke",
"structure"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "56fbda6f93a39e56663455b45b45ba804a9da07a4744c51664b463863156caf8",
"md5": "8d7faaedc2a75c67d57929e5c9ed5fc7",
"sha256": "2900dac96643f8e042b74ca0ec81de0b325d695a59b00436bedc560d6295eac2"
},
"downloads": -1,
"filename": "pyModelChecking-1.3.4-py3-none-any.whl",
"has_sig": false,
"md5_digest": "8d7faaedc2a75c67d57929e5c9ed5fc7",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.6",
"size": 47454,
"upload_time": "2024-09-02T12:07:56",
"upload_time_iso_8601": "2024-09-02T12:07:56.103593Z",
"url": "https://files.pythonhosted.org/packages/56/fb/da6f93a39e56663455b45b45ba804a9da07a4744c51664b463863156caf8/pyModelChecking-1.3.4-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "afdb20e709d417b971d45dbc32cf88f90ec134ba83f6ab795ccbb9f907912976",
"md5": "c7816634e9dde2ec1e01e7bcb835178a",
"sha256": "558afb5d0469cc800b9fc2329157ec6c3c0ee7c67138eb8cb864418a6b4ce842"
},
"downloads": -1,
"filename": "pymodelchecking-1.3.4.tar.gz",
"has_sig": false,
"md5_digest": "c7816634e9dde2ec1e01e7bcb835178a",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.6",
"size": 33519,
"upload_time": "2024-09-02T12:07:57",
"upload_time_iso_8601": "2024-09-02T12:07:57.714257Z",
"url": "https://files.pythonhosted.org/packages/af/db/20e709d417b971d45dbc32cf88f90ec134ba83f6ab795ccbb9f907912976/pymodelchecking-1.3.4.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-09-02 12:07:57",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "albertocasagrande",
"github_project": "pyModelChecking",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"circle": true,
"requirements": [
{
"name": "lark-parser",
"specs": []
}
],
"lcname": "pymodelchecking"
}
JSON
