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

*From*: José Eduardo Solsona <josedusolsona@xxxxxxxxx>*Date*: Mon, 27 Apr 2020 18:29:08 -0300*References*: <38427413-5d82-4fe4-b54f-9f5535198aa4@googlegroups.com> <17EC8615-B388-4CB6-AB3E-E691AF3B709F@gmail.com>

Hello Stephan,

I realized that what i really want is existential quantification, so i was also misusing CHOOSE from the start.

Thanks

On Mon, Apr 27, 2020 at 4:01 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

You want to use existential quantification for non-deterministic (arbitrary) choice. CHOOSE is deterministic, and randomization is useful for testing, but is not what you want for proofs (unless you consider probabilistic systems, but then TLA+ is not the method of choice).--Regards,StephanOn 27 Apr 2020, at 06:00, JosEdu Solsona <josedusolsona@xxxxxxxxx> wrote:Hello,In a place of my spec i need to consider an arbitrary value from an non-empty domain. Naturally, at first i went with CHOOSE to talk about this value.But then, when doing model checking and simulations, i observed CHOOSE was always selecting the first of the concrete model values. I wanted a more "realistic"output when doing simulations because i think is more helpful to visualize, so i replaced CHOOSE by RandomElement, and it worked fine at least for that purpose.However, TLC is just an optional tool (although very useful) for my project, my goal is to do formal proofs with TLAPS. The problem is now i canformally prove a refinement but TLC fails to check the very same refinement, which is weird, and i think this is because the presence of RandomElementand the way it works.(If i go back to CHOOSE, the proof is still valid and TLC doesn't complaint... but obviously i see again the output is taking always the same value.)A (extremely) simplified version of mi case is as follows, suppose we have a spec in module A:

VARIABLES x

Init == x = 0

Next == /\ x' = RandomElement(Nat) \* if instead we use "CHOOSE v \in Nat : TRUE" the output after "0" is always the same

/\ PrintT(x)

Spec == Init /\ [][Next]_xAnd we have another module, say B, with exactly the same spec. Then, because A!Spec and B!Spec are (literally) the same, they refine each other.We can prove this in module B:

A == INSTANCE A WITH x <- x

THEOREM Spec => A!Spec

...

But if we try TLC to model check the property A!Spec it fails, and it fails in different ways for different runs.Currently, my (maybe not completely satisfactory) workaround for this "incoherence" between what i expect from RandomElementwhen doing proofs vs doing model checking is to define in my spec a symbol:

AnyValue == CHOOSE v \in SomeDomain : TRUEIn this way, for the spec defined in terms of AnyValue,

- The refinement proof goes through.
- If i want to use TLC to see some simulations with random values, i create a model configured specifically for doing this redefining AnyValue <- RandomElement(SomeDomain).
- If i want to use TLC to model check the refinement, i create another model for it leaving AnyValue as it is. (Obviously, the output in this case would not be "random"...).
Some questions about this:

- Is RandomElement known to be problematic when used both in proof and in model checking?
- Maybe im just misusing RandomElement?.
- Is the proposed workaround a reasonable approach?
Any recommendations on this matter are helpful :)Thanks.--

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/38427413-5d82-4fe4-b54f-9f5535198aa4%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/17EC8615-B388-4CB6-AB3E-E691AF3B709F%40gmail.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/CACN5ZA4jPpcz_CDL91ra0fYC_v5wYdqrU-PFkA%2BE7is7crHXAA%40mail.gmail.com.

**References**:**[tlaplus] About the behavior of RandomElement on refinement proofs***From:*JosEdu Solsona

**Re: [tlaplus] About the behavior of RandomElement on refinement proofs***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] tlaps example** - Next by Date:
**[tlaplus] Expanding PrintT to TRUE in proofs?** - Previous by thread:
**Re: [tlaplus] About the behavior of RandomElement on refinement proofs** - Next by thread:
**[tlaplus] on tlaps** - Index(es):