Skip to main content

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

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

pymodelchecking-1.3.4.tar.gz (33.5 kB view details)

Uploaded Source

Built Distribution

pyModelChecking-1.3.4-py3-none-any.whl (47.5 kB view details)

Uploaded Python 3

File details

Details for the file pymodelchecking-1.3.4.tar.gz.

File metadata

  • Download URL: pymodelchecking-1.3.4.tar.gz
  • Upload date:
  • Size: 33.5 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/5.1.1 CPython/3.12.5

File hashes

Hashes for pymodelchecking-1.3.4.tar.gz
Algorithm Hash digest
SHA256 558afb5d0469cc800b9fc2329157ec6c3c0ee7c67138eb8cb864418a6b4ce842
MD5 c7816634e9dde2ec1e01e7bcb835178a
BLAKE2b-256 afdb20e709d417b971d45dbc32cf88f90ec134ba83f6ab795ccbb9f907912976

See more details on using hashes here.

File details

Details for the file pyModelChecking-1.3.4-py3-none-any.whl.

File metadata

File hashes

Hashes for pyModelChecking-1.3.4-py3-none-any.whl
Algorithm Hash digest
SHA256 2900dac96643f8e042b74ca0ec81de0b325d695a59b00436bedc560d6295eac2
MD5 8d7faaedc2a75c67d57929e5c9ed5fc7
BLAKE2b-256 56fbda6f93a39e56663455b45b45ba804a9da07a4744c51664b463863156caf8

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page