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

[tlaplus] Number of possible behaviors and fairness

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/db84cfb8-a73a-4c53-b4ac-58be20addc1dn%40googlegroups.com.