implement callable interface for evaluating a specification

This commit is contained in:
Marcell Vazquez-Chanlatte 2017-12-16 14:30:27 -08:00
parent 5b7fea3953
commit 80f24cf74b
2 changed files with 12 additions and 7 deletions

View file

@ -1,11 +1,12 @@
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
from collections import deque, namedtuple from collections import deque, namedtuple
from functools import lru_cache from functools import lru_cache
import funcy as fn import funcy as fn
from lenses import lens, bind from lenses import lens, bind
import stl
def flatten_binary(phi, op, dropT, shortT): def flatten_binary(phi, op, dropT, shortT):
def f(x): def f(x):
@ -47,6 +48,9 @@ class AST(object):
return phi return phi
def __call__(self, trace, time):
return stl.pointwise_sat(self)(trace, time)
@property @property
def children(self): def children(self):
return tuple() return tuple()

View file

@ -1,6 +1,6 @@
import hypothesis.strategies as st import hypothesis.strategies as st
import traces import traces
from hypothesis import given, settings, Verbosity, Phase from hypothesis import given
from pytest import raises from pytest import raises
import stl import stl
@ -81,11 +81,6 @@ def test_eval_smoke_tests(phi):
@given(SignalTemporalLogicStrategy) @given(SignalTemporalLogicStrategy)
@settings(
max_shrinks=0,
verbosity=Verbosity.verbose,
perform_health_check=False,
phases=[Phase.generate])
def test_temporal_identities(phi): def test_temporal_identities(phi):
stl_eval = stl.boolean_eval.pointwise_sat(phi) stl_eval = stl.boolean_eval.pointwise_sat(phi)
stl_eval2 = stl.boolean_eval.pointwise_sat(~phi) stl_eval2 = stl.boolean_eval.pointwise_sat(~phi)
@ -124,6 +119,12 @@ def test_fastboolean_smoketest():
stl.fastboolean_eval.pointwise_sat(stl.ast.AST()) stl.fastboolean_eval.pointwise_sat(stl.ast.AST())
def test_callable_interface():
phi = stl.parse(
'(G[0, 4](x > 0)) & ((F[2, 1](AP1)) | (AP2)) & (G[0,0](AP2))')
assert not phi(x, 0)
def test_implicit_validity_domain_rigid(): def test_implicit_validity_domain_rigid():
phi = stl.parse('(G[0, a?](x > b?)) & ((F(AP1)) | (AP2))') phi = stl.parse('(G[0, a?](x > b?)) & ((F(AP1)) | (AP2))')
vals = {'a?': 3, 'b?': 20} vals = {'a?': 3, 'b?': 20}