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