Re: [tlaplus] Evaluating an expression of the form t \o s when s is not a string: <<>>

On Friday, 12 August 2022 at 12:10:59 UTC+5:30 Stephan Merz wrote:

Hello,

On 12 Aug 2022, at 04:01, Anand Kumar <akkes...@xxxxxxxxx> wrote:

SendMessage is defined as follows:

SendMessage( blockId, channel) ==
  Append(channel, blockId)
OK, but it is used as

SendMessage(Channel,Blocks[self].outputs[index])

Aren't the two parameters reversed?

Stephan

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.

Stephan

On 11 Aug 2022, at 12:31, Anand Kumar <akkes...@xxxxxxxxx> wrote:

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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d5459d87-f821-4f36-929c-e09a302436b7n%40googlegroups.com.

--
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/710147f8-1d58-40da-98ac-308137b61685n%40googlegroups.com.