Encoding Formulas and Model Checking¶
pyModelChecking provides a user friendly support for building CTL*, CTL and LTL formulas. Each of these languages corresponds to a pyModelChecking’s sub-module which implements all the classes required to encode the corresponding formulas.
Propositional logic is also supported by pyModelChecking as a shared basis for all the possible temporal logics.
Propositional Logics¶
Propositional logics support is provided by including the
pyModelChecking.language sub-module. This sub-module allows to
represents atomic propositions and Boolean values through the
pyModelChecking.formula.AtomicProposition
and
pyModelChecking.formula.Bool
classes, respectively.
>>> from pyModelChecking.formula import *
>>> AtomicProposition('p')
p
>>> Bool(True)
True
Moreover, the pyModelChecking.language sub-module
implements the logic operators \(\land\), \(\lor\), \(\rightarrow\)
and \(\neg\) by mean of the classes
pyModelChecking.formula.And
, pyModelChecking.formula.Or
,
pyModelChecking.formula.Imply
and
pyModelChecking.formula.Not
, respectively. These classes
automatically wrap strings and Boolean values as objects of the classes
pyModelChecking.formula.AtomicProposition
and
pyModelChecking.formula.Bool
, respectively.
>>> And('p', True)
(p and True)
>>> And('p', True, 'p')
(p and True and p)
>>> f = Imply('q','p')
>>> And('p', f, Imply(Not(f), Or('q','s', f)))
(p and (q --> p) and (not (q --> p) --> (q or s or (q --> p))))
>> Imply('p', 'q', 'p')
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
TypeError: __init__() takes exactly 3 arguments (4 given)
For user convenience, the function pyModelChecking.formula.LNot()
is also provided. This function returns a formula equivalent to logic
negation of the parameter and minimise the number of outermost \(\neg\).
>>> f = Not(Not(Not(And('p',Not('q')))))
>>> f
not not not (p and not q)
>>> LNot(f)
(p and not q)
>>> LNot(Not(f))
not (p and not q)
>>> LNot(LNot(f))
not (p and not q)
Temporal Logics Implementation¶
CTL* formulas can be defined by using the
pyModelChecking.CTLS
sub-module.
>>> from pyModelChecking.CTLS import *
Path quantifiers \(A\) and \(E\) as well as temporal operators
\(X\), \(F\), \(G\), \(U\) and \(R\) are provided as
classes (see ref:CTLS sub-module<ctls_api> for more details).
As in the case of propositional logics, these classes wrap strings and
Boolean values as objects of the classes
pyModelChecking.CTLS.language.AtomicProposition
and
pyModelChecking.CTLS.language.Bool
, respectively.
>>> phi = A(G(
... Imply(And(Not('Close'),
... 'Start'),
... A(Or(G(Not('Heat')),
... F(Not('Error')))))
... ))
>>> phi
A(G(((not Close and Start) --> A((G(not Heat) or F(not Error))))))
In order to simplify the use of the library, a parsing class
pyModelChecking.CTLS.Parser
: has been implemented. Its objects
read a formula from a string and, when it is possible, translate it into a
corresponding pyModelChecking.CTLS.Formula
objects.
>>> parser = Parser()
>>> psi_str = 'A G ((not Close and Start) --> ' +
... 'A(G(not Heat) or F(not Error)))'
>>> psi = parser(psi_str)
>>> psi
A(G(((not Close and Start) --> A((G(not Heat) or F(not Error))))))
The sub-module also implements the CTL* model checking and fair model checking algorithms described in [CGP00].
>>> from pyModelChecking import Kripke
>>> K = Kripke(R=[(0, 1), (0, 2), (1, 4), (4, 1), (4, 2), (2, 0),
... (3, 2), (3, 0), (3, 3), (6, 3), (2, 5), (5, 6)],
... L={0: set(), 1: set(['Start', 'Error']), 2: set(['Close']),
... 3: set(['Close', 'Heat']),
... 4: set(['Start', 'Close', 'Error']),
... 5: set(['Start', 'Close']),
... 6: set(['Start', 'Close', 'Heat'])})
>>> modelcheck(K, psi)
set([0, 1, 2, 3, 4, 5, 6])
>>> modelcheck(K, psi, F=[6])
set([])
It is also possible to model check a string representation of a CTL* formula by
either passing an object of the class pyModelChecking.CTLS.Parser
or leaving the remit of creating such an object to the function
pyModelChecking.CTLS.modelcheck()
.
>>> modelcheck(K, psi_str)
set([0, 1, 2, 3, 4, 5, 6])
>>> modelcheck(K, psi_str, parser=parser)
set([0, 1, 2, 3, 4, 5, 6])
Analogous functionality are provided for CTL and LTL
by the sub-modules pyModelChecking.CTL
and
pyModelChecking.LTL
, respectively.