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 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 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 xInit == x = 0Next == /\ 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 <- xTHEOREM 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 : 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.