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

*From*: JosEdu Solsona <josedusolsona@xxxxxxxxx>*Date*: Sun, 26 Apr 2020 21:00:06 -0700 (PDT)

Hello,

But if we try TLC to model check the property A!Spec it fails, and it fails in different ways for different runs.

-- 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 can

formally prove a refinement but TLC fails to check the very same refinement, which is weird, and i think this is because the presence of RandomElement

and 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]_x

And 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 RandomElement

when doing proofs vs doing model checking is to define in my spec a symbol:

`AnyValue == CHOOSE v \in SomeDomain : TRUE`

In 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.

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

- Prev by Date:
**[tlaplus] TLA+ Toolbox 1.7.0 release** - Next by Date:
**Re: [tlaplus] About the behavior of RandomElement on refinement proofs** - Previous by thread:
**Re: [tlaplus] TLA+ Toolbox 1.7.0 release** - Next by thread:
**Re: [tlaplus] About the behavior of RandomElement on refinement proofs** - Index(es):