Skip to content

Commit

Permalink
Re-organized contract examples.
Browse files Browse the repository at this point in the history
  • Loading branch information
@Eric-Vin
Eric-Vin committed Jul 17, 2024
1 parent b974fdd commit d86490d
Show file tree
Hide file tree
Showing 7 changed files with 1,163 additions and 479 deletions.
193 changes: 34 additions & 159 deletions examples/contracts/acc.contract
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
import math
import random
from typing import Union
import builtins
import numpy

from scenic.core.geometry import normalizeAngle
Expand Down Expand Up @@ -31,92 +30,26 @@ component CameraDistanceSystem(model):
body:
return {"dist": model(image)}

component RadarDistanceSystem():
sensors:
self.frontRadar: float as rdist

outputs:
dist: float

body:
return {"dist": rdist}

component LaserDistanceSystem():
sensors:
self.frontLaser: float as ldist

outputs:
dist: float

body:
return {"dist": ldist}

component DistanceVotingSystem():
inputs:
c_dist: float
r_dist: float
l_dist: float

outputs:
med_dist: float

body:
# Unpacked median to make analysis easier.
# TODO: Is this necessary and how can provide syntax to scale this?
if c_dist <= r_dist and c_dist <= l_dist:
if r_dist <= l_dist:
med_dist = r_dist
else:
med_dist = l_dist
elif r_dist <= c_dist and r_dist <= l_dist:
if c_dist <= l_dist:
med_dist = c_dist
else:
med_dist = l_dist
else: #l_dist <= c_dist and l_dist <= r_dist
if c_dist <= r_dist:
med_dist = c_dist
else:
med_dist = r_dist

return {"med_dist": med_dist}

component FusionDistanceSystem():
outputs:
dist: float

compose:
cds = CameraDistanceSystem()
rds = RadarDistanceSystem()
lds = LidarDistanceSystem()
dvs = DistanceVotingSystem()

connect cds.dist to dvs.c_dist
connect rds.dist to dvs.r_dist
connect lds.dist to dvs.l_dist

connect dvs.med_dist to dist

component Speedometer():
""" A component that provides ground truth speed."""
sensors:
self.speed: builtins.float as speed_val
self.speed: float as speed_val

outputs:
speed: builtins.float
speed: float

body:
return {"speed": speed_val}

component DirectionSystem():
""" A component that provides ground truth directional information."""
sensors:
self.targetDir: builtins.float as sensors_direction
self.heading: builtins.float as sensors_heading
self.targetDir: float as sensors_direction
self.heading: float as sensors_heading

outputs:
direction: builtins.float
heading: builtins.float
direction: float
heading: float

body:
return {"direction": sensors_direction, "heading": sensors_heading}
Expand All @@ -127,11 +60,11 @@ component PIDThrottleSystem(target_dist, max_speed):
from the car in front of it while regulating its speed.
"""
inputs:
dist: builtins.float
speed: builtins.float
dist: float
speed: float

outputs:
throttle: builtins.float
throttle: float

state:
# This is for speed, so maybe we need a specific one for distance?
Expand All @@ -153,18 +86,18 @@ component ThrottleSafetyFilter(min_dist, min_slowdown, max_brake=5, buffer_paddi
the actions are swapped to brake with maximum force.
"""
sensors:
self.timestep: builtins.float as timestep
self.timestep: float as timestep

inputs:
dist: builtins.float
speed: builtins.float
throttle: builtins.float
dist: float
speed: float
throttle: float

outputs:
modulated_throttle: builtins.float
modulated_throttle: float

state:
last_dist: Union[None, builtins.float] = None
last_dist: Union[None, float] = None

body:
# In first timestep, don't take any action
Expand All @@ -188,11 +121,11 @@ component ThrottleSafetyFilter(min_dist, min_slowdown, max_brake=5, buffer_paddi

component PIDSteeringSystem():
inputs:
direction: builtins.float
heading: builtins.float
direction: float
heading: float

outputs:
steer: builtins.float
steer: float

state:
# This is for speed, so maybe we need a specific one for distance?
Expand All @@ -210,14 +143,14 @@ component PIDSteeringSystem():
component ActionGenerator():
""" Given a throttle and steer signal, outputs a RegulatedControlAction."""
inputs:
throttle: builtins.float
steer: builtins.float
throttle: float
steer: float

outputs:
control_action: RegulatedControlAction

state:
past_steer: builtins.float = 0.0
past_steer: float = 0.0

body:
action = RegulatedControlAction(throttle, steer, state.past_steer,
Expand All @@ -231,13 +164,13 @@ component ControlSystem(target_dist, max_speed, min_dist, min_slowdown):
safety filter to generate actions.
"""
inputs:
dist: builtins.float
speed: builtins.float
direction: builtins.float
heading: builtins.float
dist: float
speed: float
direction: float
heading: float

outputs:
foo: builtins.float
foo: float
control_action: RegulatedControlAction

compose:
Expand Down Expand Up @@ -278,7 +211,7 @@ component CarControls():

component Car(target_dist, max_speed, min_dist, min_slowdown):
compose:
ps = FusionDistanceSystem()
ps = CameraDistanceSystem()
sm = Speedometer()
ds = DirectionSystem()
cs = ControlSystem(target_dist, max_speed, min_dist, min_slowdown)
Expand All @@ -294,48 +227,6 @@ component Car(target_dist, max_speed, min_dist, min_slowdown):
connect cs.control_action to cc.control_action

## Contracts ##
contract RadarManufacturerSpec(perception_distance, abs_dist_err=0.5):
outputs:
dist: float

definitions:
cars = [obj for obj in objects if hasattr(obj, "isVehicle") and obj.isVehicle and obj.position is not self.position]
lead_distances = {car: leadDistance(self, car, workspace.network, maxDistance=2*perception_distance) for car in cars}
lead_car = sorted(cars, key=lambda x: lead_distances[x])[0]
lead_dist = lead_distances[lead_car]
behind_car = lead_dist <= perception_distance

radar_manufacturer_cond = False # TODO

assumptions:
# Assume we are in a lane
always self._lane is not None

guarantees:
always (behind_car and radar_manufacturer_cond) implies (lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err)
always (not behind_car) implies (dist > perception_distance+abs_dist_err)

contract LidarManufacturerSpec(perception_distance, abs_dist_err=0.5):
outputs:
dist: float

definitions:
cars = [obj for obj in objects if hasattr(obj, "isVehicle") and obj.isVehicle and obj.position is not self.position]
lead_distances = {car: leadDistance(self, car, workspace.network, maxDistance=2*perception_distance) for car in cars}
lead_car = sorted(cars, key=lambda x: lead_distances[x])[0]
lead_dist = lead_distances[lead_car]
behind_car = lead_dist <= perception_distance

lidar_manufacturer_cond = False # TODO

assumptions:
# Assume we are in a lane
always self._lane is not None

guarantees:
always (behind_car and lidar_manufacturer_cond) implies (lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err)
always (not behind_car) implies (dist > perception_distance+abs_dist_err)

contract AccurateDistance(perception_distance, abs_dist_err=0.5):
""" Contract proving that perceived distance is relatively accurate."""
globals:
Expand Down Expand Up @@ -374,7 +265,7 @@ contract AccurateRelativeSpeeds(perception_distance, abs_dist_err=0.5, abs_speed
workspace

outputs:
dist: builtins.float
dist: float

definitions:
cars = [obj for obj in objects if hasattr(obj, "isVehicle") and obj.isVehicle and obj.position is not self.position]
Expand Down Expand Up @@ -402,12 +293,12 @@ contract AccurateRelativeSpeeds(perception_distance, abs_dist_err=0.5, abs_speed
contract SafeThrottleFilter(perception_distance, min_dist, min_slowdown, abs_speed_err=0.5, max_brake=float("inf")):
""" A contract stating that if inputs indicate we are too close for safety, we issue a braking action."""
inputs:
dist: builtins.float
speed: builtins.float
throttle: builtins.float
dist: float
speed: float
throttle: float

outputs:
modulated_throttle: builtins.float
modulated_throttle: float

definitions:
# Lead speed can be roughly calculated by comparing two timesteps
Expand All @@ -425,7 +316,7 @@ contract SafeThrottleFilter(perception_distance, min_dist, min_slowdown, abs_spe
contract PassthroughBrakingActionGenerator():
""" A contract stating that the outputted action represents the input throttle"""
inputs:
throttle: builtins.float
throttle: float

outputs:
control_action: RegulatedControlAction
Expand Down Expand Up @@ -506,26 +397,10 @@ ABS_SPEED_ERR = 4
# Instantiate Car component and link to object.
implement "EgoCar" with Car(TARGET_DIST, MAX_SPEED, MIN_DIST, MIN_SLOWDOWN) as car

# Instantiate over keyword?
ad_goal = AccurateDistance(PERCEPTION_DISTANCE, abs_dist_err=ABS_DIST_ERR)

lds_manufac_guar = assume car.ps.lds
satisfies LidarManufacturerSpec(PERCEPTION_DISTANCE, abs_dist_err=ABS_DIST_ERR)
rds_manufac_guar = assume car.ps.rds
satisfies RadarManufacturerSpec(PERCEPTION_DISTANCE, abs_dist_err=ABS_DIST_ERR)

ad_known = compose over car.ps:
use lds_manufac_guar
use rds_manufac_guar

ad_missing = ad_goal - ad_known

ad_tests = test car.ps satisfies ad_missing,
accurate_distance = test car.ps satisfies AccurateDistance(PERCEPTION_DISTANCE, abs_dist_err=ABS_DIST_ERR),
using SimulationTesting(scenario=ENVIRONMENT, maxSteps=6, confidence=0.95, batchSize=10, verbose=False),
terminating after 100 samples

accurate_distance = refine (ad_known and ad_test) as ad_goal:

# TODO: Replace with proof
accurate_speed = assume car.cs satisfies AccurateRelativeSpeeds(
PERCEPTION_DISTANCE,
Expand Down
Loading

0 comments on commit d86490d

Please sign in to comment.