Sometimes when I run the TLC Model Checker, it reports "Invariant Inv is violated", but there is no error-trace. Under what conditions does the checker not show an error trace?
In some cases, when I reduce the size of the model, if the invariant is violated than a trace is available. However, in other cases I can't reproduce the error with a smaller model.
Here's an example where this happens for me (The TLC model options I'm using appear at the bottom of the email):
------------------------- MODULE ConcurrentUpdates -------------------------
EXTENDS Naturals
CONSTANT N
ASSUME N \in Nat /\ N > 1
(*
--algorithm Increment
variable count=0;
process P \in 1..N
variables temp=0,
i=0;
begin
set: i := i+1;
temp := count;
inc: count := temp+1;
if i < N then goto set end if;
end process
end algorithm
*)
\* BEGIN TRANSLATION
VARIABLES count, pc, temp, i
vars == << count, pc, temp, i >>
ProcSet == (1..N)
Init == (* Global variables *)
/\ count = 0
(* Process P *)
/\ temp = [self \in 1..N |-> 0]
/\ i = [self \in 1..N |-> 0]
/\ pc = [self \in ProcSet |-> "set"]
set(self) == /\ pc[self] = "set"
/\ i' = [i EXCEPT ![self] = i[self]+1]
/\ temp' = [temp EXCEPT ![self] = count]
/\ pc' = [pc EXCEPT ![self] = "inc"]
/\ count' = count
inc(self) == /\ pc[self] = "inc"
/\ count' = temp[self]+1
/\ IF i[self] < N
THEN /\ pc' = [pc EXCEPT ![self] = "set"]
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << temp, i >>
P(self) == set(self) \/ inc(self)
Next == (\E self \in 1..N: P(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
UpperBound == (\A self \in ProcSet: pc[self] = "Done") => count \leq N*N
TypeOK == /\ count \in Nat
/\ i \in [ProcSet -> Nat]
/\ pc \in [ProcSet -> {"set", "inc", "Done"}]
/\ temp \in [ProcSet -> Nat]
Inv == /\ TypeOK
/\ UpperBound
=============================================================================