diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index 00f66a3e4e14f1e35759b3ad3dfc791a0b5d3def..274b66bdd8a6983c4a55927ba8687b7e1cb9cd2e 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
@@ -54,6 +54,28 @@ MCLSimpleQuery (reminder):
the form of clauses containing numerical values.
Ex: dim_start, dim_inv, dim_final, dim_variant_prop
+---
+
+About shifting clauses and variables:
+
+ Initialization of the dynamic system by __forward_init_dynamic() iterates on
+ all literals of the system.
+ If a literal is a t+1 literal, its value is shifted to the right or to the
+ left depending on whether its value is positive or negative
+ (addition vs soustraction of shift_step value which is the number of
+ variables in the system).
+
+ Otherwise, the literal is a t literal and its value stays untouched.
+
+ t+1 and t literals are generated by CLDynSys object directly from the current
+ model.
+
+ Shift a clause consists to iterates on all its literals and shift their values
+ to the right or to the left depending on whether their values are positive
+ or negative.
+
+---
+
init_with_query(query):
Copy of the query attributes to temporary attributes internal to the CLUnfolder.
@@ -62,7 +84,8 @@ init_with_query(query):
and squery_solve().
ALL textual properties are susceptible to add new auxiliary variables in the
- system.
+ system (increase shift_step). This is why any shift must be made after the
+ initialization.
init_forward_unfolding():
@@ -92,6 +115,20 @@ init_forward_unfolding():
PS: __variant_constraints si already initialized for the first step
+ The following functions use the following methods to decompile textual
+ properties or events (__compile_property(), __compile_event()) and to
+ code them into DIMACS clauses constraints (__code_clause()).
+
+ __code_clause() is susceptible to add new auxiliary numeric variables
+ during this process if a variable is not found in __var_code_table or in
+ __aux_code_table.
+
+ - __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0
+ __code_clause + __compile_property
+ - __init_variant_constraints_0
+ __code_clause + __compile_event
+
+
shift():
Shift all clauses of the system to prepare it for the next step.
@@ -110,6 +147,8 @@ shift():
- __shift_final()
...
+ PS: __initial_constraints are left as this for now
+ (shifted only with BACKWARD shift direction).
"""
from __future__ import print_function
@@ -175,6 +214,7 @@ class CLUnfolder(object):
self.shift_step_init = dynamic_system.get_var_number() # shift step of system (number of variables of the system)
self.__shift_step = self.shift_step_init # current shift/step
+ # 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.
@@ -305,6 +345,10 @@ class CLUnfolder(object):
Reset only properties and dimacs clauses from the current query;
AND __list_variant_constraints.
+ => __initial_constraints, __final_constraints, __invariant_constraints,
+ __variant_constraints and __dynamic_constraints ARE NOT reset here
+ (see init_forward_unfolding())
+
This function is called from the constructor and during
MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions()
following the call of init_with_query().
@@ -596,10 +640,12 @@ class CLUnfolder(object):
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)
+ assume all variables are basic variables (t=0) (not shifted).
- @warning: MODIFIES SHIFT_STEP if auxiliary variables are present (numeric code)
- Because we add a variable in the system...
+ @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.
:param clause:
:return: List of numerical values corresponding to the literals
@@ -622,6 +668,7 @@ class CLUnfolder(object):
self.__aux_code_table[name] = self.__shift_step
# Mapping value code to name
self.__aux_list.append(name)
+ # Define var_cod
var_cod = self.__shift_step
# Add the sign to the value
@@ -644,6 +691,8 @@ 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()
+
.. note:: Called by init_forward_unfolding()
.. note:: Future variables x' are noted "name`" in Literal names.
@@ -683,7 +732,7 @@ class CLUnfolder(object):
self.__dynamic_constraints = [num_clause_list]
## Shifting variables: implementation of the shift operator ################
- def __shift_clause(self, ncl):
+ def __shift_clause(self, numeric_clause):
"""Shift a clause for the current __shift_step
(no used anymore, replaced by direct use of C++ code)
@@ -691,12 +740,13 @@ class CLUnfolder(object):
Basically, `shift_step` is added to positive variables and subtracted
from negative variables in `numeric_clause`.
+ 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.
Thus, we lock the Unfolder by turning self.__locked to True.
- @param ncl: DIMACS clause ## TODO rename
+ @param numeric_clause: DIMACS clause
@warning: lock the unfolder
"""
# Froze unfolder to avoid modifications of shift_step
@@ -704,17 +754,26 @@ class CLUnfolder(object):
# Old API
# Less efficient with abs()
- # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1) for lit in ncl]
+ # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1)
+ # for lit in numeric_clause]
# More efficient with ternary assignment
# return [(lit + self.__shift_step) if lit > 0 else (lit - self.__shift_step)
- # for lit in ncl]
+ # for lit in numeric_clause]
# New API via C++ module
- return shift_clause(ncl, self.__shift_step)
+ return shift_clause(numeric_clause, self.__shift_step)
- def __m_shift_clause(self, ncl, nb_steps):
+ def __m_shift_clause(self, numeric_clause, nb_steps):
"""Shift a clause for the given step number
+ Each literal will be shifted by (nb_steps * __shift_step).
+
+ 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.
+
+ 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.
@@ -722,8 +781,7 @@ class CLUnfolder(object):
Called by: __shift_variant()
-
- @param ncl: DIMACS clause
+ @param numeric_clause: DIMACS clause
@param nb_steps: number of shifts asked
@warning: lock the unfolder
"""
@@ -731,7 +789,7 @@ class CLUnfolder(object):
self.__locked = True
return [(lit + self.__shift_step * nb_steps) if lit > 0
- else (lit - self.__shift_step * nb_steps) for lit in ncl]
+ else (lit - self.__shift_step * nb_steps) for lit in numeric_clause]
def __shift_dynamic(self):
"""Shift clauses representing the dynamics X' = f(X,I,C)
@@ -860,6 +918,9 @@ class CLUnfolder(object):
- __final_constraints if __shift_direction is "FORWARD"
- __initial_constraints if __shift_direction is "BACKWARD"
+ PS: __initial_constraints are left as this for now
+ (shifted only with BACKWARD shift direction)
+
Called at each step by:
- squery_solve()
- squery_is_satisfied()
@@ -1045,7 +1106,8 @@ class CLUnfolder(object):
"""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...)
+ impliquant les évènements (et des places? pas sur...
+ Cf __compile_event())
=> ensemble de place/propriétés devant etre valides à chaque étape
Automatic merge of textual and DIMACS forms:
@@ -1146,6 +1208,19 @@ class CLUnfolder(object):
PS: __variant_constraints si already initialized for the first step.
+ The following functions use the following methods to decompile textual
+ properties or events (__compile_property(), __compile_event()) and to
+ code them into DIMACS clauses constraints (__code_clause()).
+
+ __code_clause() is susceptible to add new auxiliary numeric variables
+ during this process if a variable is not found in __var_code_table or
+ __aux_code_table.
+
+ - __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0
+ __code_clause + __compile_property
+ - __init_variant_constraints_0
+ __code_clause + __compile_event
+
Called at the begining of squery_is_satisfied() and squery_solve()
"""
self.__shift_direction = 'FORWARD'