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

[tlaplus] About the behavior of RandomElement on refinement proofs


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:


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:

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,
Some questions about this:
Any recommendations on this matter are helpful :)


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.