The stoplight model¶
In this notebook we want to explore a simple model of a car approaching an intersection. The model is not supposed to be representative of a real world simulation, but rather a first stage high level abstraction of one such.
We start by defining datatypes representing the state of the stoplight in the intersection:
In [1]:
(* Street light color *)
type color = Green | Yellow | Red ;;
(* State representation of an intersection. *)
type light_state = {
blinking : bool;
current_time : int;
(* Transition every X seconds *)
blink_time : int;
(* Transition period *)
light_change_time : int;
(* Intersection light *)
light_state : color;
};;
Out[1]:
type color = Green | Yellow | Red
type light_state = {
blinking : bool;
current_time : Z.t;
blink_time : Z.t;
light_change_time : Z.t;
light_state : color;
}
Next we define a transition function for the stoplight:
In [2]:
(* Update the light *)
let light_step (l : light_state) =
let l = { l with current_time = l.current_time + 1 } in
if l.current_time > l.light_change_time then
begin
let l = { l with blinking = false } in
match l.light_state with
| Green -> { l with light_state = Yellow }
| Yellow -> { l with light_state = Red }
| Red -> { l with light_state = Green }
end
else if l.current_time > l.blink_time then
begin match l.light_state with
| Green | Yellow -> { l with blinking = true }
| Red -> l
end
else
l
;;
Out[2]:
val light_step : light_state -> light_state = <fun>
We do the same for the state of the car approaching said stoplight:
In [3]:
(* Driving state *)
type driving_state = Accelerating | Steady | Braking;;
(* Current car state *)
type car_state = {
car_drive_state : driving_state;
car_speed : int; (* Speed of the car meters/time *)
car_distance : int; (* Distance to the intersection *)
(* Define some parameters. We'll condition our model
on these later. *)
car_accel_speed : int;
car_max_speed : int;
car_min_speed : int;
};;
(* Our simple car controller - takes the current state of the car
and the streetlight and adjusts the speed. *)
let car_controller (c, l : car_state * light_state) =
(* Let's define possible commands here. *)
let steady = { c with car_drive_state = Steady } in
let brake = { c with car_drive_state = Braking } in
let accelerate = { c with car_drive_state = Accelerating } in
(* Now we're going to update the speed based on the current light *)
match l.light_state with
| Green -> steady (* If it's green, let's just do what we do. *)
| Red -> brake
| Yellow ->
if not l.blinking && c.car_distance > 10 then
accelerate
else
brake
;;
Out[3]:
type driving_state = Accelerating | Steady | Braking
type car_state = {
car_drive_state : driving_state;
car_speed : Z.t;
car_distance : Z.t;
car_accel_speed : Z.t;
car_max_speed : Z.t;
car_min_speed : Z.t;
}
val car_controller : car_state * light_state -> car_state = <fun>
We can now define our intersection as a struct containing both the car and the stoplight state, and we can then define a one_step function over the state of the intersection, by first updating the state of the stoplight and then letting the car react to this new state of the world:
In [4]:
type intersection = {
c : car_state;
l : light_state;
};;
(* Our car state transition here *)
let car_step (i : intersection) =
let c = i.c in
(* Update distance given the current speed *)
let c = { c with car_distance = c.car_distance + c.car_speed } in
let c = match c.car_drive_state with
| Accelerating ->
let new_speed = c.car_speed + c.car_accel_speed in
if new_speed > c.car_max_speed then { c with car_speed = c.car_max_speed }
else { c with car_speed = new_speed }
| Steady -> c
| Braking ->
let new_speed = c.car_speed - c.car_accel_speed in
if new_speed < 0 then { c with car_speed = 0 }
else { c with car_speed = new_speed } in
(* We have our current distance, speed and acceleration. *)
let c' = car_controller (c, i.l) in
{ i with c = c'}
;;
(* State transitions of our core values... *)
let one_step (i : intersection) =
let l' = light_step (i.l) in
car_step ({i with l = l'});;
let valid_car_state (i: intersection) =
(* let's make sure the car is going in a good speed *)
i.c.car_speed = 20 &&
i.c.car_accel_speed = 10 &&
i.c.car_max_speed = 100 &&
i.c.car_min_speed = 0;;
Out[4]:
type intersection = { c : car_state; l : light_state; }
val car_step : intersection -> intersection = <fun>
val one_step : intersection -> intersection = <fun>
val valid_car_state : intersection -> bool = <fun>
Let's verify that our model ensures that the car will always brake when approaching a red light:
In [5]:
verify
(fun i ->
let i = one_step i in
valid_car_state i &&
i.l.light_state = Red
==> i.c.car_drive_state = Braking)
;;
Out[5]:
- : intersection -> bool = <fun>
Proved
proof
| ground_instances: | 0 | ||||||||||||
| definitions: | 0 | ||||||||||||
| inductions: | 0 | ||||||||||||
| search_time: | 0.015s | ||||||||||||
| details: | Expand
|
Expand
start[0.015s] let (_x_0 : car_state) = if ….light_state = Green then … else … in (_x_0.car_speed = 20) && ((_x_0.car_accel_speed = 10) && ((_x_0.car_max_speed = 100) && (_x_0.car_min_speed = 0))) && (….l.light_state = Red) ==> _x_0.car_drive_state = Brakingsimplify
into: let (_x_0 : int) = ….car_speed in let (_x_1 : int) = ….car_distance in let (_x_2 : int) = ….car_accel_speed in let (_x_3 : int) = ….car_max_speed in let (_x_4 : int) = ….car_min_speed in let (_x_5 : car_state) = {car_drive_state = Braking; car_speed = _x_0; car_distance = _x_1; car_accel_speed = _x_2; car_max_speed = _x_3; car_min_speed = _x_4} in let (_x_6 : light_state) = ( :var_0: ).l in let (_x_7 : int) = _x_6.current_time in let (_x_8 : color) = (if _x_7 <= (-1) + _x_6.light_change_time then if _x_7 <= (-1) + _x_6.blink_time then … else … else if _x_6.light_state = Green then … else …).light_state in let (_x_9 : bool) = _x_8 = Red in let (_x_10 : car_state) = if _x_8 = Green then {car_drive_state = Steady; car_speed = _x_0; car_distance = _x_1; car_accel_speed = _x_2; car_max_speed = _x_3; car_min_speed = _x_4} else if _x_9 then _x_5 else if not ….blinking && not (_x_1 <= 10) then … else _x_5 in not ((_x_10.car_speed = 20) && (_x_10.car_accel_speed = 10) && (_x_10.car_max_speed = 100) && (_x_10.car_min_speed = 0) && _x_9) || (_x_10.car_drive_state = Braking)expansions: []
rewrite_steps: forward_chaining: - Unsat
Loading..
Loading..
Let's now use Imandra's Principal Region Decomposition to enumerate all the possible distinct regions of behavior of the intersection:
In [6]:
#program;;
let d = Modular_decomp.top ~prune:true ~assuming:"valid_car_state" "one_step";;
Out[6]:
val d : Modular_decomp_intf.decomp_ref = <abstr>
Regions details
No group selected.
- Concrete regions are numbered
- Unnumbered regions are groups whose children share a particular constraint
- Click on a region to view its details
- Double click on a region to zoom in on it
- Shift+double click to zoom out
- Hit escape to reset back to the top
Direct sub-regions: -
Contained regions: -
Constraints
<constraint>
Invariant
<invariant>
decomp of (one_step i
| Reg_id | Constraints | Invariant |
|---|---|---|
| 0 | (i.c.car_distance + 20) > 10 i.c.car_drive_state = Braking 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 1 | (i.c.car_distance + 20) <= 10 i.c.car_drive_state = Braking 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 2 | (i.c.car_distance + 20) > 10 false i.c.car_drive_state = Braking 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 3 | (i.c.car_distance + 20) <= 10 false i.c.car_drive_state = Braking 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 4 | (i.c.car_distance + 20) > 10 i.c.car_drive_state = Steady 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 5 | (i.c.car_distance + 20) <= 10 i.c.car_drive_state = Steady 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 6 | (i.c.car_distance + 20) > 10 i.c.car_drive_state = Accelerating 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 7 | (i.c.car_distance + 20) <= 10 i.c.car_drive_state = Accelerating 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 8 | (i.c.car_distance + 20) > 10 false i.c.car_drive_state = Accelerating 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 9 | (i.c.car_distance + 20) <= 10 false i.c.car_drive_state = Accelerating 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 10 | i.c.car_drive_state = Braking 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Red
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 11 | false i.c.car_drive_state = Braking 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Red
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 12 | i.c.car_drive_state = Steady 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Red
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 13 | i.c.car_drive_state = Accelerating 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Red
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 14 | false i.c.car_drive_state = Accelerating 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Red
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 15 | i.c.car_drive_state = Braking i.l.light_state = Red i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Green
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 16 | false i.c.car_drive_state = Braking i.l.light_state = Red i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Green
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 17 | i.c.car_drive_state = Steady i.l.light_state = Red i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Green
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 18 | i.c.car_drive_state = Accelerating i.l.light_state = Red i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Green
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 19 | false i.c.car_drive_state = Accelerating i.l.light_state = Red i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Green
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 20 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 21 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 22 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 23 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 24 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 25 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 26 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 27 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 28 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 29 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 30 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 31 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 32 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 33 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 34 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 35 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 36 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 37 | not i.l.blinking (i.c.car_distance + 20) > 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 38 | not i.l.blinking (i.c.car_distance + 20) <= 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 39 | i.l.blinking i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 40 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 41 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 42 | not i.l.blinking (i.c.car_distance + 20) > 10 false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 43 | not i.l.blinking (i.c.car_distance + 20) <= 10 false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 44 | i.l.blinking false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = 0
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 45 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 46 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 47 | not i.l.blinking (i.c.car_distance + 20) > 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 48 | not i.l.blinking (i.c.car_distance + 20) <= 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 49 | i.l.blinking i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 50 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 51 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 52 | not i.l.blinking (i.c.car_distance + 20) > 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 53 | not i.l.blinking (i.c.car_distance + 20) <= 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 54 | i.l.blinking i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 55 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 56 | false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 57 | not i.l.blinking (i.c.car_distance + 20) > 10 false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 58 | not i.l.blinking (i.c.car_distance + 20) <= 10 false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 59 | i.l.blinking false i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_max_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
Regions details
No group selected.
- Concrete regions are numbered
- Unnumbered regions are groups whose children share a particular constraint
- Click on a region to view its details
- Double click on a region to zoom in on it
- Shift+double click to zoom out
- Hit escape to reset back to the top
Direct sub-regions: -
Contained regions: -
Constraints
<constraint>
Invariant
<invariant>
decomp of (one_step i
| Reg_id | Constraints | Invariant |
|---|---|---|
| 0 | (i.c.car_distance + 20) > 10 i.c.car_drive_state = Braking 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 1 | (i.c.car_distance + 20) <= 10 i.c.car_drive_state = Braking 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 2 | (i.c.car_distance + 20) > 10 i.c.car_drive_state = Steady 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 3 | (i.c.car_distance + 20) <= 10 i.c.car_drive_state = Steady 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 4 | (i.c.car_distance + 20) > 10 i.c.car_drive_state = Accelerating 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 5 | (i.c.car_distance + 20) <= 10 i.c.car_drive_state = Accelerating 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Yellow
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 6 | i.c.car_drive_state = Braking 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Red
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 7 | i.c.car_drive_state = Steady 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Red
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 8 | i.c.car_drive_state = Accelerating 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 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Red
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 9 | i.c.car_drive_state = Braking i.l.light_state = Red i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Green
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 10 | i.c.car_drive_state = Steady i.l.light_state = Red i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Green
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 11 | i.c.car_drive_state = Accelerating i.l.light_state = Red i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.light_change_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = false
; current_time = i.l.current_time + 1
; light_state = Green
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
}
} |
| 12 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 13 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 14 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 15 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 16 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 17 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 18 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 19 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 20 | i.l.light_change_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 (i.l.current_time + 1) > i.l.blink_time | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
blinking = true
; current_time = i.l.current_time + 1
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 21 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 22 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 23 | not i.l.blinking (i.c.car_distance + 20) > 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 24 | not i.l.blinking (i.c.car_distance + 20) <= 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 25 | i.l.blinking i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Braking i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed - i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 26 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 27 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 28 | not i.l.blinking (i.c.car_distance + 20) > 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 29 | not i.l.blinking (i.c.car_distance + 20) <= 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 30 | i.l.blinking i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Steady i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_distance = i.c.car_distance + i.c.car_speed
; car_speed = i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 31 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Green i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Steady
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 32 | i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Red i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 33 | not i.l.blinking (i.c.car_distance + 20) > 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Accelerating
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 34 | not i.l.blinking (i.c.car_distance + 20) <= 10 i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
| 35 | i.l.blinking i.l.light_change_time >= (i.l.current_time + 1) i.l.blink_time >= (i.l.current_time + 1) i.l.light_state = Yellow i.c.car_drive_state = Accelerating i.c.car_speed = 20 i.c.car_accel_speed = 10 i.c.car_max_speed = 100 i.c.car_min_speed = 0 | intersection.{
c =
car_state.{
car_drive_state = Braking
; car_speed = i.c.car_speed + i.c.car_accel_speed
; car_distance = i.c.car_distance + i.c.car_speed
; car_accel_speed = i.c.car_accel_speed
; car_max_speed = i.c.car_max_speed
; car_min_speed = i.c.car_min_speed
}
; l =
light_state.{
current_time = i.l.current_time + 1
; blinking = i.l.blinking
; blink_time = i.l.blink_time
; light_change_time = i.l.light_change_time
; light_state = i.l.light_state
}
} |
Imandra has computed all the regions of behavior, let's now implement a custom printer using the Imandra-tools library to explore the behavior of the car in plain english:
In [7]:
open Imandra_tools;;
open Region_pp_intf
module Custom = struct
type ty = string
type c =
(* todo: collapse? *)
| DriveState of driving_state
| WithinMaxSpeed of bool
| GoingForwards
| GoingBackwards
| CurrentSpeedEnough of bool
(* todo: collapse? *)
| LightState of color
| LightBlinking of bool
| TimeToBlink
| TimeToChangeLight
let compare _ _ _ = UnComparable
let map _ = id
let driving_state_string = function
| Accelerating -> "accelerating"
| Steady -> "steady"
| Braking -> "braking"
let light_state_string = function
| Green -> "green"
| Yellow -> "yellow"
| Red -> "red"
let print p ~focus out = function
| DriveState d -> Format.fprintf out "Car is %s" (driving_state_string d)
| WithinMaxSpeed b -> Format.fprintf out "Car is %s max speed limits" (if b then "within" else "exceeding")
| GoingForwards -> Format.fprintf out "Car is moving forwards"
| GoingBackwards -> Format.fprintf out "Car is moving backwards"
| LightState l -> Format.fprintf out "Light is %s" (light_state_string l)
| LightBlinking b -> Format.fprintf out "Light is%s blinking" (if b then "" else "n't")
| TimeToBlink -> Format.fprintf out "Time to blink"
| TimeToChangeLight -> Format.fprintf out "Time to change light"
| CurrentSpeedEnough b -> Format.fprintf out "Car's current speed is%s enough to make it in time"
(if b then "" else "n't")
end
module TY = Region_pp.String_conv
module PPrinter = Region_pp.Make (TY) (Custom)
module Refiner = struct
open PPrinter
open Region_pp
exception Ignore
let bool_type = TY.translate_imandra_type Type.bool
let refine_invariant (intersection_s : (string * node) list) : node list =
let open Custom in
match CCOption.map view (List.assoc "c" intersection_s), CCOption.map view (List.assoc "l" intersection_s) with
| Some Struct ("car_state", car_state_s), Some Struct ("light_state", light_state_s) ->
begin
match List.assoc "car_drive_state" car_state_s,
List.assoc "car_speed" car_state_s,
List.assoc "blinking" light_state_s,
List.assoc "light_state" light_state_s
with
| Some {view = (Obj (state, []));ty=obj_ty}, Some ({ty = speed_ty;_} as speed), Some ({ty = blinking_ty;_} as blinking), Some ({ty = light_state_ty;_} as light_state) ->
let speed : node = mk ~ty:bool_type (Eq (mk ~ty:speed_ty (Var "car_speed"), speed)) in
let blinking : node = mk ~ty:bool_type (Eq (mk ~ty:blinking_ty (Var "blinking"), blinking)) in
let light_state : node = mk ~ty:bool_type (Eq (mk ~ty:light_state_ty (Var "light_state"), light_state)) in
begin match state with
| "Accelerating" -> [mk ~ty:obj_ty (Custom (DriveState Accelerating)); speed; blinking; light_state]
| "Steady" -> [mk ~ty:obj_ty (Custom (DriveState Steady)); speed; blinking; light_state]
| "Braking" -> [mk ~ty:obj_ty (Custom (DriveState Braking)); speed; blinking; light_state]
| _ -> raise Ignore
end
| _ -> raise Ignore
end
| _, _ -> raise Ignore
let walk (x : node) : node =
let open Custom in
let r_x = match view x with
| FieldOf (Record, "current_time", {view = FieldOf (Record, "l", {view = Var "i";_});_}) ->
Ok (Var "Current time")
| FieldOf (Record, l, {view = FieldOf (Record, "l", {view = Var "i";_});_}) ->
Ok (Var l)
| FieldOf (Record, c, {view = FieldOf (Record, "c", {view = Var "i";_});_}) ->
Ok (Var c)
| Is (x, _, {view = Var "car_drive_state";_}) ->
begin match x with
| "Accelerating" -> Ok (Custom (DriveState Accelerating))
| "Steady" -> Ok (Custom (DriveState Steady))
| "Braking" -> Ok (Custom (DriveState Braking))
| _ -> Error Ignore
end
| Eq ({view = Var "light_state";ty}, {view = Obj (x, []);_}) ->
Ok (Is (x, [], mk ~ty (Var "light_state")))
| Is (x, _, {view = Var "light_state";_}) ->
begin match x with
| "Green" -> Ok (Custom (LightState Green))
| "Yellow" -> Ok (Custom (LightState Yellow))
| "Red" -> Ok (Custom (LightState Red))
| _ -> Error Ignore
end
| Minus ({view = Var "light_change_time";_}, {view = Int 1;_}) ->
Ok (Custom TimeToChangeLight)
| Minus ({view = Var "blink_time";_}, {view = Int 1;_}) ->
Ok (Custom TimeToBlink)
| Var "blinking" ->
Ok (Custom (LightBlinking true))
| Not ({view = Custom (LightBlinking true);_}) ->
Ok (Custom (LightBlinking false))
| Geq ({view = Var "car_max_speed";_}, {view = Plus ({view = Var "car_speed";_}, {view = Var "car_accel_speed";_});_})
-> Ok (Custom (WithinMaxSpeed true))
| Gt ({view = Plus ({view = Var "car_speed";_}, {view = Var "car_accel_speed";_});_}, {view = Var "car_max_speed";_})
-> Ok (Custom (WithinMaxSpeed false))
| Geq ({view = Minus ({view = Var "car_speed";_}, {view = Var "car_accel_speed";_});_}, {view = Int 0;_})
-> Ok (Custom GoingForwards)
| Gt ({view = Int 0;_}, {view = Minus ({view = Var "car_speed";_}, {view = Var "car_accel_speed";_});_})
-> Ok (Custom GoingBackwards)
(* 10 is currently hard coded in the model *)
| Geq ({view = Int 10;_}, {view = Plus ({view = Var "car_distance";_}, {view = Var "car_speed";_});_})
-> Ok (Custom (CurrentSpeedEnough false))
| Gt ({view = Plus ({view = Var "car_distance";_}, {view = Var "car_speed";_});_}, {view = Int 10;_})
-> Ok (Custom (CurrentSpeedEnough true))
| x -> Ok x
in match r_x with
| Ok node_view -> mk ~ty:x.ty node_view
| Error e -> raise e
let rec refine (node : node) =
try
match view node with
| Eq ({view = Var "F";_}, {view = Struct ("intersection", intersection);_})
-> refine_invariant intersection |> List.flat_map refine
| _ ->
[XF.walk_fix walk node]
with Ignore ->
[]
end;;
let pp_cs ?inv cs =
cs
|> PPrinter.pp ~refine:Refiner.refine ?inv
|> List.map (CCFormat.to_string (PPrinter.Printer.print ()))
let regions_doc d =
Jupyter_imandra.Decompose_render.regions_doc ~pp_cs d;;
#install_doc regions_doc;;
Out[7]:
module Custom :
sig
type ty =
string
type c =
DriveState of
driving_state
| WithinMaxSpeed of
bool
| GoingForwards
| GoingBackwards
| CurrentSpeedEnough of
bool
| LightState of
color
| LightBlinking of
bool
| TimeToBlink
| TimeToChangeLight
val compare :
'a ->
'b ->
'c ->
comparison
val map :
'a ->
'b ->
'b
val driving_state_string :
driving_state ->
ty
val light_state_string :
color ->
ty
val print :
'a ->
focus:'b ->
Format.formatter ->
c ->
unit
end
module TY = Imandra_tools.Region_pp.String_conv
module PPrinter :
sig
type custom = Custom.c
type ty = string
module TY :
sig
type ty = string
val show : ty -> ty
val equal : ty -> ty -> bool
val translate_imandra_type : Type.t -> ty
val mk_tuple : ty list -> ty
val extract_curried_types : ty -> ty list
val extract_tuple_types : ty -> ty list
val mk_list : ty -> ty
val mk_func : ty list -> ty
val type_var : ty -> ty
val mk_set : ty -> ty
end
type nonrec node = (ty, custom) node
type nonrec view = (ty, custom) view
val view : node -> view
val ty : node -> ty
val mk : ty:ty -> view -> node
module XF :
sig
val map : (node -> node) -> node -> node
val walk : pre:(node -> node) -> ?post:(node -> node) -> node -> node
val fix_ : ?bound:int -> ('a -> 'a) -> 'a -> 'a -> 'a
val fix : ?bound:int -> ('a -> 'a) -> 'a -> 'a
val walk_fix : ?bound:int -> (node -> node) -> node -> node
val iterated : unit -> 'a
val iter : f:(node -> unit) -> node -> unit
val exists : f:(node -> bool) -> node -> bool
end
val vars : node -> ty list
val has_symbolic_term : node -> bool
module Printer :
sig
val print :
?p:(node CCFormat.printer ->
Format.formatter -> node -> unit option) ->
?focus:ty -> unit -> node CCFormat.printer
val to_string :
?p:(node CCFormat.printer ->
Format.formatter -> node -> unit option) ->
?focus:ty -> node -> ty
end
module Comparator :
sig
val is_eq : comparison -> bool
val compare : node -> node -> comparison
val compare_all : node list -> node list -> comparison
end
module Simplifier :
sig
val simplify : node -> node
val propagate : node list -> node list
end
module Unifier :
sig
type unifier = node -> node -> node option
val unify : ?unify:unifier -> node list -> node list
end
module Parser : sig val parse : Term.term -> node option end
module Compactor : sig val compact : node list -> node list end
type refiner = node -> node list
type pprinter =
?unify:Unifier.unifier ->
?refine:refiner -> ?inv:bool -> Term.term list -> node list
val pp : pprinter
val print :
?pp:pprinter ->
?unify:Unifier.unifier ->
?refine:refiner ->
?print:(node CCFormat.printer ->
Format.formatter -> node -> unit option) ->
?skip_invariant:bool ->
?focus:ty ->
unit -> Format.formatter -> Top_result.modular_region -> unit
val to_string :
?unify:Unifier.unifier ->
?refine:refiner -> Top_result.modular_region -> ty
end
module Refiner :
sig
exception Ignore
val bool_type : string
val refine_invariant :
(string * PPrinter.node) list -> PPrinter.node list
val walk : PPrinter.node -> PPrinter.node
val refine : PPrinter.node -> PPrinter.node list
end
val pp_cs : ?inv:bool -> Term.term list -> string list = <fun>
val regions_doc : Modular_decomposition.concrete -> Document.t = <fun>