82 lines
1.7 KiB
Text
82 lines
1.7 KiB
Text
---- MODULE topics2_toolbox_errors ----
|
|
EXTENDS Integers, TLC
|
|
|
|
(*--algorithm errortrace
|
|
variable x=0; y=0; i=0;
|
|
|
|
define
|
|
xyleq10 == x * y <= 10
|
|
end define;
|
|
|
|
process incX = "incX"
|
|
begin
|
|
EtX:
|
|
while i < 8 do
|
|
x := x + 1;
|
|
i := i + 1;
|
|
end while;
|
|
end process;
|
|
|
|
process incY = "incY"
|
|
begin
|
|
EtY:
|
|
while i < 8 do
|
|
y := y + 1;
|
|
i := i + 1;
|
|
end while;
|
|
end process;
|
|
|
|
end algorithm; *)
|
|
\* BEGIN TRANSLATION (chksum(pcal) = "46092ab" /\ chksum(tla) = "9ab38b8e")
|
|
VARIABLES pc, x, y, i
|
|
|
|
(* define statement *)
|
|
xyleq10 == x * y <= 10
|
|
|
|
|
|
vars == << pc, x, y, i >>
|
|
|
|
ProcSet == {"incX"} \cup {"incY"}
|
|
|
|
Init == (* Global variables *)
|
|
/\ x = 0
|
|
/\ y = 0
|
|
/\ i = 0
|
|
/\ pc = [self \in ProcSet |-> CASE self = "incX" -> "EtX"
|
|
[] self = "incY" -> "EtY"]
|
|
|
|
EtX == /\ pc["incX"] = "EtX"
|
|
/\ IF i < 8
|
|
THEN /\ x' = x + 1
|
|
/\ i' = i + 1
|
|
/\ pc' = [pc EXCEPT !["incX"] = "EtX"]
|
|
ELSE /\ pc' = [pc EXCEPT !["incX"] = "Done"]
|
|
/\ UNCHANGED << x, i >>
|
|
/\ y' = y
|
|
|
|
incX == EtX
|
|
|
|
EtY == /\ pc["incY"] = "EtY"
|
|
/\ IF i < 8
|
|
THEN /\ y' = y + 1
|
|
/\ i' = i + 1
|
|
/\ pc' = [pc EXCEPT !["incY"] = "EtY"]
|
|
ELSE /\ pc' = [pc EXCEPT !["incY"] = "Done"]
|
|
/\ UNCHANGED << y, i >>
|
|
/\ x' = x
|
|
|
|
incY == EtY
|
|
|
|
(* Allow infinite stuttering to prevent deadlock on termination. *)
|
|
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
|
|
/\ UNCHANGED vars
|
|
|
|
Next == incX \/ incY
|
|
\/ Terminating
|
|
|
|
Spec == Init /\ [][Next]_vars
|
|
|
|
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
|
|
|
|
\* END TRANSLATION
|
|
====
|