Reg_id | Constraints | Invariant |
---|
59 | not (i.l.light_state = Green) not (i.l.light_state = Red) i.l.blinking i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
58 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
57 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
56 | not (i.l.light_state = Green) i.l.light_state = Red i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
55 | i.l.light_state = Green i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
54 | not (i.l.light_state = Green) not (i.l.light_state = Red) i.l.blinking i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
53 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
52 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
51 | not (i.l.light_state = Green) i.l.light_state = Red i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
50 | i.l.light_state = Green i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
49 | not (i.l.light_state = Green) not (i.l.light_state = Red) i.l.blinking not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
48 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
47 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
46 | not (i.l.light_state = Green) i.l.light_state = Red not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
45 | i.l.light_state = Green not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
44 | not (i.l.light_state = Green) not (i.l.light_state = Red) i.l.blinking not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
43 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
42 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
41 | not (i.l.light_state = Green) i.l.light_state = Red not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
40 | i.l.light_state = Green not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
39 | not (i.l.light_state = Green) not (i.l.light_state = Red) i.l.blinking not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
38 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
37 | not (i.l.light_state = Green) not (i.l.light_state = Red) not i.l.blinking let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
36 | not (i.l.light_state = Green) i.l.light_state = Red not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
35 | i.l.light_state = Green not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.blink_time) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
34 | not (i.l.light_state = Green) not (i.l.light_state = Red) i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) not Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}} |
33 | not (i.l.light_state = Green) not (i.l.light_state = Red) i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) not Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}} |
32 | not (i.l.light_state = Green) not (i.l.light_state = Red) not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) not Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}} |
31 | not (i.l.light_state = Green) not (i.l.light_state = Red) not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) not Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}} |
30 | not (i.l.light_state = Green) not (i.l.light_state = Red) not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) not Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}} |
29 | not (i.l.light_state = Green) i.l.light_state = Red i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
28 | not (i.l.light_state = Green) i.l.light_state = Red i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
27 | not (i.l.light_state = Green) i.l.light_state = Red not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
26 | not (i.l.light_state = Green) i.l.light_state = Red not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with current_time = _x_1.current_time + 1}} |
25 | not (i.l.light_state = Green) i.l.light_state = Red not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time not Is_a(Green, i.l.light_state) Is_a(Red, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with current_time = _x_2.current_time + 1}} |
24 | i.l.light_state = Green i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time Is_a(Green, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}} |
23 | i.l.light_state = Green i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time Is_a(Green, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}} |
22 | i.l.light_state = Green not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time Is_a(Green, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}} |
21 | i.l.light_state = Green not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time Is_a(Green, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}} |
20 | i.l.light_state = Green not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
not (_x_0.current_time + 1 > _x_0.light_change_time) let (_x_0 : light_state) = i.l in _x_0.current_time + 1 > _x_0.blink_time Is_a(Green, i.l.light_state) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}} |
19 | i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) not (i.l.light_state = Yellow) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Green}} |
18 | i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) not (i.l.light_state = Yellow) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l =
{_x_2 with
blinking = false; current_time = _x_2.current_time + 1; light_state = Green}} |
17 | not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) not (i.l.light_state = Yellow) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Green}} |
16 | not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) not (i.l.light_state = Yellow) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Green}} |
15 | not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) not (i.l.light_state = Yellow) i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Steady; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l =
{_x_2 with
blinking = false; current_time = _x_2.current_time + 1; light_state = Green}} |
14 | i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) i.l.light_state = Yellow i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Red}} |
13 | i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) i.l.light_state = Yellow i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l =
{_x_2 with
blinking = false; current_time = _x_2.current_time + 1; light_state = Red}} |
12 | not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) i.l.light_state = Yellow i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Red}} |
11 | not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) i.l.light_state = Yellow i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Red}} |
10 | not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time not (i.l.light_state = Green) i.l.light_state = Yellow i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l =
{_x_2 with
blinking = false; current_time = _x_2.current_time + 1; light_state = Red}} |
9 | let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}} |
8 | let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating; car_speed = _x_0.car_max_speed;
car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}} |
7 | let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l =
{_x_2 with
blinking = false; current_time = _x_2.current_time + 1; light_state = Yellow}} |
6 | let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 i.c.car_drive_state = Accelerating let (_x_0 : car_state) = i.c in
not (_x_0.car_speed + _x_0.car_accel_speed > _x_0.car_max_speed) let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating; car_speed = _x_1 + _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l =
{_x_2 with
blinking = false; current_time = _x_2.current_time + 1; light_state = Yellow}} |
5 | let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}} |
4 | let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 not (i.c.car_drive_state = Accelerating) i.c.car_drive_state = Steady let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating;
car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}} |
3 | let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}} |
2 | let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in _x_0.car_speed - _x_0.car_accel_speed < 0 let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating; car_speed = 0;
car_distance = _x_0.car_distance + _x_0.car_speed};
l =
{_x_1 with
blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}} |
1 | let (_x_0 : car_state) = i.c in not (_x_0.car_distance + _x_0.car_speed > 10) not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l =
{_x_2 with
blinking = false; current_time = _x_2.current_time + 1; light_state = Yellow}} |
0 | let (_x_0 : car_state) = i.c in _x_0.car_distance + _x_0.car_speed > 10 not (i.c.car_drive_state = Accelerating) not (i.c.car_drive_state = Steady) let (_x_0 : car_state) = i.c in
not (_x_0.car_speed - _x_0.car_accel_speed < 0) let (_x_0 : light_state) = i.l in
_x_0.current_time + 1 > _x_0.light_change_time i.l.light_state = Green i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0
| let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
{_x_0 with
car_drive_state = Accelerating; car_speed = _x_1 - _x_0.car_accel_speed;
car_distance = _x_0.car_distance + _x_1};
l =
{_x_2 with
blinking = false; current_time = _x_2.current_time + 1; light_state = Yellow}} |