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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Wed, 2 Mar 2022 09:22:18 -0800 (PST)*References*: <db84cfb8-a73a-4c53-b4ac-58be20addc1dn@googlegroups.com> <6c41ee50-4d69-4077-8337-a2f7f66c1bb2n@googlegroups.com> <d19450d9-714a-42b0-b785-4c6f2957f90cn@googlegroups.com>

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

On Wednesday, March 2, 2022 at 9:30:27 AM UTC-5 jack malkovick wrote:

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?On Wednesday, March 2, 2022 at 4:20:25 PM UTC+2 andrew...@xxxxxxxxx wrote: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?AndrewOn 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/26cb5a84-f479-458d-8104-d1239703c2acn%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

**[tlaplus] Re: Number of possible behaviors and fairness***From:*Andrew Helwer

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

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