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*)

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

- What is returned by this function?
- 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. - 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
}
```

- 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. - Using the script
`model-checker.py`

, check if`x`

is equal to`2`

when the system terminates. What can you conclude?