About CHOOSE construct

[myjul...@xxxxxxxxx]

Sir,

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?

Thanks,
Juliet