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

About CHOOSE construct


I'm writing TLA+ specification and I use TLC.
While I'm using TLC, I'm curious about CHOOSE construct.

If the statement is as follows,
  CHOOSE v \in {2, 3} : TRUE

the selected value is almost always 2 while model checked it.
But, the next state depends on which the value is chosen so I want to check all the cases.
Is it possible to solve with model checking?