From c6930a1de6e44abda8d985b2356b05114a1af883 Mon Sep 17 00:00:00 2001 From: Eric Vin Date: Mon, 27 Nov 2023 20:31:36 -0800 Subject: [PATCH] Full implementation of basic testing for Scenic+Contracts. --- examples/contracts/dev.contract | 18 ++----- src/scenic/contracts/testing.py | 63 +++++++++++++++------- src/scenic/syntax/ast.py | 20 ++++++- src/scenic/syntax/compiler.py | 92 +++++++++++++++++++++++++++++---- src/scenic/syntax/scenic.gram | 25 ++++----- src/scenic/syntax/veneer.py | 12 +++++ 6 files changed, 168 insertions(+), 62 deletions(-) diff --git a/examples/contracts/dev.contract b/examples/contracts/dev.contract index 96f0aefb0..124e5fe15 100644 --- a/examples/contracts/dev.contract +++ b/examples/contracts/dev.contract @@ -11,7 +11,6 @@ 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.testing import SimulationTesting, TimeTerminationCondition, CountTerminationCondition, GapTerminationCondition from scenic.contracts.utils import runComponentsSimulation, leadDistance # ## World File ## @@ -327,23 +326,12 @@ PERCEPTION_DISTANCE = 250 implement "EgoCar" with Car(STDDEV, TARGET_DIST, MAX_SPEED, MIN_DIST, MIN_SLOWDOWN) as car -# distance_testing = SimulationTesting( -# scenario=ENVIRONMENT, -# maxSteps=1, -# confidence=0.95, -# batchSize=5, -# contract=_SCENIC_INTERNAL_CONTRACT_AccurateDistance(PERCEPTION_DISTANCE), -# component=car.subcomponents["ps"], -# obj=car, -# termConditions=[TimeTerminationCondition(5), CountTerminationCondition(100), GapTerminationCondition(0.01)], -# reqConditions=[]) -# distance_testing.verify() - distance_testing = test car.ps satisfies AccurateDistance(PERCEPTION_DISTANCE),\ - using SimulationTesting(scenario=ENVIRONMENT, maxSteps=1, confidence=0.95), + using SimulationTesting(scenario=ENVIRONMENT, maxSteps=1, confidence=0.95, verbose=True), terminating after 5 seconds, terminating after 100 samples, terminating with 0.01 gap, requiring 0.95 correctness -verify distance_testing +distance_evidence = verify distance_testing +print(distance_evidence) diff --git a/src/scenic/contracts/testing.py b/src/scenic/contracts/testing.py index 23500c407..e0e1ec620 100644 --- a/src/scenic/contracts/testing.py +++ b/src/scenic/contracts/testing.py @@ -16,6 +16,7 @@ def __init__( scenario, maxSteps, batchSize=1, + verbose=False, *, confidence, contract, @@ -28,6 +29,7 @@ def __init__( self.scenario = scenario self.maxSteps = maxSteps self.batchSize = batchSize + self.verbose = verbose # Store general args self.confidence = confidence @@ -45,22 +47,28 @@ def verify(self): while not any(cond.check(self.evidence) for cond in self.termConditions): self.evidence.addTests(self.runTests(self.batchSize)) - print(f"{len(self.evidence)} Tests Accumulated") - print(f"Elaped Time: {self.evidence.elapsed_time}") - print( - f"{self.evidence.v_count} Verified, {self.evidence.r_count} Rejected, " - f"{self.evidence.a_count} A-Violated, {self.evidence.g_count} G-Violated" - ) - print( - f"Mean Correctness: {self.evidence.v_count/(self.evidence.v_count+self.evidence.g_count)*100:.2f}%" - ) - print(f"Confidence Gap: {self.evidence.confidenceGap}") - print(f"Correctness Guarantee (Low): {self.evidence.correctness*100:.2f}%") - print() - - print("Terminating:") - for cond in self.termConditions: - print(f" {cond} = {cond.check(self.evidence)}") + if self.verbose: + print(f"{len(self.evidence)} Tests Accumulated") + print(f"Elaped Time: {self.evidence.elapsed_time}") + print( + f"{self.evidence.v_count} Verified, {self.evidence.r_count} Rejected, " + f"{self.evidence.a_count} A-Violated, {self.evidence.g_count} G-Violated" + ) + print( + f"Mean Correctness: {self.evidence.v_count/(self.evidence.v_count+self.evidence.g_count)*100:.2f}%" + ) + print(f"Confidence Gap: {self.evidence.confidenceGap}") + print( + f"Correctness Guarantee (Low): {self.evidence.correctness*100:.2f}%" + ) + print() + + if self.verbose: + print("Terminating:") + for cond in self.termConditions: + print(f" {cond} = {cond.check(self.evidence)}") + + # Check requirements return self.evidence @@ -226,6 +234,7 @@ class ProbabilisticEvidence: def __init__(self, confidence): self.confidence = confidence self.testData = [] + self.requirements_met = None # Initialize metrics self.elapsed_time = 0 @@ -271,9 +280,12 @@ def __len__(self): def __iter__(self): return self.testData + def __str__(self): + return f"Probabilistic Evidence: {100*self.correctness:.2f}% Correctness with {100*self.confidence:.2f}% Confidence" + ## Termination/Requirement Conditions -class TerminationCondition(ABC): +class TermReqCondition(ABC): @abstractmethod def check(self, evidence): raise NotImplementedError() @@ -282,7 +294,7 @@ def __str__(self): return repr(self) -class TimeTerminationCondition(TerminationCondition): +class TimeTerminationCondition(TermReqCondition): def __init__(self, timeout): self.timeout = timeout @@ -293,7 +305,7 @@ def __repr__(self): return f"{self.__class__.__name__}({self.timeout})" -class CountTerminationCondition(TerminationCondition): +class CountTerminationCondition(TermReqCondition): def __init__(self, count): self.count = count @@ -304,7 +316,7 @@ def __repr__(self): return f"{self.__class__.__name__}({self.count})" -class GapTerminationCondition(TerminationCondition): +class GapTerminationCondition(TermReqCondition): def __init__(self, gap): self.gap = gap @@ -313,3 +325,14 @@ def check(self, evidence): def __repr__(self): return f"{self.__class__.__name__}({self.gap})" + + +class CorrectnessRequirementCondition(TermReqCondition): + def __init__(self, correctness): + self.correctness = correctness + + def check(self, evidence): + return evidence.correctness >= self.correctness + + def __repr__(self): + return f"{self.__class__.__name__}({self.correctness})" diff --git a/src/scenic/syntax/ast.py b/src/scenic/syntax/ast.py index 004904ff6..40fbb39b0 100644 --- a/src/scenic/syntax/ast.py +++ b/src/scenic/syntax/ast.py @@ -1307,6 +1307,7 @@ def __init__( *_args, **kwargs, ) -> None: + super().__init__(*_args, **kwargs) self.name = name self.args = args self.docstring = docstring @@ -1322,12 +1323,15 @@ def __init__( class ContractTest(AST): def __init__( self, - component, contract, + component, specifiers, + *args, + **kwargs, ) -> None: - self.component = component + super().__init__(*args, **kwargs) self.contract = contract + self.component = component self.specifiers = specifiers @@ -1335,7 +1339,10 @@ class ContractTestTechnique(AST): def __init__( self, technique, + *args, + **kwargs, ) -> None: + super().__init__(*args, **kwargs) self.technique = technique @@ -1344,7 +1351,10 @@ def __init__( self, cond_type, args, + *_args, + **kwargs, ) -> None: + super().__init__(*_args, **kwargs) self.cond_type = cond_type self.args = args @@ -1354,7 +1364,10 @@ def __init__( self, cond_type, args, + *_args, + **kwargs, ) -> None: + super().__init__(*_args, **kwargs) self.cond_type = cond_type self.args = args @@ -1363,5 +1376,8 @@ class ContractVerify(AST): def __init__( self, target, + *_args, + **kwargs, ) -> None: + super().__init__(*_args, **kwargs) self.target = target diff --git a/src/scenic/syntax/compiler.py b/src/scenic/syntax/compiler.py index b49287631..30263ae34 100644 --- a/src/scenic/syntax/compiler.py +++ b/src/scenic/syntax/compiler.py @@ -2637,22 +2637,94 @@ def visit_ContractDef(self, node: s.ContractDef): type_params=[], ) + def visit_ContractTest(self, node: s.ContractTest): + # Extract testing technique + technique_specs = [ + i for i in node.specifiers if isinstance(i, s.ContractTestTechnique) + ] -def visit_ContractTest(self, node: s.ContractTest): - raise NotImplentedError() + if len(technique_specs) == 0: + raise self.makeSyntaxError("No 'using' specifier used.", node) + if len(technique_specs) > 1: + raise self.makeSyntaxError("More than one 'using' specifier used.", node) -def visit_ContractTestTechnique(self, node: s.ContractTestTechnique): - raise NotImplentedError() + assert len(technique_specs) == 1 + technique = self.visit(technique_specs[0]) + # Extract termination and requirement conditions + term_conds = [ + self.visit(i) + for i in node.specifiers + if isinstance(i, s.ContractTestTermCond) + ] + req_conds = [ + self.visit(i) for i in node.specifiers if isinstance(i, s.ContractTestReqCond) + ] -def visit_ContractTestTermCond(self, node: s.ContractTestTermCond): - raise NotImplentedError() + # 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, + ) -def visit_ContractTestReqCond(self, node: s.ContractTestReqCond): - raise NotImplentedError() + # 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) + # Augment technique call keywords + technique.keywords.append(ast.keyword("contract", node.contract)) + technique.keywords.append(ast.keyword("component", component_val)) + technique.keywords.append(ast.keyword("obj", obj_val)) + technique.keywords.append( + ast.keyword("termConditions", ast.List(term_conds, loadCtx)) + ) + technique.keywords.append( + ast.keyword("reqConditions", ast.List(req_conds, loadCtx)) + ) + + return technique + + def visit_ContractTestTechnique(self, node: s.ContractTestTechnique): + if not isinstance(node.technique, ast.Call): + raise self.makeSyntaxError("Testing technique is malformed.", node) + + return node.technique + + def visit_ContractTestTermCond(self, node: s.ContractTestTermCond): + if node.cond_type == "time": + func_name = "TimeTerminationCondition" + elif node.cond_type == "samples": + func_name = "CountTerminationCondition" + elif node.cond_type == "gap": + func_name = "GapTerminationCondition" + else: + assert False, node.cond_type + + return ast.Call( + func=ast.Name(func_name, loadCtx), + args=[self.visit(a) for a in node.args], + keywords=[], + ) + + def visit_ContractTestReqCond(self, node: s.ContractTestReqCond): + if node.cond_type == "correctness": + func_name = "CorrectnessRequirementCondition" + else: + assert False, node.cond_type + + return ast.Call( + func=ast.Name(func_name, loadCtx), + args=[self.visit(a) for a in node.args], + keywords=[], + ) -def visit_ContractVerify(self, node: s.ContractVerify): - raise NotImplentedError() + def visit_ContractVerify(self, node: s.ContractVerify): + return ast.Call(ast.Attribute(node.target, "verify", loadCtx), [], []) diff --git a/src/scenic/syntax/scenic.gram b/src/scenic/syntax/scenic.gram index 7da5ffec1..f861aeb9a 100644 --- a/src/scenic/syntax/scenic.gram +++ b/src/scenic/syntax/scenic.gram @@ -561,7 +561,6 @@ scenic_stmt: | scenic_abort_stmt | scenic_simulator_stmt | scenic_implement_stmt - | scenic_verify_stmt scenic_compound_stmt: | scenic_tracked_assign_new_stmt @@ -1032,7 +1031,7 @@ scenic_assign_contract_test_stmt: } scenic_contract_test_stmt: - | a=scenic_contract_test_expr b=[scenic_contract_test_block] {s.ContractTest(a[0], a[1], a[2] + (b or []))} + | a=scenic_contract_test_expr b=[scenic_contract_test_block] {s.ContractTest(a[0], a[1], a[2] + (b or []), LOCATIONS)} scenic_contract_test_block: | ',' NEWLINE INDENT b=scenic_contract_test_block_inner DEDENT {b} @@ -1047,28 +1046,23 @@ scenic_contract_test_expr: | "test" component=scenic_subcomponent_name \ "satisfies" contract=primary \ ts=(',' x=scenic_contract_test_spec {x})* \ - {(component, contract, (ts or []))} + {(contract, component, (ts or []))} scenic_contract_test_spec: - | "using" technique=primary {s.ContractTestTechnique(technique)} + | "using" technique=primary {s.ContractTestTechnique(technique, LOCATIONS)} | tc=scenic_contract_test_term_cond {tc} | rc=scenic_contract_test_req_cond {rc} scenic_contract_test_term_cond: - | "terminating" "after" x=NUMBER "seconds" {s.ContractTestTermCond("time", [x])} - | "terminating" "after" x=NUMBER "minutes" {s.ContractTestTermCond("time", [60*x])} - | "terminating" "after" x=NUMBER "hours" {s.ContractTestTermCond("time", [60*60*x])} - | "terminating" "after" x=NUMBER "samples" {s.ContractTestTermCond("samples", [x])} - | "terminating" "with" x=NUMBER "gap" {s.ContractTestTermCond("gap", [x])} + | "terminating" "after" x=expression "seconds" {s.ContractTestTermCond("time", [x], LOCATIONS)} + | "terminating" "after" x=expression "minutes" {s.ContractTestTermCond("time", [ast.Mult(ast.Constant(60),x)], LOCATIONS)} + | "terminating" "after" x=expression "hours" {s.ContractTestTermCond("time", [ast.Mult(ast.Constant(60*60), x)], LOCATIONS)} + | "terminating" "after" x=expression "samples" {s.ContractTestTermCond("samples", [x], LOCATIONS)} + | "terminating" "with" x=expression "gap" {s.ContractTestTermCond("gap", [x], LOCATIONS)} scenic_contract_test_req_cond: - | "requiring" x=NUMBER "correctness" {s.ContractTestReqCond("correctness", x)} + | "requiring" x=expression "correctness" {s.ContractTestReqCond("correctness", [x], LOCATIONS)} -# Contract Verification -# --------------------- - -scenic_verify_stmt: - | "verify" a=NAME {s.ContractVerify(a)} # Component/Contracts General # --------------------------- @@ -1813,6 +1807,7 @@ scenic_prefix_operators: | "visible" e=scenic_prefix_operators { s.VisibleOp(region=e, LOCATIONS) } | 'not' "visible" e=scenic_prefix_operators { s.NotVisibleOp(region=e, LOCATIONS) } | p=scenic_position_of_op_position 'of' e=scenic_prefix_operators { s.PositionOfOp(position=p, target=e, LOCATIONS) } + | "verify" e=scenic_prefix_operators {s.ContractVerify(e, LOCATIONS)} | sum scenic_distance_from_op: diff --git a/src/scenic/syntax/veneer.py b/src/scenic/syntax/veneer.py index 9d935ef37..19ebdb412 100644 --- a/src/scenic/syntax/veneer.py +++ b/src/scenic/syntax/veneer.py @@ -182,9 +182,15 @@ "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, @@ -256,6 +262,12 @@ from scenic.contracts.components import ActionComponent, BaseComponent, ComposeComponent from scenic.contracts.contracts import Contract +from scenic.contracts.testing import ( + CorrectnessRequirementCondition, + CountTerminationCondition, + GapTerminationCondition, + TimeTerminationCondition, +) from scenic.core.distributions import ( Distribution, MultiplexerDistribution,