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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f735e5b2-8c89-450b-bfd7-293e16193d79n%40googlegroups.com.
stateMachine:
while TRUE do
receiveData:
await inputQueue # {} /\ componentState[self]="ready" /\ data="null" ;
either \* correct transmission
correctReceive:
if inputQueue # {} /\ tmpTakenInput # {"message1", "message2", "message3", "message4", "message5", "message6", "message7", "message8", "message9", "message10"} then
data := CHOOSE x \in inputQueue : x \notin tmpTakenInput;
componentState[self]:="processing";
tmpTakenInput := tmpTakenInput \union {data};
else
skip;
goto receiveData;
end if;
or \* transmission error
incorrectReceive:
data := "null";
goto receiveData;
end either;
TLC iterate over "receiveData" and "incorrectReceive" for the two processes,
i have written in the TLA+ spec the Strong fairness as:
/\ \A self \in {"ingress1", "ingress2"} : SF_vars(correctReceive(self))
also with putting incorrectReceive:-(if i have understood well it shouldn't be necessary with the above definition of fairness) the problem persists
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ca59de39-ed3d-45e3-86bc-ac7ce3296665n%40googlegroups.com.