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

Re: [tlaplus] ripetitive incorrect send

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 :


        while TRUE do


                await inputQueue # {} /\ componentState[self]="ready" /\ data="" ;

                either \* correct transmission


                    if inputQueue # {} /\ tmpTakenInput # {"message1", "message2", "message3", "message4", "message5", "message6", "message7", "message8", "message9", "message10"} then

                        data := CHOOSE x \in inputQueue : x \notin tmpTakenInput; 


                        tmpTakenInput := tmpTakenInput \union {data};



                        goto receiveData;

                    end if;

                or \* transmission error


                    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


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.


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:


                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+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.