EECS 356 Intro. to Formal Spec. and Verification
Jan. 15, 2013
Due: Jan. 22

			Homework 1

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. Determine which of the following formulas are tautologies.

   (F => G) /\ (G => F) <=> (F <=> G)
   
   (~F /\ ~G) <=> (~F) \/ (~G)
   
   F => (F => G)
   
   (F => G) <=> (~G => ~F)

   (F => (G => H)) => ((F => G) => H) 

   (F <=> (G <=> H)) => ((F <=> G) <=> H) 
   
   (\A x : F /\ G) <=> (\A x : F)  /\ (\A x : G) 

   (\E x : F /\ G) <=> (\E x : F)  /\ (\E x : G) 
   
   (\A x : F \/ G) <=> (\A x : F)  \/ (\A x : G) 

   (\E x : F \/ G) <=> (\E x : F)  \/ (\E x : G) 
   

2. Which of the following formulas are valid for all sets S, T, and U?

   (S \subseteq T) <=> (S \cup T = T)

   (S \subseteq T) <=> \A x \in S : x \in T
   
   (S = T) <=> (S \subseteq T) /\ (T \subseteq S)

   (S \subseteq T) <=> (S \ T = {})

   (S \ T) \cup (T \ S) = (S \cup T) \ (S \cap T)

   (S \ (T \cap U)) = (S \ T) \cup (S \ U)

3. Download and install the TLA Toolbox. Type in the Euclid's GCD algorithm specification,
   parse it for syntax correctness, typeset it to produce pdf file, and try to use to TLC to check it.
   You only need to turn in the printed pdf file and some outputs from the TLC trial. 

4. Write a module HourClockChannel by modifying the Channel
   module so it sends a sequence of hour-clock values over channel
   chan.  That is, it sends a sequence of consecutive hour values,
   starting from any value in 1..12.  For example, it might send
   the sequence of values  

      9, 10, 11, 12, 1, 2, ... , 11, 12, 1 , ...
   Please typeset it by TLATeX.

5. Write a specification of an hour-clock that sends the time to
   the environment over a channel chan.  The specification should make
   use of the definitions from the Channel and HourClock modules by
   incorporating them with an EXTENDS statement.  Write two versions
   of the specification.

      Version 1: The clock can tick at any time.

      Version 2: The clock cannot tick between sending a value on chan 
                 and the receipt of that value by the environment.

   Please include type invariants and typeset it by TLATeX.