diff --git a/README.md b/README.md index 8fa39ca3..8fb9ca2a 100644 --- a/README.md +++ b/README.md @@ -20,8 +20,9 @@ - [Dense-time Offline Monitor](#dense-time-offline-monitor) - [Discrete-time Specifics](#discrete-time-specifics) - [Working with time units and timing assumptions](#working-with-time-units-and-timing-assumptions) -- [Features] - - [Accessing evaluation of sub-formulas] +- [Features](#features) + - [Accessing evaluation of sub-formulas](#accessing-evaluation-of-sub-formulas) + - [Printing formulas](#printing-formulas) - [References](#references) @@ -136,7 +137,9 @@ for Python 3 sudo pip3 uninstall rtamt ``` -## test RTAMT +## Testing RTAMT + +For running all tests (Python and C++) tests. for Python 2 @@ -152,6 +155,22 @@ cd rtamt/ python3 -m unittest discover tests/ ``` +For running only Python tests. + +for Python 2 + +```bash +cd rtamt/ +python2 -m unittest discover tests/python +``` + +for Python 3 + +```bash +cd rtamt/ +python3 -m unittest discover tests/python +``` + # Theory RTAMT is a Python library for offline and online monitoring of (bounded-future) @@ -565,6 +584,44 @@ def monitor(): print('d: ' + str(d)) ``` +The output is: +```bash +a: [100.0, -1.0, -2.0] +b: [20.0, 2.0, 10.0] +c: [120.0, 1.0, 8.0] +d: [122.0, 3.0, 10.0] +``` + +## Printing formulas + +Online monitoring requires automatically translating bounded-future STL formulas into their equisatisfiable past STL counterparts. The user may want to see the translated formula, to understand better the semantics and debug the monitor. For this, we provide the `spec_print()` method. An example of using it is shown below: + +```python +import sys +import rtamt + +spec = rtamt.StlDiscreteTimeSpecification() +spec.declare_var('a', 'float') +spec.declare_var('b', 'float') +spec.spec = 'eventually[0,1] (a >= b)' + +try: + spec.parse() + print("Before pastification: " + spec.spec_print()) + + spec.pastify() + print("After pastification: " + spec.spec_print()) +except rtamt.RTAMTException as err: + print('RTAMT Exception: {}'.format(err)) + sys.exit() +``` + +The output of the method is shown here. + +```bash +Before pastification: eventually[0,1]((a)>=(b)) +After pastification: once[0,1]((a)>=(b)) +``` # References diff --git a/examples/documentation/example_evaluation_subformulas.py b/examples/documentation/example_evaluation_subformulas.py new file mode 100644 index 00000000..db5e6323 --- /dev/null +++ b/examples/documentation/example_evaluation_subformulas.py @@ -0,0 +1,40 @@ +import sys +import rtamt + +def monitor(): + # data + dataset = { + 'time': [0, 1, 2], + 'a': [100.0, -1.0, -2.0], + 'b': [20.0, 2.0, 10.0] + } + + # # stl + spec = rtamt.StlDiscreteTimeSpecification() + spec.name = 'HandMadeMonitor' + spec.declare_var('a', 'float') + spec.declare_var('b', 'float') + spec.declare_var('c', 'float') + spec.declare_var('d', 'float') + spec.add_sub_spec('c = a + b') + spec.spec = 'd = c >= - 2' + + try: + spec.parse() + except rtamt.RTAMTException as err: + print('RTAMT Exception: {}'.format(err)) + sys.exit() + + spec.evaluate(dataset) + a = spec.get_value('a') + b = spec.get_value('b') + c = spec.get_value('c') + d = spec.get_value('d') + + print('a: ' + str(a)) + print('b: ' + str(b)) + print('c: ' + str(c)) + print('d: ' + str(d)) + +if __name__ == '__main__': + monitor() \ No newline at end of file diff --git a/examples/documentation/example_print_pastification.py b/examples/documentation/example_print_pastification.py new file mode 100644 index 00000000..3747fe6d --- /dev/null +++ b/examples/documentation/example_print_pastification.py @@ -0,0 +1,22 @@ +import sys +import rtamt + +def monitor(): + # # stl + spec = rtamt.StlDiscreteTimeSpecification() + spec.declare_var('a', 'float') + spec.declare_var('b', 'float') + spec.spec = 'eventually[0,1] (a >= b)' + + try: + spec.parse() + print("Before pastification: " + spec.spec_print()) + + spec.pastify() + print("After pastification: " + spec.spec_print()) + except rtamt.RTAMTException as err: + print('RTAMT Exception: {}'.format(err)) + sys.exit() + +if __name__ == '__main__': + monitor() \ No newline at end of file diff --git a/examples/documentation/example_usage_stl_discrete_time_online.py b/examples/documentation/example_usage_stl_discrete_time_online.py index 6ddea915..c771a353 100755 --- a/examples/documentation/example_usage_stl_discrete_time_online.py +++ b/examples/documentation/example_usage_stl_discrete_time_online.py @@ -15,14 +15,17 @@ def monitor(): print('RTAMT Exception: {}'.format(err)) sys.exit() - rob = spec.update(0, [('a', 100.0), ('b', 20.0)]) - print('time=' + str(0) + ' rob=' + str(rob)) + t = 0 + rob = spec.update(t, [('a', 100.0), ('b', 20.0)]) + print('time=' + str(t) + ' rob=' + str(rob)) - rob = spec.update(1, [('a', -1.0), ('b', 2.0)]) - print('time=' + str(0) + ' rob=' + str(rob)) + t = 1 + rob = spec.update(t, [('a', -1.0), ('b', 2.0)]) + print('time=' + str(t) + ' rob=' + str(rob)) - rob = spec.update(2, [('a', -2.0), ('b', -10.0)]) - print('time=' + str(0) + ' rob=' + str(rob)) + t = 2 + rob = spec.update(t, [('a', -2.0), ('b', -10.0)]) + print('time=' + str(t) + ' rob=' + str(rob)) if __name__ == '__main__': monitor() \ No newline at end of file diff --git a/rtamt/spec/abstract_specification.py b/rtamt/spec/abstract_specification.py index e0c3be94..7bbf144f 100644 --- a/rtamt/spec/abstract_specification.py +++ b/rtamt/spec/abstract_specification.py @@ -127,6 +127,12 @@ def import_module(self, from_name, module_name): #TODO: send syntax layer (ast)? def set_var_topic(self, var_name, var_topic): self.ast.set_var_topic(var_name, var_topic) + def spec_print(self): + name = str() + for spec in self.ast.specs: + name = name + spec.name + '\n' + return name + def parse(self): self.ast.parse() diff --git a/setup.py b/setup.py index 3ad7db12..2f80e894 100644 --- a/setup.py +++ b/setup.py @@ -9,7 +9,7 @@ setup( name='rtamt', - version='0.4.7', + version='0.4.8', description='Library for specification-based online monitoring.', long_description=long_description, long_description_content_type="text/markdown",