Commit feeb3da0 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Add monitors to the AST

parent 76571424
......@@ -124,6 +124,9 @@ The background pattern was downloaded from www.subtlepatterns.com
Changelog
=========
**3.4.6 (04/2021)**
- Introduce monitors to support model checking observers
**3.4.5 (04/2021)**
- Fix bug affecting RPC
......
......@@ -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
......
This diff is collapsed.
......@@ -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
......
......@@ -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:
......@@ -2631,8 +2633,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 +2688,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 +2782,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 +3062,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 +3354,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)
......@@ -5226,9 +5251,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))
......
......@@ -141,7 +141,7 @@ except ImportError:
__all__ = ['opengeode', 'SDL_Scene', 'SDL_View', 'parse']
__version__ = '3.4.5'
__version__ = '3.4.6'
if hasattr(sys, 'frozen'):
# Detect if we are running on Windows (py2exe-generated)
......
This diff is collapsed.
This diff is collapsed.
......@@ -51,7 +51,7 @@ SDL_BLACKBOLD = ['\\b{word}\\b'.format(word=word) for word in (
'SET_TIMER', 'RESET_TIMER', 'VIA', 'ENTRY', 'EXIT', 'PRIORITY',
'SYNTYPE', 'ENDSYNTYPE', 'CONSTANTS', 'ENDPROCEDURE', 'FOR',
'COMMENT', 'SIGNAL', 'SIGNALLIST', 'USE', 'RETURNS', 'ANY',
'EXPORTED', 'REFERENCED',
'EXPORTED', 'REFERENCED', 'MONITOR',
'NEWTYPE', 'ENDNEWTYPE', 'ARRAY', 'STRUCT', 'SYNONYM')]
SDL_REDBOLD = ['\\b{word}\\b'.format(word=word) for word in (
......
......@@ -40,6 +40,7 @@ tokens {
CONSTANT;
CONSTANTS;
DCL;
MONITOR;
DECISION;
DIGITS;
ELSE;
......@@ -344,10 +345,12 @@ content
| syntype_definition
| newtype_definition
| variable_definition
| monitor_definition
| synonym_definition)*
-> ^(TEXTAREA_CONTENT fpar* $res? procedure* variable_definition*
syntype_definition* newtype_definition* timer_declaration*
signal_declaration* use_clause* synonym_definition*)
monitor_definition* syntype_definition* newtype_definition*
timer_declaration* signal_declaration* use_clause*
synonym_definition*)
;
......@@ -420,6 +423,14 @@ variable_definition
-> ^(DCL variables_of_sort+)
;
/* Monitors are an extension used when creating observers for model checking */
monitor_definition
: MONITOR variables_of_sort
(',' variables_of_sort)*
end
-> ^(MONITOR variables_of_sort+)
;
synonym_definition
: internal_synonym_definition
......@@ -1476,6 +1487,7 @@ DASH : '-';
ANY : A N Y;
ASTERISK : '*';
DCL : D C L;
MONITOR : M O N I T O R;
END : E N D;
KEEP : K E E P;
PARAMNAMES : P A R A M N A M E S;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment