Merge https://github.com/esa/opengeode into feature_buster

README.md

@@ -124,6 +124,12 @@ The background pattern was downloaded from www.subtlepatterns.com
 
 Changelog
 =========
+**3.5.0 (04/2021)**
+- Support Input/Ouput expressions for model checkers
+
+**3.4.6 (04/2021)**
+- Introduce monitors to support model checking observers
+
 **3.4.5 (04/2021)**
 - Fix bug affecting RPC
 

opengeode/AdaGenerator.py

@@ -92,6 +92,7 @@ TYPES = None
 MAPPING_SORT_MODULE = dict()
 
 VARIABLES = {}
+MONITORS = {}
 LOCAL_VAR = {}
 # List of output signals and procedures
 OUT_SIGNALS = []
@@ -328,6 +329,7 @@ LD_LIBRARY_PATH=./lib:.:$LD_LIBRARY_PATH opengeode-simulator
     mapping = Helper.map_input_state(process)
 
     VARIABLES.update(process.variables)
+    MONITORS.update(process.monitors)
 
     process_level_decl = []
 
@@ -476,6 +478,12 @@ LD_LIBRARY_PATH=./lib:.:$LD_LIBRARY_PATH opengeode-simulator
         ctxt += "others => <>);"
         context_decl.append(ctxt)
 
+        # Add monitors, that are pointers that must be set by an external
+        # module. They are not part of the global state of the process, and
+        # are used by observer functions to read/write the system state
+        for mon_name, (mon_type, _) in process.monitors.items():
+            context_decl.append(f"{mon_name} : access {type_name(mon_type)};")
+
         # The choice selections will allow to use the present operator
         # together with a variable of the -selection type
         context_decl.extend(choice_selections)
@@ -1743,6 +1751,9 @@ def _primary_variable(prim, **kwargs):
 
     ada_string = f'{sep}{prim.value[0]}'
 
+    if find_monitoring(prim.value[0]):
+        ada_string += ".all"
+
     return [], str(ada_string), []
 
 
@@ -3144,6 +3155,8 @@ def _inner_procedure(proc, **kwargs):
     outer_scope = dict(VARIABLES)
     local_scope = dict(LOCAL_VAR)
     VARIABLES.update(proc.variables)
+    # Note: here we ignore locally-declared monitorings.. they should be
+    # defined at process level (but this is not checked in the parser)
     # Store local variables in global context
     LOCAL_VAR.update(proc.variables)
     # Also add procedure parameters in scope
@@ -3386,6 +3399,13 @@ def find_var(var):
             return visible_var
     return None
 
+def find_monitoring(mon):
+    ''' Return a monitoring from the scope, with proper case '''
+    for visible_mon in MONITORS.keys():
+        if mon.lower() == visible_mon.lower():
+            return visible_mon
+    return None
+
 
 def is_local(var):
     ''' Check if a variable is in the global context or in a local scope
@@ -3405,7 +3425,9 @@ def path_type(path):
     if not path or not find_var(path[0]):
         return None, None
     kind = ''
-    vartype, _ = VARIABLES[find_var(path[0])]
+    declarations = dict(VARIABLES)
+    declarations.update(MONITORS)
+    vartype, _ = declarations[find_var(path[0])]
     asn1_name = vartype.ReferencedTypeName
     # Get ASN.1 type of the first element
     current = TYPES[asn1_name].type

opengeode/ogAST.py

@@ -762,6 +762,8 @@ class TextArea:
         self.height = 140
         # DCL variables in the text area {name: (sort, default_value), ...}
         self.variables = {}
+        # MONITOR variables used in observers (same structure as DCL)
+        self.monitors = {}
         # fpar and timers are also listed, useful when using autocompletion
         self.fpar = []
         self.timers = []
@@ -810,10 +812,13 @@ class Procedure:
         self.hyperlink = None
         # Local variables dictionnary (see Process)
         self.variables = {}
+        # MONITOR variables used in observers (same structure as DCL)
+        self.monitors = {}
         self.timers = []
         # Inherited variables and timers from all levels above
         self.global_variables = {}
         self.global_timers = []
+        self.global_monitors = {}
         # Formal parameters - list of dict:
         # [{'name': str, 'direction': 'in'/'out', 'type': str}]
         self.fpar = []
@@ -875,8 +880,11 @@ class Process:
         self.referenced = False
         # variables: dictionnary: {variable1Name: (asn1SccType, default value)}
         self.variables = {}
+        # MONITOR variables used in observers (same structure as DCL)
+        self.monitors = {}
         # global variables and timers can be used to inherit from a level above
         self.global_variables = {}
+        self.global_monitors = {}
         self.global_timers = []
         # Set default coordinates and width/height
         self.pos_x = 250

opengeode/ogParser.py

@@ -16,7 +16,7 @@
     During the build of the AST this library makes a number of semantic
     checks on the SDL input mode.
 
-    Copyright (c) 2012-2020 European Space Agency
+    Copyright (c) 2012-2021 European Space Agency
 
     Designed and implemented by Maxime Perrotin
 
@@ -1315,6 +1315,8 @@ def find_variable_type(var, context):
     # all DCL-variables
     all_visible_variables = dict(context.global_variables)
     all_visible_variables.update(context.variables)
+    all_visible_variables.update(context.monitors)
+    all_visible_variables.update(context.global_monitors)
 
     # First check locally, i.e. in FPAR
     try:
@@ -1627,6 +1629,70 @@ def unary_expression(root, context):
     return expr, errors, warnings
 
 
+def io_expression(root, context):
+    ''' Expressions used in the context of observers (for model checking):
+        input
+        input x [from P] to F
+        output
+        output X from P
+
+        Since this is syntactic sugar, we transform these expression into the
+        regular form based on the known structure of events: Observable_Event
+        type that is generated by kazoo.
+    '''
+    inputString = get_input_string(root)
+    event_kind = "{kind}_event"
+    target_option = " and then event.{kind}_event.{target} = {function}"
+    msg_name = " and then present(event.{kind}_event.event.{function}.msg_{direction}) = {msg}"
+
+    string = "present(event) = "
+
+    msg, src, dest = "", "", ""
+
+    if root.type == lexer.INPUT_EXPRESSION:
+        kind = "input"
+        direction = "in"
+    else:
+        kind = "output"
+        direction = "out"
+
+    string += event_kind.format(kind=kind)
+
+    for child in root.getChildren():
+        if child.type == lexer.ID:
+            msg =  child.text
+
+        elif child.type == lexer.FROM:
+            src = child.getChild(0).text
+            string += target_option.format(kind=kind,
+                                           target="source",
+                                           function=src)
+
+        elif child.type == lexer.TO:
+            dest = child.getChild(0).text
+            string += target_option.format(kind=kind,
+                                           target="dest",
+                                           function=dest)
+
+        else:
+            raise NotImplementedError("In io_expression")
+
+    if msg:
+        string += msg_name.format(kind=kind,
+                                  function=dest if kind=="input" else src,
+                                  direction=direction,
+                                  msg=msg)
+
+    parser = parser_init (string=string)
+    new_root = parser.expression()
+    tree = new_root.tree
+    tree.token_stream = parser.getTokenStream()
+
+    expr, errors, warnings = expression(tree, context)
+    expr.inputString = inputString
+
+    return expr, errors, warnings
+
 def expression(root, context, pos='right'):
     ''' Expression analysis (e.g. 5+5*hello(world)!foo) '''
     logic = (lexer.OR, lexer.AND, lexer.XOR, lexer.IMPLIES)
@@ -1675,6 +1741,10 @@ def expression(root, context, pos='right'):
         # If the procedure is not defined with a return value, a TypeError
         # has been raised in compare_type, so no need to check it again here
         return prim, errs, warns
+    elif root.type == lexer.INPUT_EXPRESSION:
+        return io_expression(root, context)
+    elif root.type == lexer.OUTPUT_EXPRESSION:
+        return io_expression(root, context)
     else:
         raise NotImplementedError(sdl92Parser.tokenNamesMap[root.type] +
                                 ' - line ' + str(root.getLine()))
@@ -2631,8 +2701,13 @@ def primary(root, context):
     return prim, errors, warnings
 
 
-def variables(root, ta_ast, context):
-    ''' Process declarations of variables (dcl a,b Type := 5) '''
+def variables(root, ta_ast, context, monitor=False):
+    ''' Process declarations of variables (dcl a,b Type := 5) 
+        if monitor is True, the result will be placed in the
+        "monitors" dictionary of the context, instead of the
+        variables. this is for use in the context of observers
+        for model checking.
+    '''
     var = []
     errors = []
     warnings = []
@@ -2681,35 +2756,45 @@ def variables(root, ta_ast, context):
 
             if not def_value.is_raw and \
                     not isinstance(def_value, ogAST.PrimConstant):
-                errors.append('In variable declaration {}: default'
-                              ' value is not a valid ground expression'.
-                              format(var[-1]))
+                errors.append(f'In variable declaration {var[-1]}: default'
+                              ' value is not a valid ground expression')
+            if monitor:
+                errors.append(f'In monitor declaration {var[-1]}: default'
+                              ' value is not allowed')
         else:
             warnings.append('Unsupported variables construct type: ' +
                     str(child.type))
     for variable in var:
         if not hasattr(context, 'variables'):
-            errors.append('Variables shall not be declared here')
+            errors.append('Variables/monitors shall not be declared here')
         # Add to the context and text area AST entries
-        elif(variable.lower() in context.variables
-                  or variable.lower() in ta_ast.variables):
+        elif(not monitor and (variable.lower() in context.variables
+                  or variable.lower() in ta_ast.variables)):
             errors.append('Variable "{}" is declared more than once'
                           .format(variable))
-        else:
+        elif (monitor and (variable.lower() in context.monitors
+                  or variable.lower() in ta_ast.monitors)):
+            errors.append('Monitor "{}" is declared more than once'
+                          .format(variable))
+
+        elif not monitor:
             context.variables[variable.lower()] = (asn1_sort, def_value)
-        ta_ast.variables[variable.lower()] = (asn1_sort, def_value)
+            ta_ast.variables[variable.lower()] = (asn1_sort, def_value)
+        else:
+            context.monitors[variable.lower()] = (asn1_sort, def_value)
+            ta_ast.monitors[variable.lower()] = (asn1_sort, def_value)
     if not DV:
         errors.append('Cannot do semantic checks on variable declarations')
     return errors, warnings
 
 
-def dcl(root, ta_ast, context):
+def dcl(root, ta_ast, context, monitor=False):
     ''' Process a set of variable declarations '''
     errors = []
     warnings = []
     for child in root.getChildren():
         if child.type == lexer.VARIABLES:
-            err, warn = variables(child, ta_ast, context)
+            err, warn = variables(child, ta_ast, context, monitor)
             errors.extend(err)
             warnings.extend(warn)
         else:
@@ -2765,6 +2850,8 @@ def composite_state(root, parent=None, context=None):
     try:
         comp.global_variables = dict(context.variables)
         comp.global_variables.update(context.global_variables)
+        comp.global_monitors = dict(context.monitors)
+        comp.global_monitors.update(context.global_monitors)
         comp.global_timers = list(context.timers)
         comp.global_timers.extend(list(context.global_timers))
         comp.input_signals = context.input_signals
@@ -3043,6 +3130,8 @@ def procedure_post(proc, content, parent=None, context=None):
     try:
         proc.global_variables = dict(context.variables)
         proc.global_variables.update(context.global_variables)
+        proc.global_monitors = dict(context.monitors)
+        proc.global_monitors.update(context.global_monitors)
         proc.global_timers = list(context.timers)
         proc.global_timers.extend(list(context.global_timers))
         proc.input_signals = context.input_signals
@@ -3333,6 +3422,10 @@ def text_area_content(root, ta_ast, context):
             err, warn = dcl(child, ta_ast, context)
             errors.extend(err)
             warnings.extend(warn)
+        elif child.type == lexer.MONITOR:
+            err, warn = dcl(child, ta_ast, context, monitor=True)
+            errors.extend(err)
+            warnings.extend(warn)
         elif child.type == lexer.SYNONYM_LIST:
             err, warn = synonym(child, ta_ast, context)
             errors.extend(err)
@@ -3675,7 +3768,8 @@ def system_definition(root, parent):
         for channel in system.channels:
             for route in channel['routes']:
                 if route['dest'].lower() != "env":
-                    route['signals'].append(proc)
+                    if proc not in route['signals']:
+                        route['signals'].append(proc)
 
     for each in blocks:
         block, err, warn = block_definition(each, parent=system)
@@ -5226,9 +5320,12 @@ def for_loop(root, context):
             forloop['var'] = child.text
             # Implicit variable declaration for the iterator
             context_scope = dict(context.variables)
+            context_scope.update(context.monitors)
             if child.text.lower() in (var.lower()
                       for var in chain (context.variables.keys(),
-                                        context.global_variables.keys())):
+                                        context.global_variables.keys(),
+                                        context.monitors.keys(),
+                                        context.global_monitors.keys())):
                 errors.append("FOR variable '{}' is already declared in the"
                               " scope (shadow variable). Please rename it."
                               .format(child.text))
@@ -5782,7 +5879,7 @@ def parseSingleElement(elem:str='', string:str='', context=None):
             # so we have to discard exceptions sent by e.g. find_variable
             pass
         except NotImplementedError as err:
-            syntax_errors.append('Syntax error in expression - Fix it.')
+            syntax_errors.append('Expression syntax not supported.')
         except SyntaxError as err:
             syntax_errors.append(err.text)
         # Check that the whole string has been consumed (ANTLR may stop parsing

opengeode/opengeode.py

@@ -141,7 +141,7 @@ except ImportError:
 
 
 __all__ = ['opengeode', 'SDL_Scene', 'SDL_View', 'parse']
-__version__ = '3.4.5'
+__version__ = '3.5.0'
 
 if hasattr(sys, 'frozen'):
     # Detect if we are running on Windows (py2exe-generated)