Commit a918a02e authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Remove dyn_sys attr from MCLAnalyser but keep a getter for it from the...

[lib] Remove dyn_sys attr from MCLAnalyser but keep a getter for it from the current unfolder object
parent 24e0363b
......@@ -95,7 +95,7 @@ class CLUnfolder(object):
:param dynamic_system: Describe a dynamic system in clause form.
:type dynamic_system: <CLDynSys>
"""
self.__dyn_sys = dynamic_system # symbolic clause dynamic system
self.dynamic_system = dynamic_system # symbolic clause dynamic system
# shift_step equals to the total number of coded variables
# (including inputs, entities, clocks/events, auxiliary variables)
......@@ -145,7 +145,7 @@ class CLUnfolder(object):
# ordered list of DIMACS codes of the simple variables/places
# Disable all variables of places (entities) in the model (except frontiers)
self.__no_frontier_init = [[-self.__var_code_table[nfp]] for nfp in self.__dyn_sys.no_frontiers]
self.__no_frontier_init = [[-self.__var_code_table[nfp]] for nfp in self.dynamic_system.no_frontiers]
# ordered list of DIMACS codes of the frontier variables/places
self.frontier_values = [self.__var_code_table[frp] for frp in self.__dyn_sys.frontiers]
......@@ -163,10 +163,10 @@ class CLUnfolder(object):
self.frontiers_negative_values | frozenset(self.frontier_values)
# DIMACS codes of the input variables/places for extraction (inv)
self.__inputs = frozenset(self.__var_code_table[inp] for inp in self.__dyn_sys.inputs)
self.__inputs = frozenset(self.__var_code_table[inp] for inp in self.dynamic_system.inputs)
# DIMACS codes of the free_clocks variables/places for extraction (invariant)
self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.__dyn_sys.free_clocks)
self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.dynamic_system.free_clocks)
# Binding for a merged version of __inputs and __free_clocks
# Convenient attribute for RawSolution.extract_frontier_values()
......@@ -316,7 +316,7 @@ class CLUnfolder(object):
"""Get number of variables in the clause constraint dynamical system
(including inputs, entities, clocks/events, auxiliary variables) (for tests)
"""
return self.__dyn_sys.get_var_number()
return self.dynamic_system.get_var_number()
def get_var_number(self):
"""Get number of principal variables (properties excluded) in the unfolder
......@@ -528,13 +528,13 @@ class CLUnfolder(object):
if self.__include_aux_clauses:
# Auxiliary clauses are supported (default)
self.__dynamic_constraints = \
forward_init_dynamic(self.__dyn_sys.list_clauses,
forward_init_dynamic(self.dynamic_system.list_clauses,
self.__var_code_table,
self.__shift_step,
self.__dyn_sys.aux_list_clauses)
self.dynamic_system.aux_list_clauses)
else:
self.__dynamic_constraints = \
forward_init_dynamic(self.__dyn_sys.list_clauses,
forward_init_dynamic(self.dynamic_system.list_clauses,
self.__var_code_table,
self.__shift_step)
......@@ -546,12 +546,12 @@ class CLUnfolder(object):
"""
num_clause_list = \
[self.__backward_code(clause)
for clause in self.__dyn_sys.list_clauses]
for clause in self.dynamic_system.list_clauses]
if self.__include_aux_clauses:
num_clause_list += \
[self.__backward_code(clause)
for clause in self.__dyn_sys.aux_list_clauses]
for clause in self.dynamic_system.aux_list_clauses]
self.__dynamic_constraints = [num_clause_list]
......@@ -765,9 +765,9 @@ class CLUnfolder(object):
# Syntax analyser and type checker
tree_prop, ste, fcl = compile_event(
property_text,
self.__dyn_sys.symb_tab,
self.dynamic_system.symb_tab,
True,
self.__dyn_sys.report
self.dynamic_system.report
)
# Avoid name collisions of aux var
prop_visitor = CLPropertyVisitor(self.__lit_cpt)
......
......@@ -79,7 +79,7 @@ class MCLAnalyser(object):
Attributes and default values:
:param cl_dyn_sys: dynamical system in clause constraint form
:param dynamical_system: dynamical system in clause constraint form
:param unfolder: computation management: unfolding
:param reporter: reporter for generic error display
:param translator_opti: turn on optimizations for ANTLR translation
......@@ -88,10 +88,10 @@ class MCLAnalyser(object):
solutions that will be pruned later, in order to find the most
optimized MAC with a reduced the number of activated frontiers.
:type cl_dyn_sys: None / <CLDynSys>
:type unfolder: None / <CLUnfolder>
:type reporter: no default value / <ErrorRep>
:type opti: True / <boolean>
:type dynamical_system: None before loading a model / <CLDynSys>
:type unfolder: None before loading a model / <CLUnfolder>
:type reporter: <ErrorRep>
:type translator_opti: True / <boolean>
:type nb_sols_to_be_pruned: 10
"""
......@@ -100,7 +100,6 @@ class MCLAnalyser(object):
@param report: a standard reporter
"""
self.cl_dyn_sys = None # dynamical system in clause constraint form
self.unfolder = None # computation management: unfolding; type <CLUnfolder>
self.reporter = report # for generic error display
self.translator_opti = True# turn on optimizations for ANTLR translation (subexpression elimination)
......@@ -111,33 +110,41 @@ class MCLAnalyser(object):
## TODO: ajuster ce paramètre dynamiquement
self.nb_sols_to_be_pruned = 10
@property
def dynamical_system(self):
"""Return the CLDynSys object of the current unfolder"""
return self.unfolder.dynamical_system
## Building MCLAnalyser ####################################################
def build_from_chart_model(self, model):
"""Build an MCLAnalyser from a chartmodel object.
"""Build an MCLAnalyser and its CLUnfolder from a chartmodel object.
Every parser uses this function at the end.
@param model: ChartModel
@param model: <ChartModel>
"""
# Reloading a MCLAnalyser is forbidden - create a new one is mandatory
if self.unfolder:
raise MCLException("This MCLAnalyser is already initialized")
# Build CLDynSys (dynamical system in clause constraint form)
# Parse the model data
vtab = TableVisitor(self.reporter)
model.accept(vtab)
if self.reporter.error:
return
# PS:
# Here, all keys of vtab.tab_symb = no_frontiers + frontiers + model name
# (probably a bug for this last one)
dynamic_system = CLDynSys(vtab.tab_symb, self.reporter)
if self.reporter.error:
return
# Build clauses and auxiliary variables from events and places in the model
comp_visitor = GT2Clauses(dynamic_system, self.reporter, self.translator_opti)
model.accept(comp_visitor)
if self.reporter.error:
return
self.cl_dyn_sys = dynamic_system
# Build unfolder
self.unfolder = CLUnfolder(dynamic_system)
......
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