In this assignment you will implement a symbolic algorithm for the verification of a special class of LTL formulas, using BDDs as data structure to represent and manipulate regions. The class of formulas considered by the algorithm is called "reactivity" properties and have the special form:
-
If the west train is repeatedly waiting, then it will be repeatedly on the bridge:
$\square\diamond train_w.mode = wait \rightarrow \square\diamond train_w.mode = bridge$ -
If the west train is repeatedly waiting, then it will be repeatedly on the bridge:
$\square\diamond train_w.mode = wait \rightarrow \square\diamond (signal_w = green\ \vee\ train_e.mode = bridge)$ -
If the west train is repeatedly waiting with the east train off the bridge, then the west train will be repeatedly on the bridge:
$\square\diamond(\neg(train_e.mode = bridge)\ \wedge\ train_w.mode = wait ) \rightarrow \square\diamond train_w.mode = bridge$
-
$\square(train_w.mode = wait \rightarrow \diamond signal_w = green)$ -
$\square\diamond \neg (train_e.mode = bridge ) \rightarrow \square\diamond train_w.mode = wait \rightarrow \square\diamond train_w.mode = bridge$ -
$\square\diamond train_w.mode = wait \rightarrow \square\diamond (signal_w = green\ \wedge\ \bigcirc train_w.mode = bridge )$
The attached react_mc.smv
file contains a python script that uses the pynusmv
library to verify reactivity properties of SMV programs. The script uses the function parse_react(spec)
to check if spec
is a reactivity formula, and skips all formulas that are not in the correct form.
Using the react_mc.smv
script as a starting point, (re)implement the function check_react_spec(spec)
, respecting the following specifications:
-
the function checks if the reactivity formula
spec
is satisfied by the loaded SMV model or not, that is, whether all the executions of the model satisfyspec
or not. -
the return value of
check_react_spec(spec)
is a tuple where the first element isTrue
and the second element isNone
if the formula is true. When the formula is not verified, the first element isFalse
and the second element is an execution of the SMV model that violatesspec
. The function returnsNone
ifspec
is not a reactivity formula; -
the execution is a tuple of alternating states and inputs, starting and ending with a state. States and inputs are represented by dictionaries where keys are state and inputs variable of the loaded SMV model, and values are their value;
-
the execution is looping: the last state should be somewhere else in the sequence to indicate the starting point of the loop.