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