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.

*a*U*b*- ⋄
*a*(compare to the previous automaton) - □
*a*(compare to the previous automaton) - ⋄□
*a* - □⋄
*a* - □(
*a*⟹ ⋄*b*)

In order to simplify our model-checker, transition systems will be defined directly in `python`

using Spot libraries. Labelled transition systems are often called Kripke structures. Here is an example of the definition of a Kirpke structure using Spot libraries, where `bdddict`

is a dictionnary implemented using Binary Decision Diagrams (BDDs) that maps atomic propositions (i.e. strings) to identifiers.

```
def create_kripke_dvm(bdddict):
= spot.make_kripke_graph(bdddict)
k = bdd_ithvar(k.register_ap("pay"))
pay = bdd_ithvar(k.register_ap("drink"))
drink = k.new_state(pay & -drink)
s_idle = k.new_state(-pay & -drink)
s_select = k.new_state(-pay & drink)
s_coke = k.new_state(-pay & drink)
s_sprite
k.set_init_state(s_idle)
k.new_edge(s_idle, s_select)
k.new_edge(s_select, s_coke)
k.new_edge(s_select, s_sprite)
k.new_edge(s_coke, s_idle)
k.new_edge(s_sprite, s_idle)'idle','select','coke','sprite'])
k.set_state_names([return k
```

Download the file model-checker.py, and run the command `./model-checker.py --output drink-vendor-machine true`

. Then, run the command `dot -Tpdf -o drink-vendor-machine-kripke.pdf drink-vendor-machine-kripke.dot`

to get a graphical representation of the Kripke structure defined above in the PDF file `drink-vendor-machine-kripke.pdf`

.

- Open the file
`drink-vendor-machine-kripke.pdf`

and explain the instructions in the`create_kripke_dvm`

function above.

We implement the following model-checking function:

```
def model_check(model, formula):
""" model-check model w.r.t. LTL formula """
= spot.make_bdd_dict()
d # Create the Kripke structure
= create_kripke_structure(model, d)
k # 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 (k, a_neg_formula, product, run)
```

- What is returned by this function?
- Run the
`model-checker.py`

script for model`drink-vendor-machine`

and specification`[](pay -> X(!pay U drink))`

with option`--output`

. Produce PDF files from the`.dot`

files output by the script. Explain what you observe in the three files. - Proceed similarly with specification
`[](pay -> !pay U drink)`

- Does the combination of requirements
`[](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? - Check that the drink vendor machine is correct: one cannot get a drink without paying, and one is guaranteed a drink after having paid.
- Refine the model to deliver drinks only after 2 euros have been paid. Coins of 0.5 euros, 1 euro and 2 euros can be used. The drink vendor machine does not make change. Check that your new model satisfies the requirements above.

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
}
```

- Implement a
`python`

function`create_kripke_shared`

similar to function`create_kripke_dvm`

that defines the Kripke structure corresponding to the model above. Update the function`create_kripke`

to call function`create_kripke_shared`

when model`shared`

is selected. Add an atomic proposition to observe whether`x=2`

. - Using the script
`model-checker.py`

, check if`x`

is equal to`2`

when the system terminates.