[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] ripetitive incorrect send

Hi, i have two processes with in the body a while true an inside that a part of the code is the following:


                await data # "null" /\ componentState[self]="processing";

                either \* correct transmission


                    intermediateQueue := intermediateQueue \union {data};


                or \* transmission error



                    goto transmissionToKafka;

                end either;

checking that the messages are correctly trnasmitted from an initial set to a second set (intermediateQueue) TLC gives me error with the following trace:


1 -> transmissionToKafka

2 -> transmissionToKafka

step +1 pc:

1 -> incorrectSend

2 -> transmissionToKafka

step+1 pc:

1 -> transmissionToKafka

2 -> transmissionToKafka

step+1 pc:

1 -> transmissionToKaka

2 -> incorrectSend 

return to the initial state

shouldn't this problem be solved using strong fairness of the processes? I defined my processes as fair+ but the problem persists

could someone help? thanks

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/f735e5b2-8c89-450b-bfd7-293e16193d79n%40googlegroups.com.