Addressed issues 183-186.

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)
 
 <!-- markdown-toc end -->
@@ -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
 

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()

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()

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()

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()
 

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",