Here is the full spec:
EXTENDS Integers, Sequences, TLC
CONSTANTS MaxChannelSize
RemoveMessagesForBlock(block, channel) ==
[j \in 1..(Len(channel)-1) |-> IF block.id = channel[j] THEN channel[j+1]
ELSE channel[j]]
BlockHasMessages(block, channel) ==
\E message \in channel : block.id = message
SendMessage( blockId, channel) ==
Append(channel, blockId)
(*--algorithm flow
variables
StateSet = { "waiting", "processing", "end"};
Blocks = [
a |-> [ id |-> "a", state |-> "waiting", inputs |->0, outputs|-> <<"b","c">>],
b |-> [ id |-> "b", state |-> "waiting", inputs |->1, outputs|-> <<"c","d">>],
c |-> [ id |-> "c", state |-> "waiting", inputs |->2, outputs|-> <<"d">>],
d |-> [ id |-> "d", state |-> "waiting", inputs |->2, outputs|-> <<>>]
];
Channel = <<>>;
define
BoundedQueue == Len(Channel) <= MaxChannelSize
TypeOK ==
\A block \in Blocks: block.state \in StateSet
EventuallyTerminates ==
<>[] \A block \in Blocks: block.state = "end"
end define;
process blockDefs \in {"a", "b", "c", "d"}
variables
index =1;
begin execute:
while Blocks[self].state /= "end" do
if Blocks[self].state = "waiting" /\ Blocks[self].inputs = 0 then
Blocks[self].state := "processing";
elsif Blocks[self].state ="waiting" /\ Blocks[self].inputs >0 then
waitInput:
if BlockHasMessages(Blocks[self],Channel) then
Channel := RemoveMessagesForBlock(Blocks[self],Channel);
Blocks[self].state := "processing";
else
skip;
end if;
elsif Blocks[self].state = "processing" then
writeOutputs:
while index < Len(Blocks[self].outputs) do
Channel := SendMessage(Channel,Blocks[self].outputs[index]);
index := index+1;
end while;
end_state:
Blocks[self].state := "end";
else
skip;
end if;
end while;
end process;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "24e11c4a" /\ chksum(tla) = "22972279")
VARIABLES StateSet, Blocks, Channel, pc
(* define statement *)
BoundedQueue == Len(Channel) <= MaxChannelSize
TypeOK ==
\A block \in Blocks: block.state \in StateSet
EventuallyTerminates ==
<>[] \A block \in Blocks: block.state = "end"
VARIABLE index
vars == << StateSet, Blocks, Channel, pc, index >>
ProcSet == ({"a", "b", "c", "d"})
Init == (* Global variables *)
/\ StateSet = { "waiting", "processing", "end"}
/\ Blocks = [
a |-> [ id |-> "a", state |-> "waiting", inputs |->0, outputs|-> <<"b","c">>],
b |-> [ id |-> "b", state |-> "waiting", inputs |->1, outputs|-> <<"c","d">>],
c |-> [ id |-> "c", state |-> "waiting", inputs |->2, outputs|-> <<"d">>],
d |-> [ id |-> "d", state |-> "waiting", inputs |->2, outputs|-> <<>>]
]
/\ Channel = <<>>
(* Process blockDefs *)
/\ index = [self \in {"a", "b", "c", "d"} |-> 1]
/\ pc = [self \in ProcSet |-> "execute"]
execute(self) == /\ pc[self] = "execute"
/\ IF Blocks[self].state /= "end"
THEN /\ IF Blocks[self].state = "waiting" /\ Blocks[self].inputs = 0
THEN /\ Blocks' = [Blocks EXCEPT ![self].state = "processing"]
/\ pc' = [pc EXCEPT ![self] = "execute"]
ELSE /\ IF Blocks[self].state ="waiting" /\ Blocks[self].inputs >0
THEN /\ pc' = [pc EXCEPT ![self] = "waitInput"]
ELSE /\ IF Blocks[self].state = "processing"
THEN /\ pc' = [pc EXCEPT ![self] = "writeOutputs"]
ELSE /\ TRUE
/\ pc' = [pc EXCEPT ![self] = "execute"]
/\ UNCHANGED Blocks
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED Blocks
/\ UNCHANGED << StateSet, Channel, index >>
waitInput(self) == /\ pc[self] = "waitInput"
/\ IF BlockHasMessages(Blocks[self],Channel)
THEN /\ Channel' = RemoveMessagesForBlock(Blocks[self],Channel)
/\ Blocks' = [Blocks EXCEPT ![self].state = "processing"]
ELSE /\ TRUE
/\ UNCHANGED << Blocks, Channel >>
/\ pc' = [pc EXCEPT ![self] = "execute"]
/\ UNCHANGED << StateSet, index >>
writeOutputs(self) == /\ pc[self] = "writeOutputs"
/\ IF index[self] < Len(Blocks[self].outputs)
THEN /\ Channel' = SendMessage(Channel,Blocks[self].outputs[index[self]])
/\ index' = [index EXCEPT ![self] = index[self]+1]
/\ pc' = [pc EXCEPT ![self] = "writeOutputs"]
ELSE /\ pc' = [pc EXCEPT ![self] = "end_state"]
/\ UNCHANGED << Channel, index >>
/\ UNCHANGED << StateSet, Blocks >>
end_state(self) == /\ pc[self] = "end_state"
/\ Blocks' = [Blocks EXCEPT ![self].state = "end"]
/\ pc' = [pc EXCEPT ![self] = "execute"]
/\ UNCHANGED << StateSet, Channel, index >>
blockDefs(self) == execute(self) \/ waitInput(self) \/ writeOutputs(self)
\/ end_state(self)
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == (\E self \in {"a", "b", "c", "d"}: blockDefs(self))
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
On Thursday, 11 August 2022 at 17:45:53 UTC+5:30 Stephan Merz wrote:
Since you do not show your full spec, I can only make a guess on what is going on here. It looks like Channel is a sequence, and you are trying to send some data item on that channel. In that case, SendMessage(ch, d) should be defined as Append(ch, d), not as ch \o d, since \o represents sequence concatenation.
TLC generates this error>
There is also a warning that "writeOutputs" is never enabled
elsif Blocks[self].state = "processing" then
writeOutputs:
while index < Len(Blocks[self].outputs) do
Channel := SendMessage(Channel,Blocks[self].outputs[index]);
index := index+1;
end while;
>>> generated TLA code
writeOutputs(self) == /\ pc[self] = "writeOutputs"
/\ IF index[self] < Len(Blocks[self].outputs)
THEN /\ Channel' = SendMessage(Channel,Blocks[self].outputs[index[self]])
/\ index' = [index EXCEPT ![self] = index[self]+1]
/\ pc' = [pc EXCEPT ![self] = "writeOutputs"]
ELSE /\ pc' = [pc EXCEPT ![self] = "end_state"]
/\ UNCHANGED << Channel, index >>
/\ UNCHANGED << StateSet, Blocks >>
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/710147f8-1d58-40da-98ac-308137b61685n%40googlegroups.com.