/* 
   To compile this file you can type:
   g++ model-checking-example-9-30.c -o example

   To run it then type:
   ./example

   We have the following labels (note that good and bad are not necessarily
   opposites):

   good: 5 | 6 | (!v3 & v2 & v1 & v0) | 8
   bad: v3 & [(v2 & !v1 & v0) | (!v2 & v1 & v0) | (!v2 & v1 & !v0)]

   Some properties to try to verify are:
   (1) (G intersect B) == empty set
   (2) Forall X g

   Kripke structure as presented in class:
   (1, 
   0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15, 
   0->1 1->2 2->3 3->4 4->5 5->6 6->7 7->8 8->9 9->0 10->11 11->10 12->12 13->14 14->15 15->0,
   good: 0 1 2 3 4 5 6 7 8 9
   i: 13 14 15
   bad: 10 11 12)
   
*/

#include <iostream>
#include <string>

using namespace std;

int next_st (int load, int init_st, int cur_st) { 

  // load; Boolean value [0...1]
  // init_st; a state to direct our state machine [0...15]
  // cur_st;  current state [0...15]

  if (load) {
    cur_st = init_st;
  } else {
    switch (cur_st) {

	case 0:
	case 1:		
	case 2:
	case 3:
	case 4:
	case 5:
	case 6:
	case 7:
	case 8: 
	case 13:
	case 14:
	  cur_st = cur_st + 1;
	  break;

	case 9: 
	  cur_st = 0;
	  break;

	case 10:
	  cur_st = 11;
	  break;

	case 11: 
	  cur_st = 10;
	  break;

	case 12:
	  break;

	case 15: 
	default:
	  cur_st = 0;
  
	} 
  }
  return cur_st;
}

int main (int argc, char * argv[], char * envp[]) {

  // Variable uninitialized to help demonstrate that it's possible to have
  // state that's not in the [0...15] range
  int st; // state
  int load; // whether to load
  int init; // initial value

  while (1) {
	cout << "Current state is: " << st << endl;
	cout << "Input 1 to load the initial state and 0 to use the current state: ";
    cin >> load;
	cout << "Input what the initial might be: ";
	cin >> init;
	st = next_st(load, init, st);
	cout << "The next state has been computed to be: " << st << endl << endl;
	
  }
	  
}