We will use the tool Spot to write an LTL model-checker in Python. The LTL modalities are denoted: []
“Always”, <>
“Eventually”, X
“Next” and U
“Until”. Boolean operators are written: !
“Not”, &
“And”, |
“Or” and ->
“Implies”. Atomic propositions are strings, like "a"
, "b"
, etc. The true formula is denoted true
, and false
denotes the false formula.
For each of LTL formula Φ below, compute a Büchi automaton using Spot tool ltl2tgba
, and associate to each state the maximal coherent subset of the subformulas of Φ that are true in any accepting run from that state.
NB: use the command ltl2tgba -Bd -f 'a U b' | dot -Tpdf -o aUb.pdf
to compute a Büchi automaton for the formula aUb, and obtain a graphical representation of the automaton in the PDF file aUb.pdf
. Add option -C
to ltl2tgba
to obtain a complete automaton.
Our simple model-checker reads transitions systems specified using the graphviz/dot file format. Here follows a description of the drink vendor machine (depicted below):
digraph dvm {
idle [initial="true", labels="pay"];
coke [labels="drink"];
sprite [labels="drink"];
idle -> select;
select -> coke;
select -> sprite;
coke -> idle;
sprite -> idle;
}
The file specifies a graph named dvm
with four nodes: idle
, select
, coke
and sprite
, and five edges. The node select
is implicitly defined. The other nodes are explicitly defined. Our model-checker accepts two optional attributes on nodes:
initial
(which can have any non-empty string value) defines the initial node of the transition system. There must be exactly one initial node in the transition system.labels
(non-empty comma-separated list of string) defines the set of atomic propositions that label the node. As an example, the declaration n [labels="a,b,c"];
defines a node n
with labels a
, b
and c
(i.e. labels set {a,b,c}
).In the specification above, the node idle
is initial and labeled {pay}
. The nodes coke
and sprite
are labeled {drink}
. The node select
is not labeled (i.e. it has empty label set {}
).
Download the file model-checker.py
from the GitHub repository (or directly clone the repository). Copy and paste the dvm
graph above in a file dvm.dot
. Then, run the command ./model-checker.py --output dvm dvm.dot true
, and finally, the command dot -Tpdf -o dvm-kripke.pdf dvm-kripke.dot
. Nota bene: run ./model-checker.py -h
for how to run the model-checker.
Check that the transition system in the file dvm-kripke.pdf
corresponds to the drink vendor machine depicted below.
We implement the following model-checking function:
def model_check(k, formula, d):
""" model-check LTL formula on transition system k using dictionary d for atomic
propositions """
# Create the automaton for the negation of the formula
= "!(" + formula + ")"
neg_formula = build_automaton(neg_formula, d)
a_neg_formula # Compute the product
= spot.twa_product(k, a_neg_formula)
product # Check emptiness of the product
= product.accepting_run()
run return (a_neg_formula, product, run)
model-checker.py
script for model dvm.dot
and specification [](pay -> X(!pay U drink))
with option --output dvm
. Produce PDF files from the .dot
files output by the script. Explain what you observe in the three files.[](pay -> !pay U drink)
[](pay -> X(!pay U drink))
and [](drink -> X(!drink U pay))
ensures that one cannot get a drink without paying and one is guaranteed a drink after having paid?Consider a concurrent algorithm with one shared integer-valued variable x
, and two processes:
variable
x = 0;
process (P = 1)
variable
y = 0;
{
p0: y := x;
p1: x := y + 1
}
process (Q = 2)
variable
y = 0;
{
q0: y := x;
q1: x := y + 1
}
concurrent_inc.dot
. Add atomic propositions all_done
and x_eq_2
that label states where all processes have terminated, and where x
is equal to 2
, respectively. Nota bene: the transition system should describe the state-space and transitions of the entire algorithm, taking into account the two processes and the three variables.model-checker.py
, check if x
is equal to 2
when the system terminates. What can you conclude?