Modelling Reactive Systems

Directed Graphs

Directed graphs can be represented in pyModelChecking by using the class DiGraph (see Graph API).

>>> from pyModelChecking import *
>>> G = DiGraph(V=['a',3],
...             E=[('a','a'), ('a','b')])
>>> print(G)

(V=['a', 3, 'b'], E=[('a', 'a'), ('a', 'b')])

>>> G.nodes()

['a', 3, 'b']

>>> G.edges()

[('a','a'), ('a','b')]

>>> G.add_edge('c','b')
>>> G.nodes()

['a', 'c', 3, 'b']

>>> G.edges()

[('a', 'a'), ('a', 'b'), ('c', 'b')]

The same class provides methods to compute reachable sets, reversed graphs and subgraphs of a given directed graph.

>>> print(G.get_reversed_graph())

(V=['a', 'c', 3, 'b'], E=[('a', 'a'), ('b', 'a'), ('b', 'c')])

>>> print(G.get_subgraph(['a','b',3]))

(V=['a', 3, 'b'], E=[('a', 'a'), ('a', 'b')])

>>> print(G.get_reachable_set_from(['a', 3]))

set(['a', 3, 'b'])

>>> print(G.get_reachable_set_from(['d']))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "pyModelChecking/graph.py", line 203, in get_reachable_set_from
    for d in self.next(s):
  File "pyModelChecking/graph.py", line 120, in next
    'of this DiGraph')
RuntimeError: src = 'd' is not a node of this DiGraph

pyModelChecking can also compute the strongly connected components of a directed graph.

>>> G.add_edge('b','a')
>>> print(list(compute_SCCs(G)))
[['a', 'b'], ['c'], [3]]

Refer to Graph API for more details.

Kripke Structures

Kripke structures are representable by using the class Kripke (see Kripke API).

>>> from pyModelChecking import *
>>> K = Kripke(S=[0, 1, 3],
...            R=[(0, 2), (2, 2), (0, 1), (1, 0), (3, 2)],
...            L={1: ['p', 'q'], 2: ['p', 'q'], 3: ['q']})
>>> print(K)

(S=[0, 1, 2, 3],S0=set([]),R=[(0, 1), (0, 2), (1, 0), (2, 2), (3, 2)],L={0: set([]), 1: set(['q', 'p']), 2: set(['q', 'p']), 3: set(['q'])})

The sets of Kripke’s states and transitions can be obtained by using the following syntax:

>>> K.states()

[0, 1, 2, 3]

>>> K.transitions()

[(0, 1), (0, 2), (1, 0), (2, 2), (3, 2)]

It is possible to get the successors of a given state with respect to the Kripke’s transitions:

>>> K.next(0)

set([1, 2])

Finally, the API provides a method for getting the labels of Kripke’s states.

>>> K.labels()

set(['q', 'p'])

>>> K.labels(3)

set(['q'])