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-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.