| 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. Thanks, Jonathan === (* --algorithm simpleMutex \* atomicity is determined by labels variables 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 fair+ process ProcName1 = "P1" begin L1: print <<"P1 at L1">>; L2: request(r); L3: print <<"P1 at L3 criitical region">>; L4: release(r); goto L1; end process fair+ process ProcName2 = "P2" begin 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. |