Thank you very much! This explanation helps a lot.
And thanks to Jones and Stephen also for the original explanations.
On Saturday, December 25, 2021 at 11:15:43 AM UTC-8 Markus Alexander Kuppe wrote:
On 12/24/21 5:20 PM, Jones Martins wrote:
> I think I have an answer. You didn't mention invariants, but when I
> checked your model with TypeOK as an invariant, I saw it had been
> violated because of coin0 < upperZero in the second step. Since it's
> violated in the second step, you'll see "<other action> is not enabled."
> Now, why is the first action in the disjunction always "chosen"? I
> believe it's because, when TLC is generating the state graph, it's the
> first action it parses (instead of deciding between "A" and "B" in "A \/
> B", it always picks "A" to evaluate first). When evaluated, TLC
> immediately verifies all invariants. Since TypeOK is false during this
> verification step, TLC stops, nothing else happens.
>
> This is my speculation, because I'm fairly new to TLA+. Maybe a few
> experts in this group will be able to respond to your question and
> resolve our doubts.
This explanation is correct! From Specifying Systems page 238:
"The first difference in evaluating the next-state action is that TLC
does not evaluate disjunctions from left to right." Instead, when it
evaluates a subformula A1 \/ ... \/ An, it splits the computation into n
separate evaluations, each taking the subformula to be one of the Ai."
With a single worker, TLC evaluates the subactions A1, ..., An
sequentially in an order derived from the order of the subformulas of
the next-state relation. Evaluating a subaction Ai yields successor
states, for which TLC checks the invariants *before* evaluating Ai+1.
For the uniswapV1 spec, with Next == tradeOneForZero \/ tradeZeroForOne,
TLC evaluates tradeOneForZero and checks the invariant TypeOK for each
successor state given by tradeOneForZero. Since at least one such
successor state violates TypeOK, TLC prints a counterexample and stops.
If you want TLC to continue and evaluate the subaction tradeZeroForOne,
run TLC with "-continue".
Running TLC with multiple workers causes non-determinism. However, it
will report tradeZeroForOne not to be covered with very high probability.
Markus