Please inspect the TLA+ specification generated for your PlusCal algorithm: strong fairness for processes generates a conjunct of the form
\A self \in Procs : SF_vars(proc(self))
where proc(self) is a disjunction that includes disjuncts for transmissionToKafka(self), correctSend(self), and incorrectSend(self). Since infinitely many proc(self) steps occur, the counter-example generated by TLC is fair.
The simple fix is to remove fairness for incorrectSend (since clearly you do not mean to assert a fairness condition for transmission error) by writing
incorrectSend:-
Should you want to assert fairness for two actions in conflict (such as correctSend and incorrectSend), you would have to write
/\ \A self \in Procs : SF_vars(correctSend(self)) /\ \A self \in Procs : SF_vars(incorrectSend(self))
This condition would have to be written in TLA+, the PlusCal translator will not generate it for you.
Regards, Stephan
Hi, i have two processes with in the body a while true an inside that a part of the code is the following:
transmissionToKafka: await data # "null" /\ componentState[self]="processing"; either \* correct transmission correctSend: intermediateQueue := intermediateQueue \union {data}; componentState[self]:="processed"; or \* transmission error incorrectSend: skip; 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: pc: 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.
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/13814DBE-4382-4CAD-A523-19D6BA7DD8DC%40gmail.com.
|