State Machine Exercises

Consider the following state machine:

               0
     +====+ --------> +----+
 --> # q0 #           | q1 |
     +====+ <-------- +----+
                1
      | ^               |
      | |               |
    1 | | 0           0 |
      | |               |
      v |               v
     
     +----+     1     +----+
     | q2 | --------> | q3 | <-+
     +----+           +----+   |
                        |      | 0,1
                        +------+

This machines operates over the input language of binary strings where at each step it reads a 0 or 1. The machine starts in the q0 state and accepts if it finishes in the q0 state.

1. Encode this state machine in Lustre with an output variable called 'accept' which is true when the machine accepts on the input so far.

2. Define bias = total number of ones - total number of zeros (computed in whichever way you like). Prove

   accept => bias = 0

   Using the command jkind -pdr_max 0 filename.lus

3. The proof should require k = 2. Let's figure out why. To see why k = 1 is not sufficient run jkind -pdr_max 0 -induct_cex -n 1 filename.lus. This produces an inductive counterexample which is a trace which shows the property is not 1-inductive.

4. Strengthen the property so that it passes with k = 1. You should be able to do this by using inductive counterexamples. The inductive counterexamples should all start from a state that is not actually reachable. Strengthen the property to exclude these unreachable states until the property passes with k = 1.

5. Prove your original property and the strengthened property at the same time. They should both prove with k = 1. Figure out why the original property now proves with k = 1 instead of k = 2.

6. Prove that if you accept then you have never seen 111 or 000 anytime in the past.

   Hint: Let running_zeros be the number of input zeros in a row up to and including the current point (similarily, running_ones). Note that when you see a one, runnings_zeros will reset to 0 (and vice-versa for running_ones). Define a node called historically which returns true if its input is and has always been true. Prove

       accept => historically(running_ones <= 2) and
                 historically(running_zeros <= 2)

 Remember to use `jkind -pdr_max 0`. What k does this require and
 why?

7. Using 'bias' and 'historically' come up with an alternate acceptance criteria. That is, prove

   `? = accept`
   

   For some useful expression ?.

8. Find a way to state and prove that if you reach state q3 then you never accept after that.

9. Comment out all other properties (we usually do this by changing --%PROPERTY to -- %PROPERTY). State and try to prove

   `state = q1 => bias = -1`
   

   using jkind -pdr_max 0. this should fail to prove or disprove. Comment that property out, and try again with

   `state = q2 => bias = 1`
   

   You should observe the same behavior. Now include both properties and try to prove them together. Why does this succeed easily where neither of the individual properties did? If you need help, try using the -induct_cex flag to look at why proofs are failing.

10. Try these exercises again without -pdr_max 0. The PDR engine is always uses k = 1 but is very good at coming up with invariants.