Commit 91d95056 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Fix typos; Review doc and comments

parent b68c2446
......@@ -202,7 +202,7 @@ class CLUnfolder(object):
Glossary
========
- ground variables/ground dimacs code: variables at time 0/their encoding.
- ground variables/ground DIMACS code: variables at time t=0 (not shifted).
- solution: a solution of the logical dynamic constraint from SAT solver
- state vector: list of DIMACS code of original (not shifted) variables
corresponding to a step.
......@@ -227,17 +227,18 @@ class CLUnfolder(object):
# shift_step equals to the total number of coded variables of the system
# (including inputs, entities, clocks/events, auxiliary variables)
# This number can change if auxiliary clauses are added.
# shift_step_init: the shift step ss (if n is X_0 code, n+ss is X_1 code)
self.shift_step_init = dynamic_system.get_var_number()
self.__shift_step = self.shift_step_init # current shift/step
self.__shift_step = self.shift_step_init
# About unfolder lock and shift_step:
# shift_step must be frozen in order to avoid problems during the
# unflatten() step of RawSolutions.
# => Each step MUST have the same number of variables.
# Thus, we lock the Unfolder by turning self.__locked to True.
# See __shift_clause() and __m_shift_clause()
# See __shift_clause() and __shift_ground_clause()
self.__locked = False
self.__current_step = 1 # current number of unfolding
# For reachability optimisation. Number of shifts before checking
......@@ -262,6 +263,7 @@ class CLUnfolder(object):
# keys: are the names of the variables, values: their values
self.__var_code_table = \
{var_name: var_num for var_num, var_name in enumerate(base_var_set, 1)}
# Optimization: for forward_init_dynamic() and forward_code() (mostly
# implemented in C.
# Precompute __var_code_table with the literal names in "future" format;
......@@ -436,7 +438,7 @@ class CLUnfolder(object):
values.update(it.chain(*query.dim_inv))
if query.dim_variant:
# Handle empty steps:
# Ex: [[], [[4]], [[6], [7]], []]
# Ex: [[[12], [1]], [[58], [47]], [[104], [93]]
g = (step for step in query.dim_variant if step)
[values.update(it.chain(*step)) for step in g]
......@@ -449,7 +451,7 @@ class CLUnfolder(object):
# Since the auxiliary clauses are reset here, this literal is suspect
# and its use dangerous because its value is not reproductible.
raise ValueError(
"%s variable is not in the initial system.\n"
"%s variable(s) is/are not in the initial system.\n"
"Insertion of auxiliary variables is not allowed here."
% out_of_range_values
)
......@@ -592,7 +594,7 @@ class CLUnfolder(object):
def get_var_name(self, var_num):
"""Get name of the variable
.. seealso:: Explanations are on :meth:`get_var_indexed_name`
.. seealso:: Explanations on :meth:`get_var_indexed_name`
@param var_num: DIMACS literal coding of an initial variable
@return: name of the variable
......@@ -711,18 +713,20 @@ class CLUnfolder(object):
## Translation from names to num codes #####################################
## The translation depends on the shift direction
def __forward_code(self, clause):
"""(deprecated, directly included in C++ module: forward_init_dynamic())
"""Deprecated, directly included in C++ module
.. seelalso:: :meth:`forward_init_dynamic`
Numerically code a clause with the numeric codes found in
self.__var_code_table for a base variable x,
and numeric_code +/- shift_step (according to the sign) for x' variable.
..note:: Future variables x' are noted "name`" in Literal names.
.. note:: Future variables x' are noted "name`" in Literal names.
The absolute value of these variables will increase by shift_step
in the next step.
@param clause: a Clause object
@return: the DIMACS coding of the forward shifted clause
:param clause: A Clause object
:return: The DIMACS coding of the forward shifted clause
"""
# Old API
# num_clause = []
......@@ -773,15 +777,15 @@ class CLUnfolder(object):
def __code_clause(self, clause):
"""Numerically code a clause
The numerical values are found in
self.__var_code_table for variables in the dynamic system,
or in self.__aux_code_table for other auxiliary variables;
assume all variables are basic variables (t=0) (not shifted).
The numerical values are found in:
- self.__var_code_table for variables in the dynamic system,
- or in self.__aux_code_table for other auxiliary variables;
We assume all variables are ground variables (not shifted).
@warning: This function MODIFIES SHIFT_STEP because we add a variable
in the system if a variable is not found in __var_code_table or in
__aux_code_table.
A new auxiliary variable will be created in __aux_code_table.
.. warning:: This function MODIFIES SHIFT_STEP because we add a variable
in the system if a variable is found neither in __var_code_table nor
in __aux_code_table.
Thus, a new auxiliary variable will be created.
:param clause:
:return: List of numerical values corresponding to the literals
......@@ -826,9 +830,9 @@ class CLUnfolder(object):
Each sublist of __dynamic_constraints corresponds to a step in the unfolder;
the last step is the last element.
.. seealso:: __forward_code()
.. seealso:: :meth:`__forward_code`
.. note:: Called by init_forward_unfolding()
.. note:: Called by :meth:`init_forward_unfolding`
.. note:: Future variables x' are noted "name`" in Literal names.
The absolute value of these variables will increase by shift_step
......@@ -902,7 +906,7 @@ class CLUnfolder(object):
# New API via C++ module
return shift_clause(numeric_clause, self.__shift_step)
def __m_shift_clause(self, numeric_clause, nb_steps):
def __shift_ground_clause(self, numeric_clause, nb_steps):
"""Shift a clause for the given step number
Each literal will be shifted by (nb_steps * __shift_step).
......@@ -910,12 +914,12 @@ class CLUnfolder(object):
Why ?
Such function is used for clauses that are not already shifted during
previous steps. It is the case of variant_constraints which come from a
reloaded/forced trajectory.
reloaded/forced trajectory and is composed of ground variables.
About unfolder lock and shift_step:
self.shift_step must be frozen in order to avoid problems during the
unflatten() step of RawSolutions.
=> Each step MUST have the same number of variables.
=> Indeed, each step MUST have the same number of variables.
Thus, we lock the Unfolder by turning self.__locked to True.
Called by: __shift_variant()
......@@ -927,8 +931,9 @@ class CLUnfolder(object):
# Froze unfolder to avoid modifications of shift_step
self.__locked = True
return [(lit + self.__shift_step * nb_steps) if lit > 0
else (lit - self.__shift_step * nb_steps) for lit in numeric_clause]
shift_offset = self.__shift_step * nb_steps
return [(lit + shift_offset) if lit > 0 else (lit - shift_offset)
for lit in numeric_clause]
def __shift_dynamic(self):
"""Shift clauses representing the dynamics X' = f(X,I,C)
......@@ -1053,11 +1058,11 @@ class CLUnfolder(object):
current_constraint = self.__precomputed_variant_constraints[self.__current_step]
# 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)
s_clause = self.__shift_ground_clause(clause, self.__current_step)
self.__variant_constraints.append(s_clause)
return # ?????
elif self.__shift_direction == "BACKWARD":
raise MCLException("Not yet implemented")
raise MCLException("Shift direction 'BACKWARD' is not yet implemented")
else:
raise MCLException("Shift incoherent data: " + self.__shift_direction)
......@@ -1106,10 +1111,11 @@ class CLUnfolder(object):
def __compile_property(self, property_text):
"""Compile a property (logical formula) into clauses
Type checking uses the symbol table of dyn_sys
Error reporting is made through the dyn_sys reporter
Type checking uses the symbol table of dynamic_system.
Error reporting is made through the dynamic_system reporter.
.. warning:: MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)
.. warning:: MODIFIES __lit_cpt for numbering of auxiliary variables
(not coding)
.. note:: Called by:
- __init_initial_constraint_0()
......@@ -1117,7 +1123,7 @@ class CLUnfolder(object):
- __init_invariant_constraint_0()
"""
if self.__locked:
raise MCLException("Trying to compile property while unfolder is locked")
raise MCLException("Trying to compile property with a locked unfolder")
# Syntax analyser and type checker
# Compile a condition expression to a tree representation
......@@ -1135,16 +1141,17 @@ class CLUnfolder(object):
def __compile_event(self, property_text):
"""Compile an event (biosignal expression) into clauses
Type checking uses the symbol table of dyn_sys
Error reporting is made through the dyn_sys reporter
Type checking uses the symbol table of dynamic_system.
Error reporting is made through the dynamic_system reporter.
.. warning:: MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)
.. warning:: MODIFIES __lit_cpt for numbering of auxiliary variables
(not coding)
.. note:: Called by:
- __init_variant_constraints_0()
"""
if self.__locked:
raise MCLException("Trying to compile property while unfolder is locked")
raise MCLException("Trying to compile event with a locked unfolder")
# Syntax analyser and type checker
# Compile an event expression to a tree representation
......@@ -1166,16 +1173,14 @@ class CLUnfolder(object):
def __init_initial_constraint_0(self, no_frontier_init=True):
"""Code initial constraints in a numerical clause.
If initial property is set (in text format of logical formulas, or
in dimacs format of numerical values), this function generates
constraints clauses in numerical form.
Automatic merge of textual and DIMACS forms:
If initial property is set (in text format of logical formulas, or
in dimacs format of numerical values), this function generates
constraints clauses in numerical form.
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)
......@@ -1183,7 +1188,7 @@ class CLUnfolder(object):
:key no_frontier_init: (optional) boolean to force all variables of
places/entities that are not frontiers to be disabled before each
search.
search with a clause with their negative values.
default: True
:type no_frontier_init: <boolean>
"""
......@@ -1208,9 +1213,10 @@ class CLUnfolder(object):
def __init_final_constraint_0(self):
"""Code final constraints in a numerical clause.
If final property is set (in text format of logical formulas, or
in dimacs format of numerical values), this function generates
constraints clauses in numerical form.
Automatic merge of textual and DIMACS forms:
If final property is set (in text format of logical formulas, or
in dimacs format of numerical values), this function generates
constraints clauses in numerical form.
Initialisation of self.__final_constraints:
List of DIMACS clauses (lists of values).
......@@ -1236,21 +1242,30 @@ class CLUnfolder(object):
def __init_invariant_constraint_0(self):
"""Code final constraints in a numerical clause.
If trajectory property is set (in text format of logical formulas, or
in dimacs format of numerical values), this function generates
constraints clauses in numerical form.
Automatic merge of textual and DIMACS forms:
If invariant property is set (in text format of logical formulas, or
in DIMACS format of numeric values), this function generates
constraints clauses in numeric form.
Initialisation of self.__invariant_constraints:
List of lists of DIMACS clauses (lists of values).
We have to wait until all variables are num coded before shifting anything!
:Example:
[[[12], [1]], [[58], [47]], [[104], [93]]
t0 t1 t2
.. note:: __invariant_property and __dimacs_invariant should contain
at most 1 item; it's the initial state only (will be shifted later).
.. note:: pourquoi une liste de listes ?
La propriété invariante doit etre vérifiée à chaque étape de la
recherche de satisfiabilité (tout comme variant_constraints).
1 étape = 1 item = 1 ensemble de clauses
`1 étape = 1 item = 1 ensemble de clauses`,
forçant le respect de la propriété définie au départ.
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.
"""
......@@ -1274,10 +1289,10 @@ class CLUnfolder(object):
def __init_variant_constraints_0(self):
"""Code variant constraints in a numerical clause.
.. TODO:: variant_property list d'étapes, chaque étape a une formule logique
impliquant les évènements (et des places? pas sur...
Cf __compile_event())
=> 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? NON,
on utilise __compile_event() et pas __compile_property())
=> ensemble de 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
......@@ -1285,13 +1300,15 @@ class CLUnfolder(object):
The two variant constraint forms must be compatible (same length) in
order to allow a merge.
self.__precomputed_variant_constraints:
Built here and is used later to shift current variant properties
and update self.__variant_constraints in __shift_variant().
Attributes initialized:
self.__precomputed_variant_constraints:
Built here and is used later to shift current variant properties
and update self.__variant_constraints in __shift_variant().
self.__variant_constraints:
- the only element passed to the solver.
- initilised with the first item of self.__precomputed_variant_constraints
self.__variant_constraints:
- the only element passed to the solver.
- initilised with the first item of
self.__precomputed_variant_constraints
"""
# coding of variant properties
# Take __variant_property in priority on __dimacs_variant
......@@ -1305,7 +1322,6 @@ class CLUnfolder(object):
[self.__code_clause(clause)
for clause in self.__compile_event(prop)]
)
print(self.__precomputed_variant_constraints)
if self.__dimacs_variant:
# Add DIMACS aux clauses initial properties
......@@ -1332,14 +1348,14 @@ class CLUnfolder(object):
# No __variant_property, keep only __dimacs_variant
self.__precomputed_variant_constraints = self.__dimacs_variant
# Initialisation
# Initialisation of __variant_constraints
if self.__precomputed_variant_constraints:
if self.__shift_direction == "FORWARD":
# For now, keep only the events of the first step (t0)
# Other steps are taken during shift() calls
self.__variant_constraints = self.__precomputed_variant_constraints[0]
elif self.__shift_direction == "BACKWARD":
raise MCLException("Not yet implemented")
raise MCLException("shift 'BACKWARD' is not yet implemented")
else:
raise MCLException("Shift incoherent data: " + self.__shift_direction)
......
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