update reelay to new version, update readme

Author: AngeloFerrando

README.md

@@ -31,9 +31,16 @@ $ sudo apt-get install swi-prolog
 ```
 
 ## Reelay (https://github.com/doganulus/reelay)
-In order to use TL oracle we need to install Reelay. If the user is not interested in using the RML Oracle, this step can be skipped.
+In order to use TL oracle we need to install Reelay. If the user is not interested in using the TL Oracle, this step can be skipped.
 To install Reelay, follow the instructions at: https://github.com/doganulus/reelay/blob/master/docs/install.md
 
+Note: Reelay requires Python 3.
+
+Using pip:
+```bash
+$ python -m pip install reelay
+```
+
 ## Java (https://openjdk.java.net/install/):
 The following instructions are for installing OpenJDK-11.
 ```bash
@@ -250,9 +257,14 @@ More information about RML can be found at: https://rmlatdibris.github.io/
 Alternatively, we can analyse the log file using the TL oracle.
 ```bash
 $ cd ~/ROSMonitoring/oracle/TLOracle/
-$ ./oracle.py --offline --trace ../../log.txt
+$ ./oracle.py --offline --property property --trace ../../log.txt --discrete
 ```
-The MTL property defined now into 'property.py' is only an example (in the chatter example there is nothing interesting enough to be checked).
+The TL property defined now into 'property.py' is only an example (in the chatter example there is nothing interesting enough to be checked). The property says that 'chatter' is always contained inside the message.
+Note:
+
+--discrete means that we are assuming the events homogeneously distributed (the time between two events is fixed)
+
+--dense means that the events can be observed at a different rate (the time between two events is not always the same)
 
 ### Adding a monitor in the middle.
 
@@ -290,7 +302,7 @@ monitors: # here we list the monitors we are going to generate
 
 This configuration file is very similar to the previous one. But this time we are asking for the generation of an online monitor. In order to do so, we need to inform the generator where the Oracle is listening and on which port. In this way, the generated monitor will be capable of communicating with it using WebSockets.
 Another addition to this configuration file is the 'publishers' field inside the chatter topic.
-Since we are doing online RV, the monitor is checking the events at runtime. Now, if we wanted just to log each event, we could maintain the action set to 'log'. The behaviour in this way would be exactly the same as for the offline monitor, with the only difference that each time an event is observed, the monitor propagates this event to the oracle and waits for the current verdict against a chosen property. Consequently, rather than the offline case, in the online scenario, the monitor will also log the satisfaction/violation of the property (but nothing more). This can be useful if we are debugging a system, but in a real scenario we could need to enforce the correcteness of the events. For instance, filtering the events which are considered wrong by the Oracle. For doing this, we can change the action from 'log' to 'filter'.
+Since we are doing online RV, the monitor is checking the events at runtime. Now, if we wanted just to log each event, we could maintain the action set to 'log'. The behaviour in this way would be exactly the same as for the offline monitor, with the only difference that each time an event is observed, the monitor propagates this event to the oracle and waits for the current verdict against a chosen property. Consequently, rather than the offline case, in the online scenario, the monitor will also log the satisfaction/violation of the property (but nothing more). This can be useful if we are debugging a system, but in a real scenario we could need to enforce the correctness of the events. For instance, filtering the events which are considered wrong by the Oracle. For doing this, we can change the action from 'log' to 'filter'.
 
 Once the action 'filter' is selected, the monitor will filter the wrong messages. But, to be able to do so, it must be in the middle of the communication. Until now the monitor was only another node in the system and was just subscribing the topics. This is not enough if we want to filter the wrong messages. In order to solve this problem, ROSMonitoring instrument the nodes changing the names and creating gaps in the communications. Thanks to this communication gaps, the monitor can become a bridge for the topics of our interest, and filter the messages in case they are wrong.
 
@@ -331,11 +343,20 @@ The monitor will now check the events at runtime. But, since the property is alw
 Alternatively, we can use the online oracle with TL properties.
 ```bash
 $ cd ~/ROSMonitoring/oracle/TLOracle/
-$ ./oracle.py --online --port 8080
+$ ./oracle.py --online --property property --port 8080 --discrete
 
 ```
 In this way, the Python oracle will start listening on the 8080 port. Each message observed on this connection will be passed to Reelay and checked against the property defined in property.py.
 
+## Additional information published by the monitor (online)
+
+The monitor reports constantly information about its analysis.
+
+- When a violation of the formal property is observed, the monitor publishes a message on the topic '/{monitor_id}/monitor_error' of type MonitorError (monitor/msg/MonitorError.msg). Where {monitor_id} is the monitor id added in the configuration file (see generation section above). For instance, if monitor id is 'monitor_1', then the error messages will be reported on the topic '/monitor_1/monitor_error'.
+- On the topic '/{monitor_id}/monitor_verdict' it is possible to keep track of the current monitor's verdict. The message is of type String, and can be: 'true', 'false', 'currently_true', 'currently_false', 'unknown'. Depending on the chosen oracle, all or a subset of these verdicts can be reported by the monitor. 
+
+Note: To enable the publishing of error messages, the user has to set the warning field to 1 or 2 (0 no warnings will be published). If the warning level is set to 1, then an error will be reported when the monitor's verdict is 'currently_false' or 'false'. If the warning level is set to 2, then an error will be reported only when the monitor's verdict is 'false'. Thanks to the warning level we can customise how strict we want to be on the monitor's verdict. There might be scenarios where we might be more interested in checking a property against the system (in this case warning level 2, since we only care about the system satisfying/violating the property); while there might be other scenarios where we care about the current satisfaction/violation of a property in the current system state (warning level 2), even though in the future the verdict might change. In practice, warning level has to be set to 2 when we only care about final verdicts, so we want the monitor to report an error only when it has proven the property has been violated by the system and will always be violated; warning level to 1, when we are not interested only in the final verdict, and we want to give importance to the current observed trace, and its satisfaction/violation of the property under analysis. In this case, the current state of the system might be satisfying/violating the property, but the monitor cannot conclude it will always be satisfied/violated.
+
 # License:
 ROSMonitoring project is released under MIT license
 

generator/generator.py

@@ -194,7 +194,7 @@ def on_message(ws, message):
  other_callbacks += '''
  else:
  logging(json_dict)
- if (json_dict['verdict'] == 'false' and actions[json_dict['topic']][1] == 2) or (json_dict['verdict'] == 'currently_false' and actions[json_dict['topic']][1] == 1):'''
+ if (json_dict['verdict'] == 'false' and actions[json_dict['topic']][1] >= 1) or (json_dict['verdict'] == 'currently_false' and actions[json_dict['topic']][1] == 1):'''
  if not silent:
  other_callbacks += '''
  rospy.loginfo('The event ' + message + ' is inconsistent..')'''

oracle/TLOracle/examples/grasping/property_R2_1.py

@@ -0,0 +1,42 @@
+# MIT License
+#
+# Copyright (c) [2020] [Angelo Ferrando]
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+import oracle
+
+
+# property to verify
+PROPERTY = r'historically{x > 0, y > 0, z > 0}'
+
+# predicates used in the property (initialization for time 0)
+predicates = dict(
+)
+# in here we can add all the predicates we are interested in.. Of course, we also need to define how to translate Json messages to predicates.
+
+# function to abstract a dictionary (obtained from Json message) into a list of predicates
+def abstract_message(message):
+ return message
+# This function has to be defined by the user depending on the property defined.
+# In this case we have just implemented a simple and general function which
+# updates the predicates if it finds the topic in the list of predicates.
+# Since the property is defined on predicates, we need this function to update the
+# predicates each time a message is observed. This abstraction of course is totally
+# dependent on the specific application.

…le/TLOracle/examples/radiation_orange.py …e/examples/radiation/radiation_orange.pyoracle/TLOracle/examples/radiation_orange.py renamed to oracle/TLOracle/examples/radiation/radiation_orange.py oracle/TLOracle/examples/radiation_orange.py renamed to oracle/TLOracle/examples/radiation/radiation_orange.py

@@ -22,17 +22,14 @@
 
 import oracle
 
-# type of the property (PLTL, PMTL, or PSTL)
-TYPE = oracle.TypeOfProperty.PMTL
 
 # MTL property to verify
-PROPERTY = "(once[0:3](not radiation_level_high))"
+PROPERTY = "once[0:3](not {radiation_level_high})"
 # In this case is Past-MTL, but it can also be a Past-LTL or Past-STL
 
 # predicates used in the property (initialization for time 0)
 predicates = dict(
  time = 0,
- radiation_level = 0,
  radiation_level_high = False
 )
 # in here we can add all the predicates we are interested in.. Of course, we also need to define how to translate Json messages to predicates.

oracle/TLOracle/examples/radiation_red.py …acle/examples/radiation/radiation_red.pyoracle/TLOracle/examples/radiation_red.py renamed to oracle/TLOracle/examples/radiation/radiation_red.py oracle/TLOracle/examples/radiation_red.py renamed to oracle/TLOracle/examples/radiation/radiation_red.py

@@ -22,17 +22,13 @@
 
 import oracle
 
-# type of the property (PLTL, PMTL, or PSTL)
-TYPE = oracle.TypeOfProperty.PMTL
-
 # MTL property to verify
-PROPERTY = "(once[0:3](not radiation_level_high))"
+PROPERTY = "(once[0:3](not {radiation_level_high}))"
 # In this case is Past-MTL, but it can also be a Past-LTL or Past-STL
 
 # predicates used in the property (initialization for time 0)
 predicates = dict(
  time = 0,
- radiation_level = 0,
  radiation_level_high = False
 )
 # in here we can add all the predicates we are interested in.. Of course, we also need to define how to translate Json messages to predicates.

oracle/TLOracle/oracle.py

@@ -30,7 +30,6 @@
 import argparse
 import importlib
 from enum import Enum
-import time
 
 # type of properties available in reelay
 class TypeOfProperty(Enum):
@@ -63,26 +62,33 @@ def message_received(client, server, message):
 
 # Function checking the event against the specification (it simply calls Reelay, nothing more)
 def check_event(event):
-global last_time
+global last_time, tl_oracle, property, last_res
 event_dict = json.loads(event)
+if not tl_oracle:
+if model == 'dense' and 'time' in event_dict:
+tl_oracle = reelay.dense_timed_monitor(pattern = property.PROPERTY)
+else:
+tl_oracle = reelay.discrete_timed_monitor(pattern = property.PROPERTY)
 if 'time' in event_dict:
-if not last_time:
+if last_time is None:
 last_time = event_dict['time']
 event_dict['time'] = 0
 else:
 event_dict['time'] = event_dict['time'] - last_time
-else:
-if not last_time:
-last_time = time.time()
-event_dict['time'] = 0
-else:
-event_dict['time'] = int(time.time() - last_time)
-return tl_oracle.update(property.abstract_message(event_dict))
+abs_msg = property.abstract_message(event_dict)
+res = tl_oracle.update(abs_msg)
+if model == 'discrete' and res:
+last_res = res['value']
+if model == 'dense' and res:
+last_res = True
+for d in res:
+if not d['value']:
+last_res = False
+break
+return last_res
 
 def main(argv):
-global property
-global tl_oracle
-global last_time
+global property, tl_oracle, last_time, model, last_res
 
 parser = argparse.ArgumentParser(
  description='this is an Oracle Python implementation based on Reelay for monitoring PTL, MTL and STL properties',
@@ -95,6 +101,10 @@ def main(argv):
 action='store_true')
 parser.add_argument('--offline',
 action='store_true')
+parser.add_argument('--discrete',
+action='store_true')
+parser.add_argument('--dense',
+action='store_true')
 parser.add_argument('--port',
 help='Port where the Websocket Oracle has to listen on',
 default = 8080,
@@ -106,20 +116,15 @@ def main(argv):
 
 property = importlib.import_module(args.property)
 last_time = None
+tl_oracle = None
+last_res = True
 
-if property.TYPE.value == TypeOfProperty.PLTL.value:
-tl_oracle = reelay.past_ltl.monitor(
- pattern = property.PROPERTY)
-elif property.TYPE.value == TypeOfProperty.PMTL.value:
-tl_oracle = reelay.past_mtl.monitor(
- pattern = property.PROPERTY,
- time_model = 'discrete')
-elif property.TYPE.value ==TypeOfProperty.PSTL.value:
-tl_oracle = reelay.past_stl.monitor(
- pattern = property.PROPERTY,
- time_model = 'dense')
+if args.discrete:
+model = 'discrete'
+elif args.dense:
+model = 'dense'
 else:
-print('Property type not supported by reelay')
+print('You have to specify if the time is discrete or dense (example, --discrete, -- dense)')
 return
 
 if args.online:
@@ -139,7 +144,7 @@ def main(argv):
 if not check_event(event):
 print('Property violated: ' + property.PROPERTY)
 print('The event: \n' + event + '\n' + 'is not consistent with the specification.')
-return
+#return
 else:
 print('You have to specify if the oracle has to perform Online (--online) or Offline (--offline) verification')
 

oracle/TLOracle/property_example.py oracle/TLOracle/property.pyoracle/TLOracle/property_example.py renamed to oracle/TLOracle/property.py

@@ -22,35 +22,27 @@
 
 import oracle
 
-# type of the property (PLTL, PMTL, or PSTL)
-TYPE = oracle.TypeOfProperty.PMTL
-
-# MTL property to verify
-PROPERTY = "(historically[0:5]((door_open) and not dow_suppressed) or (not chatter)) -> door_open_warning"
-# In this case is Past-MTL, but it can also be a Past-LTL or Past-STL
+# property to verify
+PROPERTY = "historically[0:3]{hello}"
 
 # predicates used in the property (initialization for time 0)
 predicates = dict(
  time = 0,
- door_open = False,
- dow_suppressed = False,
- door_open_warning = False,
- chatter = False
+ hello = False
 )
 # in here we can add all the predicates we are interested in.. Of course, we also need to define how to translate Json messages to predicates.
 
 # function to abstract a dictionary (obtained from Json message) into a list of predicates
 def abstract_message(message):
- if message['topic'] in predicates:
- if isinstance(message['data'], bool):
- predicates[message['topic']] = message['data']
- else:
- predicates[message['topic']] = False
- predicates['time'] = int(message['time'])
+ if message['topic'] == 'chatter' and message['data'] == 'hello':
+ predicates['hello'] = True
+ else:
+ predicates['hello'] = False
+ predicates['time'] = message['time']
  return predicates
 # This function has to be defined by the user depending on the property defined.
 # In this case we have just implemented a simple and general function which
 # updates the predicates if it finds the topic in the list of predicates.
 # Since the property is defined on predicates, we need this function to update the
 # predicates each time a message is observed. This abstraction of course is totally
-# dependent on the specific application. 
+# dependent on the specific application.

oracle/TLOracle/property_R2_1.py

@@ -22,25 +22,17 @@
 
 import oracle
 
-# type of the property (PLTL, PMTL, or PSTL)
-TYPE = oracle.TypeOfProperty.PLTL
-
-# MTL property to verify
-PROPERTY = "(historically(dist_x > 0 or dist_y > 0 or dist_z > 0))"
-# In this case is Past-LTL
+# property to verify
+PROPERTY = r'historically{x > 0, y > 0, z > 0}'
 
 # predicates used in the property (initialization for time 0)
-predicates = dict()
+predicates = dict(
+)
 # in here we can add all the predicates we are interested in.. Of course, we also need to define how to translate Json messages to predicates.
 
 # function to abstract a dictionary (obtained from Json message) into a list of predicates
 def abstract_message(message):
- predicates['dist_x'] = message['data'][0]
- predicates['dist_y'] = message['data'][1]
- predicates['dist_z'] = message['data'][2]
- predicates['time'] = message['time']
- print(predicates)
- return predicates
+ return message
 # This function has to be defined by the user depending on the property defined.
 # In this case we have just implemented a simple and general function which
 # updates the predicates if it finds the topic in the list of predicates.