A simple Python model checking package
Project description
pyModelChecking
pyModelChecking is a small Python model checking package. Currently, it is able to represent Kripke structures, CTL, LTL, and CTL* formulas and it provides model checking methods for LTL, CTL, and CTL*. In future, it will hopefully support symbolic model checking.
Documentation
Here 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
Examples
First of all, import all the functions and all the classes in the package.
>>> 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.
>>> 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.
>>> 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
.
>>> 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.
>>> 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.
>>> 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.
>>> 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.
>>> 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.
>>> 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-2019 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.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for pyModelChecking-1.3.2-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 454b06cb844687f3c66124b461f99f7453e8d046dc359fe098aa3c0bd4f0bb0c |
|
MD5 | 081f4d614f80846bf0e0e3595c3f1007 |
|
BLAKE2b-256 | 7da94a65231a03bf1f723bfc89234b545e9bdad05a6ba394f8be763624035ff0 |