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

*From*: Guo Hua <fchdir@xxxxxxxxx>*Date*: Fri, 8 Dec 2023 03:31:13 -0800 (PST)*References*: <0587c5ac-dabc-42d1-9914-e96b3e43b0c3n@googlegroups.com> <0856582c-74af-43c7-bb30-acdefaf2b590n@googlegroups.com> <e3dfaa78-3d81-4463-8fdd-afc213c62c30n@googlegroups.com>

Thank you for your reply.

However, I am sorry for not describing it clearly.

What I said was "generating distinct new states in the entire search space of TLC model checking", rather than "not changing the value of variables".

Hua

On Sunday, December 3, 2023 at 10:26:31 PM UTC+8 Andrew Helwer wrote:

Here's my attempt:---- MODULE Test ----

EXTENDS TLC

VARIABLES a, b, c

Vars == <<a, b, c>>

TypeOK ==

/\ a \in BOOLEAN

/\ b \in BOOLEAN

/\ c \in BOOLEAN

GeneratesNewState == Vars' /= Vars

SomeAction(msg) == Print(msg, TRUE)

Action1 == UNCHANGED Vars

Action2 ==

/\ a' = ~a

/\ b' = ~b

/\ c' = ~c

Init ==

/\ a = TRUE

/\ b = TRUE

/\ c = TRUE

Next ==

\/ /\ Action1

/\ GeneratesNewState => SomeAction("Action1")

\/ /\ Action2

/\ GeneratesNewState => SomeAction("Action2")

Spec ==

/\ Init

/\ [][Next]_Vars

====If you run TLC on this it will print "Action2" but never "Action1". Note how the prime operator distributes over the variables in Vars; a neat feature!AndrewOn Sunday, December 3, 2023 at 2:41:35 AM UTC-5 Guo Hua wrote:Also, I thought, can I simply achieve this by adding OperatorX to Invariants?On Sunday, December 3, 2023 at 3:00:17 PM UTC+8 Guo Hua wrote:Does TLA+ have a feature where a certain operator is true if and only if a new, different state is produced in the next action?If there are no built-in features like this, could I write new overriding operators or modules to implement this? I need some tips.Just like in the following example,OperatorX is true if and only if Next produces a new state. In this case, OperatorX cannot change the state and does not have prime operators.Next ==

/\ (\/ Next1

\/ Next2)

/\ (NextCanProduceNewState => OperatorX )ThanksHua

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/58808b68-abcf-4078-9594-7046cb225f86n%40googlegroups.com.

**Follow-Ups**:

**References**:**[tlaplus] Does TLA+ have a feature where a certain operator is true if and only if a new, different state is produced in the next action?***From:*Guo Hua

**[tlaplus] Re: Does TLA+ have a feature where a certain operator is true if and only if a new, different state is produced in the next action?***From:*Guo Hua

**[tlaplus] Re: Does TLA+ have a feature where a certain operator is true if and only if a new, different state is produced in the next action?***From:*Andrew Helwer

- Prev by Date:
**[tlaplus] Re: TLA+ specifications request for project** - Next by Date:
**Re: [tlaplus] Does TLA+ have a feature where a certain operator is true if and only if a new, different state is produced in the next action?** - Previous by thread:
**[tlaplus] Re: Does TLA+ have a feature where a certain operator is true if and only if a new, different state is produced in the next action?** - Next by thread:
**Re: [tlaplus] Does TLA+ have a feature where a certain operator is true if and only if a new, different state is produced in the next action?** - Index(es):