VerifAI Dynamic Sampling

src/verifai/samplers/domain_sampler.py

@@ -47,22 +47,12 @@ def update(self, sample, info, rho):
         """
         pass
 
-    def nextSample(self, feedback=None):
-        """Generate the next sample, given feedback from the last sample.
-
-        This exists only for backwards-compatibility. It has been replaced by
-        the getSample and update APIs.
-        """
-        if self.last_sample is not None:
-            self.update(self.last_sample, self.last_info, feedback)
-        self.last_sample, self.last_info = self.getSample()
-        return self.last_sample
-
     def __iter__(self):
         try:
-            feedback = None
             while True:
-                feedback = yield self.nextSample(feedback)
+                sample, info = self.getSample()
+                rho = yield sample
+                self.update(sample, info, rho)
         except TerminationException:
             return
 

src/verifai/samplers/feature_sampler.py

@@ -8,8 +8,10 @@
 import dill
 from dotmap import DotMap
 import numpy as np
+from abc import ABC, abstractmethod
+from contextlib import contextmanager
 
-from verifai.features import FilteredDomain
+from verifai.features import FilteredDomain, TimeSeriesFeature, Sample, CompleteSample
 from verifai.samplers.domain_sampler import SplitSampler, TerminationException
 from verifai.samplers.rejection import RejectionSampler
 from verifai.samplers.halton import HaltonSampler
@@ -23,7 +25,7 @@
 
 ### Samplers defined over FeatureSpaces
 
-class FeatureSampler:
+class FeatureSampler(ABC):
     """Abstract class for samplers over FeatureSpaces."""
 
     def __init__(self, space):
@@ -149,29 +151,14 @@ def makeDomainSampler(domain):
                 makeRandomSampler)
         return LateFeatureSampler(space, RandomSampler, makeDomainSampler)
 
-    def getSample(self):
-        """Generate a sample, along with any sampler-specific info.
-
-        Must return a pair consisting of the sample and arbitrary
-        sampler-specific info, which will be passed to the `update`
-        method after the sample is evaluated.
-        """
-        raise NotImplementedError('tried to use abstract FeatureSampler')
-
-    def update(self, sample, info, rho):
+    def update(self, sample_id, rho):
         """Update the state of the sampler after evaluating a sample."""
         pass
 
-    def nextSample(self, feedback=None):
-        """Generate the next sample, given feedback from the last sample.
-
-        This function exists only for backwards compatibility. It has been
-        superceded by the `getSample` and `update` APIs.
-        """
-        if self.last_sample is not None:
-            self.update(self.last_sample, self.last_info, feedback)
-        self.last_sample, self.last_info = self.getSample()
-        return self.last_sample
+    @abstractmethod
+    def getSample(self):
+        """Generate a `Sample`."""
+        pass
 
     def set_graph(self, graph):
         self.scenario.set_graph(graph)
@@ -194,15 +181,22 @@ def restoreFromFile(path):
 
     def __iter__(self):
         try:
-            feedback = None
             while True:
-                feedback = yield self.nextSample(feedback)
+                sample = self.getSample()
+                rho = yield sample
+                sample.update(rho)
         except TerminationException:
             return
 
+
 class LateFeatureSampler(FeatureSampler):
-    """FeatureSampler that works by first sampling only lengths of feature
-    lists, then sampling from the resulting fixed-dimensional Domain.
+    """ FeatureSampler that greedily samples a CompleteSample.
+
+    LateFeatureSampler works as follows:
+        1. Sample lengths of feature lists.
+        2. Expand TimeSeriesFeatures into flattened features of length
+           space.timeBound.
+        3. Sample from the resulting fixed-dimensional Domains.
 
     e.g. LateFeatureSampler(space, RandomSampler, HaltonSampler) creates a
     FeatureSampler which picks lengths uniformly at random and applies
@@ -211,41 +205,76 @@ class LateFeatureSampler(FeatureSampler):
 
     def __init__(self, space, makeLengthSampler, makeDomainSampler):
         super().__init__(space)
+
         lengthDomain, fixedDomains = space.domains
         if lengthDomain is None:    # space has no feature lists
             self.lengthSampler = None
-            self.domainSampler = makeDomainSampler(fixedDomains)
+            self.domainSamplers = {None: makeDomainSampler(fixedDomains)}
         else:
             self.lengthDomain = lengthDomain
             self.lengthSampler = makeLengthSampler(lengthDomain)
             self.domainSamplers = {
                 point: makeDomainSampler(domain)
                 for point, domain in fixedDomains.items()
             }
-            self.lastLength = None
+
+        self._id_metadata_dict = {}
+        self._last_id = 0
+
+    def _get_info_id(self, info, length, sample):
+        self._last_id += 1
+        self._id_metadata_dict[self._last_id] = (info, length, sample)
+        return self._last_id
 
     def getSample(self):
         if self.lengthSampler is None:
-            domainPoint, info = self.domainSampler.getSample()
+            length, info1 = None, None
         else:
             length, info1 = self.lengthSampler.getSample()
-            self.lastLength = length
-            domainPoint, info2 = self.domainSamplers[length].getSample()
-            info = (info1, info2)
-        return self.space.makePoint(*domainPoint), info
-
-    def update(self, sample, info, rho):
+
+        domainPoint, info2 = self.domainSamplers[length].getSample()
+        info = (info1, info2)
+
+        sample_id = self._get_info_id(info, length, domainPoint)
+        update_callback = lambda rho: self.update(sample_id, rho)
+
+        # Make static points and iterable over dynamic points
+        static_features = [v for v in domainPoint._asdict().items()
+                            if v[0] in self.space.staticFeatureNamed]
+        dynamic_features = [v for v in domainPoint._asdict().items()
+                            if v[0] not in self.space.staticFeatureNamed]
+        static_point = self.space.makeStaticPoint(*[v[1] for v in static_features])
+
+        dynamic_points = []
+        if self.space.hasTimeSeries:
+            for t in range(self.space.timeBound):
+                point_dict = {}
+
+                for f, val in dynamic_features:
+                    if not self.space.featureNamed[f].lengthDomain:
+                        point_dict[f] = val[t]
+                    else:
+                        point_dict[f] = tuple(v[t] for v in val)
+
+                dynamic_points.append(self.space.makeDynamicPoint(*point_dict.values()))
+
+
+        dynamicSampleLengths = ({feature_name: getattr(length, feature_name)[0]
+                                 for feature_name, feature in self.space.dynamicFeatureNamed.items()
+                                 if feature.lengthDomain}
+                                if self.lengthSampler else {})
+
+        return CompleteSample(self.space, static_point, dynamic_points, update_callback, dynamicSampleLengths)
+
+    def update(self, sample_id, rho):
+        info, lengthPoint, domainPoint = self._id_metadata_dict[sample_id]
+
         if self.lengthSampler is None:
-            self.domainSampler.update(sample, info, rho)
+            self.domainSamplers[None].update(domainPoint, info[1], rho)
         else:
-            self.lengthSampler.update(sample, info[0], rho)
-            lengths = []
-            for name, feature in self.space.namedFeatures:
-                if feature.lengthDomain:
-                    lengths.append((len(getattr(sample, name)),))
-            lengthPoint = self.lengthDomain.makePoint(*lengths)
-            self.domainSamplers[lengthPoint].update(sample, info[1], rho)
+            self.lengthSampler.update(domainPoint, info[0], rho)
 
+            self.domainSamplers[lengthPoint].update(domainPoint, info[1], rho)
 ### Utilities
 
 def makeRandomSampler(domain):

src/verifai/samplers/scenic_sampler.py

@@ -16,7 +16,7 @@
 
 from verifai.features import (Constant, Categorical, Real, Box, Array, Struct,
                               Feature, FeatureSpace)
-from verifai.samplers.feature_sampler import FeatureSampler
+from verifai.samplers.feature_sampler import FeatureSampler, Sample
 from verifai.utils.frozendict import frozendict
 
 scenicMajorVersion = int(importlib.metadata.version('scenic').split('.')[0])
@@ -223,6 +223,22 @@ def spaceForScenario(scenario, ignoredProperties):
     })
     return space, quotedParams
 
+class ScenicSample(Sample):
+    def __init__(self, space, staticSample, updateCallback, dynamicSampleLengths):
+        super().__init__(space, dynamicSampleLengths)
+        self._staticSample = staticSample
+        self._updateCallback = updateCallback
+
+    @property
+    def staticSample(self):
+        return self._staticSample
+
+    def _getDynamicSample(self, info):
+        raise RuntimeError("ScenicSampler does not support dynamic sampling.")
+
+    def update(self, rho):
+        self._updateCallback(rho)
+
 class ScenicSampler(FeatureSampler):
     """Samples from the induced distribution of a Scenic scenario.
 
@@ -236,14 +252,16 @@ class ScenicSampler(FeatureSampler):
     def __init__(self, scenario, maxIterations=None, ignoredProperties=None):
         self.scenario = scenario
         self.maxIterations = 2000 if maxIterations is None else maxIterations
+        self._nextScene = None
         self.lastScene = None
+        self.lastFeedback = None
         if ignoredProperties is None:
             ignoredProperties = defaultIgnoredProperties
         space, self.quotedParams = spaceForScenario(scenario, ignoredProperties)
         super().__init__(space)
 
     @classmethod
-    def fromScenario(cls, path, maxIterations=None,
+    def fromScenario(cls, path, maxIterations=None, maxSteps=None,
                      ignoredProperties=None, **kwargs):
         """Create a sampler corresponding to a Scenic program.
 
@@ -262,25 +280,44 @@ def fromScenario(cls, path, maxIterations=None,
               e.g. ``params`` to override global parameters or ``model`` to set the
               :term:`world model`.
         """
+        if "params" not in kwargs:
+            kwargs["params"] = {}
+
+        kwargs["params"]["timeBound"] = maxSteps if maxSteps else 0
+
         scenario = scenic.scenarioFromFile(path, **kwargs)
         return cls(scenario, maxIterations=maxIterations,
                    ignoredProperties=ignoredProperties)
 
     @classmethod
-    def fromScenicCode(cls, code, maxIterations=None,
+    def fromScenicCode(cls, code, maxIterations=None, maxSteps=None,
                        ignoredProperties=None, **kwargs):
         """As above, but given a Scenic program as a string."""
+        if "params" not in kwargs:
+            kwargs["params"] = {}
+
+        kwargs["params"]["timeBound"] = maxSteps if maxSteps else 0
+
         scenario = scenic.scenarioFromString(code, **kwargs)
         return cls(scenario, maxIterations=maxIterations,
                    ignoredProperties=ignoredProperties)
 
-    def nextSample(self, feedback=None):
+    def getSample(self):
         ret = self.scenario.generate(
-            maxIterations=self.maxIterations, feedback=feedback, verbosity=0
+            maxIterations=self.maxIterations, feedback=self.lastFeedback, verbosity=0
         )
+
+        self.lastFeedback = None
         self.lastScene, _ = ret
+
         return self.pointForScene(self.lastScene)
 
+    def update(self, sample_id, rho):
+        assert sample_id == 0
+        if self.lastFeedback is not None:
+            raise RuntimeError("Called `update` twice in a row (ScenicSampler does not support non-sequential sampling)")
+        self.lastFeedback = rho
+
     def pointForScene(self, scene):
         """Convert a sampled Scenic :obj:`~scenic.core.scenarios.Scene` to a point in our feature space.
 
@@ -314,7 +351,12 @@ def pointForScene(self, scene):
             params[param] = pointForValue(subdom, scene.params[originalName])
         paramPoint = paramDomain.makePoint(**params)
 
-        return self.space.makePoint(objects=objPoint, params=paramPoint)
+        staticSample = self.space.makeStaticPoint(objects=objPoint, params=paramPoint)
+
+        updateCallback = lambda rho: self.update(0, rho)
+        dynamicSampleLengths = []
+
+        return ScenicSample(self.space, staticSample, updateCallback, dynamicSampleLengths)
 
     @staticmethod
     def nameForObject(i):

src/verifai/server.py

@@ -144,6 +144,8 @@ def __init__(self, sampling_data, monitor, options={}):
                 sampler_params=params
             )
 
+        if self.sample_space.hasTimeSeries:
+            raise ValueError("Sample space for `Server` cannot contain `TimeSeriesFeature`")
 
     def listen(self):
         client_socket, addr = self.socket.accept()
@@ -176,8 +178,8 @@ def terminate(self):
     def close_connection(self):
         self.client_socket.close()
 
-    def get_sample(self, feedback):
-        return self.sampler.nextSample(feedback)
+    def get_sample(self):
+        return self.sampler.getSample()
 
     def flatten_sample(self, sample):
         return self.sampler.space.flatten(sample)
@@ -193,9 +195,10 @@ def evaluate_sample(self, sample):
 
     def run_server(self):
         start = time.time()
-        sample = self.get_sample(self.lastValue)
+        sample = self.get_sample()
         after_sampling = time.time()
-        self.lastValue = self.evaluate_sample(sample)
+        self.lastValue = self.evaluate_sample(sample.staticSample)
+        sample.update(self.lastValue)
         after_simulation = time.time()
         timings = ServerTimings(sample_time=(after_sampling - start),
                                 simulate_time=(after_simulation - after_sampling))

tests/scenic/scenic_driving_behavior.scenic

@@ -0,0 +1,19 @@
+param map = localPath('Town01.xodr')
+param carla_map = 'Town01'
+
+model scenic.domains.driving.model
+
+foo = TimeSeries(VerifaiRange(0,0.01))
+
+behavior TestBehavior():
+    lastVal = None
+    while True:
+        newVal = foo.getSample()
+        assert newVal != lastVal, (newVal, lastVal)
+        lastVal = newVal
+        take SetThrottleAction(newVal)
+
+ego = new Car on road, with behavior TestBehavior()
+new Car behind ego by VerifaiRange(1,4)
+
+terminate after 5 seconds