To use the model with default options, first click SETUP, then click GO-EFFICIENT. Detailed instructions are below.
An extended version of the paper with additional proofs can be found here.
To use KeYmaera to prove safety of the local lane control, first launch KeYmaera and then load llc.key.proof.
powered by NetLogo
view/download model file: dccs.nlogo
This model models the movement of cars on a highway. Each car follows a simple set of rules: it slows down (decelerates) if it is not safely following the car ahead, and speeds up (accelerates) as soon as it is safely behind the car ahead. This model is a visual aid for the paper "Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified." It demonstrates a concrete example of the models verified in section 6.
Click on the SETUP button to set up the cars at the beginning of the lane. Set the NUMBER-OF-CARS to change the number of cars on the road.
Click on GO-EFFICIENT to start the cars moving.
The MAX-ACCELERATION button sets the limit for how the cars may accelerate. (The unit for acceleration is miles per hour per second, so if you know a car can go from 0 to 60mph in 3 seconds, its acceleration may be entered as 60mph/3sec.) In the GO-EFFICIENT simulation, the cars will either accelerate at this maximum, brake in the range of MAX-BRAKING and MIN-BRAKING or coast if the car is stopped or has reached the MAX-SPEED if SPEED-LIMIT is enabled.
The length of the lane may be changed with LANE-LENGTH. The cars will get very small and difficult to see, but the plots will become more interesting.
The RANDOM-SETUP starts the cars in random positions. The GO-RANDOM simulation allows the cars to choose any safe acceleration.
While you experiment with this model, it is important to remember that this is just an example of what has been verified. For instance, the frequent and drastic changes in acceleration would be terrible for passanger comfort. However, the verification proves safety for a large range of models, so a model which follows the overall safety parameters and gives a smooth ride by choosing a more graudaul acceleration is also verified. This demo is provided only as a visual aid.
The cars tend to platoon when they start out in groups and are given a long enough lane to reach the speed limit. This behavior is not programmed in, but rather happens automatically, so verification of this emergent behavior is also automatic. If you choose to SEE-PLATOONS, the cars will change color when they are driving at the speed-limit. If you reduce the speed limit and lengthen the lane, the platoons are more likely to form.
(Note: With a speed-limit of 45mph and default acceleration and braking, it takes 10 cars approximately 14 seconds to form a platoon.)
The plots show three values of the red and green cars as the model runs:
- the position of the car
- the speed of the car (this doesn't exceed the speed limit when the limit is enabled)
- the acceleration of the car (this is plotted point-wise since the value is not continuous)
A single time tick is equivalent to 1/100th of a second.
Our verification model proves the system for lanes with any (finite) length. To deal with the eventual end of a lane, we allow a "stopped car" to act as a permanent barrier, keeping the active cars from driving off the end of the road.
When running the GO-RANDOM simulation, cars will stop or slow down during the simulation. This allows us to observe traffic waves, which are not present in the efficient version.
globals [ hit-limit sample-car lead-car time maxr maxa maxb minb maxs lanel ]
turtles-own [ speed speed-min leader acc eps prev-speed]
to setup
set lanel lane-length / 15
resize-world 0 lanel -4 4
set-patch-size min list ((50 / lanel) * 15.75) 15.75
clear-all
ask patches [ setup-road ]
set maxr (max-reaction * 100)
set maxa (max-acceleration * 0.000009765)
set maxb (max-braking * 0.000009765)
set minb (min-braking * 0.000009765)
set maxs (max-speed * 0.0009771)
setup-cars-inorder
end
to random-setup
set lanel lane-length / 15
resize-world 0 lanel -4 4
set-patch-size min list ((50 / lanel) * 15.75) 15.75
clear-all
ask patches [ setup-road ]
set maxr (max-reaction * 100)
set maxa (max-acceleration * 0.000009765)
set maxb (max-braking * 0.000009765)
set minb (min-braking * 0.000009765)
set maxs (max-speed * 0.0009771)
setup-cars-randomly
end
to random-acc-setup
clear-all
ask patches [ setup-road ]
setup-random-acc
end
to setup-road ;; patch procedure
if ( pycor < 2 ) and ( pycor > -2 ) [ set pcolor white ]
set time 0
end
to setup-cars-inorder
if ( number-of-cars > world-width )
[
user-message (word "There are too many cars for the amount of road. Please decrease the NUMBER-OF-CARS slider to below "
(world-width + 1)
" and press the SETUP button again. The setup has stopped.")
stop
]
set-default-shape turtles "car"
repeat number-of-cars [
crt 1 [
set color blue
setxy random-xcor 0
set heading 90
set speed random-float .005 ;; initial speed has a max val so all cars will fit.
set speed-min 0
set acc ((0 - maxb) + (random-float (maxb + maxa)))
]
]
set sample-car (turtle (random (number-of-cars - 2)))
ask sample-car [ set color red ]
set lead-car (turtle (number-of-cars - 2))
ask lead-car [ set color green ]
let i number-of-cars - 1
ask turtle i [
set leader nobody
setxy max-pxcor 0
set speed 0
set acc 0
]
; set cars stopped and lined up at the starting line
repeat number-of-cars - 1 [
set i i - 1
ask turtle i [
set leader turtle (i + 1)
setxy i 0
set speed 0
set acc 0
]
]
end
to setup-cars-randomly
if ( number-of-cars > world-width )
[
user-message (word "There are too many cars for the amount of road. Please decrease the NUMBER-OF-CARS slider to below "
(world-width + 1)
" and press the SETUP button again. The setup has stopped.")
stop
]
set-default-shape turtles "car"
repeat number-of-cars [
crt 1 [
set color blue
setxy random-xcor 0
set heading 90
set speed random-float .005 ;; initial speed has a max val so all cars will fit.
set speed-min 0
set acc ((0 - maxb) + (random-float (maxb + maxa)))
]
]
set sample-car (turtle (random (number-of-cars - 2)))
ask sample-car [ set color red ]
let i number-of-cars - 1
ask turtle i [
set leader nobody
setxy max-pxcor 0
set speed 0
set acc 0
]
; set cars stopped in random position
let n number-of-cars - 1
create-cars-rand-pos n min-pxcor (max-pxcor - 1) 0
ask turtles [
if who != number-of-cars - 1
[
set leader turtle (who + 1)
set speed 0
set acc 0
]
]
set lead-car ([leader] of sample-car)
ask lead-car [ set color green ]
end
to setup-random-acc
if ( number-of-cars > world-width )
[
user-message (word "There are too many cars for the amount of road. Please decrease the NUMBER-OF-CARS slider to below "
(world-width + 1)
" and press the SETUP button again. The setup has stopped.")
stop
]
set-default-shape turtles "car"
repeat number-of-cars [
crt 1 [
set color blue
setxy random-xcor 0
set heading 90
set speed random-float .005 ;; initial speed has a max val so all cars will fit.
set speed-min 0
set acc ((0 - maxb) + (random-float (maxb + maxa)))
]
]
set sample-car (turtle (random (number-of-cars - 1)))
ask sample-car [ set color red ]
let i number-of-cars - 1
ask turtle i [
set leader nobody
setxy max-pxcor 0
set speed 0
set acc 0
]
;; set up cars with random starting acc and speed
set hit-limit 0
repeat number-of-cars - 1 [
set i i - 1
ask turtle i
[ set leader turtle (i + 1)
;create-link-to leader
let safe-limit (([xcor] of leader) - 1 - ((speed ^ 2) / (2 * minb)) + ((([speed] of leader) ^ 2) / (2 * maxb)) - ((maxa / minb) + 1) * ((maxa / 2) * (maxr ^ 2) + maxr * speed))
set safe-limit min (list safe-limit ([xcor] of leader - 1))
if-else i < (safe-limit - (max-pxcor / number-of-cars)) and hit-limit = 0 ; lower limit of pos of car must be ahead of i, else not room for all cars on road
[ set-car-pos (safe-limit - (max-pxcor / number-of-cars)) safe-limit ]
;set-car-pos i safe-limit ]
[
setxy i 0
set speed 0
set acc 0
set hit-limit 1
]
]
]
end
to create-cars-rand-pos [n lower upper i]
if n != 0 [
if-else n = 1
[ ask turtle i
[
setxy ((upper + lower) / 2) 0
]
]
[ let mid (lower + random-float (upper - lower))
if (mid - lower) < (ceiling (n / 2))
[set mid ((ceiling (n / 2)) + lower)]
if (upper - mid) < (floor (n / 2))
[set mid (upper - (floor (n / 2)))]
;set mid ((upper + lower) / 2)
create-cars-rand-pos (ceiling (n / 2)) lower mid i
create-cars-rand-pos (floor (n / 2)) mid upper (i + (ceiling (n / 2)))
]
]
end
to set-car-pos[lower upper]
let rand random-float (upper - lower)
set rand rand + lower
;show rand
setxy rand 0
end
;; this procedure is needed so when we click "Setup" we
;; don't end up with any two cars on the same patch
to separate-cars ;; turtle procedure
if any? other turtles in-radius 1
[ setxy random-xcor 0 ;fd 1
separate-cars ]
end
to go-random
ask turtles
[
if eps >= (1 / maxr) or (random-float 1) < .01 ;eps = random (1 / maxr)
[
set eps 0
if who != (number-of-cars - 1)
[
let safe-limit (([xcor] of leader) - 1 - ((speed ^ 2) / (2 * minb)) + ((([speed] of leader) ^ 2) / (2 * maxb)) - ((maxa / minb) + 1) * ((maxa / 2) * (maxr ^ 2) + maxr * speed))
if-else xcor < safe-limit
;[ set-car-acc (0 - maxb) maxa ]
[
if (((ceiling time * 100) mod 300) = 0)
[set-car-acc 0 maxa
if ((random-float 1) < .05)
[set-car-acc (0 - maxb) 0 ]]
]
[ set-car-acc (0 - maxb) (0 - minb) ]
move-car
if speed < 0
[ set speed 0
set acc 0 ]
if speed-limit
[ if speed >= maxs
[ set speed maxs
set acc 0 ]
]
]
]
]
ask turtles
[
set eps eps + 1
fd speed
]
tick
plot-cars
plot-cars2
if (max [speed] of turtles) = 0 and time > 6
[ stop ]
end
to go-efficient
ask turtles
[
if eps >= (1 / maxr) or (random-float 1) < .08 ;eps = random (1 / maxr)
[
set eps 0
if who != (number-of-cars - 1)
[
let safe-limit (([xcor] of leader) - 1 - ((speed ^ 2) / (2 * minb)) + ((([speed] of leader) ^ 2) / (2 * maxb)) - ((maxa / minb) + 1) * ((maxa / 2) * (maxr ^ 2) + maxr * speed))
if-else xcor < safe-limit
[ set acc maxa ]
[ set-car-acc (0 - maxb) (0 - minb) ]
move-car
if speed < 0
[ set speed 0
set acc 0 ]
if speed-limit
[ if-else speed >= maxs
[ set speed maxs
set acc 0
if see-platoons
[set color pink]]
[
if see-platoons
[
if-else self = sample-car
[set color red]
[
if-else self = lead-car
[set color green]
[set color blue]
]
]
]
]
]
]
]
ask turtles
[
set eps eps + 1
fd speed
]
tick
plot-cars
plot-cars2
if (max [speed] of turtles) = 0 and time > 2
[ stop ]
end
to set-car-acc[lower upper]
let rand random-float (upper - lower)
set rand rand + lower
set acc rand
end
to move-car
set speed (speed + acc)
end
to plot-cars
set time time + .01
set-current-plot "Red Car"
set-current-plot-pen "Position"
plot [xcor] of sample-car
set-current-plot-pen "Velocity"
plot ([speed] of sample-car) * (1 / 0.0009771)
set-current-plot-pen "Acceleration"
plot ([acc] of sample-car) * (1 / 0.000009765)
;set-plot-x-range (time - 200) time
end
to plot-cars2
set-current-plot "Green Car"
set-current-plot-pen "Position"
plot [xcor] of lead-car
set-current-plot-pen "Velocity"
plot ([speed] of lead-car) * (1 / 0.0009771)
set-current-plot-pen "Acceleration"
plot ([acc] of lead-car) * (1 / 0.000009765)
end