[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.


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.