Skip to content
This repository was archived by the owner on Aug 1, 2023. It is now read-only.

Commit 94fa1ab

Browse files
ksaricCodiePP
ksaric
authored and
CodiePP
committed
[GH-355] Split TLA+ launcher spec into separate processes. (#356)
1 parent 4d26bce commit 94fa1ab

File tree

2 files changed

+285
-5
lines changed

2 files changed

+285
-5
lines changed

‎cardano-shell/specs/CardanoShellSpec.lhs

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@
2222
\usepackage{bussproofs}
2323
% for inserting images
2424
\usepackage{graphicx}
25-
% for code syntax highlighting
25+
% for code highlighting
2626
\usepackage{listings}
2727

2828
\usetikzlibrary{calc,positioning,arrows}
@@ -713,15 +713,17 @@ Let's take a look at some of the key functions we will use:
713713

714714
%endif
715715

716+
716717
If we take a look at the typical state transition of such a system, we can easily imagine something like this on ~\ref{fig:updateStateMachineFig}.\\.
717718

719+
718720
\begin{figure}[ht] % ’ht’ tells LaTeX to place the figure ’here’ or at the top of the page
719721
\centering % centers the figure
720722
\begin{tikzpicture}
721723
\node[state, accepting, initial] (q1) {$UpdateMode$};
722724
\node[state, right of=q1] (q2) {$WalletNormal$};
723725
\node[state, right of=q2] (q3) {$WalletSafe$};
724-
\node[state, below of=q1] (q4) {$Failure$};
726+
\node[state, below of=q2] (q4) {$Failure$};
725727
\node[state, accepting, right of=q4] (q5) {$Success$};
726728
\draw
727729
(q1) edge[above] node{} (q2)
@@ -731,7 +733,7 @@ If we take a look at the typical state transition of such a system, we can easil
731733
(q3) edge[bend right, above] node{} (q1) %return
732734
(q2) edge[bend left, below] node{} (q1)
733735

734-
(q1) edge[below] node{} (q4)
736+
%(q1) edge[below] node{} (q4)
735737
%(q1) edge[below] node{} (q5)
736738

737739
(q2) edge[below] node{} (q4)
@@ -761,12 +763,14 @@ state_transition(start,init,run_update).
761763
state_transition(run_update,update_fail, updater_file_missing).
762764
state_transition(run_update,update_success,run_wallet_normal).
763765

764-
state_transition(run_wallet_normal, safe_mode, run_wallet_safe).
766+
state_transition(run_wallet_normal, safe_mode,
767+
run_wallet_safe).
765768
state_transition(run_wallet_normal, update_mode, run_update).
766769
state_transition(run_wallet_normal, failure, run_failure).
767770
state_transition(run_wallet_normal, success, run_success).
768771

769-
state_transition(run_wallet_safe, normal_mode, run_wallet_normal).
772+
state_transition(run_wallet_safe, normal_mode,
773+
run_wallet_normal).
770774
state_transition(run_wallet_safe, update_mode, run_update).
771775
state_transition(run_wallet_safe, failure, run_failure).
772776
state_transition(run_wallet_safe, success, run_success).

‎cardano-shell/specs/tla/UpdateSystemWallet.tla

Lines changed: 276 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,276 @@
1+
---------------------- MODULE UpdateSystemWallet ------------------------
2+
3+
EXTENDS TLC, Integers, Sequences
4+
5+
CONSTANTS launcher_state_depth \* How many state depth we want to check?
6+
7+
(*--algorithm launcher
8+
variables
9+
current_launcher_state_depth = launcher_state_depth,
10+
current_wallet_exit_code = 0,
11+
update_exists \in {TRUE, FALSE},
12+
13+
next_state = "update_mode",
14+
15+
wallet_exit_codes = <<>>,
16+
updater_exit_codes = <<>>,
17+
18+
\* Tracking global state changes
19+
update_running = FALSE,
20+
wallet_running = FALSE
21+
22+
define
23+
IsElementInSeq(el,seq)==\E i \in DOMAIN seq:seq[i]=el
24+
end define;
25+
26+
27+
\* Simply defining the update to be non-deterministic.
28+
macro update_arrived() begin
29+
30+
either
31+
update_exists := TRUE;
32+
or
33+
update_exists := FALSE;
34+
end either;
35+
36+
end macro;
37+
38+
macro check_end_state(wallet_exit_codes) begin
39+
40+
(* We always must pass through at least two labels before we end the proceess. *)
41+
assert Len(wallet_exit_codes) >= 2;
42+
43+
(* We must pass through the "wallet_normal_mode" when running the spec. *)
44+
assert IsElementInSeq("update_mode", wallet_exit_codes);
45+
assert IsElementInSeq("wallet_normal_mode", wallet_exit_codes);
46+
47+
goto Done;
48+
49+
end macro;
50+
51+
(* The Wallet process *)
52+
fair process Wallet = "Wallet"
53+
begin
54+
WalletRun:
55+
await wallet_running /\ next_state \in {"normal_mode", "safe_mode"};
56+
57+
current_launcher_state_depth := current_launcher_state_depth - 1;
58+
59+
\* This is before the actual "wallet run", so we can see with which "mode"
60+
\* was run with.
61+
if next_state = "normal_mode" then
62+
wallet_exit_codes := Append(wallet_exit_codes, "wallet_normal_mode");
63+
elsif next_state = "safe_mode" then
64+
wallet_exit_codes := Append(wallet_exit_codes, "wallet_safe_mode");
65+
end if;
66+
67+
68+
if current_launcher_state_depth <= 0 then
69+
goto Done;
70+
else
71+
either
72+
current_wallet_exit_code := 0; \* Success
73+
next_state := "success";
74+
75+
\* Check the end state
76+
check_end_state(wallet_exit_codes);
77+
78+
or
79+
current_wallet_exit_code := 1; \* Failure
80+
next_state := "failure";
81+
82+
\* Check the end state
83+
check_end_state(wallet_exit_codes);
84+
85+
or
86+
current_wallet_exit_code := 20; \* Update
87+
next_state := "update_mode";
88+
89+
goto WalletRun;
90+
or
91+
current_wallet_exit_code := 21; \* Safe mode
92+
next_state := "safe_mode";
93+
\* Each time we go into safe mode, we can simulate an update.
94+
update_arrived();
95+
96+
goto WalletRun;
97+
or
98+
current_wallet_exit_code := 22; \* Normal mode
99+
next_state := "normal_mode";
100+
101+
\* Each time we go into safe mode, we can simulate an update.
102+
update_arrived();
103+
104+
goto WalletRun;
105+
end either;
106+
end if;
107+
108+
end process;
109+
110+
111+
(* The Launcher process *)
112+
fair process Launcher = "Launcher"
113+
114+
begin
115+
Update:
116+
await next_state = "update_mode";
117+
118+
update_running := TRUE;
119+
wallet_running := FALSE;
120+
121+
wallet_exit_codes := Append(wallet_exit_codes, "update_mode");
122+
123+
if update_exists then
124+
updater_exit_codes := Append(updater_exit_codes, "updater_success");
125+
update_exists := FALSE;
126+
else
127+
updater_exit_codes := Append(updater_exit_codes, "updater_failure");
128+
end if;
129+
130+
next_state := "normal_mode";
131+
\* We have to run the wallet after the update
132+
133+
134+
135+
Launching:
136+
137+
update_running := FALSE;
138+
wallet_running := TRUE;
139+
140+
\* The wallet is dictating the states the launcher has to handle.
141+
if next_state = "success" \/ next_state = "failure" \/ current_launcher_state_depth <= 0 then
142+
goto Done;
143+
elsif next_state = "update_mode" then
144+
goto Update;
145+
else
146+
goto Launching;
147+
end if;
148+
149+
end process;
150+
151+
152+
end algorithm;*)
153+
\* BEGIN TRANSLATION
154+
VARIABLES current_launcher_state_depth, current_wallet_exit_code,
155+
update_exists, next_state, wallet_exit_codes, updater_exit_codes,
156+
update_running, wallet_running, pc
157+
158+
(* define statement *)
159+
IsElementInSeq(el,seq)==\E i \in DOMAIN seq:seq[i]=el
160+
161+
162+
vars == << current_launcher_state_depth, current_wallet_exit_code,
163+
update_exists, next_state, wallet_exit_codes, updater_exit_codes,
164+
update_running, wallet_running, pc >>
165+
166+
ProcSet == {"Wallet"} \cup {"Launcher"}
167+
168+
Init == (* Global variables *)
169+
/\ current_launcher_state_depth = launcher_state_depth
170+
/\ current_wallet_exit_code = 0
171+
/\ update_exists \in {TRUE, FALSE}
172+
/\ next_state = "update_mode"
173+
/\ wallet_exit_codes = <<>>
174+
/\ updater_exit_codes = <<>>
175+
/\ update_running = FALSE
176+
/\ wallet_running = FALSE
177+
/\ pc = [self \in ProcSet |-> CASE self = "Wallet" -> "WalletRun"
178+
[] self = "Launcher" -> "Update"]
179+
180+
WalletRun == /\ pc["Wallet"] = "WalletRun"
181+
/\ wallet_running /\ next_state \in {"normal_mode", "safe_mode"}
182+
/\ current_launcher_state_depth' = current_launcher_state_depth - 1
183+
/\ IF next_state = "normal_mode"
184+
THEN /\ wallet_exit_codes' = Append(wallet_exit_codes, "wallet_normal_mode")
185+
ELSE /\ IF next_state = "safe_mode"
186+
THEN /\ wallet_exit_codes' = Append(wallet_exit_codes, "wallet_safe_mode")
187+
ELSE /\ TRUE
188+
/\ UNCHANGED wallet_exit_codes
189+
/\ IF current_launcher_state_depth' <= 0
190+
THEN /\ pc' = [pc EXCEPT !["Wallet"] = "Done"]
191+
/\ UNCHANGED << current_wallet_exit_code,
192+
update_exists, next_state >>
193+
ELSE /\ \/ /\ current_wallet_exit_code' = 0
194+
/\ next_state' = "success"
195+
/\ Assert(Len(wallet_exit_codes') >= 2,
196+
"Failure of assertion at line 41, column 5 of macro called at line 76, column 17.")
197+
/\ Assert(IsElementInSeq("update_mode", wallet_exit_codes'),
198+
"Failure of assertion at line 44, column 5 of macro called at line 76, column 17.")
199+
/\ Assert(IsElementInSeq("wallet_normal_mode", wallet_exit_codes'),
200+
"Failure of assertion at line 45, column 5 of macro called at line 76, column 17.")
201+
/\ pc' = [pc EXCEPT !["Wallet"] = "Done"]
202+
/\ UNCHANGED update_exists
203+
\/ /\ current_wallet_exit_code' = 1
204+
/\ next_state' = "failure"
205+
/\ Assert(Len(wallet_exit_codes') >= 2,
206+
"Failure of assertion at line 41, column 5 of macro called at line 83, column 17.")
207+
/\ Assert(IsElementInSeq("update_mode", wallet_exit_codes'),
208+
"Failure of assertion at line 44, column 5 of macro called at line 83, column 17.")
209+
/\ Assert(IsElementInSeq("wallet_normal_mode", wallet_exit_codes'),
210+
"Failure of assertion at line 45, column 5 of macro called at line 83, column 17.")
211+
/\ pc' = [pc EXCEPT !["Wallet"] = "Done"]
212+
/\ UNCHANGED update_exists
213+
\/ /\ current_wallet_exit_code' = 20
214+
/\ next_state' = "update_mode"
215+
/\ pc' = [pc EXCEPT !["Wallet"] = "WalletRun"]
216+
/\ UNCHANGED update_exists
217+
\/ /\ current_wallet_exit_code' = 21
218+
/\ next_state' = "safe_mode"
219+
/\ \/ /\ update_exists' = TRUE
220+
\/ /\ update_exists' = FALSE
221+
/\ pc' = [pc EXCEPT !["Wallet"] = "WalletRun"]
222+
\/ /\ current_wallet_exit_code' = 22
223+
/\ next_state' = "normal_mode"
224+
/\ \/ /\ update_exists' = TRUE
225+
\/ /\ update_exists' = FALSE
226+
/\ pc' = [pc EXCEPT !["Wallet"] = "WalletRun"]
227+
/\ UNCHANGED << updater_exit_codes, update_running,
228+
wallet_running >>
229+
230+
Wallet == WalletRun
231+
232+
Update == /\ pc["Launcher"] = "Update"
233+
/\ next_state = "update_mode"
234+
/\ update_running' = TRUE
235+
/\ wallet_running' = FALSE
236+
/\ wallet_exit_codes' = Append(wallet_exit_codes, "update_mode")
237+
/\ IF update_exists
238+
THEN /\ updater_exit_codes' = Append(updater_exit_codes, "updater_success")
239+
/\ update_exists' = FALSE
240+
ELSE /\ updater_exit_codes' = Append(updater_exit_codes, "updater_failure")
241+
/\ UNCHANGED update_exists
242+
/\ next_state' = "normal_mode"
243+
/\ pc' = [pc EXCEPT !["Launcher"] = "Launching"]
244+
/\ UNCHANGED << current_launcher_state_depth,
245+
current_wallet_exit_code >>
246+
247+
Launching == /\ pc["Launcher"] = "Launching"
248+
/\ update_running' = FALSE
249+
/\ wallet_running' = TRUE
250+
/\ IF next_state = "success" \/ next_state = "failure" \/ current_launcher_state_depth <= 0
251+
THEN /\ pc' = [pc EXCEPT !["Launcher"] = "Done"]
252+
ELSE /\ IF next_state = "update_mode"
253+
THEN /\ pc' = [pc EXCEPT !["Launcher"] = "Update"]
254+
ELSE /\ pc' = [pc EXCEPT !["Launcher"] = "Launching"]
255+
/\ UNCHANGED << current_launcher_state_depth,
256+
current_wallet_exit_code, update_exists,
257+
next_state, wallet_exit_codes, updater_exit_codes >>
258+
259+
Launcher == Update \/ Launching
260+
261+
(* Allow infinite stuttering to prevent deadlock on termination. *)
262+
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
263+
/\ UNCHANGED vars
264+
265+
Next == Wallet \/ Launcher
266+
\/ Terminating
267+
268+
Spec == /\ Init /\ [][Next]_vars
269+
/\ WF_vars(Wallet)
270+
/\ WF_vars(Launcher)
271+
272+
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
273+
274+
\* END TRANSLATION
275+
276+
===========================================================================

0 commit comments

Comments
 (0)