#define state byte

bool Fail = false;
bool input;
bool output;
state current_state = 0;


never{
 do
   ::assert(((0 <= current_state)&&(current_state <= 7)));
 od;
}



proctype COUNTER() {
do
  ::atomic{
    !input ->
    output = false;
    };
  ::atomic{
    ((input)&&(current_state!=7)) ->
    current_state = current_state+1;
    output = false;
    };
  ::atomic{
    ((input)&&(current_state==7)) ->
    current_state = 0;
    output = true;
    };
od;
}

init {
    if
      ::input = true;
      ::input = false;
    fi;


 atomic{
 run COUNTER();
 };
}