Exercice 1

Chiffres dans les ronds = numéros de lignes de l’algorithme de Dekker
Étiquette : Condition/action

Mutex LTL : G(\neg (\text{l9} \wedge \text{l'9})) ou \neg F(\text{l9} \wedge \text{l'9}) ou G(\neg\text{l9} \vee \neg\text{l'9})

euh

Prouvons que 99 n’est pas atteignable
Supposons que P1 y entre le premier en section critique
On a donc w1 = 1 depuis 4 et P2 n’y changes pas la valeur.
Donc P2 ne franchira jamais sa transition 9 \xleftarrow{w1=0} 4 et n’entrera pas en 9 en même temps que P1.

Exercice 2

triangle_a_queue

Spec

Rappel :
FG : À partir d’un moment, il va pleuvoir pour toujours
GF : Il pleut infiniment souvent

\varphi = FG(c=15)

Calcul qui ne satisfait pas `c = 15`

P1 fait 10 boucles, va en 5 et boucle.
P2 ne bouge pas : rien oblige P2 de changer d’état, ce n’est pas préciser.

A la fin, c = 10 et ne bouge plus

Une spec vraie

\varphi = G(\text{l5} \wedge \text{l5'} \RA C = 15)

Cette spec peut être violée si on prend en compte l’atomicité de la ligne 4.

Atomicité

atomic_ex2
\Psi n’est pas satisfait (si on perd une écriture)

Exercice 3

Question 1

\begin{aligned} \varphi_{1} &= \neg (\text{POn} \wedge \text{POff}) \\\\ \varphi_{1'} &= (\text{POn} \Leftrightarrow \text{VOn}) \end{aligned}

Question 2

Rappel : X = demain
\varphi_{2} = G((\text{Poff} \wedge \text{Boff} \RA X\text{Pon}) \wedge (\text{Pon} \wedge \text{Boff} \RA X\text{Poff})) \\\\

Question 3

\begin{aligned} \varphi_{3} &= G(\text{Pon} \RA ((\text{at} \wedge \neg \text{ma} \wedge \neg \text{fin}) \vee (\neg \text{at} \wedge \text{ma} \wedge \neg \text{fin}) \vee (\neg \text{at} \wedge \neg\text{ma} \wedge \text{fin}))) \\\\ \varphi_{3} &= G(\text{Poff} \wedge X\text{Pon} \RA X\text{att}) \end{aligned}

Question 4

G(\text{Bstart/reset} \wedge \text{att} \RA X\text{marche})

Question 5

G(\text{Bstart/reset}\wedge X\text{Bstart/reset}\wedge XX\text{Bstart/reset} \RA XXX\text{att})
Là, on raisonne sur quatre instants de temps. \wedge permet de séparer les ticks de temps.

Question 6

((V \RA X \neg V) \wedge(\neg V \RA XV))\ U \text{ Poff}

Question 7

G(\text{fin} \RA \varphi(V\neg)\wedge \varphi(\text{Vlavage})\wedge \varphi(\text{Vsechage}))