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

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 <akkeshavan@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+unsubscribe@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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/34152EC3-A5F6-4265-8643-CF5BAE8D2C2E%40gmail.com.