EECS 356: Intro. to Formal Spec. and Verification Mar 5, 2013 Due: Mar 14 Homework 4 You may discuss the assignments with your classmates but need to write down your solutions independently. Be careful with your handwriting. Unclear solutions will be assumed to be wrong. 1. (a) Use TLC to print all Pythagorean triples <> with i^2 + j^2 = k^2 for natural numbers i,j,k \leq N. Start with N=20. (Don't be clever and use the formula for generating Pythagorean triples; have TLC do it in a straightforward fashion.) (b) Next, get TLC to print only essentially Pythagorean triples--that is, Pythagorean triples <> such that i \leq j and i,j, and k have no common factor. Try it with N = 50, 100, ... . Why does TLC take longer to generate each example as N increases? 2. Use TLC to check that the BigSpec implies the ImpliedTemporal in the MCRealTimeHourClock module. 3. There are three different ways of categorizing composite specifications: interleaving vs. noninterleaving, disjoint-state vs. shared-state, and joint-action vs. separate-action. Please consider all eight combinations and elaborate the possibility and benefit of each. 4. Please write composite specifications of two clocks that are almost synchronous, that is, the difference between readings is at most one. Please write specifications spanning all the possibilities: interleaving vs. noninterleaving, disjoint-state vs. shared-state, and joint-action vs. separate-action. 5. Please use the hand-out on Peterson's Algorithm for Mutual Exclusion for n number of processes, to specify the algorithm for 4 processes, and then use TLC to check the correctness of the algorithm.