You are asked to run TLC to verify properties of distributed mutual exclusion algorithms through 3 specifications written in TLA+:
You are expected to check both safety and liveness properties that are given with the specification or are in the slides.
Your main task is to run TLC on these specifications to verify those properties, and report your results in the following two aspects:
(1) Summarize and compare the specifications of the algorithms and of the correctness properties. Include at least these 4 attributes: specification sizes; ease of understanding; how closely are different aspects of the algorithms followed; and what properties are specified and in what way.
(2) Summarize and compare the efficiency of running TLC, separately for checking safety and liveness. Include at least these attributes: ease of setting up and running; and for different process numbers and maximum clock values, the number of states searched and the time taken to check (in a similar form as Page 278 of Lamport's PODC 2000 Tutorial slides)