[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 :

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.