Evaluating an expression of the form t \o s when s is not a string: <<>>
Anand Kumar
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 >>
Stephan Merz
--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d5459d87-f821-4f36-929c-e09a302436b7n%40googlegroups.com.
Anand Kumar
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
Stephan Merz
On 12 Aug 2022, at 04:01, Anand Kumar <akkes...@gmail.com> wrote:SendMessage is defined as follows:SendMessage( blockId, channel) ==
Append(channel, blockId)
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/710147f8-1d58-40da-98ac-308137b61685n%40googlegroups.com.