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