Number of possible behaviors and fairness

[jack malkovick]

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?

[Andrew Helwer]

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

[jack malkovick]

The problem is that after action C I want to check some temporal property (something like <>MyProperty). So I need for C to always happen at some point.

But if I can get an infinite number of behaviours like AB....BBA + C, I'm not sure how can I check this. When do I stop the checker? How am I sure that C happened?

[Andrew Helwer]

To be clear is your state space finite or infinite? You can only perform liveness checking on a finite state space with no state constraints.

If you want to check that eventually C occurs and that this eventually leads to some other property being true, I think you have to add another state variable like didCHappen \in BOOLEAN which is initialized to FALSE then set to TRUE once a C step occurs. Then the property you're looking for becomes:

  /\ <>didCHappen

  /\ didCHappen ~> MyProperty

Andrew

[jack malkovick]

Yes, it's infinite and it needs limiting. You were right, I guess the only way is to compromise the model and check in fact some derived finite space state spec.