Commit 40e42366 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] MCLQuery, MCLMCLAnalyser, CLUnfolder: Add doc, module doc, fix typos

parent b9781777
......@@ -39,8 +39,78 @@
##
## Contributor(s): Geoffroy Andrieux IRSET
##
"""
Main engine for constraint unfolding and solving
"""Main engine for constraints unfolding and solving.
Process from the intialization with a query to the finding of a solution.
MCLSimpleQuery (reminder):
Object containing 2 main types of attributes describing properties:
- Attributes in text format: These are logical formulas that are humanly
readable.
Ex: start_prop, inv_prop, final_prop, variant_prop
- Attributes in DIMACS format: These are logical formulas encoded in
the form of clauses containing numerical values.
Ex: dim_start, dim_inv, dim_final, dim_variant_prop
init_with_query(query):
Copy of the query attributes to temporary attributes internal to the CLUnfolder.
Textual properties of query are compiled into numeric clauses in
init_forward_unfolding(), just at the beginning of squery_is_satisfied()
and squery_solve().
ALL textual properties are susceptible to add new auxiliary variables in the
system.
init_forward_unfolding():
Organization of the initialization of the system (its clauses) for
the current request and first variables shift.
Initialized attributes:
- __initial_constraints:
Query data + negative values of all places that are not frontiers.
- __final_constraints:
Query data
- __invariant_constraints:
List of Query data
- __list_variant_constraints:
Query data (automatic merge of textual and DIMACS forms)
- __variant_constraints:
Initilized with the first item of __list_variant_constraints
Shifted attributes with __shift_step (nb of variables in the system):
- __forward_init_dynamic(): __dynamic_constraints:
Shift dynamic_system.list_clauses + dynamic_system.aux_list_clauses + init
- __shift_final(): __final_constraints:
Shift + replace __final_constraints
- __shift_invariant(): _invariant_constraints:
Shift + append of the last element of __invariant_constraints
PS: __variant_constraints si already initialized for the first step
shift():
Shift all clauses of the system to prepare it for the next step.
Called at each step by:
- squery_solve()
- squery_is_satisfied()
Modified attributes:
- __shift_dynamic(): __dynamic_constraints:
Shift + append of the last element of __dynamic_constraints
- __shift_variant(): __variant_constraints:
Shift clauses of the current step in __list_variant_constraints, and
append them to __variant_constraints.
- __shift_invariant()
...
- __shift_final()
...
"""
from __future__ import print_function
......@@ -268,9 +338,12 @@ class CLUnfolder(object):
variant_prop, dim_variant_prop, steps_before_check
Textual properties of query are compiled into numeric clauses in
init_forward_unfolding(), just before squery_is_satisfied() and
squery_solve().
init_forward_unfolding(), just at the beginning of squery_is_satisfied()
and squery_solve().
This compilation step is costly due to ANTLR performances...
.. warning:: ALL textual properties are susceptible to add new auxiliary
variables in the system (increase shift_step).
"""
# Reset the unfolder before a new query
self.reset()
......@@ -687,6 +760,8 @@ class CLUnfolder(object):
def __shift_initial(self):
"""Shift initialisation condition
Shift + replace __initial_constraints
.. note:: Called by:
- shift()
- init_backward_unfolding()
......@@ -700,6 +775,8 @@ class CLUnfolder(object):
def __shift_final(self):
"""Shift final property
Shift + replace __final_constraints
.. note:: Called by:
- shift()
- init_forward_unfolding()
......@@ -713,6 +790,8 @@ class CLUnfolder(object):
def __shift_invariant(self):
"""Shift invariant property
Shift + append of the last element of __invariant_constraints
.. note:: Called by:
- shift()
- init_forward_unfolding()
......@@ -730,7 +809,8 @@ class CLUnfolder(object):
def __shift_variant(self):
"""Shift variant property - depends on unfolding direction
## TODO audit...
Shift clauses of the current step in __list_variant_constraints, and
append them to __variant_constraints.
.. warning:: Refactor note: unclear function. No apparent reason for
only the first clause to be shifted...
......@@ -753,7 +833,7 @@ class CLUnfolder(object):
if self.__shift_direction == "FORWARD":
# Constraint t0 already included from the query during initialisation
current_constraint = self.__list_variant_constraints[self.__current_step]
# shift constraint at current step and add to var_constraints
# Shift constraints at current step and append them to __variant_constraints
for clause in current_constraint:
s_clause = self.__m_shift_clause(clause, self.__current_step)
self.__variant_constraints.append(s_clause)
......@@ -765,16 +845,24 @@ class CLUnfolder(object):
def shift(self):
"""Shift all clauses of one step
"""Shift all clauses of the system to prepare it for the next step.
self.__current_step is incremented here!
Clauses shifted:
Modified attributes:
- __dynamic_constraints[-1] (last element)
Shift + append of the last element of __dynamic_constraints
- __invariant_constraints[-1] (last element)
- __list_variant_constraints => TODO: audit...
Shift + append of the last element of __invariant_constraints
- __list_variant_constraints[current_step]
Shift clauses of the current step in __list_variant_constraints,
and append them to __variant_constraints.
- __final_constraints if __shift_direction is "FORWARD"
- __initial_constraints if __shift_direction is "BACKWARD"
Called at each step by:
- squery_solve()
- squery_is_satisfied()
"""
# Froze unfolder to avoid modifications of shift_step
self.__locked = True
......@@ -864,13 +952,17 @@ class CLUnfolder(object):
Initialisation of self.__initial_constraints:
List of DIMACS clauses (lists of values).
self.__initial_constraints is filled with the current query data AND
with a clause with ALL places that are not frontiers (negative values).
We have to wait until all variables are num coded before shifting anything!
.. note:: Compilation of properties in text format (logical formulas)
to numeric format is expensive when they must be parsed at each query.
:key no_frontier_init: (optional) boolean to force all variables of
places/entities to be disabled before each search.
places/entities that are not frontiers to be disabled before each
search.
default: True
:type no_frontier_init: <boolean>
"""
......@@ -952,15 +1044,23 @@ class CLUnfolder(object):
def __init_variant_constraints_0(self):
"""Code variant constraints in a numerical clause.
variant_property list d'étapes, chaque étape a une formule logique impliquant les évènements (et les places? pas sur.;)
=> ensemble de place/propriétés devant ^etre valides à chaque étape
.. TODO:: variant_property list d'étapes, chaque étape a une formule logique
impliquant les évènements (et des places? pas sur...)
=> ensemble de place/propriétés devant etre valides à chaque étape
Automatic merge of textual and DIMACS forms:
If variant_property is set, compile each property into clauses and
encode these clauses. Clauses already in DIMACS form are added.
The two variant constraint forms must be compatible (same length) in
order to allow a merge.
If variant_property is set, compile each property into clauses and
encode these clauses. Clauses already in dimacs form are added.
The two variant constraint forms must be compatible (same length)
self.__list_variant_constraints:
Built here and is used later to shift current variant properties
and update self.__variant_constraints in __shift_variant().
self.__list_variant_constraints is built here and is used later to shift
given variant properties in __shift_variant().
self.__variant_constraints:
- the only element passed to the solver.
- initilised with the first item of self.__list_variant_constraints
"""
# coding of variant properties
# Take __variant_property in priority on __dimacs_variant
......@@ -1016,6 +1116,36 @@ class CLUnfolder(object):
def init_forward_unfolding(self):
"""Initialisation before generating constraints - forward trajectory
Organization of the initialization of the system (its clauses) for
the current request and first variables shift.
.. warning:: ALL textual properties are susceptible to add new auxiliary
variables in the system (increase shift_step).
This is why the shift is made after initialization.
Initialized attributes:
- __initial_constraints:
Query data + negative values of all places that are not frontiers.
- __final_constraints:
Query data
- __invariant_constraints:
List of Query data
- __list_variant_constraints:
Query data (automatic merge of textual and DIMACS forms)
- __variant_constraints:
Initilized with the first item of __list_variant_constraints
Shifted attributes with __shift_step (nb of variables in the system):
- __dynamic_constraints:
Shift dynamic_system.list_clauses + dynamic_system.aux_list_clauses + init
- __final_constraints:
Shift + replace __final_constraints
- __invariant_constraints:
Shift + append of the last element of __invariant_constraints
PS: __variant_constraints si already initialized for the first step.
Called at the begining of squery_is_satisfied() and squery_solve()
"""
self.__shift_direction = 'FORWARD'
......@@ -1024,13 +1154,13 @@ class CLUnfolder(object):
self.__aux_code_table = dict() # flush auxiliary variables
self.__aux_list = [] # idem
# init properties to generate all variable num codes
# Init properties to generate all variable num codes
self.__init_initial_constraint_0()
self.__init_final_constraint_0()
self.__init_invariant_constraint_0()
self.__init_variant_constraints_0()
# now shifting is possible
# Now shifting is possible
self.__forward_init_dynamic()
self.__shift_final()
self.__shift_invariant()
......@@ -1046,13 +1176,13 @@ class CLUnfolder(object):
self.__aux_code_table = dict() # flush auxiliary variables
self.__aux_list = [] # idem
# init properties to generate all variable num codes
# Init properties to generate all variable num codes
self.__init_initial_constraint_0()
self.__init_final_constraint_0()
self.__init_invariant_constraint_0()
self.__init_variant_constraints_0()
# now shifting is possible
# Now shifting is possible
self.__backward_init_dynamic()
self.__shift_initial()
self.__shift_invariant()
......
......@@ -42,6 +42,13 @@
"""
Main class to perform dynamic analysis of Cadbiom chart models.
Discrete event system simulation is a standard simulation scheme which consists
in the repetition of the following actions until some halting condition
is satisfied:
- Find the current events and inputs (including free events)
- Find the state variables subject to change
- Perform the state evolution
## Here you will find a global view of the process of dynamic analysis
mac_search:
......
......@@ -52,6 +52,18 @@ LOGGER = cm.logger()
class MCLSimpleQuery(object):
"""Class packaging the elements of a query
Object containing 2 main types of attributes describing properties:
- Attributes in text format: These are logical formulas that are humanly
readable.
Ex: start_prop, inv_prop, final_prop, variant_prop
- Attributes in DIMACS format: These are logical formulas encoded in
the form of clauses containing numerical values.
Ex: dim_start, dim_inv, dim_final, dim_variant_prop
Textual properties of query are compiled into numeric clauses in the unfolder
with init_forward_unfolding(), just at the beginning of squery_is_satisfied()
and squery_solve().
Attributes:
......
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