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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Wed, 2 Mar 2022 06:20:24 -0800 (PST)*References*: <db84cfb8-a73a-4c53-b4ac-58be20addc1dn@googlegroups.com>

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

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

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 \/ CAll 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 likeSpec == Init /\ [][Next]_vars /\ WF_vars(Next) /\ WF_vars(C)The question is, how could we limit the number of possible behaviors that is processed?Alevelbased 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.

**Follow-Ups**:**[tlaplus] Re: Number of possible behaviors and fairness***From:*jack malkovick

**References**:**[tlaplus] Number of possible behaviors and fairness***From:*jack malkovick

- Prev by Date:
**[tlaplus] Number of possible behaviors and fairness** - Next by Date:
**[tlaplus] Re: Number of possible behaviors and fairness** - Previous by thread:
**[tlaplus] Number of possible behaviors and fairness** - Next by thread:
**[tlaplus] Re: Number of possible behaviors and fairness** - Index(es):