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?