[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Spurious coverage warning in TLC

In a simple 2-process mutex (see below) there are no errors but there is a coverage warning which is coloured yellow. Clicking on the warning points to the following line in the translation:

vars == << r, pc >>

TLC warns one when some action is never exercised during a run of the model checker. But here the warning appears to be meaningless because the definition of vars is not an action. 

Stephan suggested that I post here to mention the issue. He also mentions that he has seen similar examples of spurious warnings by TLC, but he ignores them. (However, knowing that an actual action is never executed is meaningful information.)

In a more complex process version of mutex, the problem does not occur. 



(* --algorithm simpleMutex
\* atomicity is determined by labels
r = 1; \* global mutex variable

macro request(x) begin await x > 0; x := x-1; end macro   
macro release(x) begin  x := x + 1; end macro         

\* Strongly fair processes, L3 and M3 are the critical regions
\* Liveness requires strong fairness
fairprocess ProcName1 = "P1"
L1: print <<"P1 at L1">>; 
L2: request(r); 
L3: print <<"P1 at L3 criitical region">>; 
L4: release(r); goto L1;
end process

fairprocess ProcName2 = "P2"
M1: print <<"P2 at M1">>; 
M2: request(r); 
M3: print <<"P2 at M3 critical region">>; 
M4: release(r); goto M1;
end process

end algorithm *)

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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.