SoftwareConcepts/Apps/Restaurant1.tla at main · alcinocunha/SoftwareConcepts · GitHub

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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
------------- MODULE Restaurant1 -------------

VARIABLES action, reactions

error == FALSE

CONSTANTS Client, Table

Reserved == "Reserved"

VARIABLES available, reservations, labels

vars == <<action, reactions, available, reservations, labels>>

R == "Reservation"
L == "Label"

Reservation == INSTANCE Reservation WITH Reservation <- {R}, User <- Client, Resource <- Table
Label == INSTANCE Label WITH Label <- {L}, Item <- Table, Tag <- {Reserved}

Actions == Reservation!Actions \cup Label!Actions

InitAction == action \in Actions
NextAction == action' \in Actions

InitConcepts ==
    /\ Reservation!Init
    /\ Label!Init

NextConcepts ==
    /\ Reservation!Next
    /\ Label!Next

tables == available[R]
active_reservations == [ u \in Client |-> reservations[R][u] \cap tables ]
reserved == { t \in Table : labels[L][t] # {} }

Invariant == reserved = { t \in Table : \E u \in Client : t \in active_reservations[u] }

(*
reaction reserve_affix
when
	R.reserve[c,t]
then
	L.affix[t,Reserved]
*)

reserve_affix_add == { <<r, t>> \in {"reserve_affix"} \X Table : \E c \in Client : Reservation!reserve(R,c,t) }
reserve_affix_remove == { <<r, t>> \in {"reserve_affix"} \X Table : Label!affix(L,t,Reserved) }

(*
reaction cancel_detach
when
	R.cancel[c,t]
then
	L.detach[t,Reserved] or L.clear[t]
*)

cancel_detach_add == { <<r, t>> \in {"cancel_detach"} \X Table : \E c \in Client : Reservation!cancel(R,c,t) }
cancel_detach_remove == { <<r, t>> \in {"cancel_detach"} \X Table : Label!detach(L,t,Reserved) \/ Label!clear(L,t) }

(*
reaction use_detach
when
	R.use[c,t]
then
	L.detach[t,Reserved] or L.clear[t]
*)

use_detach_add == { <<r, t>> \in {"use_detach"} \X Table : \E c \in Client : Reservation!use(R,c,t) }
use_detach_remove == { <<r, t>> \in {"use_detach"} \X Table : Label!detach(L,t,Reserved) \/ Label!clear(L,t) }

(*
reaction affix_error
when
	L.affix[t,Reserved]
where
	t not in Client.active_reservations
then
	error
*)

affix_error_add == { <<r>> \in {<<"affix_error">>} : \E t \in Table : Label!affix(L,t,Reserved) /\ \A c \in Client : t \notin active_reservations[c] }
affix_error_remove == { <<r>> \in {<<"affix_error">>} : error }

(*
reaction detach_error
when
	L.detach[t,Reserved]
where
	t in Client.active_reservations
then
	error
*)

detach_error_add == { <<r>> \in {<<"detach_error">>} : \E t \in Table : Label!detach(L,t,Reserved) /\ \E c \in Client : t \in active_reservations[c] }
detach_error_remove == { <<r>> \in {<<"detach_error">>} : error }

(*
reaction clear_error
when
	L.clear[t]
where
	t in Client.active_reservations
then
	error
*)

clear_error_add == { <<r>> \in {<<"clear_error">>} : \E t \in Table : Label!clear(L,t) /\ \E c \in Client : t \in active_reservations[c] }
clear_error_remove == { <<r>> \in {<<"clear_error">>} : error }

\* Reaction semantics

reactions_to_add == reserve_affix_add \cup cancel_detach_add \cup use_detach_add \cup affix_error_add \cup detach_error_add \cup clear_error_add
reactions_to_remove == reserve_affix_remove \cup cancel_detach_remove \cup use_detach_remove \cup affix_error_remove \cup detach_error_remove \cup clear_error_remove

InitReactions ==
    /\ reactions = {}

NextReactions ==
    /\ reactions # {} => reactions_to_remove \cap reactions # {}
    /\ reactions' = (reactions \ reactions_to_remove) \cup reactions_to_add

Spec == InitAction /\ InitConcepts /\ InitReactions /\ [][NextAction /\ NextConcepts /\ NextReactions]_vars

Design == reactions = {} <=> Invariant

==============================================