Full implementation of basic testing for Scenic+Contracts.

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)

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})"

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,20 +1323,26 @@ 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
 
 
 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

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), [], [])

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: