[lib] CLUnfolder: Add doc; doc module; fix typos

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'