SendMessage( blockId, channel) ==
Append(channel, blockId)
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
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.StephanOn 11 Aug 2022, at 12:31, Anand Kumar <akkes...@xxxxxxxxx> wrote:TLC generates this error>There is also a warning that "writeOutputs" is never enabledelsif 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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d5459d87-f821-4f36-929c-e09a302436b7n%40googlegroups.com.