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?

[Guo Hua]

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 )

Thanks

Hua

[Guo Hua]

Also, I thought, can I simply achieve this by adding OperatorX to Invariants?

[Andrew Helwer]

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!

Andrew

[Guo Hua]

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

[Markus Kuppe]

TLC exposes TLCGet(“distinct”) among other statistics [1].

Markus

[1] https://lamport.azurewebsites.net/tla/current-tools.pdf

[Guo Hua]

Thank you for your reply.  I got it.

[Akash]

I'm a beginner to TLA+, so I may be wrong, but, I think you are referring to "leads to" in temporal logic.

F squiggly arrow G.

If F is true then eventually G must be true. 

Then you can apply this concept to your operator and make it nested.

Kind regards,

Akash

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/abdbce77-89f5-4964-8151-75946c390b37n%40googlegroups.com.