ripetitive incorrect send

19 views
Skip to first unread message

p.to...@studenti.unipi.it

unread,
Jun 13, 2021, 9:46:34 AMJun 13
to tlaplus
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

Stephan Merz

unread,
Jun 13, 2021, 12:52:49 PMJun 13
to tla...@googlegroups.com
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


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

p.to...@studenti.unipi.it

unread,
Jun 13, 2021, 3:08:14 PMJun 13
to tlaplus
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="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

Stephan Merz

unread,
Jun 14, 2021, 2:37:54 AMJun 14
to tla...@googlegroups.com
Is correctReceive ever enabled in the counter-example? The await condition in receiveData clearly ensures the condition inputQueue # {} but what about the second conjunct? Also, comparing tmpTakenInput for equality to a set of ten messages looks suspicious, perhaps you meant to write "tmpTakenInput \notin ..."?

Getting fairness conditions right is difficult, and I suggest you start by considering simpler algorithms.

Stephan

Reply all
Reply to author
Forward
0 new messages