action never enabled

[Mark Ettinger]

TLA+ newbie here with what is probably a newbie-ish question.  I'll describe it abstractly with actions A and B.   My spec has the form:

Next == A \/ B

Spec == Init /\ []Next_<<vars>>

When I run TLC I get a warning "B is never enabled".  If I change the ordering in Next to:

Next == B \/ A

I get the warning "A is never enabled."  Am I missing something obvious about disjunction?

Thanks for any insights in advance!

[Jones Martins]

Hello,

From your example, it seems Spec should be: Init /\ [][Next]_vars, assuming vars is already a tuple/sequence. I am not sure if that solves your problem, though.

Jones

[Mark Ettinger]

 Sorry, I mistyped.  Indeed my spec is already:

Spec == Init /\ [][Next]_vars

[Jones Martins]

Hi,

No problem. I can't think of a solution unless you show a reduced (if possible) version of your spec?

Jones

[Mark Ettinger]

Here is the actual spec:

----------------------------- MODULE uniswapV1 -----------------------------
EXTENDS Naturals, Integers
CONSTANTS liquidityBound, coin0Init, coin1Init, upperZero, lowerZero
VARIABLES coin0, coin1, liquidityTokens

max(a,b) == IF a > b THEN a ELSE b

outputPrice(delta_y, coin_x, coin_y) == ((delta_y * coin_x) \div (coin_y - delta_y)) + 1
inputPrice(delta_x, coin_x, coin_y) ==  (delta_x * coin_y) \div (coin_x + delta_x)

TypeOK == /\ coin0 \in Nat
          /\ coin1 \in Nat
          /\ (coin0 = 0 <=> coin1 = 0)
          /\ coin0 < upperZero
          /\ coin0 > lowerZero

tradeOneForZero == \exists delta_1 \in 1..outputPrice(coin0-1, coin1, coin0):
        /\ coin1' = coin1 + delta_1
        /\ coin0' = coin0 - inputPrice(delta_1, coin1, coin0)
        /\ liquidityTokens' = liquidityTokens
       
tradeZeroForOne == \exists delta_0 \in 1..outputPrice(coin1-1, coin0, coin1):
        /\ coin0' = coin0 + delta_0
        /\ coin1' = coin1 - inputPrice(delta_0, coin0, coin1)
        /\ liquidityTokens' = liquidityTokens
                                                             
Init == coin0 = coin0Init /\ coin1 = coin1Init /\ liquidityTokens = max(coin0,coin1)
\*Next == tradeZeroForOne \/ tradeOneForZero
Next == tradeOneForZero \/ tradeZeroForOne

Spec == Init /\ [][Next]_<<coin0, coin1, liquidityTokens>>
=============================================================================

[Jones Martins]

Hi,

Yeah, nothing caught my eye… Could you give me the constant values for me to test locally?

Jones

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/xSLCjuLi9ck/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ce797f94-fd78-4dc8-bf46-267c5e91ccfbn%40googlegroups.com.

[Mark Ettinger]

Hi Jones,

Here are the constant values.  By the way, thank you very much for helping me out!

liquidityBound <- 10

coin0Init <- 100

coin1Init <- 1000

lowerZero <- 80

upperZero <- 120

[Jones Martins]

Hi, Mark

I'm glad to help!

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.

Best,

Jones

[Stephan Merz]

Hello,

this might be an artefact of TLC evaluating formulas from left to right. Perhaps we could say more if you could share your spec (or a minimum working example if it is too big).

Regards,

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ecbf0cb0-29ad-4af6-81c1-4b6d08a7647an%40googlegroups.com.

[Mark Ettinger]

Jones:

I do not think your hypothesis is consistent with the description in section 14.2.6 of "Specifying System" which describes how TLC computes states.   TLC "should" calculate all possible histories which would prohibit calculating A "first."   As far as I understand these things, temporal logic, disjunction in particular, has no notion of calculating something "first", in contrast to a programming language.

Stephan:

My reply above to Jones' explanation also applies to your comment about TLC's evaluation strategy.  Also, my post earlier in this thread contains the spec.

I'm really quite stumped!

[Markus Kuppe]

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

[Mark Ettinger]

Markus:

Thank you very much!  This explanation helps a lot.

And thanks to Jones and Stephen also for the original explanations.