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 a U b, 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 the program below that consists in a shared variable
x
and N
threads that run the function
increment
. This function first stores the value of
x
in a local variable y
. Then, it writes
y+1
into x
. We assume that each assignment is
an atomic instruction.
int x = 0;
void increment()
{
int y = x;
= y + 1;
x }
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.x
has value 2
when the system terminates. Using the script
model-checker.py
, check if your formula holds on your
model. What can you conclude?