Re: [tlaplus] ripetitive incorrect send

Stephan

On 13 Jun 2021, at 21:08, p.to...@xxxxxxxxxxxxxxxxx <p.tollot@xxxxxxxxxxxxxxxxx> wrote:

Thanks for answering, now is more clear but still I have the problem, at a different point but it is substantially the same

for the following spec :
stateMachine:
while TRUE do
receiveData:
await inputQueue # {} /\ componentState[self]="ready" /\ data="" ;
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

Il giorno domenica 13 giugno 2021 alle 18:52:49 UTC+2 Stephan Merz ha scritto:
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

On 13 Jun 2021, at 15:46, p.to...@xxxxxxxxxxxxxxxxx <p.to...@xxxxxxxxxxxxxxxxx> wrote:

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+u...@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/ca59de39-ed3d-45e3-86bc-ac7ce3296665n%40googlegroups.com.