diff --git a/examples/contracts/acc.contract b/examples/contracts/acc.contract index 681ee8b71..56641d406 100644 --- a/examples/contracts/acc.contract +++ b/examples/contracts/acc.contract @@ -3,7 +3,6 @@ import math import random from typing import Union -import builtins import numpy from scenic.core.geometry import normalizeAngle @@ -31,79 +30,13 @@ 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} @@ -111,12 +44,12 @@ component Speedometer(): 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} @@ -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? @@ -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 @@ -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? @@ -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, @@ -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: @@ -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) @@ -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: @@ -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] @@ -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 @@ -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 @@ -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, diff --git a/examples/contracts/dev.contract b/examples/contracts/dev.contract index 9fdaf02c6..9a7c593d3 100644 --- a/examples/contracts/dev.contract +++ b/examples/contracts/dev.contract @@ -3,7 +3,6 @@ import math import random from typing import Union -import builtins import numpy from scenic.core.geometry import normalizeAngle @@ -19,17 +18,17 @@ numpy.random.seed(SEED) ## Components ## -# sensors components +# Dummy Sensors components component NoisyDistanceSystem(stddev, init_seed=1, overestimate=False): """ A component that provides noisy distance to the car in front.""" sensors: - self.leadDist: builtins.float as sensors_distance + self.leadDist: float as sensors_distance outputs: - dist: builtins.float + dist: float state: - seed: builtins.int = init_seed + seed: int = init_seed body: noise = random.gauss(sigma=stddev) @@ -42,10 +41,10 @@ component NoisyDistanceSystem(stddev, init_seed=1, overestimate=False): component Speedometer(): """ Fetches and outputss 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} @@ -53,12 +52,12 @@ component Speedometer(): 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} @@ -69,11 +68,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? @@ -95,18 +94,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 @@ -130,11 +129,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? @@ -152,14 +151,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, @@ -173,13 +172,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: @@ -273,8 +272,8 @@ contract AccurateRelativeSpeeds(perception_distance, abs_dist_err=0.5, abs_speed objects workspace - inputs: - dist: builtins.float + outputs: + dist: float definitions: cars = [obj for obj in objects if hasattr(obj, "isVehicle") and obj.isVehicle and obj.position is not self.position] @@ -300,41 +299,32 @@ contract AccurateRelativeSpeeds(perception_distance, abs_dist_err=0.5, abs_speed always (behind_car implies (relative_speed-abs_speed_err <= true_relative_speed <= relative_speed+abs_speed_err)) contract SafeThrottleFilter(perception_distance, min_dist, min_slowdown, abs_speed_err=0.5, max_brake=float("inf")): - globals: - objects - workspace - + """ 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: - 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 - # Lead speed can be roughly calculated by comparing two timesteps relative_speed = ((next dist) - dist)/self.timestep if (next(next dist)) else ((next dist) - dist)/self.timestep - true_relative_speed = lead_car.speed - self.speed + true_relative_speed = lead_car.speed - speed - stopping_time = math.ceil(self.speed/min_slowdown)+1 - rel_dist_covered = stopping_time*self.speed + (true_relative_speed+abs_speed_err)(max_brake-min_slowdown)*(stopping_time*(stopping_time+1))/2 + stopping_time = math.ceil(speed/min_slowdown)+1 + rel_dist_covered = stopping_time*speed + (true_relative_speed+abs_speed_err)(max_brake-min_slowdown)*(stopping_time*(stopping_time+1))/2 buffer_dist = min_dist + rel_dist_covered guarantees: - # Guarantee that if we are ACTUALLY too close to the car in front of us, we brake with max force. - always behind_car implies ( - lead_dist < buffer_dist implies modulated_throttle == -1) + # Guarantee that if we sense we are too close to the car in front of us, we brake with max force. + always (dist < buffer_dist) implies (modulated_throttle == -1) contract PassthroughBrakingActionGenerator(): + """ A contract stating that the outputted action represents the input throttle""" inputs: - throttle: builtins.float + throttle: float outputs: control_action: RegulatedControlAction @@ -349,7 +339,6 @@ contract PassthroughBrakingActionGenerator(): # TODO: Remove below when PACTI can deduce them from the above always throttle == -1 implies (control_action.throttle == 0 and control_action.brake == 1) -# This contract is an example of an assumption we can make to help prove larger contracts, ideally from our specs or testing. contract MaxBrakingForce(min_slowdown): actions: control_action: RegulatedControlAction @@ -360,57 +349,12 @@ contract MaxBrakingForce(min_slowdown): guarantees: always ((no_throttle and full_brake) - implies ((next self.speed) <= self.speed - min_slowdown) - ) - - -contract SlowdownMaintainsDistance(perception_distance, min_dist, min_slowdown, abs_dist_err=0.5, abs_speed_err=0.5, max_brake=float("inf")): - """ Contract guaranteeing that we always stay at least min_dist away from - any car in front of us. - """ - globals: - objects - workspace - - 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 - - true_relative_speed = lead_car.speed - self.speed - - stopping_time = math.ceil(self.speed/min_slowdown)+1 - rel_dist_covered = stopping_time*self.speed + (true_relative_speed+abs_speed_err)(max_brake-min_slowdown)*(stopping_time*(stopping_time+1))/2 - buffer_dist = min_dist + rel_dist_covered - - no_throttle = throttle_action.throttle == 0 - full_brake = brake_action.brake == 1 - - assumptions: - # Assume we are in a lane - always self._lane is not None - - # Assume the lead car will not brake with more power than max_brake - always behind_car implies ((next lead_car.speed) >= max(0, lead_car.speed - max_brake)) - - # Assume the lead car is not reversing - always behind_car implies (lead_car.speed >= 0) - - # Assume we start outside the danger zone - lead_dist > buffer_dist - - # Assume that we slowdown if we are behind a car and relatively close - always behind_car implies ( - lead_dist < buffer_dist implies ((next self.speed) <= self.speed - min_slowdown) + implies (self.speed == 0 or ((next self.speed) <= self.speed - min_slowdown)) ) - guarantees: - # Guarantee that we always stay at least min_dist behind the lead car - always behind_car implies (lead_dist > min_dist) - +## Overall System Spec ## contract KeepsDistance(perception_distance, min_dist, max_brake=float("inf"), max_accel=float("inf")): + """ A contract stating we stay a safe distance from the car in front of us.""" globals: objects workspace @@ -445,7 +389,7 @@ contract KeepsDistance(perception_distance, min_dist, max_brake=float("inf"), ma # Guarantee that we always stay at least min_dist behind the lead car always behind_car implies (lead_dist > min_dist) - +## Verification Steps ## # Constants STDDEV = 0.1 TARGET_DIST = 10 @@ -463,25 +407,14 @@ ABS_SPEED_ERR = 4 # NOTE: This will set the behavior of the object (based off the Car component). implement "EgoCar" with Car(STDDEV, TARGET_DIST, MAX_SPEED, MIN_DIST, MIN_SLOWDOWN) as car - -accurate_distance = test car.ps satisfies AccurateDistance(PERCEPTION_DISTANCE, abs_dist_err=ABS_DIST_ERR), +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 - max_braking_force = assume car.cc satisfies MaxBrakingForce(MIN_SLOWDOWN), with correctness 0.99, with confidence 0.99 cs_safety = compose over car.cs: # TODO: Replace with proof - test car.cs satisfies AccurateRelativeSpeeds( - PERCEPTION_DISTANCE, - abs_dist_err=ABS_DIST_ERR, - abs_speed_err=ABS_SPEED_ERR, - max_brake=MAX_BRAKE, - max_accel=MAX_ACCEL), - using SimulationTesting(scenario=ENVIRONMENT, maxSteps=6, confidence=0.95, batchSize=10, verbose=False), - terminating after 100 samples - assume car.cs.tsf satisfies SafeThrottleFilter( PERCEPTION_DISTANCE, MIN_DIST, @@ -492,47 +425,9 @@ cs_safety = compose over car.cs: # TODO: Replace with proof assume car.cs.ag satisfies PassthroughBrakingActionGenerator() - # TODO:Replace with proof - assume car.cs satisfies BrakesWhenClose( - PERCEPTION_DISTANCE, - MIN_DIST, - MIN_SLOWDOWN, - abs_dist_err=ABS_DIST_ERR, - abs_speed_err=ABS_SPEED_ERR, - max_brake=MAX_BRAKE, - max_accel=MAX_ACCEL) - keeps_distance_raw = compose over car: use accurate_distance - - # TODO: Replace with proof - test car.cs satisfies AccurateRelativeSpeeds( - PERCEPTION_DISTANCE, - abs_dist_err=ABS_DIST_ERR, - abs_speed_err=ABS_SPEED_ERR, - max_brake=MAX_BRAKE, - max_accel=MAX_ACCEL), - using SimulationTesting(scenario=ENVIRONMENT, maxSteps=6, confidence=0.95, batchSize=10, verbose=False), - terminating after 100 samples - use cs_safety - use max_braking_force - # TODO: Replace with proof - assume car satisfies SlowdownMaintainsDistance( - PERCEPTION_DISTANCE, - MIN_DIST, - MIN_SLOWDOWN, - abs_dist_err=ABS_DIST_ERR, - abs_speed_err=ABS_SPEED_ERR, - max_brake=MAX_BRAKE) - verify keeps_distance_raw - -# keeps_distance = refine keeps_distance_raw as KeepsDistance(PERCEPTION_DISTANCE, -# MIN_DIST, -# abs_dist_err=ABS_DIST_ERR, -# abs_speed_err=ABS_SPEED_ERR, -# max_brake=MAX_BRAKE, -# max_accel=MAX_ACCEL) \ No newline at end of file diff --git a/examples/contracts/dummy1.contract b/examples/contracts/dummy1.contract deleted file mode 100644 index 678fefdb6..000000000 --- a/examples/contracts/dummy1.contract +++ /dev/null @@ -1,47 +0,0 @@ - -component PerceptionSystem(model): - sensors: - self.frontCamera: Image as img - - outputs: - dist: float - - body: - dist = model(img) # Evaluate NN - return {"dist": dist} - -component Controller(target_dist=10): - inputs: - dist: float - - outputs: - action: RegulatedControlAction - - body: - if dist > target_dist: - throttle = 1 - brake = 0 - else: - throttle = 0 - brake = 1 - - action = RegulatedControlAction( - throttle=throttle, - brake=brake - ) - return {"action": action} - -component VehicleActuator: - actions: - control_action: RegulatedControlAction - -component Car: - compose: - ps = PerceptionSystem() - c = Controller() - va = VehicleActuator() - - connect ps.dist to c.dist - connect c.action to va.control_action - - diff --git a/examples/contracts/dummy2.contract b/examples/contracts/dummy2.contract deleted file mode 100644 index 87a35647f..000000000 --- a/examples/contracts/dummy2.contract +++ /dev/null @@ -1,79 +0,0 @@ - - -contract AccurateDistance(abs_dist_err=0.5): - globals: - objects - workspace - - outputs: - dist: float - - definitions: - lead_car = getLeadCar(objects, self) - lead_dist = distance from self to lead_car - - assumptions: - always workspace.weather != "FOG" - - guarantees: - always lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err - -contract SafeControls(min_dist): - globals: - objects - - inputs: - dist: float - - outputs: - action: RegulatedControlAction - - definitions: - lead_car = getLeadCar(objects, self) - lead_dist = distance from self to lead_car - full_braking = action.throttle == 0 and action.brake == 1 - - assumptions: - always lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err - - guarantees: - always (lead_dist < min_dist) implies full_braking - - -contract MinBrakingEffect(min_dist, min_slowdown): - globals: - workspace - - definitions: - full_braking = action.throttle == 0 and action.brake == 1 - vehicle_slowed = self.speed - (next self.speed) > min_slowdown - vehicle_stopped = self.speed == 0 - - inputs: - action: RegulatedControlAction - - assumptions: - always workspace.weather != "SNOW" - - guarantees: - always full_braking implies vehicle_slowed or vehicle_stopped - -contract SafeAutoBrake(): - globals: - objects - workspace - - definitions: - lead_car = getLeadCar(objects, self) - lead_dist = distance from self to lead_car - vehicle_slowed = self.speed - (next self.speed) > min_slowdown - vehicle_stopped = self.speed == 0 - - assumptions: - always workspace.weather not in ("FOG", "SNOW", "RAIN") - - guarantees: - always (lead_dist < min_dist implies - vehicle_slowed or vehicle_stopped) - - diff --git a/examples/contracts/dummy3.contract b/examples/contracts/dummy3.contract deleted file mode 100644 index 72366b677..000000000 --- a/examples/contracts/dummy3.contract +++ /dev/null @@ -1,17 +0,0 @@ - - -raw_safe_auto_brake = compose over car: - test car.ps satisfies AccurateDistance(), - using SimulationTesting(), - terminating after 100 samples - - prove car.c satisfies SafeControls(10), - using Lean4Proof("proof.lean") - - assume car.va satisfies MinBrakingEffect(10, 0.1) - -safe_auto_brake = refine raw_safe_auto_brake as SafeAutoBrake() - -verify safe_auto_brake - - diff --git a/examples/contracts/multisensor_acc.contract b/examples/contracts/multisensor_acc.contract index 1b1ddf26c..4e0237c00 100644 --- a/examples/contracts/multisensor_acc.contract +++ b/examples/contracts/multisensor_acc.contract @@ -1,4 +1,25 @@ +""" A contract describing an automatic cruise control system""" +import math +import random +from typing import Union +import builtins +import numpy + +from scenic.core.geometry import normalizeAngle +from scenic.domains.driving.controllers import PIDLongitudinalController, PIDLateralController +from scenic.domains.driving.actions import RegulatedControlAction + +# ## World File ## +ENVIRONMENT = scenarioFromFile(localPath("highway.scenic"), mode2D=True) + +SEED=5 +random.seed(SEED) +numpy.random.seed(SEED) + +## Components ## + +# Sensors component CameraDistanceSystem(model): """ A component that provides noisy distance to the car in front.""" sensors: @@ -11,10 +32,24 @@ component CameraDistanceSystem(model): return {"dist": model(image)} component RadarDistanceSystem(): - # TODO: Do research but directional distance/velocity? + sensors: + self.frontRadar: float as rdist -component LidarDistanceSystem(): - # TODO: Point cloud + 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: @@ -26,9 +61,25 @@ component DistanceVotingSystem(): med_dist: float body: - # TODO: Do we need to unpack this or can we use stdlib? (For analysis) - median_dist = median(c_dist, r_dist, l_dist) - return {"dist": median_dist} + # 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: @@ -46,48 +97,469 @@ component FusionDistanceSystem(): connect dvs.med_dist to dist -# QUESTION: Can we paramterize the manufacturer condition? -contract RadarManufacturerSpec(abs_dist_err, perception_distance): +component Speedometer(): + """ A component that provides ground truth speed.""" + sensors: + self.speed: float as speed_val + + outputs: + speed: float + + body: + return {"speed": speed_val} + +component DirectionSystem(): + """ A component that provides ground truth directional information.""" + sensors: + self.targetDir: float as sensors_direction + self.heading: float as sensors_heading + outputs: + direction: float + heading: float + + body: + return {"direction": sensors_direction, "heading": sensors_heading} + +# Controller Signal Systems +component PIDThrottleSystem(target_dist, max_speed): + """ A simple PID controller that attempts to maintain a set distance + from the car in front of it while regulating its speed. + """ + inputs: dist: float + speed: float + + outputs: + throttle: float + + state: + # This is for speed, so maybe we need a specific one for distance? + # Not sure what assumptions are made. + pid_controller: PIDLongitudinalController = PIDLongitudinalController(K_D=0.1, K_I=0) + + body: + throttle = state.pid_controller.run_step(dist-target_dist) + + # Basic speed limiter, don't accelerate if we're already going too fast. + if speed >= max_speed: + throttle = min(0, throttle) + + return {"throttle": float(throttle)} + +component ThrottleSafetyFilter(min_dist, min_slowdown, max_brake=5, buffer_padding=0): + """ A component that modulates actions, passing them through unchanged + unless we are dangerously close to the car in front of us, in which case + the actions are swapped to brake with maximum force. + """ + sensors: + self.timestep: float as timestep + + inputs: + dist: float + speed: float + throttle: float + + outputs: + modulated_throttle: float + + state: + last_dist: Union[None, float] = None + + body: + # In first timestep, don't take any action + if state.last_dist is None: + state.last_dist = dist + return {"modulated_throttle": 0.0} + + # If we are in the "danger zone", brake HARD. Otherwise, pass through the inputs actions action. + rel_speed = (state.last_dist - dist)/timestep + stopping_time = math.ceil(rel_speed/min_slowdown)+1 + rel_dist_covered = stopping_time*speed + (max_brake - min_slowdown)*(stopping_time*(stopping_time+1))/2 + danger_dist = min_dist + buffer_padding + max(0, rel_dist_covered) + + # Update last_dist + state.last_dist = dist + + if dist < danger_dist: + return {"modulated_throttle": -1.0} + else: + return {"modulated_throttle": float(throttle)} + +component PIDSteeringSystem(): + inputs: + direction: float + heading: float + + outputs: + steer: float + + state: + # This is for speed, so maybe we need a specific one for distance? + # Not sure what assumptions are made. + pid_controller: PIDLateralController = PIDLateralController() + + body: + direction_err = normalizeAngle(normalizeAngle(heading) - normalizeAngle(direction)) + steer = state.pid_controller.run_step(direction_err) + + return {"steer": steer} + +# Controller Boilerplate + +component ActionGenerator(): + """ Given a throttle and steer signal, outputs a RegulatedControlAction.""" + inputs: + throttle: float + steer: float + + outputs: + control_action: RegulatedControlAction + + state: + past_steer: float = 0.0 + + body: + action = RegulatedControlAction(throttle, steer, state.past_steer, + max_throttle=1, max_brake=1, max_steer=1) + state.past_steer = steer + return {"control_action": action} + + +component ControlSystem(target_dist, max_speed, min_dist, min_slowdown): + """ The control system for a car, combining a PID controller with a + safety filter to generate actions. + """ + inputs: + dist: float + speed: float + direction: float + heading: float + + outputs: + foo: float + control_action: RegulatedControlAction + + compose: + # Create sub-components + pid_ts = PIDThrottleSystem(target_dist, max_speed) + tsf = ThrottleSafetyFilter(min_dist, min_slowdown) + pid_ss = PIDSteeringSystem() + ag = ActionGenerator() + + # DEBUG + connect dist to foo + + # Connect sensors inputss + connect dist to pid_ts.dist + connect speed to pid_ts.speed + connect dist to tsf.dist + connect speed to tsf.speed + connect direction to pid_ss.direction + connect heading to pid_ss.heading + + # Connect pid throttle to filter + connect pid_ts.throttle to tsf.throttle + + # Connect control signals to action generator + connect tsf.modulated_throttle to ag.throttle + connect pid_ss.steer to ag.steer + + # outputs the generated action + connect ag.control_action to control_action + +component CarControls(): + """ This component receives actions for the car and executes them + Convention is that any non-None action passed into an action component + is taken each turn. + """ + actions: + control_action: RegulatedControlAction + +component Car(target_dist, max_speed, min_dist, min_slowdown): + compose: + ps = FusionDistanceSystem() + sm = Speedometer() + ds = DirectionSystem() + cs = ControlSystem(target_dist, max_speed, min_dist, min_slowdown) + cc = CarControls() + + # Connect sensors inputss to controller + connect ps.dist to cs.dist + connect sm.speed to cs.speed + connect ds.direction to cs.direction + connect ds.heading to cs.heading + + # Connect controller actions to car controls + 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: - always in_lane + # 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(abs_dist_err, perception_distance): +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: - always in_lane + # 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(abs_dist_err, perception_distance): +contract AccurateDistance(perception_distance, abs_dist_err=0.5): + """ Contract proving that perceived distance is relatively accurate.""" + globals: + objects + workspace + 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 + assumptions: - always in_lane + # Assume we are in a lane + always self._lane is not None guarantees: - always behind_car implies (lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err) - always (not behind_car) implies (dist > perception_distance+abs_dist_err) + # Guarantee that if we're behind a car (in visible range), that the reported distance + # is relatively accurate. + always (behind_car implies (lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err)) + # Guarantee that if we are not behind a car (or out of visible range), that any reported + # distance is greater than our visible range. + always ((not behind_car) implies (dist > perception_distance+abs_dist_err)) + +contract AccurateRelativeSpeeds(perception_distance, abs_dist_err=0.5, abs_speed_err=0.5, max_brake=float("inf"), max_accel=float("inf")): + """ Contract proving that if we have access to relatively accurate distance, + we can get a relatively accurate relative speed between the two cars (Assuming + max braking/acceleration forces). + """ + globals: + objects + workspace + + 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 + + # Lead speed can be roughly calculated by comparing two timesteps + relative_speed = ((next dist) - dist)/self.timestep if (next(next dist)) else ((next dist) - dist)/self.timestep + true_relative_speed = lead_car.speed - self.speed + + assumptions: + # Assume we are in a lane and have relatively accurate distance + always self._lane is not None + always (behind_car implies (lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err)) + + # Assume that the lead car is not going to brake or accelerate with too much force. + always behind_car implies (-max_brake <= (next lead_car.speed) - lead_car.speed <= max_accel) + + guarantees: + # Guarantee that the perceived speed of the lead car is relatively accurate + always (behind_car implies (relative_speed-abs_speed_err <= true_relative_speed <= relative_speed+abs_speed_err)) + +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: float + speed: float + throttle: float + + outputs: + modulated_throttle: float + + definitions: + # Lead speed can be roughly calculated by comparing two timesteps + relative_speed = ((next dist) - dist)/self.timestep if (next(next dist)) else ((next dist) - dist)/self.timestep + true_relative_speed = lead_car.speed - speed + + stopping_time = math.ceil(speed/min_slowdown)+1 + rel_dist_covered = stopping_time*speed + (true_relative_speed+abs_speed_err)(max_brake-min_slowdown)*(stopping_time*(stopping_time+1))/2 + buffer_dist = min_dist + rel_dist_covered + + guarantees: + # Guarantee that if we sense we are too close to the car in front of us, we brake with max force. + always (dist < buffer_dist) implies (modulated_throttle == -1) + +contract PassthroughBrakingActionGenerator(): + """ A contract stating that the outputted action represents the input throttle""" + inputs: + throttle: float + + outputs: + control_action: RegulatedControlAction + + definitions: + accelerating = throttle >= 0 + braking = throttle < 0 + + guarantees: + always accelerating implies (control_action.throttle == throttle and control_action.brake == 0) + always braking implies (control_action.throttle == 0 and control_action.brake == -throttle) + # TODO: Remove below when PACTI can deduce them from the above + always throttle == -1 implies (control_action.throttle == 0 and control_action.brake == 1) + +contract MaxBrakingForce(min_slowdown): + actions: + control_action: RegulatedControlAction + + definitions: + no_throttle = control_action.throttle == 0 + full_brake = control_action.brake == 1 + + guarantees: + always ((no_throttle and full_brake) + implies (self.speed == 0 or ((next self.speed) <= self.speed - min_slowdown)) + ) + +## Overall System Spec ## +contract KeepsDistance(perception_distance, min_dist, max_brake=float("inf"), max_accel=float("inf")): + """ A contract stating we stay a safe distance from the car in front of us.""" + globals: + objects + workspace + + 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 + + true_relative_speed = lead_car.speed - self.speed + + stopping_time = math.ceil(self.speed/min_slowdown)+1 + rel_dist_covered = stopping_time*self.speed + (true_relative_speed+abs_speed_err)(max_brake-min_slowdown)*(stopping_time*(stopping_time+1))/2 + buffer_dist = min_dist + rel_dist_covered + + assumptions: + # Assume we are in a lane + always self._lane is not None + + # Assume that the lead car is not going to brake or accelerate with too much force. + always behind_car implies (-max_brake <= (next lead_car.speed) - lead_car.speed <= max_accel) + + # Assume the lead car is not reversing + always behind_car implies (lead_car.speed >= 0) + + # Assume we start outside the danger zone + lead_dist > buffer_dist + + guarantees: + # Guarantee that we always stay at least min_dist behind the lead car + always behind_car implies (lead_dist > min_dist) + +## Verification Steps ## +# Constants +TARGET_DIST = 10 +MAX_SPEED = 26.8224 # 60 mph in m/s +MIN_DIST = 5 +MIN_SLOWDOWN = 4.57 # 15 feet per second in m/s +MAX_BRAKE = 5 # TODO: Find reasonable value +MAX_ACCEL = 5 # TODO: Find reasonable value +PERCEPTION_DISTANCE = 250 + +ABS_DIST_ERR = 0.5 +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, + 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, + abs_dist_err=ABS_DIST_ERR, + abs_speed_err=ABS_SPEED_ERR, + max_brake=MAX_BRAKE, + max_accel=MAX_ACCEL) + +ps_accuracy = accurate_distance and accurate_speed + +max_braking_force = assume car.cc satisfies MaxBrakingForce(MIN_SLOWDOWN), with correctness 0.99, with confidence 0.99 + +cs_safety = compose over car.cs: + # TODO: Replace with proof + assume car.cs.tsf satisfies SafeThrottleFilter( + PERCEPTION_DISTANCE, + MIN_DIST, + MIN_SLOWDOWN, + abs_speed_err=ABS_SPEED_ERR, + max_brake=MAX_BRAKE) -implement "EgoCar" with FusionDistanceSystem() as fds + # TODO: Replace with proof + assume car.cs.ag satisfies PassthroughBrakingActionGenerator() -fds_manufacturer_specs = compose over fds: - assume fds.rds satisfies RadarManufacturerSpec(ABS_DIST_ERR, PERCEPTION_DISTANCE) - assume fds.rds satisfies RadarManufacturerSpec(ABS_DIST_ERR, PERCEPTION_DISTANCE) +keeps_distance_raw = compose over car: + use ps_accuracy + use cs_safety + use max_braking_force -missing_specs = AccurateDistance(ABS_DIST_ERR, PERCEPTION_DISTANCE) - fds_manufacturer_specs +keeps_distance = refine keeps_distance_raw as KeepsDistance(PERCEPTION_DISTANCE, + MIN_DIST, + abs_dist_err=ABS_DIST_ERR, + abs_speed_err=ABS_SPEED_ERR, + max_brake=MAX_BRAKE, + max_accel=MAX_ACCEL) using PROOF -# TODO: Scenic verifies missing_specs. Many different routes -# (e.g. test unconfirmed parts of radar/lidar system or test camera system, -# or combination of both?) +verify keeps_distance diff --git a/examples/contracts/orig_dev.contract b/examples/contracts/orig_dev.contract new file mode 100644 index 000000000..3b6a791eb --- /dev/null +++ b/examples/contracts/orig_dev.contract @@ -0,0 +1,585 @@ +""" A contract describing an automatic cruise control system""" + +import math +import random +from typing import Union +import numpy + +from scenic.core.geometry import normalizeAngle +from scenic.domains.driving.controllers import PIDLongitudinalController, PIDLateralController +from scenic.domains.driving.actions import RegulatedControlAction + +# ## World File ## +ENVIRONMENT = scenarioFromFile(localPath("highway.scenic"), mode2D=True) + +SEED=5 +random.seed(SEED) +numpy.random.seed(SEED) + +## Components ## + +# Dummy Sensors components +component NoisyDistanceSystem(stddev, init_seed=1, overestimate=False): + """ A component that provides noisy distance to the car in front.""" + sensors: + self.leadDist: float as sensors_distance + + outputs: + dist: float + + state: + seed: int = init_seed + + body: + noise = random.gauss(sigma=stddev) + if overestimate: + noise = abs(noise) + noisy_distance = sensors_distance + noise + state.seed = random.randint(1,1000000) + return {"dist": noisy_distance} + +component Speedometer(): + """ Fetches and outputss ground truth speed.""" + sensors: + self.speed: float as speed_val + + outputs: + speed: float + + body: + return {"speed": speed_val} + +component DirectionSystem(): + """ A component that provides ground truth directional information.""" + sensors: + self.targetDir: float as sensors_direction + self.heading: float as sensors_heading + + outputs: + direction: float + heading: float + + body: + return {"direction": sensors_direction, "heading": sensors_heading} + +# Controller Signal Systems +component PIDThrottleSystem(target_dist, max_speed): + """ A simple PID controller that attempts to maintain a set distance + from the car in front of it while regulating its speed. + """ + inputs: + dist: float + speed: float + + outputs: + throttle: float + + state: + # This is for speed, so maybe we need a specific one for distance? + # Not sure what assumptions are made. + pid_controller: PIDLongitudinalController = PIDLongitudinalController(K_D=0.1, K_I=0) + + body: + throttle = state.pid_controller.run_step(dist-target_dist) + + # Basic speed limiter, don't accelerate if we're already going too fast. + if speed >= max_speed: + throttle = min(0, throttle) + + return {"throttle": float(throttle)} + +component ThrottleSafetyFilter(min_dist, min_slowdown, max_brake=5, buffer_padding=0): + """ A component that modulates actions, passing them through unchanged + unless we are dangerously close to the car in front of us, in which case + the actions are swapped to brake with maximum force. + """ + sensors: + self.timestep: float as timestep + + inputs: + dist: float + speed: float + throttle: float + + outputs: + modulated_throttle: float + + state: + last_dist: Union[None, float] = None + + body: + # In first timestep, don't take any action + if state.last_dist is None: + state.last_dist = dist + return {"modulated_throttle": 0.0} + + # If we are in the "danger zone", brake HARD. Otherwise, pass through the inputs actions action. + rel_speed = (state.last_dist - dist)/timestep + stopping_time = math.ceil(rel_speed/min_slowdown)+1 + rel_dist_covered = stopping_time*speed + (max_brake - min_slowdown)*(stopping_time*(stopping_time+1))/2 + danger_dist = min_dist + buffer_padding + max(0, rel_dist_covered) + + # Update last_dist + state.last_dist = dist + + if dist < danger_dist: + return {"modulated_throttle": -1.0} + else: + return {"modulated_throttle": float(throttle)} + +component PIDSteeringSystem(): + inputs: + direction: float + heading: float + + outputs: + steer: float + + state: + # This is for speed, so maybe we need a specific one for distance? + # Not sure what assumptions are made. + pid_controller: PIDLateralController = PIDLateralController() + + body: + direction_err = normalizeAngle(normalizeAngle(heading) - normalizeAngle(direction)) + steer = state.pid_controller.run_step(direction_err) + + return {"steer": steer} + +# Controller Boilerplate + +component ActionGenerator(): + """ Given a throttle and steer signal, outputs a RegulatedControlAction.""" + inputs: + throttle: float + steer: float + + outputs: + control_action: RegulatedControlAction + + state: + past_steer: float = 0.0 + + body: + action = RegulatedControlAction(throttle, steer, state.past_steer, + max_throttle=1, max_brake=1, max_steer=1) + state.past_steer = steer + return {"control_action": action} + + +component ControlSystem(target_dist, max_speed, min_dist, min_slowdown): + """ The control system for a car, combining a PID controller with a + safety filter to generate actions. + """ + inputs: + dist: float + speed: float + direction: float + heading: float + + outputs: + foo: float + control_action: RegulatedControlAction + + compose: + # Create sub-components + pid_ts = PIDThrottleSystem(target_dist, max_speed) + tsf = ThrottleSafetyFilter(min_dist, min_slowdown) + pid_ss = PIDSteeringSystem() + ag = ActionGenerator() + + # DEBUG + connect dist to foo + + # Connect sensors inputss + connect dist to pid_ts.dist + connect speed to pid_ts.speed + connect dist to tsf.dist + connect speed to tsf.speed + connect direction to pid_ss.direction + connect heading to pid_ss.heading + + # Connect pid throttle to filter + connect pid_ts.throttle to tsf.throttle + + # Connect control signals to action generator + connect tsf.modulated_throttle to ag.throttle + connect pid_ss.steer to ag.steer + + # outputs the generated action + connect ag.control_action to control_action + +component CarControls(): + """ This component receives actions for the car and executes them + Convention is that any non-None action passed into an action component + is taken each turn. + """ + actions: + control_action: RegulatedControlAction + +component Car(stddev, target_dist, max_speed, min_dist, min_slowdown): + compose: + ps = NoisyDistanceSystem(stddev) + sm = Speedometer() + ds = DirectionSystem() + cs = ControlSystem(target_dist, max_speed, min_dist, min_slowdown) + cc = CarControls() + + # Connect sensors inputss to controller + connect ps.dist to cs.dist + connect sm.speed to cs.speed + connect ds.direction to cs.direction + connect ds.heading to cs.heading + + # Connect controller actions to car controls + connect cs.control_action to cc.control_action + +## Contracts ## +contract AccurateDistance(perception_distance, abs_dist_err=0.5): + """ Contract proving that perceived distance is relatively accurate.""" + globals: + objects + workspace + + 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 + + assumptions: + # Assume we are in a lane + always self._lane is not None + + guarantees: + # Guarantee that if we're behind a car (in visible range), that the reported distance + # is relatively accurate. + always (behind_car implies (lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err)) + # Guarantee that if we are not behind a car (or out of visible range), that any reported + # distance is greater than our visible range. + always ((not behind_car) implies (dist > perception_distance+abs_dist_err)) + +contract AccurateRelativeSpeeds(perception_distance, abs_dist_err=0.5, abs_speed_err=0.5, max_brake=float("inf"), max_accel=float("inf")): + """ Contract proving that if we have access to relatively accurate distance, + we can get a relatively accurate relative speed between the two cars (Assuming + max braking/acceleration forces). + """ + globals: + objects + workspace + + inputs: + 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 + + # Lead speed can be roughly calculated by comparing two timesteps + relative_speed = ((next dist) - dist)/self.timestep if (next(next dist)) else ((next dist) - dist)/self.timestep + true_relative_speed = lead_car.speed - self.speed + + assumptions: + # Assume we are in a lane and have relatively accurate distance + always self._lane is not None + always (behind_car implies (lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err)) + + # Assume that the lead car is not going to brake or accelerate with too much force. + always behind_car implies (-max_brake <= (next lead_car.speed) - lead_car.speed <= max_accel) + + guarantees: + # Guarantee that the perceived speed of the lead car is relatively accurate + always (behind_car implies (relative_speed-abs_speed_err <= true_relative_speed <= relative_speed+abs_speed_err)) + +contract SafeThrottleFilter(perception_distance, min_dist, min_slowdown, abs_speed_err=0.5, max_brake=float("inf")): + globals: + objects + workspace + + inputs: + dist: float + speed: float + throttle: float + + outputs: + modulated_throttle: 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 + + # Lead speed can be roughly calculated by comparing two timesteps + relative_speed = ((next dist) - dist)/self.timestep if (next(next dist)) else ((next dist) - dist)/self.timestep + true_relative_speed = lead_car.speed - self.speed + + stopping_time = math.ceil(self.speed/min_slowdown)+1 + rel_dist_covered = stopping_time*self.speed + (true_relative_speed+abs_speed_err)(max_brake-min_slowdown)*(stopping_time*(stopping_time+1))/2 + buffer_dist = min_dist + rel_dist_covered + + guarantees: + # Guarantee that if we are ACTUALLY too close to the car in front of us, we brake with max force. + always behind_car implies ( + lead_dist < buffer_dist implies modulated_throttle == -1) + +contract PassthroughBrakingActionGenerator(): + inputs: + throttle: float + + outputs: + control_action: RegulatedControlAction + + definitions: + accelerating = throttle >= 0 + braking = throttle < 0 + + guarantees: + always accelerating implies (control_action.throttle == throttle and control_action.brake == 0) + always braking implies (control_action.throttle == 0 and control_action.brake == -throttle) + # TODO: Remove below when PACTI can deduce them from the above + always throttle == -1 implies (control_action.throttle == 0 and control_action.brake == 1) + +contract BrakesWhenClose(perception_distance, min_dist, min_slowdown, abs_dist_err=0.5, abs_speed_err=0.5, max_brake=float("inf"), max_accel=float("inf")): + """ A contract that just says that if we are in the "danger zone", + we will issue an action to brake with max force. + """ + globals: + objects + workspace + + inputs: + dist: float + + outputs: + control_action: RegulatedControlAction + + 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 + + # Lead speed can be roughly calculated by comparing two timesteps + relative_speed = ((next dist) - dist)/self.timestep if (next(next dist)) else ((next dist) - dist)/self.timestep + true_relative_speed = lead_car.speed - self.speed + + stopping_time = math.ceil(self.speed/min_slowdown)+1 + rel_dist_covered = stopping_time*self.speed + (true_relative_speed+abs_speed_err)(max_brake-min_slowdown)*(stopping_time*(stopping_time+1))/2 + buffer_dist = min_dist + rel_dist_covered + + no_throttle = control_action.throttle == 0 + full_brake = control_action.brake == 1 + + assumptions: + # Assume we are in a lane + always self._lane is not None + + # Assume we have relatively accurate distance and relative speed + always (behind_car implies (lead_dist-abs_dist_err <= dist <= lead_dist+abs_dist_err)) + always (behind_car implies (relative_speed-abs_speed_err <= true_relative_speed <= relative_speed+abs_speed_err)) + + # Assume that the lead car is not going to brake or accelerate with too much force. + always behind_car implies (-max_brake <= (next lead_car.speed) - lead_car.speed <= max_accel) + + guarantees: + # Guarantee that if we are ACTUALLY too close to the car in front of us, we brake with max force. + always behind_car implies ( + lead_dist < buffer_dist implies (no_throttle and full_brake)) + +# This contract is an example of an assumption we can make to help prove larger contracts, ideally from our specs or testing. +contract MaxBrakingForce(min_slowdown): + actions: + control_action: RegulatedControlAction + + definitions: + no_throttle = control_action.throttle == 0 + full_brake = control_action.brake == 1 + + guarantees: + always ((no_throttle and full_brake) + implies ((next self.speed) <= self.speed - min_slowdown) + ) + + +contract SlowdownMaintainsDistance(perception_distance, min_dist, min_slowdown, abs_dist_err=0.5, abs_speed_err=0.5, max_brake=float("inf")): + """ Contract guaranteeing that we always stay at least min_dist away from + any car in front of us. + """ + globals: + objects + workspace + + 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 + + true_relative_speed = lead_car.speed - self.speed + + stopping_time = math.ceil(self.speed/min_slowdown)+1 + rel_dist_covered = stopping_time*self.speed + (true_relative_speed+abs_speed_err)(max_brake-min_slowdown)*(stopping_time*(stopping_time+1))/2 + buffer_dist = min_dist + rel_dist_covered + + no_throttle = throttle_action.throttle == 0 + full_brake = brake_action.brake == 1 + + assumptions: + # Assume we are in a lane + always self._lane is not None + + # Assume the lead car will not brake with more power than max_brake + always behind_car implies ((next lead_car.speed) >= max(0, lead_car.speed - max_brake)) + + # Assume the lead car is not reversing + always behind_car implies (lead_car.speed >= 0) + + # Assume we start outside the danger zone + lead_dist > buffer_dist + + # Assume that we slowdown if we are behind a car and relatively close + always behind_car implies ( + lead_dist < buffer_dist implies ((next self.speed) <= self.speed - min_slowdown) + ) + + guarantees: + # Guarantee that we always stay at least min_dist behind the lead car + always behind_car implies (lead_dist > min_dist) + +contract KeepsDistance(perception_distance, min_dist, max_brake=float("inf"), max_accel=float("inf")): + globals: + objects + workspace + + 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 + + true_relative_speed = lead_car.speed - self.speed + + stopping_time = math.ceil(self.speed/min_slowdown)+1 + rel_dist_covered = stopping_time*self.speed + (true_relative_speed+abs_speed_err)(max_brake-min_slowdown)*(stopping_time*(stopping_time+1))/2 + buffer_dist = min_dist + rel_dist_covered + + assumptions: + # Assume we are in a lane + always self._lane is not None + + # Assume that the lead car is not going to brake or accelerate with too much force. + always behind_car implies (-max_brake <= (next lead_car.speed) - lead_car.speed <= max_accel) + + # Assume the lead car is not reversing + always behind_car implies (lead_car.speed >= 0) + + # Assume we start outside the danger zone + lead_dist > buffer_dist + + guarantees: + # Guarantee that we always stay at least min_dist behind the lead car + always behind_car implies (lead_dist > min_dist) + + +# Constants +STDDEV = 0.1 +TARGET_DIST = 10 +MAX_SPEED = 26.8224 # 60 mph in m/s +MIN_DIST = 5 +MIN_SLOWDOWN = 4.57 # 15 feet per second in m/s +MAX_BRAKE = 5 # TODO: Find reasonable value +MAX_ACCEL = 5 # TODO: Find reasonable value +PERCEPTION_DISTANCE = 250 + +ABS_DIST_ERR = 0.5 +ABS_SPEED_ERR = 4 + +# Instantiate Car component and link to object. +# NOTE: This will set the behavior of the object (based off the Car component). +implement "EgoCar" with Car(STDDEV, TARGET_DIST, MAX_SPEED, MIN_DIST, MIN_SLOWDOWN) as car + + +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 + + +max_braking_force = assume car.cc satisfies MaxBrakingForce(MIN_SLOWDOWN), with correctness 0.99, with confidence 0.99 + +cs_safety = compose over car.cs: + # TODO: Replace with proof + test car.cs satisfies AccurateRelativeSpeeds( + PERCEPTION_DISTANCE, + abs_dist_err=ABS_DIST_ERR, + abs_speed_err=ABS_SPEED_ERR, + max_brake=MAX_BRAKE, + max_accel=MAX_ACCEL), + using SimulationTesting(scenario=ENVIRONMENT, maxSteps=6, confidence=0.95, batchSize=10, verbose=False), + terminating after 100 samples + + assume car.cs.tsf satisfies SafeThrottleFilter( + PERCEPTION_DISTANCE, + MIN_DIST, + MIN_SLOWDOWN, + abs_speed_err=ABS_SPEED_ERR, + max_brake=MAX_BRAKE) + + # TODO: Replace with proof + assume car.cs.ag satisfies PassthroughBrakingActionGenerator() + + # TODO:Replace with proof + assume car.cs satisfies BrakesWhenClose( + PERCEPTION_DISTANCE, + MIN_DIST, + MIN_SLOWDOWN, + abs_dist_err=ABS_DIST_ERR, + abs_speed_err=ABS_SPEED_ERR, + max_brake=MAX_BRAKE, + max_accel=MAX_ACCEL) + +keeps_distance_raw = compose over car: + use accurate_distance + + # TODO: Replace with proof + test car.cs satisfies AccurateRelativeSpeeds( + PERCEPTION_DISTANCE, + abs_dist_err=ABS_DIST_ERR, + abs_speed_err=ABS_SPEED_ERR, + max_brake=MAX_BRAKE, + max_accel=MAX_ACCEL), + using SimulationTesting(scenario=ENVIRONMENT, maxSteps=6, confidence=0.95, batchSize=10, verbose=False), + terminating after 100 samples + + use cs_safety + + use max_braking_force + + # TODO: Replace with proof + assume car satisfies SlowdownMaintainsDistance( + PERCEPTION_DISTANCE, + MIN_DIST, + MIN_SLOWDOWN, + abs_dist_err=ABS_DIST_ERR, + abs_speed_err=ABS_SPEED_ERR, + max_brake=MAX_BRAKE) + +verify keeps_distance_raw + +# keeps_distance = refine keeps_distance_raw as KeepsDistance(PERCEPTION_DISTANCE, +# MIN_DIST, +# abs_dist_err=ABS_DIST_ERR, +# abs_speed_err=ABS_SPEED_ERR, +# max_brake=MAX_BRAKE, +# max_accel=MAX_ACCEL) \ No newline at end of file