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

[Anand Kumar <akkeshavan@xxxxxxxxx>]

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.