This one ends up in stuttering. Th error trace is given below the spec:-------------------------- MODULE multiuser_flows --------------------------
EXTENDS Integers, Sequences, TLC
CONSTANT Users, NULL, Data
(*
Inputs == { "none","start_edit", "end_edit", "start_run", "end_run" , "exit"};
States == { "start", "idle", "editing", "running"};
*)
(*--algorithm multiuser
variables
queues = [u \in Users |-> <<>>]; \* Ordered messages
flow_state = [ u \in Users |-> "changed"];
user_state = [ u \in Users |-> "start"];
define
Inputs == { "none","start_edit", "end_edit", "start_run", "end_run" , "exit"}
States == { "start", "idle", "editing", "running"}
CheckIfUpdated(u) == IF ( user_state[u] = "start" \/ user_state[u] = "running") \/ flow_state="updated"
THEN TRUE
ELSE FALSE
EventuallyConsistent == (\A u \in Users:
(CheckIfUpdated(u) = TRUE))
WriteToUserQueue(u) == IF queues[u] /= "terminated"
THEN Append(queues[u], "changed")
ELSE queues
end define
macro get_flow_data(result) begin
result := CHOOSE d \in Data: TRUE;
end macro;
macro broadcast_change() begin
queues := [u \in Users |-> WriteToUserQueue(u)];
end macro;
macro at_least_one_active_user() begin
end macro
process user \in Users
variables
result = NULL;
input = "none";
begin
execute:
while (user_state[self] /= "terminated") do
if input = "exit" then
terminate:
flow_state[self] := "updated";
user_state[self] := "terminated";
(*
elsif user_state[self] = "terminated" then
either user_state[self] := "start";
or user_state[self] := "terminated";
end either; *)
elsif user_state[self] = "start" then
start:
get_flow_data(result);
user_state[self] := "idle";
elsif user_state[self] = "idle" then
idle:
if Len(queues[self]) > 0 then
queues[self] := Tail(queues[self]);
flow_state[self] := "updated";
elsif input = "start_edit" then
user_state[self] := "editing";
elsif input = "start_run" then
user_state[self] := "running";
else
either input := "start_edit"
or input:="start_run";
or input := "exit";
end either;
end if;
elsif user_state[self] = "editing" then
editing:
if Len(queues[self]) > 0 then
queues[self] := Tail(queues[self]);
flow_state[self] := "updated";
elsif input = "end_edit" then
broadcast_change();
user_state[self] := "idle";
else
either input := "end_edit";
(* or input := "none" *)
or input :="exit";
end either;
end if;
elsif user_state[self] = "running" then
running:
if input = "end_run" then
user_state[self] := "idle";
else
either input := "end_run";
or input := "none";
end either;
end if
else
user_state[self] := "idle";
end if;
end while;
end process
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "f21b3a52" /\ chksum(tla) = "159fc027")
VARIABLES queues, flow_state, user_state, pc
(* define statement *)
Inputs == { "none","start_edit", "end_edit", "start_run", "end_run" , "exit"}
States == { "start", "idle", "editing", "running"}
CheckIfUpdated(u) == IF ( user_state[u] = "start" \/ user_state[u] = "running") \/ flow_state="updated"
THEN TRUE
ELSE FALSE
EventuallyConsistent == (\A u \in Users:
(CheckIfUpdated(u) = TRUE))
WriteToUserQueue(u) == IF queues[u] /= "terminated"
THEN Append(queues[u], "changed")
ELSE queues
VARIABLES result, input
vars == << queues, flow_state, user_state, pc, result, input >>
ProcSet == (Users)
Init == (* Global variables *)
/\ queues = [u \in Users |-> <<>>]
/\ flow_state = [ u \in Users |-> "changed"]
/\ user_state = [ u \in Users |-> "start"]
(* Process user *)
/\ result = [self \in Users |-> NULL]
/\ input = [self \in Users |-> "none"]
/\ pc = [self \in ProcSet |-> "execute"]
execute(self) == /\ pc[self] = "execute"
/\ IF (user_state[self] /= "terminated")
THEN /\ IF input[self] = "exit"
THEN /\ pc' = [pc EXCEPT ![self] = "terminate"]
/\ UNCHANGED user_state
ELSE /\ IF user_state[self] = "start"
THEN /\ pc' = [pc EXCEPT ![self] = "start"]
/\ UNCHANGED user_state
ELSE /\ IF user_state[self] = "idle"
THEN /\ pc' = [pc EXCEPT ![self] = "idle"]
/\ UNCHANGED user_state
ELSE /\ IF user_state[self] = "editing"
THEN /\ pc' = [pc EXCEPT ![self] = "editing"]
/\ UNCHANGED user_state
ELSE /\ IF user_state[self] = "running"
THEN /\ pc' = [pc EXCEPT ![self] = "running"]
/\ UNCHANGED user_state
ELSE /\ user_state' = [user_state EXCEPT ![self] = "idle"]
/\ pc' = [pc EXCEPT ![self] = "execute"]
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED user_state
/\ UNCHANGED << queues, flow_state, result, input >>
terminate(self) == /\ pc[self] = "terminate"
/\ flow_state' = [flow_state EXCEPT ![self] = "updated"]
/\ user_state' = [user_state EXCEPT ![self] = "terminated"]
/\ pc' = [pc EXCEPT ![self] = "execute"]
/\ UNCHANGED << queues, result, input >>
start(self) == /\ pc[self] = "start"
/\ result' = [result EXCEPT ![self] = CHOOSE d \in Data: TRUE]
/\ user_state' = [user_state EXCEPT ![self] = "idle"]
/\ pc' = [pc EXCEPT ![self] = "execute"]
/\ UNCHANGED << queues, flow_state, input >>
idle(self) == /\ pc[self] = "idle"
/\ IF Len(queues[self]) > 0
THEN /\ queues' = [queues EXCEPT ![self] = Tail(queues[self])]
/\ flow_state' = [flow_state EXCEPT ![self] = "updated"]
/\ UNCHANGED << user_state, input >>
ELSE /\ IF input[self] = "start_edit"
THEN /\ user_state' = [user_state EXCEPT ![self] = "editing"]
/\ input' = input
ELSE /\ IF input[self] = "start_run"
THEN /\ user_state' = [user_state EXCEPT ![self] = "running"]
/\ input' = input
ELSE /\ \/ /\ input' = [input EXCEPT ![self] = "start_edit"]
\/ /\ input' = [input EXCEPT ![self] = "start_run"]
\/ /\ input' = [input EXCEPT ![self] = "exit"]
/\ UNCHANGED user_state
/\ UNCHANGED << queues, flow_state >>
/\ pc' = [pc EXCEPT ![self] = "execute"]
/\ UNCHANGED result
editing(self) == /\ pc[self] = "editing"
/\ IF Len(queues[self]) > 0
THEN /\ queues' = [queues EXCEPT ![self] = Tail(queues[self])]
/\ flow_state' = [flow_state EXCEPT ![self] = "updated"]
/\ UNCHANGED << user_state, input >>
ELSE /\ IF input[self] = "end_edit"
THEN /\ queues' = [u \in Users |-> WriteToUserQueue(u)]
/\ user_state' = [user_state EXCEPT ![self] = "idle"]
/\ input' = input
ELSE /\ \/ /\ input' = [input EXCEPT ![self] = "end_edit"]
\/ /\ input' = [input EXCEPT ![self] = "exit"]
/\ UNCHANGED << queues, user_state >>
/\ UNCHANGED flow_state
/\ pc' = [pc EXCEPT ![self] = "execute"]
/\ UNCHANGED result
running(self) == /\ pc[self] = "running"
/\ IF input[self] = "end_run"
THEN /\ user_state' = [user_state EXCEPT ![self] = "idle"]
/\ input' = input
ELSE /\ \/ /\ input' = [input EXCEPT ![self] = "end_run"]
\/ /\ input' = [input EXCEPT ![self] = "none"]
/\ UNCHANGED user_state
/\ pc' = [pc EXCEPT ![self] = "execute"]
/\ UNCHANGED << queues, flow_state, result >>
user(self) == execute(self) \/ terminate(self) \/ start(self) \/ idle(self)
\/ editing(self) \/ running(self)
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == (\E self \in Users: user(self))
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
=============================================================================
\* Modification History
\* Last modified Tue Sep 20 09:08:56 IST 2022 by anand.k...@xxxxxxxxxxx
\* Created Thu Sep 15 10:56:26 IST 2022 by anand.k...@xxxxxxxxxxx
If you see in state 14:
_TEAction |-> [
position |-> 14,
name |-> "terminate",
location |-> "line 168, col 20 to line 172, col 59 of module multiuser_flows"
],
flow_state |-> [u1 |-> "updated", u2 |-> "updated"],
input |-> [u1 |-> "exit", u2 |-> "exit"],
pc |-> [u1 |-> "Done", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "a"],
user_state |-> [u1 |-> "terminated", u2 |-> "terminated"]
user_state for both u1 and u2 is "terminated".
Shouldn't the model terminate? why is it stuttering?
Thanks for your help in advance
<<
[
_TEAction |-> [
position |-> 1,
name |-> "Initial predicate",
location |-> "Unknown location"
],
flow_state |-> [u1 |-> "changed", u2 |-> "changed"],
input |-> [u1 |-> "none", u2 |-> "none"],
pc |-> [u1 |-> "execute", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "null", u2 |-> "null"],
user_state |-> [u1 |-> "start", u2 |-> "start"]
],
[
_TEAction |-> [
position |-> 2,
name |-> "execute",
location |-> "line 145, col 18 to line 166, col 69 of module multiuser_flows"
],
flow_state |-> [u1 |-> "changed", u2 |-> "changed"],
input |-> [u1 |-> "none", u2 |-> "none"],
pc |-> [u1 |-> "start", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "null", u2 |-> "null"],
user_state |-> [u1 |-> "start", u2 |-> "start"]
],
[
_TEAction |-> [
position |-> 3,
name |-> "start",
location |-> "line 174, col 16 to line 178, col 59 of module multiuser_flows"
],
flow_state |-> [u1 |-> "changed", u2 |-> "changed"],
input |-> [u1 |-> "none", u2 |-> "none"],
pc |-> [u1 |-> "execute", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "null"],
user_state |-> [u1 |-> "idle", u2 |-> "start"]
],
[
_TEAction |-> [
position |-> 4,
name |-> "execute",
location |-> "line 145, col 18 to line 166, col 69 of module multiuser_flows"
],
flow_state |-> [u1 |-> "changed", u2 |-> "changed"],
input |-> [u1 |-> "none", u2 |-> "none"],
pc |-> [u1 |-> "idle", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "null"],
user_state |-> [u1 |-> "idle", u2 |-> "start"]
],
[
_TEAction |-> [
position |-> 5,
name |-> "idle",
location |-> "line 180, col 15 to line 197, col 33 of module multiuser_flows"
],
flow_state |-> [u1 |-> "changed", u2 |-> "changed"],
input |-> [u1 |-> "exit", u2 |-> "none"],
pc |-> [u1 |-> "execute", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "null"],
user_state |-> [u1 |-> "idle", u2 |-> "start"]
],
[
_TEAction |-> [
position |-> 6,
name |-> "execute",
location |-> "line 145, col 18 to line 166, col 69 of module multiuser_flows"
],
flow_state |-> [u1 |-> "changed", u2 |-> "changed"],
input |-> [u1 |-> "exit", u2 |-> "none"],
pc |-> [u1 |-> "terminate", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "null"],
user_state |-> [u1 |-> "idle", u2 |-> "start"]
],
[
_TEAction |-> [
position |-> 7,
name |-> "terminate",
location |-> "line 168, col 20 to line 172, col 59 of module multiuser_flows"
],
flow_state |-> [u1 |-> "updated", u2 |-> "changed"],
input |-> [u1 |-> "exit", u2 |-> "none"],
pc |-> [u1 |-> "execute", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "null"],
user_state |-> [u1 |-> "terminated", u2 |-> "start"]
],
[
_TEAction |-> [
position |-> 8,
name |-> "execute",
location |-> "line 145, col 18 to line 166, col 69 of module multiuser_flows"
],
flow_state |-> [u1 |-> "updated", u2 |-> "changed"],
input |-> [u1 |-> "exit", u2 |-> "none"],
pc |-> [u1 |-> "Done", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "null"],
user_state |-> [u1 |-> "terminated", u2 |-> "start"]
],
[
_TEAction |-> [
position |-> 9,
name |-> "execute",
location |-> "line 145, col 18 to line 166, col 69 of module multiuser_flows"
],
flow_state |-> [u1 |-> "updated", u2 |-> "changed"],
input |-> [u1 |-> "exit", u2 |-> "none"],
pc |-> [u1 |-> "Done", u2 |-> "start"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "null"],
user_state |-> [u1 |-> "terminated", u2 |-> "start"]
],
[
_TEAction |-> [
position |-> 10,
name |-> "start",
location |-> "line 174, col 16 to line 178, col 59 of module multiuser_flows"
],
flow_state |-> [u1 |-> "updated", u2 |-> "changed"],
input |-> [u1 |-> "exit", u2 |-> "none"],
pc |-> [u1 |-> "Done", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "a"],
user_state |-> [u1 |-> "terminated", u2 |-> "idle"]
],
[
_TEAction |-> [
position |-> 11,
name |-> "execute",
location |-> "line 145, col 18 to line 166, col 69 of module multiuser_flows"
],
flow_state |-> [u1 |-> "updated", u2 |-> "changed"],
input |-> [u1 |-> "exit", u2 |-> "none"],
pc |-> [u1 |-> "Done", u2 |-> "idle"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "a"],
user_state |-> [u1 |-> "terminated", u2 |-> "idle"]
],
[
_TEAction |-> [
position |-> 12,
name |-> "idle",
location |-> "line 180, col 15 to line 197, col 33 of module multiuser_flows"
],
flow_state |-> [u1 |-> "updated", u2 |-> "changed"],
input |-> [u1 |-> "exit", u2 |-> "exit"],
pc |-> [u1 |-> "Done", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "a"],
user_state |-> [u1 |-> "terminated", u2 |-> "idle"]
],
[
_TEAction |-> [
position |-> 13,
name |-> "execute",
location |-> "line 145, col 18 to line 166, col 69 of module multiuser_flows"
],
flow_state |-> [u1 |-> "updated", u2 |-> "changed"],
input |-> [u1 |-> "exit", u2 |-> "exit"],
pc |-> [u1 |-> "Done", u2 |-> "terminate"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "a"],
user_state |-> [u1 |-> "terminated", u2 |-> "idle"]
],
[
_TEAction |-> [
position |-> 14,
name |-> "terminate",
location |-> "line 168, col 20 to line 172, col 59 of module multiuser_flows"
],
flow_state |-> [u1 |-> "updated", u2 |-> "updated"],
input |-> [u1 |-> "exit", u2 |-> "exit"],
pc |-> [u1 |-> "Done", u2 |-> "execute"],
queues |-> [u1 |-> <<>>, u2 |-> <<>>],
result |-> [u1 |-> "a", u2 |-> "a"],
user_state |-> [u1 |-> "terminated", u2 |-> "terminated"]
]
>>