# Model-checking LTL specifications

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.

## Translating LTL formulas into Büchi automata

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.

1. aUb
2. a (compare to the previous automaton)
3. a (compare to the previous automaton)
4. ⋄□a
5. □⋄a
6. □(a ⟹ ⋄b)

## Defining a transition system

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):
k = spot.make_kripke_graph(bdddict)
pay = bdd_ithvar(k.register_ap("pay"))
drink = bdd_ithvar(k.register_ap("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.new_state(-pay & drink)
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)
k.set_state_names(['idle','select','coke','sprite'])
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`.

1. Open the file `drink-vendor-machine-kripke.pdf` and explain the instructions in the `create_kripke_dvm` function above.

## Model-checking LTL specifications over Kripke structures

We implement the following model-checking function:

``````def model_check(model, formula):
""" model-check model w.r.t. LTL formula """
d = spot.make_bdd_dict()
# Create the Kripke structure
k = create_kripke_structure(model, d)
# Create the automaton for the negation of the formula
neg_formula = "!(" + formula + ")"
a_neg_formula = build_automaton(neg_formula, d)
# Compute the product
product = spot.twa_product(k, a_neg_formula)
# Check emptiness of the product
run = product.accepting_run()
return (k, a_neg_formula, product, run)``````
1. What is returned by this function?
2. 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.
3. Proceed similarly with specification `[](pay -> !pay U drink)`

## Model-checking the drink vendor machine

1. 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?
2. Check that the drink vendor machine is correct: one cannot get a drink without paying, and one is guaranteed a drink after having paid.
3. 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.

## Model-checking a concurrent algorithm

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
}``````
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`.
2. Using the script `model-checker.py`, check if `x` is equal to `2` when the system terminates.