# 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 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.

1. a U b
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

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 `{}`).

1. 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.

2. Check that the transition system in the file `dvm-kripke.pdf` corresponds to the drink vendor machine depicted below.

## Model-checking LTL specifications over Kripke structures

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
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 (a_neg_formula, product, run)``````
1. What is returned by this function?
2. Run the `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.
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. Refer back to the model of the drink vendor machine that takes into account the stock of available drinks. Check that your model satisfies the two requirements above. Express in LTL that the machine is refilled infinitely often (add new atomic propositions if needed). Check that your model satisfies this property.
4. Refine the abstract 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 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;
x = y + 1;
}``````
1. Write a transition system using the graphviz/dot format explained above in a file `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.
2. Write an LTL formula that is true on runs such that `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?