Audience
- Frédéric Boulanger
- Chantal Keller
- Safouan Taha
- Frédéric Tuong
- Yakoub Nemouchi
- Burkhart Wolff
- Zeye DU
- Hai Nguyen Van
Support pédagogique pour Isabelle
Frédéric B & Burkhart
Frédéric présente un petit langage de description d'automate énumérant des inputs, outputs et des rules. Une rule est une [garde] input -> output. Un exemple portant sur un contrôleur de vitesse est présenté:
cruise
inputs: on off cruise brake standby
outputs: on=false cruise=false
rules:
[] off -> on=false cruise=false
[!on] on -> on=true cruise=false
[on] cruise -> cruise=true
[cruise] brake -> cruise=false
[cruise] standby -> cruise=false
Une génération de code (automatisée via Acceleo) permet de générer un fichier Isabelle comprenant la fonction de transition qui traduit les rules:
theory Cruise
imports Machine
begin
datatype Cruise =
Cruise (on: bool) (cruise: bool)
definition CruiseInit :: Cruise
where
"CruiseInit ≡ Cruise False False"
abbreviation on :: nat where "on ≡ 0"
abbreviation off :: nat where "off ≡ Suc on"
abbreviation cruise :: nat where "cruise ≡ Suc off"
abbreviation brake :: nat where "brake ≡ Suc cruise"
abbreviation standby :: nat where "standby ≡ Suc brake"
instantiation Cruise :: machine
begin
fun behavior_Cruise :: "Cruise ⇒ nat ⇒ Cruise"
where
"behavior_Cruise (Cruise _ _) off = Cruise False False"
| "behavior_Cruise (Cruise False _) on = Cruise True False"
| "behavior_Cruise (Cruise True _) cruise = Cruise True True"
| "behavior_Cruise (Cruise isOn True) brake = Cruise isOn False"
| "behavior_Cruise (Cruise isOn True) standby = Cruise isOn False"
| "behavior_Cruise some_cruise _ = some_cruise"
instance ..
end (* instantiation *)
end
La théorie générée instancie la classe Machine (théorie ad-hoc développée par Frédéric) qui regroupe un certain nombre de fonctions et de prédicats, dont la notion d'état accessible par un chemin (liste d'inputs).
theory Machine
imports Main
begin
(*
* A machine behaves when receiving an input (encoded as a nat)
* and becomes a new machine.
*)
class machine =
fixes behavior :: "'a ⇒ nat ⇒ 'a" (infixl "→" 60)
begin
(* Machine m2 is a successor of m1 if m1 can become m2 when receiving an input. *)
definition successor :: "'a ⇒ 'a ⇒ nat set ⇒ bool"
where
"successor m1 m2 inp ≡ (∃i ∈ inp. m2 = m1 → i)"
(* Machine m2 is reachable from m1 by path p if the succession
of behaviors triggered by the inputs in p lead from m1 to m2.
*)
(* Definition as a function (for computation) *)
fun reach_by_path_f :: "'a ⇒ 'a ⇒ nat list ⇒ bool"
where
"reach_by_path_f m1 m2 [] = (m1 = m2)"
| "reach_by_path_f m1 m2 [inp] = (m2 = m1 → inp)"
| "reach_by_path_f m1 m2 (i1#i2#seq) = reach_by_path_f (m1 → i1) m2 (i2#seq)"
(* Definition as an inductive predicate (for proofs) *)
inductive reach_by_path :: "'a ⇒ 'a ⇒ nat list ⇒ bool"
where
"m1 = m2 ⟹ reach_by_path m1 m2 []"
| "m1 → inp = m2 ⟹ reach_by_path m1 m2 [inp]"
| "reach_by_path (m1 → inp) m2 (i#seq) ⟹ reach_by_path m1 m2 (inp#i#seq)"
(* Generate elimination rules for proof automation *)
inductive_cases empty_path[elim!]:"reach_by_path m1 m2 []"
inductive_cases step_path[elim!]:"reach_by_path m1 m2 [inp]"
inductive_cases long_path[elim]:"reach_by_path m1 m2 (inp#i#seq)"
(* Proof that the function and the inductive predicate are the same *)
lemma [code]:"reach_by_path m1 m2 seq = reach_by_path_f m1 m2 seq"
proof (induction seq arbitrary: m1 m2) print_cases
case Nil
show ?case using reach_by_path.intros(1) by auto
next
case (Cons i s)
show ?case
proof (cases s)
case Nil
have "reach_by_path m1 m2 (i#[]) = reach_by_path (m1 → i) m2 []"
using reach_by_path.simps and step_path by metis
moreover have "reach_by_path_f m1 m2 (i#[]) = reach_by_path_f (m1 → i) m2 []"
using reach_by_path_f.simps(2) by auto
ultimately show "reach_by_path m1 m2 (i # s) = reach_by_path_f m1 m2 (i # s)"
using Cons.IH and Nil by auto
next
case (Cons i' s')
have "reach_by_path m1 m2 (i#i'#s') = reach_by_path (m1 → i) m2 (i'#s')"
using reach_by_path.simps and long_path by metis
moreover have "reach_by_path_f m1 m2 (i#i'#s') = reach_by_path_f (m1 → i) m2 (i'#s')"
using reach_by_path_f.simps(3) by auto
ultimately show "reach_by_path m1 m2 (i # s) = reach_by_path_f m1 m2 (i # s)"
using Cons.IH and Cons and reach_by_path.intros(3) by auto
qed
qed
(* Machine m2 is reachable from m1 with a set of inputs
if there exists a sequence of inputs taken from the set
that leads from m1 to m2. *)
definition reachable :: "'a ⇒ 'a ⇒ nat set ⇒ bool"
where
"reachable m1 m2 inp ≡ (∃seq. (set seq) ⊆ inp ∧ reach_by_path m1 m2 seq)"
end (* class machine *)
end
En vu de simplifier les preuves et d'en améliorer l'automatisation, on propose d'utiliser des théories alternatives à Machine:
- Burkhart présente une formalisation alternative à base de monades. la théorie Monads encode de manière naturelle les machines de Mealy. Notre fonction de transition devient une fonction d'input vers monades.
theory Cruise_Monad
imports Monads
begin
record cruise_state =
on :: bool
cruise :: bool
definition σ⇩0 where "σ⇩0 = ⦇ on = False, cruise = False⦈"
datatype inputs = on | off | cruise | brake | standby
fun step :: "inputs ⇒ (unit, cruise_state) MON⇩S⇩E"
where "step on = (λσ.(if cruise_state.on σ
then Some((), σ⦇on:=True, cruise:=False⦈)
else Some((), σ)))"
| "step cruise = (λσ.(if cruise_state.on σ
then Some((), σ⦇on:=True, cruise:=True⦈)
else Some((), σ)))"
| "step off = (λσ. Some((), σ⦇on:=True, cruise:=False⦈))"
| "step brake = (λσ.(if cruise_state.cruise σ
then Some((), σ⦇cruise:=False⦈)
else Some((), σ)))"
| "step standby = (λσ.(if cruise_state.cruise σ
then Some((), σ⦇cruise:=False⦈)
else Some((), σ)))"
lemma step_is_total : "step X σ ≠ None"
by(induct X, simp_all)
theorem unreacheable :
assumes "set S ⊆ {on, off, brake, standby}"
shows " σ⇩0 ⊨ (_ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p S step ; assert⇩S⇩E(λ σ. ¬ (cruise_state.cruise σ)))"
txt{* All valid execution sequences from @{term σ⇩0} to anywhere via a sequence @{term S}
not containing @{term cruise} leads to a safe state. *}
proof(rule assms [THEN rev_mp], rule List.rev_induct)
show "set [] ⊆ {inputs.on, off, brake, standby} ⟶
(σ⇩0 ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p [] step; assert⇩S⇩E (λσ. ¬ cruise_state.cruise σ)))"
by(simp add: Monads.assert_disch4 σ⇩0_def)
next
fix x xs
show "set xs ⊆ {inputs.on, off, brake, standby} ⟶
(σ⇩0 ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p xs step; assert⇩S⇩E (λσ. ¬ cruise_state.cruise σ))) ⟹
set (xs @ [x]) ⊆ {inputs.on, off, brake, standby} ⟶
(σ⇩0 ⊨ ( _ ← mbind⇩F⇩a⇩i⇩l⇩S⇩t⇩o⇩p (xs @ [x]) step; assert⇩S⇩E (λσ. ¬ cruise_state.cruise σ)))"
apply(rule impI, erule impE, simp, erule assert_suffix_inv)
by(auto simp: valid_SE_def bind_SE_def assert_SE_def)
qed
On note ici l'usage de la règle List.rev_induct
qui permet de raisonner sur un invariant d'exécution. Le théorème prouve que l'état de régulation est inatteignable sans l'occurence de l'input cruise .
- Chantal propose d'utiliser les relations pour formaliser la fonction de transition. Il suffit ensuite de générer la fermeture transitive pour raisonner sur les chemins d'exécution.
definition step' :: "inputs ⇒ cruise_state rel"
where "step' x = {(σ,σ'). step x σ = Some((), σ') }"
definition steps' where "steps' ≡ step' inputs.on ∪ step' off ∪ step' brake ∪ step' standby "
find_theorems name:"induct" "_⇧*"
theorem "(σ⇩0,σ) ∈ (steps')⇧* ⟹ ¬ cruise_state.cruise σ"
apply(erule rtrancl.induct)
Nouvelle version utilisant la clôture reflexive et transitive
Je regroupe la définition de la relation successors s
(transitions possibles sur un alphabet d'entrée s
) et de la relation reachable s
(états entre lesquels il existe un chemin sur l'alphabet d'entrée s
) dans une locale :
theory Machine
imports Main
begin
(*
* A machine behaves when receiving an input (of type 'inp) and becomes a new machine.
*)
locale machine =
fixes behavior :: "'inp ⇒ 'a ⇒ 'a" (infixl "→" 60)
begin
(* Machine m2 is a successor of m1 if m1 can become m2 when receiving an input. *)
definition successors :: "'inp set ⇒ 'a rel"
where
"successors s ≡ ⋃i∈s. {(σ, σ'). σ'= i → σ}"
(* Alternate definition
definition successors :: "CruiseInput set ⇒ Cruise rel"
where
"successors s ≡ {(σ, σ'). ∃i ∈ s. σ' = i → σ}"
*)
(* Machine m2 is reachable from m1 with a set of inputs
if there exists a sequence of inputs taken from the set
that leads from m1 to m2. *)
abbreviation reachable :: "'inp set ⇒ 'a rel"
where
"reachable s ≡ (successors s)⇧*"
lemma successors_sub:"successors s ⊆ successors UNIV"
using successors_def by auto
lemma reachable_mono: "s ⊆ s' ⟹ reachable s ⊆ reachable s'"
unfolding successors_def by (simp add: SUP_subset_mono rtrancl_mono)
end (* locale machine *)
print_locale! machine
end
La transformation Acceleo (Trans2Isabelle.mtl) a été mise à jour pour générer une théorie qui utilise cette locale. Elle génère également quelques lemmes utiles qui sont prouvés automatiquement :
theory Cruise
imports Machine
begin
datatype Cruise =
Cruise (s_on: bool) (s_cruise: bool)
(* Some lemmas to get an instance from a simple property on the state *)
lemma on_ex:
assumes "s_on m = X"
shows "∃ p_cruise. m = Cruise X p_cruise"
proof -
from Cruise.nchotomy obtain p_on p_cruise
where "m = Cruise p_on p_cruise" by blast
with assms show ?thesis by simp
qed
lemma cruise_ex:
assumes "s_cruise m = X"
shows "∃p_on . m = Cruise p_on X"
proof -
from Cruise.nchotomy obtain p_on p_cruise
where "m = Cruise p_on p_cruise" by blast
with assms show ?thesis by simp
qed
(* The initial state of a Cruise *)
abbreviation CruiseInit :: Cruise
where
"CruiseInit ≡ Cruise False False"
(* Possible inputs for a Cruise machine *)
datatype CruiseInput = on | off | cruise | brake | standby
(* Behavior of a Cruise machine *)
fun CruiseBehavior :: "CruiseInput ⇒ Cruise ⇒ Cruise"
where
"CruiseBehavior off (Cruise _ _) = Cruise False False"
| "CruiseBehavior on (Cruise False _) = Cruise True False"
| "CruiseBehavior cruise (Cruise True _) = Cruise True True"
| "CruiseBehavior brake (Cruise isOn True) = Cruise isOn False"
| "CruiseBehavior standby (Cruise isOn True) = Cruise isOn False"
| "CruiseBehavior _ some_cruise = some_cruise"
(* A Cruise can be interpreted as a machine *)
interpretation machine "CruiseBehavior" .
end
Il est alors possible de démontrer des propriétés sur le comportement de la machine :
theory CruiseProofs
imports Cruise
begin
(* It is possible to switch the machine on *)
lemma 1:"(CruiseInit, (Cruise True False)) ∈ successors UNIV"
proof -
from CruiseBehavior.simps(2) have "CruiseBehavior on CruiseInit = (Cruise True False)" by simp
hence "(CruiseInit, (Cruise True False)) ∈ successors {on}" unfolding successors_def by simp
thus ?thesis using successors_sub ..
qed
(* It is possible to turn on cruising when the machine is on *)
lemma 2:"((Cruise True False), (Cruise True True)) ∈ successors UNIV"
proof -
from CruiseBehavior.simps(3) have "CruiseBehavior cruise (Cruise True False) = (Cruise True True)" .
hence "(Cruise True False, Cruise True True) ∈ successors {cruise}" unfolding successors_def by simp
thus ?thesis using successors_sub ..
qed
(* It is possible to turn cruising on from the initial state *)
lemma "(CruiseInit, (Cruise True True)) ∈ reachable UNIV"
proof -
from 1 and 2 show ?thesis by simp
qed
(* Without the cruise input, you cannot turn cruising on (function version) *)
lemma no_magic_cruise :
assumes "i ∈ {on, off, brake, standby}"
shows "s_cruise (CruiseBehavior i (Cruise a False)) = False"
proof (cases i) print_cases
case cruise (* impossible case *)
thus ?thesis using assms by simp
next
case on print_facts
thus ?thesis by (case_tac a, simp_all)
qed simp_all
(* Without the cruise input, you cannot turn cruising on (relation version) *)
lemma no_magic_cruise_suc :
"((Cruise a False), (Cruise a' True)) ∉ successors {on, off, brake, standby}" (is "(?a,?b) ∉ successors ?inpset")
proof -
from no_magic_cruise have
"∀i ∈ ?inpset. CruiseBehavior i ?a ≠ ?b"
by (metis Cruise.sel(2))
hence
"¬(∃i ∈ ?inpset. CruiseBehavior i ?a = ?b)" by simp
thus ?thesis unfolding successors_def by simp
qed
(* From any state with cruise off, all the reachable state without the cruise input have cruise off *)
lemma no_reach_cruise: "((Cruise a False), s) ∈ reachable {on, off, brake, standby} ⟹ ¬ s_cruise s"
proof (induction rule: rtrancl_induct)
case base thus ?case by simp (* cruise is initially off *)
next
case (step y z) thus ?case (* show that no step can switch is on *)
proof -
from cruise_ex step.IH obtain p where yfalse:"y = Cruise p False" by blast
{
assume "s_cruise z"
with cruise_ex obtain g where "z = Cruise g True" by blast
with yfalse and step.hyps(2) and no_magic_cruise_suc[of p g] have "False" by simp
}
thus ?thesis ..
qed
qed
(* Dual version of the same theorem:
From any state where cruise is off, if we reach a state where cruise is on, we received a cruise input *)
lemma reach_imp_cruise:"(Cruise a False, Cruise a' True) ∈ (reachable s) ⟹ cruise ∈ s" (is "?P ⟹ ?Q")
proof -
{
assume hyp:"¬?Q"
hence "s ⊆ {on, off, brake, standby}" using CruiseInput.exhaust by blast
from reachable_mono[OF this] have "reachable s ⊆ reachable {on, off, brake, standby}" .
hence "?P ⟹ (Cruise a False, Cruise a' True) ∈ reachable {on, off, brake, standby}" by blast
with no_reach_cruise have "¬?P" using Cruise.sel(2) by blast
}
thus "?P ⟹ ?Q" by blast
qed
end
Autre exemple, un peu plus complexe, avec des feux pour un passage piéton :
/*
* A model of traffic lights for pedestrians
*
* Properties to check (Promela/Spin syntax):
* ltl {[] !(car_green && ped_green)} (safety)
* ltl {[] (car_red -> <> car_green)} (liveness)
* ltl {[] (ped_red -> <> ped_green)} (liveness)
*/
traffic
inputs: pedestrian car time
outputs: ped_green=true ped_red=false ped_waiting=false car_green=false car_orange=false car_red=true car_waiting=false
rules:
[ped_red !ped_waiting !car_waiting !car_orange]
pedestrian -> car_green=false car_orange=true
[car_orange]
time -> car_orange=false car_red=true ped_waiting=true
[ped_waiting]
time -> ped_red=false ped_green=true ped_waiting=false
[car_red !car_waiting !ped_waiting]
car -> ped_green=false ped_red=true car_waiting=true
[car_waiting]
time -> car_red=false car_green=true car_waiting=false
Transformation Acceleo pour générer le code Promela/Spin permettant de vérifier les formules LTL : Trans2promela.mtl.
Théorie Isabelle :
theory Traffic
imports Machine
begin
datatype Traffic =
Traffic (s_ped_green: bool) (s_ped_red: bool) (s_ped_waiting: bool) (s_car_green: bool) (s_car_orange: bool) (s_car_red: bool) (s_car_waiting: bool)
(* Some lemmas to get an instance from a simple property on the state *)
lemma ped_green_ex:
assumes "s_ped_green m = X"
shows "∃ p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting. m = Traffic X p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting"
proof -
from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
with assms show ?thesis by simp
qed
lemma ped_red_ex:
assumes "s_ped_red m = X"
shows "∃p_ped_green p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting. m = Traffic p_ped_green X p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting"
proof -
from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
with assms show ?thesis by simp
qed
lemma ped_waiting_ex:
assumes "s_ped_waiting m = X"
shows "∃p_ped_green p_ped_red p_car_green p_car_orange p_car_red p_car_waiting. m = Traffic p_ped_green p_ped_red X p_car_green p_car_orange p_car_red p_car_waiting"
proof -
from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
with assms show ?thesis by simp
qed
lemma car_green_ex:
assumes "s_car_green m = X"
shows "∃p_ped_green p_ped_red p_ped_waiting p_car_orange p_car_red p_car_waiting. m = Traffic p_ped_green p_ped_red p_ped_waiting X p_car_orange p_car_red p_car_waiting"
proof -
from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
with assms show ?thesis by simp
qed
lemma car_orange_ex:
assumes "s_car_orange m = X"
shows "∃p_ped_green p_ped_red p_ped_waiting p_car_green p_car_red p_car_waiting. m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green X p_car_red p_car_waiting"
proof -
from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
with assms show ?thesis by simp
qed
lemma car_red_ex:
assumes "s_car_red m = X"
shows "∃p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_waiting. m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange X p_car_waiting"
proof -
from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
with assms show ?thesis by simp
qed
lemma car_waiting_ex:
assumes "s_car_waiting m = X"
shows "∃p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red . m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red X"
proof -
from Traffic.nchotomy obtain p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting
where "m = Traffic p_ped_green p_ped_red p_ped_waiting p_car_green p_car_orange p_car_red p_car_waiting" by blast
with assms show ?thesis by simp
qed
(* The initial state of a Traffic *)
abbreviation TrafficInit :: Traffic
where
"TrafficInit ≡ Traffic True False False False False True False"
(* Possible inputs for a Traffic machine *)
datatype TrafficInput = pedestrian | car | time
(* Behavior of a Traffic machine *)
fun TrafficBehavior :: "TrafficInput ⇒ Traffic ⇒ Traffic"
where
"TrafficBehavior pedestrian (Traffic isPed_green True False _ False isCar_red False) = Traffic isPed_green True False False True isCar_red False"
| "TrafficBehavior time (Traffic isPed_green isPed_red _ isCar_green True _ isCar_waiting) = Traffic isPed_green isPed_red True isCar_green False True isCar_waiting"
| "TrafficBehavior time (Traffic _ _ True isCar_green isCar_orange isCar_red isCar_waiting) = Traffic True False False isCar_green isCar_orange isCar_red isCar_waiting"
| "TrafficBehavior car (Traffic _ _ False isCar_green isCar_orange True False) = Traffic False True False isCar_green isCar_orange True True"
| "TrafficBehavior time (Traffic isPed_green isPed_red isPed_waiting _ isCar_orange _ True) = Traffic isPed_green isPed_red isPed_waiting True isCar_orange False False"
| "TrafficBehavior _ some_traffic = some_traffic"
(* A Traffic can be interpreted as a machine *)
interpretation machine "TrafficBehavior" .
end
Preuves :
theory TrafficProofs
imports Traffic
begin
(* definition only_one where "only_one boollist ≡ fold (λb s. if b then Suc s else s) boollist 0 = 1" *)
(*abbreviation "car_excl s ≡ only_one [s_car_green s, s_car_orange s, s_car_red s]"*)
abbreviation "car_excl s ≡ (s_car_green s ∨ s_car_orange s ∨ s_car_red s) ∧ ¬(s_car_green s ∧ s_car_orange s) ∧ ¬(s_car_orange s ∧ s_car_red s) ∧ ¬(s_car_green s ∧ s_car_red s)"
(*abbreviation "ped_excl s ≡ only_one [s_ped_green s, s_ped_red s]"*)
abbreviation "ped_excl s ≡ (s_ped_green s ∨ s_ped_red s) ∧ ¬(s_ped_green s ∧ s_ped_red s)"
(* Some invariants thet must be proven to hold together *)
abbreviation "traffic_inv s ≡
car_excl s
∧ ped_excl s
∧ ¬(s_ped_green s ∧ s_car_green s)
∧ (s_ped_waiting s ⟶ s_ped_red s)
∧ (s_ped_waiting s ⟶ s_car_red s)
∧ (s_car_waiting s ⟶ s_car_red s)
∧ (s_car_waiting s ⟶ s_ped_red s)
∧ (s_car_orange s ⟶ s_ped_red s)
∧ ¬(s_ped_waiting s ∧ s_car_waiting s)
∧ (s_ped_red s ∧ ¬s_ped_waiting s ∧ ¬s_car_waiting s ⟶ s_car_green s ∨ s_car_orange s)"
(* Proof that the invariants are preserved for each reaction of the machine *)
lemma invariants_step:
assumes "(s, t) ∈ successors UNIV"
and "traffic_inv s"
shows "traffic_inv t"
proof -
from input_ex[OF assms(1)] obtain i where hyp:"t = TrafficBehavior i s" by blast
show ?thesis
proof (cases i)
case pedestrian show ?thesis
proof (cases "∀pg cg cr. s ≠ Traffic pg True False cg False cr False")
case True
hence "TrafficBehavior pedestrian s = s" by (metis (full_types) Traffic.collapse TrafficBehavior.simps(10,25,29,33))
thus ?thesis using assms and hyp and pedestrian by auto
next
case False
hence "∃pg cg cr. s = Traffic pg True False cg False cr False" by simp
from this obtain pg cg cr where "s = Traffic pg True False cg False cr False" by blast
with assms(2) have "s = Traffic False True False True False False False" by auto
hence "t = Traffic False True False False True False False" using hyp pedestrian by simp
thus ?thesis using hyp by auto
qed
next
case car show ?thesis
proof (cases "∀pg pr cg co. s ≠ Traffic pg pr False cg co True False")
case True
hence "TrafficBehavior car s = s" by (metis (full_types) Traffic.collapse TrafficBehavior.simps(7, 26, 34))
thus ?thesis using assms and hyp and car by auto
next
case False
hence "∃pg pr cg co. s = Traffic pg pr False cg co True False" by simp
from this obtain pg pr cg co where "s = Traffic pg pr False cg co True False" by blast
with assms(2) have "s = Traffic pg pr False False False True False" by simp
hence "t = Traffic False True False False False True True" using hyp and car by simp
thus ?thesis using hyp by auto
qed
next
case time show ?thesis
proof (cases "∃pg pr pw cg cr cw. s = Traffic pg pr pw cg True cr cw")
case True
from this obtain pg pr pw cg cr cw where "s = Traffic pg pr pw cg True cr cw" by blast
with assms(2) have "s = Traffic False True pw False True False False" by auto
hence "t = Traffic False True True False False True False" using hyp time by simp
thus ?thesis using hyp assms by auto
next
case False
hence "¬(∃pg pr pw cg cr cw. s = Traffic pg pr pw cg True cr cw)" by simp
hence "s_car_orange s = False" using car_orange_ex by blast
hence "∃pg pr pw cg cr cw. s = Traffic pg pr pw cg False cr cw" using car_orange_ex by simp
from this obtain pg pr pw cg cr cw where sprop:"s = Traffic pg pr pw cg False cr cw" by blast
show ?thesis
proof (cases pw)
case True
hence "s = Traffic False True True False False True False" using sprop assms by auto
hence "t = Traffic True False False False False True False" using hyp time by simp
thus ?thesis using sprop hyp assms by auto
next
case False
hence h:"s = Traffic pg pr False cg False cr cw" using sprop by simp
show ?thesis
proof (cases cw)
case True
hence "s = Traffic False True False cg False cr True" using assms sprop h by auto
hence "t = Traffic False True False True False False False" using hyp time by simp
thus ?thesis using h hyp assms by auto
next
case False
hence "s = Traffic pg pr False cg False cr False" using sprop h by simp
hence "TrafficBehavior time s = s" using Traffic.collapse TrafficBehavior.simps(2,3,5,9,19,22) by simp
thus ?thesis using assms hyp time by auto
qed
qed
qed
qed
qed
(* Proof that the invariants hold for any reachable state from the initial state *)
lemma invariants:"(TrafficInit, t) ∈ reachable UNIV ⟹ traffic_inv t"
proof (induction rule: rtrancl_induct)
case base thus ?case by auto
next
case step thus ?case using invariants_step by simp
qed
(* Both lights are never green at the same time *)
lemma "(TrafficInit, t) ∈ reachable UNIV ⟹ ¬(s_ped_green t ∧ s_car_green t)"
using invariants by simp
end
Previous meeting -- Next meeting