Merge pull request BerkeleyLearnVerify#27 from UCSCFormalMethods/comp…

…ositional_monitors

Compositional monitors

docs/reference/statements.rst

@@ -61,14 +61,19 @@ Monitor Definition
 
 .. code-block:: scenic-grammar
 
-    monitor <name>:
+    monitor <name>(<arguments>):
         <statement>+
 
-Defines a Scenic :term:`monitor`, which runs in parallel with the simulation like a :term:`dynamic behavior`.
+Defines a type of :term:`monitor`, which can be run in parallel with the simulation like a :term:`dynamic behavior`.
 Monitors are not associated with an `Object` and cannot take actions, but can :keyword:`wait` to wait for the next time step (or :keyword:`terminate` the simulation).
+A monitor can be instantiated in a scenario with the :keyword:`require monitor` statement.
+
 The main purpose of monitors is to evaluate complex temporal properties that do not fit into the :keyword:`require always` and :keyword:`require eventually` statements: they can maintain state and use :keyword:`require` to enforce requirements depending on that state.
 For examples of monitors, see our tutorial on :ref:`dynamics`.
 
+.. versionchanged:: 3.0
+    Monitors may take arguments, and must be explicitly instantiated using a :keyword:`require monitor` statement.
+
 .. _modularScenarioDef:
 .. _scenario-stmt:
 .. _setup:
@@ -200,6 +205,29 @@ require (always | eventually) *boolean*
 ---------------------------------------
 Require a condition hold at each time step (``always``) or at some point during the simulation (``eventually``).
 
+.. _require monitor {monitor}:
+.. _require monitor:
+
+require monitor *monitor*
+-------------------------
+Require a condition encoded by a :term:`monitor` hold during the scenario.
+See :ref:`monitorDef` for how to define types of monitors.
+
+It is legal to create multiple instances of a monitor with varying parameters.
+For example::
+
+    monitor ReachesBefore(obj1, region, obj2):
+        reached = False
+        while not reached:
+            if obj1 in region:
+                reached = True
+            else:
+                require obj2 not in region
+                wait
+
+    require monitor ReachesBefore(ego, goal, racecar2)
+    require monitor ReachesBefore(ego, goal, racecar3)
+
 .. _terminate when {boolean}:
 .. _terminate when:
 

docs/syntax_guide.rst

@@ -46,7 +46,7 @@ Compound Statements
      - Defines a Scenic class.
    * - :sampref:`behavior {name}({arguments}): <behaviorDef>`
      - Defines a :term:`dynamic behavior`.
-   * - :sampref:`monitor {name}: <monitorDef>`
+   * - :sampref:`monitor {name}({arguments}): <monitorDef>`
      - Defines a :term:`monitor`.
    * - :sampref:`scenario {name}({arguments}): <modularScenarioDef>`
      - Defines a :term:`modular scenario`.
@@ -73,6 +73,8 @@ Simple Statements
      - Define a soft requirement.
    * - :sampref:`require (always | eventually) {boolean}`
      - Define a dynamic hard requirement.
+   * - :sampref:`require monitor {monitor}`
+     - Define a dynamic requirement using a monitor.
    * - :sampref:`terminate when {boolean}`
      - Define a termination condition.
    * - :sampref:`terminate after {scalar} (seconds | steps)`

docs/tutorials/dynamics.rst

@@ -273,7 +273,7 @@ for the property "``car1`` and ``car2`` enter the intersection before ``car3``":
 .. code-block::
     :linenos:
 
-    monitor Car3EntersLast:
+    monitor Car3EntersLast():
         seen1, seen2 = False, False
         while not (seen1 and seen2):
             require car3 not in intersection
@@ -290,6 +290,14 @@ either ``car1`` or ``car2``, the requirement on line 4 will fail and we will rej
 simulation. Note the necessity of the :keyword:`wait` statement on line 9: if we omitted it, the
 loop could run forever without any time actually passing in the simulation.
 
+Like behaviors, monitors can take parameters, allowing a monitor defined in a library to
+be reused in various situations. To instantiate a monitor in a scenario, use the
+:keyword:`require monitor` statement::
+
+    require monitor Car3EntersLast()
+    require monitor FollowsDrivingRules(ego, speedLimit=65)
+    require monitor FollowsDrivingRules(speedDemon, speedLimit=80)
+
 ..  _guards:
 
 Preconditions and Invariants

src/scenic/core/dynamics.py

@@ -202,6 +202,7 @@ def __init__(self, *args, **kwargs):
         self._agents = []
         self._monitors = []
         self._behaviors = []
+        self._monitorRequirements = []
         self._temporalRequirements = []
         self._terminationConditions = []
         self._terminateSimulationConditions = []
@@ -266,6 +267,7 @@ def _bindTo(self, scene):
         self._workspace = scene.workspace
         self._objects = list(scene.objects)
         self._agents = [obj for obj in scene.objects if obj.behavior is not None]
+        self._monitors = list(scene.monitors)
         self._temporalRequirements = scene.temporalRequirements
         self._terminationConditions = scene.terminationConditions
         self._terminateSimulationConditions = scene.terminateSimulationConditions
@@ -403,6 +405,11 @@ def _stop(self, reason, quiet=False):
                     raise RejectSimulationException(str(req))
         self._requirementMonitors = None
 
+        for monitor in self._monitors:
+            if monitor._isRunning:
+                monitor._stop()
+        self._monitors = []
+
         super()._stop(reason)
         veneer.endScenario(self, reason, quiet=quiet)
         for obj, oldVals in self._overrides.items():
@@ -507,6 +514,13 @@ def _addDynamicRequirement(self, ty, req, line, name):
         dreq = DynamicRequirement(ty, req, line, name)
         self._temporalRequirements.append(dreq)
 
+    def _addMonitor(self, monitor):
+        """Add a monitor during a dynamic simulation."""
+        assert isinstance(monitor, Monitor)
+        self._monitors.append(monitor)
+        if self._isRunning:
+            monitor._start()
+
     def _compileRequirements(self):
         namespace = self._dummyNamespace if self._dummyNamespace else self.__dict__
         requirementSyntax = self._requirementSyntax
@@ -521,6 +535,8 @@ def _compileRequirements(self):
     def _registerCompiledRequirement(self, req):
         if req.ty is RequirementType.require:
             place = self._requirements
+        elif req.ty is RequirementType.monitor:
+            place = self._monitorRequirements
         elif req.ty is RequirementType.terminateWhen:
             place = self._terminationConditions
         elif req.ty is RequirementType.terminateSimulationWhen:
@@ -571,7 +587,7 @@ def _toScenario(self, namespace):
                             self._instances, self._objects, self._ego,
                             self._globalParameters, self._externalParameters,
                             self._requirements, self._requirementDeps,
-                            self._monitors, self._behaviorNamespaces,
+                            self._monitorRequirements, self._behaviorNamespaces,
                             self, astHash)   # TODO unify these!
         return scenario
 
@@ -696,21 +712,9 @@ class Monitor(Behavior):
 
     Monitor statements are translated into definitions of subclasses of this class.
     """
-    def __init_subclass__(cls):
-        super().__init_subclass__()
-        veneer.currentScenario._monitors.append(cls())
-
     def _start(self):
         return super()._start(None)
 
-monitorPrefix = '_Scenic_monitor_'
-def functionForMonitor(name):
-    return monitorPrefix + name
-def isAMonitorName(name):
-    return name.startswith(monitorPrefix)
-def monitorName(name):
-    return name[len(monitorPrefix):]
-
 # Guards
 
 class GuardViolation(Exception):

src/scenic/core/requirements.py

@@ -19,6 +19,7 @@ class RequirementType(enum.Enum):
     require = 'require'
 
     # requirements used only during simulation
+    monitor = 'require monitor'
     terminateWhen = 'terminate when'
     terminateSimulationWhen = 'terminate simulation when'
 

src/scenic/core/scenarios.py

@@ -13,8 +13,9 @@
 from scenic.core.external_params import ExternalSampler
 from scenic.core.regions import EmptyRegion, convertToFootprint
 from scenic.core.vectors import Vector
-from scenic.core.errors import InvalidScenarioError, optionallyDebugRejection
-from scenic.core.dynamics import Behavior
+from scenic.core.errors import (InvalidScenarioError, RuntimeParseError,
+                                optionallyDebugRejection)
+from scenic.core.dynamics import Behavior, Monitor
 from scenic.core.requirements import BoundRequirement
 from scenic.core.serialization import Serializer, dumpAsScenicCode
 
@@ -405,6 +406,14 @@ def _makeSceneFromSample(self, sample):
 			sampledNamespace = { name: sample[value] for name, value in namespace.items() }
 			sampledNamespaces[modName] = (namespace, sampledNamespace, namespace.copy())
 		temporalReqs = (BoundRequirement(req, sample, req.proposition) for req in self.requirements)
+		monitors = []
+		for req in self.monitors:
+			breq = BoundRequirement(req, sample, None)
+			monitor = breq.evaluate()
+			if not isinstance(monitor, Monitor):
+				raise RuntimeParseError('"require monitor X" with X not a monitor'
+				                        f' on line {breq.line}')
+			monitors.append(monitor)
 		terminationConds = (BoundRequirement(req, sample, req.proposition)
  							for req in self.terminationConditions)
 		termSimulationConds = (BoundRequirement(req, sample, req.proposition)
@@ -417,8 +426,8 @@ def _makeSceneFromSample(self, sample):
 		scene = Scene(self.workspace, sampledObjects, ego, sampledParams,
 					  temporalReqs, terminationConds, termSimulationConds,
 					  recordedExprs, recordedInitialExprs,recordedFinalExprs,
-					  self.monitors, sampledNamespaces, self.dynamicScenario,
-					  sample)
+                      monitors, sampledNamespaces, self.dynamicScenario,
+                      sample)
 		return scene
 
 	def resetExternalSampler(self):

src/scenic/core/simulators.py

@@ -337,9 +337,6 @@ def run(self, maxSteps, *, replay=None, enableReplay=True,
             for agent in self.agents:
                 if agent.behavior._isRunning:
                     agent.behavior._stop()
-            for monitor in self.scene.monitors:
-                if monitor._isRunning:
-                    monitor._stop()
             # If the simulation was terminated by an exception (including rejections),
             # some scenarios may still be running; we need to clean them up without
             # checking their requirements, which could raise rejection exceptions.

src/scenic/syntax/ast.py

@@ -162,21 +162,23 @@ def __init__(
 
 
 class MonitorDef(AST):
-    __match_args__ = ("name", "docstring", "body")
+    __match_args__ = ("name", "args", "docstring", "body")
 
     def __init__(
         self,
         name: str,
+        args: ast.arguments,
         docstring: Optional[str],
         body: typing.List[ast.AST],
-        *args: any,
+        *_args: any,
         **kwargs: any
     ) -> None:
-        super().__init__(*args, **kwargs)
+        super().__init__(*_args, **kwargs)
         self.name = name
+        self.args = args
         self.docstring = docstring
         self.body = body
-        self._fields = ["name", "docstring", "body"]
+        self._fields = ["name", "args", "docstring", "body"]
 
 
 class Precondition(AST):
@@ -280,6 +282,22 @@ def __init__(
         self._fields = ["cond", "prob", "name"]
 
 
+class RequireMonitor(AST):
+    __match_args__ = ("monitor", "name")
+
+    def __init__(
+        self,
+        monitor: ast.AST,
+        name: Optional[str] = None,
+        *args: any,
+        **kwargs: any
+    ) -> None:
+        super().__init__(*args, **kwargs)
+        self.monitor = monitor
+        self.name = name
+        self._fields = ["monitor", "name"]
+
+
 class Always(AST):
     __match_args__ = ("value",)
 

src/scenic/syntax/compiler.py

@@ -783,15 +783,7 @@ def visit_MonitorDef(self, node: s.MonitorDef):
         return self.makeBehaviorLikeDef(
             baseClassName="Monitor",
             name=node.name,
-            args=ast.arguments(
-                posonlyargs=[],
-                args=[],
-                vararg=None,
-                kwonlyargs=[],
-                kw_defaults=[],
-                kwarg=None,
-                defaults=[],
-            ),
+            args=node.args,
             docstring=node.docstring,
             header=[],
             body=node.body,
@@ -1090,6 +1082,11 @@ def visit_Require(self, node: s.Require):
             "require", node.cond, node.lineno, node.name, node.prob
         )
 
+    def visit_RequireMonitor(self, node: s.RequireMonitor):
+        return self.createRequirementLike(
+            "require_monitor", node.monitor, node.lineno, node.name
+        )
+
     def visit_Override(self, node: s.Override):
         return ast.Expr(
             value=ast.Call(

src/scenic/syntax/scenic.gram

@@ -845,15 +845,22 @@ scenic_invariant_stmt:
 # -------
 
 scenic_monitor_def:
-    | "monitor" a=NAME &&':' b=scenic_monitor_def_block {
+    | invalid_monitor
+    | "monitor" a=NAME '(' b=[params] ')' &&':' c=scenic_monitor_def_block {
         s.MonitorDef(
             a.string,
-            b[0],
-            b[1],
+            args=b or self.make_arguments(None, [], None, [], None),
+            docstring=c[0],
+            body=c[1],
             LOCATIONS
         )
      }
 
+invalid_monitor[NoReturn]:
+    | "monitor" NAME a=':' {
+            self.raise_syntax_error_known_location("2.0-style monitor must be converted to use parentheses and explicit require", a)
+         }
+
 scenic_monitor_def_block:
     | NEWLINE INDENT a=[x=STRING NEWLINE { x.string }] b=scenic_monitor_statements DEDENT { (a, b) }
 
@@ -1813,6 +1820,9 @@ scenic_param_stmt_id:
     | a=STRING { a.string[1:-1] } # strip quotes
 
 scenic_require_stmt:
+    | 'require' "monitor" e=expression n=['as' scenic_require_stmt_name] {
+        s.RequireMonitor(monitor=e, name=n, LOCATIONS)
+     }
     | 'require' p=['[' a=NUMBER ']' { float(a.string) }] e=expression n=['as' a=scenic_require_stmt_name { a }] {
         s.Require(cond=e, prob=p, name=n, LOCATIONS)
      }

src/scenic/syntax/veneer.py

@@ -13,6 +13,7 @@
 	'ego', 'workspace',
 	'new', 'require', 'resample', 'param', 'globalParameters', 'mutate', 'verbosePrint',
 	'localPath', 'model', 'simulator', 'simulation',
+	'require_monitor',
 	'terminate_when', 'terminate_simulation_when', 'terminate_after', 'in_initial_scenario',
 	'override',
 	'record', 'record_initial', 'record_final',
@@ -463,6 +464,22 @@ def require(reqID, req, line, name, prob=1):
 		currentScenario._addRequirement(requirements.RequirementType.require,
                                         reqID, req, line, name, prob)
 
+def require_monitor(reqID, value, line, name):
+	if not name:
+		name = f'requirement on line {line}'
+	if currentSimulation is not None:
+		monitor = value.evaluate()
+		assert not needsSampling(monitor)
+		if needsLazyEvaluation(monitor):
+			raise RuntimeParseError(f'requirement on line {line} uses value'
+			                        ' undefined outside of object definition')
+		if not isinstance(monitor, Monitor):
+			raise RuntimeParseError(f'"require monitor X" with X not a monitor on line {line}')
+		currentScenario._addMonitor(monitor)
+	else:
+		currentScenario._addRequirement(requirements.RequirementType.monitor,
+		                                reqID, value, line, name, 1)
+
 def record(reqID, value, line, name):
 	if not name:
 		name = f'record{line}'