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

*From*: Vic Putz <vbputz@xxxxxxxxx>*Date*: Wed, 25 Nov 2020 18:06:52 -0800 (PST)*References*: <df467f71-77d1-4bed-a83c-d126d5da226fn@googlegroups.com> <32D3FDF4-6067-44C3-97E3-77595B362A48@gmail.com> <1db3377c-78a4-3e97-5f16-76bc701ca3f1@lemmster.de>

Aha! Thanks, Stephan; I had noticed when I evaluated CHOOSE in TLC it seemed to come up with the same function every time, but I had thought that in a "proper" simulation it behaved like \in and represented a state branch over all possibilities. I should be set with whatever it picks, though (this is a bit of a toy problem in the sense that this round I'm mostly using TLA+ for the exercise of writing things down rather than exploring the state space, but your point on ASSUME is interesting; I hadn't thought of it and I confess don't think of using ASSUME much).

Hadn't noticed the randomization module, Markus. Thanks very much!

Vic

On Wednesday, November 25, 2020 at 1:55:18 PM UTC-5 Markus Alexander Kuppe wrote:

On 25.11.20 10:31, Stephan Merz wrote:

> CHOOSE is arbitrary but deterministic choice. In other words, with your

> definition, TLC will generate one function (likely a very trivial one,

> perhaps mapping every instruction of A to the same instruction of B) and

> explore the spec for that particular function. If you want to explore

> the spec for every possible function, make the mapping a variable of

> your spec, add

>

> translateFn \in [...]

>

> to the initial condition and UNCHANGED translateFn to all actions. And

> if you want to play with different hand-picked functions, add a CONSTANT

> TranslateFn to your module and write

>

> ASSUME TranslateFn \in [...]

>

> then you define the particular function in the model. What is the right

> way to go depends on whether you want to explore if your transpiler

> works for some fixed function, for all functions or for some specific ones.

With the new-ish Randomization module [1,2], you could trick TLC to

check a more "interesting" subset of all functions.

Markus

[1]

https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/Randomization.tla

[2] https://lamport.azurewebsites.net/tla/inductive-invariant.pdf

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/fbcebe05-0510-4b69-a75e-6bc451e1d7e5n%40googlegroups.com.

**References**:**[tlaplus] Specifying an arbitrary function and then using it in TLC***From:*Vic Putz

**Re: [tlaplus] Specifying an arbitrary function and then using it in TLC***From:*Stephan Merz

**Re: [tlaplus] Specifying an arbitrary function and then using it in TLC***From:*Markus Kuppe

- Prev by Date:
**[tlaplus] Re: Including TLA+ in a Pandoc paper.** - Next by Date:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Previous by thread:
**Re: [tlaplus] Specifying an arbitrary function and then using it in TLC** - Next by thread:
**[tlaplus] TLC throughput decreases by 3 orders of magnitude over time** - Index(es):