TLC reports that "temporal properties were violated" even though the algorithm was declared fair

[Francisco José Letterio]

I have the following spec for the DIeHarder algorithm from the book:

--------------------------- MODULE DieHarderBook ---------------------------

EXTENDS Integers, GCD

Min(n,m) == IF n < m THEN n ELSE m

CONSTANTS Goal, Jugs, Capacity

ASSUME CONSTANTS_OK == /\ Goal \in Nat
                       /\ Capacity \in [Jugs -> Nat \ {0}]

(***************************************************************************
--fair algorithm DieHarder {
  variable injug = [j \in Jugs |-> 0] ;
  { while (~\E j \in Jugs : injug[j] = Goal)
     { either with (j \in Jugs) \* fill jug j
                { injug[j] := Capacity[j] }
       or     with (j \in Jugs) \* empty jug j
                { injug[j] := 0 }
       or     with (j \in Jugs, k \in Jugs \ {j}) \* pour from jug j to jug k
                { with ( poured =
                           Min(injug[j] + injug[k], Capacity[k]) - injug[k] )
                    { injug[j] := injug[j] - poured ||
                      injug[k] := injug[k] + poured
                    }
                }
     }
  }
}
 ***************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) = "b157a2cd" /\ chksum(tla) = "88d18fa9")
VARIABLES injug, pc

vars == << injug, pc >>

Init == (* Global variables *)
        /\ injug = [j \in Jugs |-> 0]
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ IF ~\E j \in Jugs : injug[j] = Goal
               THEN /\ \/ /\ \E j \in Jugs:
                               injug' = [injug EXCEPT ![j] = Capacity[j]]
                       \/ /\ \E j \in Jugs:
                               injug' = [injug EXCEPT ![j] = 0]
                       \/ /\ \E j \in Jugs:
                               \E k \in Jugs \ {j}:
                                 LET poured == Min(injug[j] + injug[k], Capacity[k]) - injug[k] IN
                                   injug' = [injug EXCEPT ![j] = injug[j] - poured,
                                                          ![k] = injug[k] + poured]
                    /\ pc' = "Lbl_1"
               ELSE /\ pc' = "Done"
                    /\ UNCHANGED <<injug>>

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == Lbl_1
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(Next)

Termination == <>(pc = "Done")

\* END TRANSLATION
=============================================================================

However, checking for property Termination makes TLC report that "Temporal properties were violated" and the trace has a single step where it begins with injug = [0,0], pc = Lbl_1 and goes to injug = [0,3], pc = Lbl_1 (so it fills the small jug)

I don't understand what temporal property is being violated, and why this trace proves it

[Hillel Wayne]

Hi Francisco,

1. What constants did you use for Goal, Jugs, Capacity?

2. When you say "it begins with injug = [0,0], pc = Lbl_1 and goes to injug = [0,3], pc = Lbl_1", does it say "back to step 1" or "stuttering" after? Because a valid trace seems to be

Fill jug 1 -> empty jug 1 -> fill jug 1 -> empty jug 1 -> etc

`Termination` checks the spec always terminates, while for this case we want to show the spec terminates in at least one circumstance (which means it finds a solution). How can you change your property to reflect that?

H

--
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 visit https://groups.google.com/d/msgid/tlaplus/5f7269ec-35dc-41aa-9f37-3bd32efdaa30n%40googlegroups.com.

[Francisco José Letterio]

I think I might need to read up a bit more on temporal logic before tackling this one 😅

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/AEWv1o8c7KM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/63fd64c3-901c-4661-90bc-3dafc10e301e%40gmail.com.

[Francisco José Letterio]

I can't think of how to ask this without using CTL frankly

[Hillel Wayne]

Reachability properties are not directly expressible in TLA, but we can cheat and say that `~Termination` is a property (the system is guaranteed to never terminate). Then TLC will find a counterexample, which "proves" reachability.

H

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/799a8cad-4e75-48e9-8e01-6efc8ebb8074n%40googlegroups.com.