test-procedure-checker-3.ucl

module traffic_light
{
  type light_t = enum { red, yellow, green };
  var step : integer;
  output light : light_t;

  procedure next_light()
    modifies light;
    modifies step;
  {
    if (step == 0) {
      case
	    (light == green) : {
	      light = yellow;
	    }
	    (light == yellow) : {
	      light = red;
	      step = 2;
	    }
	    (light == red) : {
	      light = green;
	      step = 1;
	    }
	  esac
    } else {
      step = step - 1;
    }
  }

  next {
    call next_light();
  }
}

module main
{
  type light_t = traffic_light.light_t;

  instance light1 : traffic_light();
  instance light2 : traffic_light();
  
  init {
    assume (light1.light == red && light1.step == 2);
    assume (light2.light == green && light2.step == 1);
  }

  next {
    next (light1);
    next (light2);
  }
  
  invariant atleast_one_red    : (light1.light == red) || (light2.light == red);
  invariant steps_non_negative : (light1.step >= 0) && (light2.step >= 0);
  invariant steps_upper_bound  : (light1.step <= 2) && (light2.step <= 2);
  control {
    v = induction(1);
    check;
    print_results;
    // v.print_cex(light1.light, light1.step, light2.light, light2.step);
  }
}