CODEWITHSUNDEEP
tla+
urxvtcd
urxvtcd

Reputation: 65

TLC model checker doesn't terminate on an and/or list version of formula

This is probably a very stupid question, but I'll ask anyway.

I'm watching Leslie Lamport's videos about TLA+. In video number four, called "Die Hard", he gives an exercise of implementing BigToSmall and SmallToBig formulas. Long story short: we need to correctly calculate how much water is in 3 and 5 gallon jugs after pouring from one to another.

This is his solution:

SmallToBig == IF big + small =< 5
               THEN /\ big'   = big + small
                    /\ small' = 0
               ELSE /\ big'   = 5
                    /\ small' = small - (5 - big)

BigToSmall == IF big + small =< 3
               THEN /\ big'   = 0 
                    /\ small' = big + small
               ELSE /\ big'   = small - (3 - big)
                    /\ small' = 3

I tried to go with this and/or list thingy:

SmallToBig == \/ /\ big + small =< 5
                 /\ big'   = big + small
                 /\ small' = 0
              \/ /\ big'   = 5
                 /\ small' = small - (5 - big)

BigToSmall == \/ /\ big + small =< 3
                 /\ big'   = 0 
                 /\ small' = big + small
              \/ /\ big'   = small - (3 - big)
                 /\ small' = 3

however it when I run it, the checking doesn't terminate, and I cannot figure out why.

Upvotes: 0

Views: 102

Answers (2)

Hovercouch
Hovercouch

Reputation: 2314

If I rewrite it as 

\* Old
SmallToBig == 
   IF Condition
     THEN A
     ELSE B

\* New
SmallToBig == 
  \/ /\ Condition
     /\ A
  \/ B

In both versions, we can't have A without Condition. In the old version, we can't have B with Condition. In the new version, though, we can have B with Condition: it's a valid action.

Upvotes: 2

M.K.
M.K.

Reputation: 354

Have TLC check the invariant TypeOK. The counterexample will show you what is going on.

Upvotes: 1

Related Questions