From 997940f5cb27ba500dffa7138026a20cc1defc96 Mon Sep 17 00:00:00 2001 From: Eric Vin Date: Tue, 12 Mar 2024 16:07:00 -0700 Subject: [PATCH] Progress on contracts. --- examples/contracts/dev.contract | 27 +- src/scenic/__main__.py | 412 +++++++++++++++-------------- src/scenic/contracts/assumption.py | 20 ++ src/scenic/contracts/contracts.py | 64 ++++- src/scenic/contracts/testing.py | 133 +++------- src/scenic/contracts/translator.py | 29 ++ src/scenic/contracts/utils.py | 2 + src/scenic/contracts/veneer.py | 41 +++ src/scenic/syntax/ast.py | 13 + src/scenic/syntax/compiler.py | 31 ++- src/scenic/syntax/scenic.gram | 17 +- src/scenic/syntax/veneer.py | 11 - test.py | 15 ++ 13 files changed, 492 insertions(+), 323 deletions(-) create mode 100644 src/scenic/contracts/assumption.py create mode 100644 src/scenic/contracts/translator.py create mode 100644 src/scenic/contracts/veneer.py create mode 100644 test.py diff --git a/examples/contracts/dev.contract b/examples/contracts/dev.contract index a79a78887..02d6b6f41 100644 --- a/examples/contracts/dev.contract +++ b/examples/contracts/dev.contract @@ -7,11 +7,8 @@ import builtins import numpy from scenic.core.geometry import normalizeAngle -from scenic.syntax.veneer import * -from scenic.syntax.translator import scenarioFromFile from scenic.domains.driving.controllers import PIDLongitudinalController, PIDLateralController from scenic.domains.driving.actions import RegulatedControlAction -from scenic.contracts.utils import runComponentsSimulation, leadDistance # ## World File ## ENVIRONMENT = scenarioFromFile(localPath("highway.scenic"), mode2D=True) @@ -245,7 +242,7 @@ contract AccurateDistance(perception_distance, abs_dist_err=0.5): dist: float definitions: - cars = [obj for obj in objects if hasattr(obj, "isVehicle") and obj.isVehicle and obj is not self] + 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] @@ -276,7 +273,7 @@ contract AccurateRelativeSpeeds(perception_distance, abs_dist_err=0.5, abs_speed dist: float definitions: - cars = [obj for obj in objects if hasattr(obj, "isVehicle") and obj.isVehicle and obj is not self] + 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] @@ -314,22 +311,16 @@ ABS_SPEED_ERR = 4 implement "EgoCar" with Car(STDDEV, TARGET_DIST, MAX_SPEED, MIN_DIST, MIN_SLOWDOWN) as car distance_testing = test car.ps satisfies AccurateDistance(PERCEPTION_DISTANCE, abs_dist_err=ABS_DIST_ERR),\ - using SimulationTesting(scenario=ENVIRONMENT, maxSteps=6, confidence=0.95, batchSize=1, verbose=False), - terminating after 1 samples + using SimulationTesting(scenario=ENVIRONMENT, maxSteps=6, confidence=0.95, batchSize=10, verbose=False), + terminating after 100 samples speed_testing = test car.cs satisfies AccurateRelativeSpeeds( - PERCEPTION_DISTANCE, + PERCEPTION_DISTANCE, abs_dist_err=ABS_DIST_ERR, abs_speed_err=ABS_SPEED_ERR), - using SimulationTesting(scenario=ENVIRONMENT, maxSteps=6, confidence=0.95, batchSize=1, verbose=False), - terminating after 1 samples + using SimulationTesting(scenario=ENVIRONMENT, maxSteps=6, confidence=0.95, batchSize=10, verbose=False), + terminating after 100 samples -SEED=5 -random.seed(SEED) -numpy.random.seed(SEED) -distance_evidence = verify distance_testing +distance_assumption = assume car.ps satisfies AccurateDistance(PERCEPTION_DISTANCE, abs_dist_err=ABS_DIST_ERR) -SEED=5 -random.seed(SEED) -numpy.random.seed(SEED) -speed_evidence = verify speed_testing +verify distance_assumption diff --git a/src/scenic/__main__.py b/src/scenic/__main__.py index dd72bf8b4..d56a60d16 100644 --- a/src/scenic/__main__.py +++ b/src/scenic/__main__.py @@ -11,11 +11,207 @@ import numpy import scenic +from scenic.contracts.translator import compileContractsFile from scenic.core.distributions import RejectionException import scenic.core.errors as errors from scenic.core.simulators import SimulationCreationError import scenic.syntax.translator as translator + +def scenic_generate(args): + delay = args.delay + mode2D = getattr(args, "2d") + + if not mode2D: + if args.delay is not None: + warnings.warn("Delay parameter is not supported by the 3D viewer.") + if args.zoom != 1: + warnings.warn("Zoom parameter is not supported by the 3D viewer.") + + scenic.setDebuggingOptions( + verbosity=args.verbosity, + fullBacktrace=args.full_backtrace, + debugExceptions=args.pdb, + debugRejections=args.pdb_on_reject, + ) + params = {} + for name, value in args.param: + # Convert params to ints or floats if possible + try: + value = int(value) + except ValueError: + try: + value = float(value) + except ValueError: + pass + params[name] = value + translator.dumpScenicAST = args.dump_scenic_ast + translator.dumpFinalAST = args.dump_ast + translator.dumpASTPython = args.dump_python + translator.usePruning = not args.no_pruning + if args.seed is not None: + if args.verbosity >= 1: + print(f"Using random seed = {args.seed}") + + random.seed(args.seed) + numpy.random.seed(args.seed) + + # Load scenario from file + if args.verbosity >= 1: + print("Beginning scenario construction...") + startTime = time.time() + scenario = errors.callBeginningScenicTrace( + lambda: translator.scenarioFromFile( + args.scenicFile, + params=params, + model=args.model, + scenario=args.scenario, + mode2D=mode2D, + ) + ) + totalTime = time.time() - startTime + if args.verbosity >= 1: + print(f"Scenario constructed in {totalTime:.2f} seconds.") + + if args.simulate: + simulator = errors.callBeginningScenicTrace(scenario.getSimulator) + + def generateScene(maxIterations=2000): + startTime = time.time() + scene, iterations = errors.callBeginningScenicTrace( + lambda: scenario.generate( + maxIterations=maxIterations, verbosity=args.verbosity + ) + ) + if args.verbosity >= 1: + totalTime = time.time() - startTime + print( + f" Generated scene in {iterations} iterations, {totalTime:.4g} seconds." + ) + if args.show_params: + for param, value in scene.params.items(): + print(f' Parameter "{param}": {value}') + return scene, iterations + + def runSimulation(scene): + startTime = time.time() + if args.verbosity >= 1: + print(f" Beginning simulation of {scene.dynamicScenario}...") + try: + simulation = errors.callBeginningScenicTrace( + lambda: simulator.simulate( + scene, + maxSteps=args.time, + verbosity=args.verbosity, + maxIterations=args.max_sims_per_scene, + ) + ) + except SimulationCreationError as e: + if args.verbosity >= 1: + print(f" Failed to create simulation: {e}") + return False + if args.verbosity >= 1: + totalTime = time.time() - startTime + print(f" Ran simulation in {totalTime:.4g} seconds.") + if simulation and args.show_records: + for name, value in simulation.result.records.items(): + if isinstance(value, list): + print(f' Record "{name}": (time series)') + for step, subval in value: + print(f" {step:4d}: {subval}") + else: + print(f' Record "{name}": {value}') + return simulation is not None + + try: + if args.gather_stats is None: + # Generate scenes interactively until killed/count reached + if not args.simulate: # will need matplotlib to draw scene schematic + import matplotlib + import matplotlib.pyplot as plt + + if matplotlib.get_backend().lower() == "agg": + raise RuntimeError( + "need an interactive matplotlib backend to display scenes\n" + "(try installing python3-tk)" + ) + + successCount = 0 + while True: + scene, _ = generateScene() + if args.simulate: + success = runSimulation(scene) + if success: + successCount += 1 + else: + successCount += 1 + if mode2D: + if delay is None: + scene.show2D(zoom=args.zoom) + else: + scene.show2D(zoom=args.zoom, block=False) + plt.pause(delay) + plt.clf() + else: + scene.show(axes=args.axes) + + if 0 < args.count <= successCount: + break + + else: # Gather statistics over the specified number of scenes/iterations + its = [] + maxIterations = 2000 + iterations = 0 + totalIterations = 0 + if args.gather_stats >= 0: # scenes + + def keepGoing(): + return len(its) < args.gather_stats + + else: # iterations + maxIterations = -args.gather_stats + + def keepGoing(): + global maxIterations + maxIterations -= iterations + return maxIterations > 0 + + startTime = time.time() + while keepGoing(): + try: + scene, iterations = generateScene(maxIterations=maxIterations) + except RejectionException: + if args.gather_stats >= 0: + raise + iterations = maxIterations + else: + its.append(iterations) + totalIterations += iterations + totalTime = time.time() - startTime + + count = len(its) if its else float("nan") + print(f"Sampled {len(its)} scenes in {totalTime:.2f} seconds.") + print(f"Average iterations/scene: {totalIterations/count}") + print(f"Average time/iteration: {totalTime/totalIterations:.2g} seconds.") + print(f"Average time/scene: {totalTime/count:.2f} seconds.") + + except KeyboardInterrupt: + pass + + finally: + if args.simulate: + simulator.destroy() + + +def scenic_verify(args): + compileContractsFile(args.scenicFile) + + +def dummy(): # for the 'scenic' entry point to call after importing this module + pass + + +# Intialize parser parser = argparse.ArgumentParser( prog="scenic", add_help=False, @@ -23,8 +219,18 @@ description="Sample from a Scenic scenario, optionally " "running dynamic simulations.", ) +subparsers = parser.add_subparsers() + +parser.add_argument( + "-h", "--help", action="help", default=argparse.SUPPRESS, help=argparse.SUPPRESS +) + +## Scenic "generate" Command ## +generate_parser = subparsers.add_parser("generate") +generate_parser.set_defaults(func=scenic_generate) + -mainOptions = parser.add_argument_group("main options") +mainOptions = generate_parser.add_argument_group("main options") mainOptions.add_argument( "-S", "--simulate", @@ -67,7 +273,7 @@ ) # Simulation options -simOpts = parser.add_argument_group("dynamic simulation options") +simOpts = generate_parser.add_argument_group("dynamic simulation options") simOpts.add_argument( "--time", help="time bound for simulations (default none)", type=int, default=None ) @@ -81,7 +287,7 @@ ) # Interactive rendering options -intOptions = parser.add_argument_group("static scene diagramming options") +intOptions = generate_parser.add_argument_group("static scene diagramming options") intOptions.add_argument( "-d", "--delay", @@ -101,7 +307,7 @@ ) # Debugging options -debugOpts = parser.add_argument_group("debugging options") +debugOpts = generate_parser.add_argument_group("debugging options") debugOpts.add_argument( "--show-params", help="show values of global parameters", action="store_true" ) @@ -142,197 +348,19 @@ " (or iterations, if negative)", ) -parser.add_argument( - "-h", "--help", action="help", default=argparse.SUPPRESS, help=argparse.SUPPRESS -) +## Scenic "verify" Command ## +verify_parser = subparsers.add_parser("verify") +verify_parser.set_defaults(func=scenic_verify) # Positional arguments parser.add_argument("scenicFile", help="a Scenic file to run", metavar="FILE") # Parse arguments and set up configuration -args = parser.parse_args() -delay = args.delay -mode2D = getattr(args, "2d") - -if not mode2D: - if args.delay is not None: - warnings.warn("Delay parameter is not supported by the 3D viewer.") - if args.zoom != 1: - warnings.warn("Zoom parameter is not supported by the 3D viewer.") - -scenic.setDebuggingOptions( - verbosity=args.verbosity, - fullBacktrace=args.full_backtrace, - debugExceptions=args.pdb, - debugRejections=args.pdb_on_reject, -) -params = {} -for name, value in args.param: - # Convert params to ints or floats if possible - try: - value = int(value) - except ValueError: - try: - value = float(value) - except ValueError: - pass - params[name] = value -translator.dumpScenicAST = args.dump_scenic_ast -translator.dumpFinalAST = args.dump_ast -translator.dumpASTPython = args.dump_python -translator.usePruning = not args.no_pruning -if args.seed is not None: - if args.verbosity >= 1: - print(f"Using random seed = {args.seed}") - - random.seed(args.seed) - numpy.random.seed(args.seed) - -# Load scenario from file -if args.verbosity >= 1: - print("Beginning scenario construction...") -startTime = time.time() -scenario = errors.callBeginningScenicTrace( - lambda: translator.scenarioFromFile( - args.scenicFile, - params=params, - model=args.model, - scenario=args.scenario, - mode2D=mode2D, - ) -) -totalTime = time.time() - startTime -if args.verbosity >= 1: - print(f"Scenario constructed in {totalTime:.2f} seconds.") - -if args.simulate: - simulator = errors.callBeginningScenicTrace(scenario.getSimulator) - - -def generateScene(maxIterations=2000): - startTime = time.time() - scene, iterations = errors.callBeginningScenicTrace( - lambda: scenario.generate(maxIterations=maxIterations, verbosity=args.verbosity) - ) - if args.verbosity >= 1: - totalTime = time.time() - startTime - print(f" Generated scene in {iterations} iterations, {totalTime:.4g} seconds.") - if args.show_params: - for param, value in scene.params.items(): - print(f' Parameter "{param}": {value}') - return scene, iterations - - -def runSimulation(scene): - startTime = time.time() - if args.verbosity >= 1: - print(f" Beginning simulation of {scene.dynamicScenario}...") - try: - simulation = errors.callBeginningScenicTrace( - lambda: simulator.simulate( - scene, - maxSteps=args.time, - verbosity=args.verbosity, - maxIterations=args.max_sims_per_scene, - ) - ) - except SimulationCreationError as e: - if args.verbosity >= 1: - print(f" Failed to create simulation: {e}") - return False - if args.verbosity >= 1: - totalTime = time.time() - startTime - print(f" Ran simulation in {totalTime:.4g} seconds.") - if simulation and args.show_records: - for name, value in simulation.result.records.items(): - if isinstance(value, list): - print(f' Record "{name}": (time series)') - for step, subval in value: - print(f" {step:4d}: {subval}") - else: - print(f' Record "{name}": {value}') - return simulation is not None - - -try: - if args.gather_stats is None: - # Generate scenes interactively until killed/count reached - if not args.simulate: # will need matplotlib to draw scene schematic - import matplotlib - import matplotlib.pyplot as plt - - if matplotlib.get_backend().lower() == "agg": - raise RuntimeError( - "need an interactive matplotlib backend to display scenes\n" - "(try installing python3-tk)" - ) - - successCount = 0 - while True: - scene, _ = generateScene() - if args.simulate: - success = runSimulation(scene) - if success: - successCount += 1 - else: - successCount += 1 - if mode2D: - if delay is None: - scene.show2D(zoom=args.zoom) - else: - scene.show2D(zoom=args.zoom, block=False) - plt.pause(delay) - plt.clf() - else: - scene.show(axes=args.axes) - - if 0 < args.count <= successCount: - break - - else: # Gather statistics over the specified number of scenes/iterations - its = [] - maxIterations = 2000 - iterations = 0 - totalIterations = 0 - if args.gather_stats >= 0: # scenes - - def keepGoing(): - return len(its) < args.gather_stats +# Use generate if no subcommand specified +sys.argv = sys.argv +subcommand_list = ["generate", "verify"] +if sys.argv[1] not in subcommand_list: + sys.argv.insert(1, "generate") - else: # iterations - maxIterations = -args.gather_stats - - def keepGoing(): - global maxIterations - maxIterations -= iterations - return maxIterations > 0 - - startTime = time.time() - while keepGoing(): - try: - scene, iterations = generateScene(maxIterations=maxIterations) - except RejectionException: - if args.gather_stats >= 0: - raise - iterations = maxIterations - else: - its.append(iterations) - totalIterations += iterations - totalTime = time.time() - startTime - - count = len(its) if its else float("nan") - print(f"Sampled {len(its)} scenes in {totalTime:.2f} seconds.") - print(f"Average iterations/scene: {totalIterations/count}") - print(f"Average time/iteration: {totalTime/totalIterations:.2g} seconds.") - print(f"Average time/scene: {totalTime/count:.2f} seconds.") - -except KeyboardInterrupt: - pass - -finally: - if args.simulate: - simulator.destroy() - - -def dummy(): # for the 'scenic' entry point to call after importing this module - pass +args = parser.parse_args() +args.func(args) diff --git a/src/scenic/contracts/assumption.py b/src/scenic/contracts/assumption.py new file mode 100644 index 000000000..6be470dea --- /dev/null +++ b/src/scenic/contracts/assumption.py @@ -0,0 +1,20 @@ +from scenic.contracts.contracts import ContractEvidence, ContractResult + + +class Assumption: + def __init__( + self, + ## Compiler Provided ## + contract, + component, + ): + self.contract = contract + self.component = component + + def verify(self): + return ContractResult(self.contract, self.component, AssumptionEvidence()) + + +class AssumptionEvidence(ContractEvidence): + def __str__(self): + return "Assumed" diff --git a/src/scenic/contracts/contracts.py b/src/scenic/contracts/contracts.py index feea15ab7..db0365228 100644 --- a/src/scenic/contracts/contracts.py +++ b/src/scenic/contracts/contracts.py @@ -12,14 +12,19 @@ def __init__(self, **kwargs): assert len(self.objects) <= 1 -class ContractResult: - def __init__(self, assumptions, guarantees, evidence): - self.assumptions = assumptions - self.guarantees = guarantees +class _ContractResultBase: + def __init__(self, contract, component, evidence): + self.contract = contract + self.component = component + self.assumptions = contract.assumptions + self.guarantees = contract.guarantees self.evidence = evidence + +class ContractResult(_ContractResultBase): def __str__(self): string = "ContractResult:\n" + string += f" Component: {self.component}\n" string += " Assumptions:\n" for a in self.assumptions: @@ -35,5 +40,56 @@ def __str__(self): return string +class ProbabilisticContractResult(_ContractResultBase): + def __init__(self, contract, component, evidence): + from scenic.contracts.testing import ProbabilisticEvidence + + if not isinstance(evidence, ProbabilisticEvidence): + raise ValueError("Evidence provided is not ProbabilisticEvidence") + + super().__init__(contract, component, evidence) + + def __str__(self): + string = "ContractResult:\n" + string += f" Component: {self.component}\n" + string += " Assumptions:\n" + + for ai, a in enumerate(self.assumptions): + if self.evidence.a_count == 0: + percent_violated = 0 + else: + percent_violated = ( + sum( + 1 / len(at.violations) + for at in self.evidence.testData + if at.result == TestResult.A and ai in at.violations + ) + / self.evidence.a_count + ) + + string += f" ({percent_violated*100:6.2f}%) {a}\n" + + string += " Guarantees:\n" + + for gi, g in enumerate(self.guarantees): + if self.evidence.g_count == 0: + percent_violated = 0 + else: + percent_violated = ( + sum( + 1 / len(gt.violations) + for gt in self.evidence.testData + if gt.result == TestResult.G and gi in gt.violations + ) + / self.evidence.g_count + ) + + string += f" ({percent_violated*100:6.2f}%) {g}\n" + + string += f" Evidence: \n" + string += " " + str(self.evidence).replace("\n", "\n ") + return string + + class ContractEvidence: pass diff --git a/src/scenic/contracts/testing.py b/src/scenic/contracts/testing.py index 86afc710d..60e51eae1 100644 --- a/src/scenic/contracts/testing.py +++ b/src/scenic/contracts/testing.py @@ -6,10 +6,11 @@ import rv_ltl import scipy -from scenic.contracts.contracts import ContractEvidence, ContractResult +from scenic.contracts.contracts import ContractEvidence, ProbabilisticContractResult from scenic.contracts.utils import linkSetBehavior, lookuplinkedObject from scenic.core.distributions import RejectionException from scenic.core.dynamics import GuardViolation, RejectSimulationException +import scenic.core.object_types from scenic.core.scenarios import Scenario @@ -39,9 +40,7 @@ def __init__( def verify(self): evidence = self._newEvidence() - result = ProbabilisticContractResult( - self.contract.assumptions, self.contract.guarantees, evidence - ) + result = ProbabilisticContractResult(self.contract, self.component, evidence) activeTermConditions = ( self.termConditions if self.termConditions else self.reqConditions @@ -203,33 +202,7 @@ def testScene(self, scene): # Step contract till termination with simulator.simulateStepped(scene, maxSteps=self.maxSteps) as simulation: - print(self.contract.max_lookahead) - # Populate with lookahead values - for _ in range(self.contract.max_lookahead): - # Advance simulation one time step, catching any rejections - try: - simulation.advance() - except ( - RejectSimulationException, - RejectionException, - GuardViolation, - ) as e: - return self._createTestData( - TestResult.R, [], self.scenario, scene, simulation, start_time - ) - - # If the simulation finished, move on. - if simulation.result: - break - - # Update all base value windows - for vw_name, vw in base_value_windows.items(): - vw.update() - - sim_step += 1 - - # Run remaining simulation - while eval_step <= sim_step: + while not simulation.result or eval_step < sim_step: # If simulation not terminated, advance simulation one time step, catching any rejections if not simulation.result: try: @@ -243,18 +216,23 @@ def testScene(self, scene): TestResult.R, [], self.scenario, scene, simulation, start_time ) - # If the simulation didn't finish, update value windows - if not simulation.result: - # Update all base value windows - for vw_name, vw in base_value_windows.items(): - vw.update() + # If the simulation finished, no need to update value windows. + if simulation.result: + continue + + # If the simulation didn't finish, update all base value windows + for vw_name, vw in base_value_windows.items(): + vw.update() - # Increment simulation step - sim_step += 1 + # Increment simulation step + sim_step += 1 - print(value_windows["lead_dist"].window) + # If the sim_step isn't sufficiently ahead of eval_step, hold off on assumption/guarantee + # evaluation for now. + if sim_step - eval_step <= self.contract.max_lookahead: + continue - # Check all assumptions and guarantees + # Check all assumptions prop_params = [eval_step] + list(value_windows.values()) for a_iter, assumption in enumerate(assumptions_monitors): try: @@ -281,6 +259,7 @@ def testScene(self, scene): start_time, ) + # Check all guarantees for g_iter, guarantee in enumerate(guarantees_monitors): try: r_val = guarantee.update(prop_params) @@ -330,17 +309,33 @@ def testScene(self, scene): class EagerValueWindow: def __init__(self, get_val): - self.elapsed_time = 0 + self._elapsed_time = 0 self.get_val = get_val self.window = [] def update(self): new_val = self.get_val() - self.elapsed_time += 1 + + # Try to replace objects with their concrete proxies. + # TODO: Find a better approach for this? + if isinstance(new_val, scenic.core.object_types.Object): + new_val = new_val._copyWith() + elif isinstance(new_val, list): + new_val = [ + v._copyWith() if isinstance(v, scenic.core.object_types.Object) else v + for v in new_val + ] + elif isinstance(new_val, tuple): + new_val = tuple( + v._copyWith() if isinstance(v, scenic.core.object_types.Object) else v + for v in new_val + ) + + self._elapsed_time += 1 self.window.append(new_val) def __getitem__(self, time): - if not time < self.elapsed_time: + if not time < self._elapsed_time: raise InvalidTimeException(time) return self.window[time] @@ -348,13 +343,11 @@ def __getitem__(self, time): class LazyValueWindow: def __init__(self, get_val): - self.elapsed_time = 0 self.get_val = get_val self.window = {} def update(self, time): self.window[time] = self.get_val(time) - self.elapsed_time += max(self.elapsed_time, time) def __getitem__(self, time): if time not in self.window: @@ -458,7 +451,7 @@ def __iter__(self): def __str__(self): string = ( f"Probabilistic Evidence\n" - f"{100*self.correctness:.2f}% Correctness with {100*self.confidence:.2f}% Confidence\n" + f"Minimum {100*self.correctness:.2f}% Correctness with {100*self.confidence:.2f}% Confidence\n" f"Sampled from {self._source_info}\n" f"{self.v_count} Verified, {self.r_count} Rejected, " f"{self.a_count} A-Violated, {self.g_count} G-Violated\n" @@ -493,54 +486,6 @@ def _source_info(self): return f"Scenario '{Path(self.source_filename).name}' (Hash={int.from_bytes(self.source_hash)})" -class ProbabilisticContractResult(ContractResult): - def __init__(self, assumptions, guarantees, evidence): - if not isinstance(evidence, ProbabilisticEvidence): - raise ValueError("Evidence provided is not ProbabilisticEvidence") - - super().__init__(assumptions, guarantees, evidence) - - def __str__(self): - string = "ContractResult:\n" - string += " Assumptions:\n" - - for ai, a in enumerate(self.assumptions): - if self.evidence.a_count == 0: - percent_violated = 0 - else: - percent_violated = ( - sum( - 1 / len(at.violations) - for at in self.evidence.testData - if at.result == TestResult.A and ai in at.violations - ) - / self.evidence.a_count - ) - - string += f" ({percent_violated*100:6.2f}%) {a}\n" - - string += " Guarantees:\n" - - for gi, g in enumerate(self.guarantees): - if self.evidence.g_count == 0: - percent_violated = 0 - else: - percent_violated = ( - sum( - 1 / len(gt.violations) - for gt in self.evidence.testData - if gt.result == TestResult.G and gi in gt.violations - ) - / self.evidence.g_count - ) - - string += f" ({percent_violated*100:6.2f}%) {g}\n" - - string += f" Evidence: \n" - string += " " + str(self.evidence).replace("\n", "\n ") - return string - - ## Termination/Requirement Conditions class Condition(ABC): @abstractmethod diff --git a/src/scenic/contracts/translator.py b/src/scenic/contracts/translator.py new file mode 100644 index 000000000..7da29fd51 --- /dev/null +++ b/src/scenic/contracts/translator.py @@ -0,0 +1,29 @@ +import scenic.contracts.veneer +from scenic.syntax.compiler import compileScenicAST +from scenic.syntax.parser import parse_file + +preamble = """\ +from scenic.syntax.veneer import * +from scenic.contracts.veneer import * +""" + + +def compileContractsFile(filename): + namespace = {} + + # Execute preamble + exec(compile(preamble, "", "exec"), namespace) + + # Execute contract code + scenic_ast = parse_file(filename) + python_ast, _ = compileScenicAST(scenic_ast, filename=filename) + + import ast + + print(ast.unparse(python_ast)) + + compiled_code = compile(python_ast, filename, "exec") + exec(compiled_code, namespace) + + for v_stmt in scenic.contracts.veneer._verifyStatements: + print(v_stmt.verify()) diff --git a/src/scenic/contracts/utils.py b/src/scenic/contracts/utils.py index 4d5d529c0..9e21c52b8 100644 --- a/src/scenic/contracts/utils.py +++ b/src/scenic/contracts/utils.py @@ -122,6 +122,8 @@ def leadDistanceInner(pos, tpos, lane, maxDistance): def leadDistance(source, target, network, maxDistance=250): + # print(source.position, target.position, hash(network)) + # Find all lanes this point could be a part of and recurse on them. viable_lanes = [lane for lane in network.lanes if lane.containsPoint(source.position)] diff --git a/src/scenic/contracts/veneer.py b/src/scenic/contracts/veneer.py new file mode 100644 index 000000000..89676497f --- /dev/null +++ b/src/scenic/contracts/veneer.py @@ -0,0 +1,41 @@ +__all__ = ( + "scenarioFromFile", + # Scenic+Contracts + "BaseComponent", + "ActionComponent", + "ComposeComponent", + "Contract", + "SimulationTesting", + "TimeTerminationCondition", + "CountTerminationCondition", + "GapTerminationCondition", + "CorrectnessRequirementCondition", + "runComponentsSimulation", + "leadDistance", + "registerVerifyStatement", + "Assumption", +) + +# various Python types and functions used in the language but defined elsewhere +from scenic.contracts.testing import SimulationTesting +from scenic.contracts.utils import leadDistance, runComponentsSimulation +from scenic.syntax.translator import scenarioFromFile + +# everything that should not be directly accessible from the language is imported here: +from scenic.contracts.assumption import Assumption +from scenic.contracts.components import ActionComponent, BaseComponent, ComposeComponent +from scenic.contracts.contracts import Contract +from scenic.contracts.testing import ( + CorrectnessRequirementCondition, + CountTerminationCondition, + GapTerminationCondition, + TimeTerminationCondition, +) + +### Internals +_verifyStatements = [] + + +def registerVerifyStatement(stmt): + """Add a verify statement to the global tracker""" + _verifyStatements.append(stmt) diff --git a/src/scenic/syntax/ast.py b/src/scenic/syntax/ast.py index 0603b3115..435fcbf69 100644 --- a/src/scenic/syntax/ast.py +++ b/src/scenic/syntax/ast.py @@ -1372,6 +1372,19 @@ def __init__( self.args = args +class ContractAssume(AST): + def __init__( + self, + contract, + component, + *args, + **kwargs, + ) -> None: + super().__init__(*args, **kwargs) + self.contract = contract + self.component = component + + class ContractVerify(AST): def __init__( self, diff --git a/src/scenic/syntax/compiler.py b/src/scenic/syntax/compiler.py index a30aceae7..f69a7d0f5 100644 --- a/src/scenic/syntax/compiler.py +++ b/src/scenic/syntax/compiler.py @@ -2810,8 +2810,37 @@ def visit_ContractTestReqCond(self, node: s.ContractTestReqCond): keywords=[], ) + def visit_ContractAssume(self, node: s.ContractTest): + # Create component keyword + obj_val = ast.Name(node.component[0], loadCtx) + component_val = obj_val + + if len(node.component) > 1: + for sub_name in node.component[1:]: + component_val = ast.Subscript( + ast.Attribute(component_val, "subcomponents", loadCtx), + ast.Constant(sub_name), + loadCtx, + ) + + # Map contract name + assert isinstance(node.contract, ast.Call) + assert isinstance(node.contract.func, ast.Name) + node.contract.func.id = self.toContractName(node.contract.func.id) + + # Package keywords + keywords = [] + keywords.append(ast.keyword("contract", node.contract)) + keywords.append(ast.keyword("component", component_val)) + + return ast.Call( + func=ast.Name("Assumption", loadCtx), + args=[], + keywords=keywords, + ) + def visit_ContractVerify(self, node: s.ContractVerify): - return ast.Call(ast.Attribute(node.target, "verify", loadCtx), [], []) + return ast.Call(ast.Name("registerVerifyStatement", loadCtx), [node.target], []) def visit_ContractNext(self, node: s.ContractNext): raise self.makeSyntaxError("'next' used outside of temporal requirement.", node) diff --git a/src/scenic/syntax/scenic.gram b/src/scenic/syntax/scenic.gram index 4fdea2ef5..ab87e9cad 100644 --- a/src/scenic/syntax/scenic.gram +++ b/src/scenic/syntax/scenic.gram @@ -574,7 +574,7 @@ scenic_compound_stmt: | scenic_component_def | scenic_contract_def | scenic_assign_contract_test_stmt - | scenic_contract_test_stmt + | scenic_assign_contract_assume_stmt # SIMPLE STATEMENTS # ================= @@ -1022,8 +1022,8 @@ scenic_contract_definition: scenic_contract_temporal_expression_line: | a=scenic_temporal_expression NEWLINE {a} -# Contract Testing -# ---------------- +# Contract Test Statements +# ------------------------ scenic_assign_contract_test_stmt: | a=(z=star_targets '=' { z })+ b=scenic_contract_test_stmt { @@ -1063,6 +1063,17 @@ scenic_contract_test_term_cond: scenic_contract_test_req_cond: | "requiring" x=expression "correctness" {s.ContractTestReqCond("correctness", [x], LOCATIONS)} +# Contract Assume Statements +# -------------------------- + +scenic_assign_contract_assume_stmt: + | a=(z=star_targets '=' { z })+ b=scenic_contract_assume_expr NEWLINE { + ast.Assign(targets=a, value=b, LOCATIONS) + } + +scenic_contract_assume_expr: + | "assume" component=scenic_subcomponent_name \ + "satisfies" contract=primary {s.ContractAssume(contract, component)} # Component/Contracts General # --------------------------- diff --git a/src/scenic/syntax/veneer.py b/src/scenic/syntax/veneer.py index 93622dfa6..544164e7b 100644 --- a/src/scenic/syntax/veneer.py +++ b/src/scenic/syntax/veneer.py @@ -177,20 +177,9 @@ "Always", "Eventually", "Next", - # Scenic+Contracts - "BaseComponent", - "ActionComponent", - "ComposeComponent", - "Contract", - "SimulationTesting", - "TimeTerminationCondition", - "CountTerminationCondition", - "GapTerminationCondition", - "CorrectnessRequirementCondition", ) # various Python types and functions used in the language but defined elsewhere -from scenic.contracts.testing import SimulationTesting from scenic.core.distributions import ( DiscreteRange, Normal, diff --git a/test.py b/test.py new file mode 100644 index 000000000..f45462a08 --- /dev/null +++ b/test.py @@ -0,0 +1,15 @@ +import math +from pathlib import Path + +import pytest +import shapely.geometry +import trimesh.voxel + +from scenic.core.object_types import Object, OrientedPoint +from scenic.core.regions import * +from scenic.core.vectors import VectorField +from tests.utils import sampleSceneFrom + +plane_region = MeshVolumeRegion.fromFile("assets/meshes/classic_plane.obj.bz2") +vr = plane_region.voxelized(max(plane_region.mesh.extents) / 100) +mr = vr.mesh()