[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: action never enabled
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
--
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/f9bec688-67fd-c58c-627b-b9ed16bde9fa%40lemmster.de.