[tlaplus] Re: Number of possible behaviors and fairness

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

It is but it might compromise your model. Suppose your module with actions A, B, and C is called MySpec. You might create a module called MCMySpec that looks similar to the following:

------------------------------- MODULE MCMySpec -----------------------------

EXTENDS Naturals

CONSTANT OtherActionLimit
VARIABLE otherActionCount

S == INSTANCE MySpec

Init ==
    /\ otherActionCount = 0
    /\ S!Init

OtherAction ==
    /\ otherActionCount < OtherActionLimit
    /\ otherActionCount' = otherActionCount + 1
    /\  \/ S!A
        \/ S!B

Action ="">    /\ S!C

Next ==
    \/ OtherAction
    \/ Action

Spec ==
    /\ Init
    /\ S!Init

=============================================================================

However, I doubt this will be very useful for demonstrating liveness properties which by definition reason over behaviors of infinite length. Are you running into an issue with your liveness checks taking too long?

Andrew

On Wednesday, March 2, 2022 at 2:38:58 AM UTC-5 jack malkovick wrote:

Hello. Suppose we have a spec that allows A, B and C actions.

Next == A \/ B \/ C

All are always enabled but we want for C to be executed at some point in all behaviors. It is my understanding that the Spec should be something like

Spec == Init /\ [][Next]_vars /\ WF_vars(Next) /\ WF_vars(C)

The question is, how could we limit the number of possible behaviors that is processed?

A level based state constraint would work, but I don't think we get a guarantee that C will execute if we "cut" the behavior by level. We basically need to limit the number, of A, B behaviors until the first C... It this possible?

-- 
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/6c41ee50-4d69-4077-8337-a2f7f66c1bb2n%40googlegroups.com.