-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathBuildingEntry_17_1.thy
101 lines (73 loc) · 3.58 KB
/
BuildingEntry_17_1.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
section \<open> Building Entry System \<close>
theory BuildingEntry_17_1
imports "Z_Machines.Z_Machine"
begin
text \<open>Usingz ex 17.1: We model a system that will monitor the access to a building.
The system should keep track of the people who are inside the building, and should forbid entry by more than a specified number of people at any time.\<close>
text \<open>we define a basic type\<close>
type_synonym staff = nat
consts
Staff :: "staff set"
maxentry :: nat
\<comment>\<open>maxentry is the maximum number of people that may enter the building at any time\<close>
text \<open>an abstract state space, s is to record the names of those currently inside the building; the state invariant restricts the number of people to be less or equal than maxentry.\<close>
zstore ASystem =
s :: "\<bbbP> staff"
where "s \<in> \<bbbF> Staff" "#s \<le> maxentry"
text \<open>A person who is not already recorded as being inside the building may enter it, providing there is enough room, i.e., s has not reached the maximum number.\<close>
zoperation AEnterBuilding =
over ASystem
params p\<in>Staff
pre "#s < maxentry \<and> p \<notin> s"
update "[s\<Zprime> = s \<union> {p}]"
text \<open>A person who is in the building may leave it.\<close>
zoperation ALeaveBuilding =
over ASystem
params p\<in>Staff
pre "p \<in> s"
update "[s\<Zprime> = s - {p}]"
text \<open>Initially, there is no-one in the building\<close>
zmachine ABuildingEntry =
over ASystem
init "[s\<Zprime> = {}]"
operations AEnterBuilding ALeaveBuilding
def_consts
Staff = "{0..10}"
maxentry = "5"
animate ABuildingEntry
text \<open>A more CONCRETE specification might model the state of the system as an injective sequence: a sequence with no repetitions - iseq. The length of this sequence
must be less than maxentry\<close>
zstore CSystem =
l :: "staff list"
where
"l \<in> iseq Staff" "#l \<le> maxentry" \<comment>\<open>The length of l (#l) represents the number of people inside the building.\<close>
text \<open>A person who is not already inside the building may enter it, providing there is enough room.\<close>
zoperation CEnterBuilding =
params p \<in> Staff
pre "#l < maxentry \<and> p \<notin> ran l"
update "[l\<Zprime> = l @ [p]]"
text \<open>A person who is in the building may leave it.\<close>
zoperation CLeaveBuilding =
params p \<in> Staff
pre "#l < maxentry \<and> p \<in> ran l"
update "[l\<Zprime> = l\<restriction> (Staff-{p}) ]"
text \<open>Initially, there is no one in the building\<close>
zmachine CBuildingEntry =
over CSystem
init "[l\<Zprime> = []]"
operations CEnterBuilding CLeaveBuilding
(*what to do with ListRetrieveSet ? ? ? ?*)
term CSystem_inv
definition ListRetrieveSet :: "CSystem \<Rightarrow> (_, ASystem) itree" where
"ListRetrieveSet = \<questiondown>CSystem_inv? ;; \<langle>\<lblot>s \<leadsto> set l\<rblot>\<rangle>\<^sub>a"
definition SetRetrieveList :: "ASystem \<Rightarrow> (_, CSystem) itree" where
"SetRetrieveList = \<questiondown>ASystem_inv? ;; \<langle>\<lblot>l \<leadsto> sorted_list_of_set s\<rblot>\<rangle>\<^sub>a"
find_theorems "(\<circ>\<^sub>s)"
lemma "ListRetrieveSet ;; SetRetrieveList = \<questiondown>CSystem?"
apply (simp add: ListRetrieveSet_def SetRetrieveList_def ASystem_inv_def assigns_seq kcomp_assoc assigns_assume assigns_seq_comp usubst usubst_eval)
lemma "p \<in> Staff \<Longrightarrow> (ListRetrieveSet ;; AEnterBuilding p) \<sqsubseteq> (CEnterBuilding p ;; ListRetrieveSet)"
unfolding ListRetrieveSet_def AEnterBuilding_def CEnterBuilding_def
apply refine_auto
apply (simp add: distinct_card)
done
end