Re: [tlaplus] How to add an auxiliary variable but not increase the state space?

[Guo Hua <fchdir@xxxxxxxxx>]

Thank you for the answer. Using view solves the problem.

On Tuesday, November 8, 2022 at 10:31:30 PM UTC+8 Leslie Lamport wrote:

Forget what I just wrote.  I don't know where my brain was when I wrote it.  Yes, use view.

Leslie

On Tuesday, November 8, 2022 at 6:23:25 AM UTC-8 Leslie Lamport wrote:

Changing the view won't hurt.  But a history variable h is generally added by conjoining to each action a formula of the form h' = ... .  Doing that doesn't add any states; it just adds a new component to each state.  That shouldn't significantly increase TLC's running time, and little of any increase in running time will be saved by the view change.

Leslie

On Tuesday, November 8, 2022 at 1:48:28 AM UTC-8 hwa...@xxxxxxxxx wrote:

You'll want to define a custom VIEW, see https://learntla.com/topics/toolbox.html#additional-tlc-options

On Tue, Nov 8, 2022, 9:54 AM Guo Hua <fch...@xxxxxxxxx> wrote:

In TLA+, when I add my auxiliary variable "history," the specification behaviors depend on the  "history" variable, and the state space would increase.
Can I specify the specification next state behavior does not depend on the auxiliary variable, and the additional variable does not increase the state space?

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/17e51ae3-1f1b-48df-bcaa-5f8474412ed5n%40googlegroups.com.

-- 
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/d2e93eae-d3d1-4374-9200-09382abe2199n%40googlegroups.com.