[lib] Fix typos; update doc

library/_cadbiom/cadbiom.c

@@ -370,12 +370,13 @@ PyDoc_STRVAR(forward_code_doc,
 "forward_code(clause, var_code_table, shift_step)\n\
 Translation from names to num codes. The translation depends on the shift direction.\n\
 \n\
-Numerically code a clause with the numeric codes found in self.__var_code_table for\n\
-a base variable x and numeric_code + shift_step for x'\n\
-variable integer coding increases in future steps.\n\
+Numerically code a clause with the numeric codes found in\n\
+self.__var_code_table for a base variable x,\n\
+and numeric_code +/- shift_step (according to the sign) for x' variable.\n\
 \n\
-..note:: Future variables x' are noted \"name`\" in Literal names.\n\
-    Values of variables increases of __shift_step in future steps.\n\
+.. note:: Future variables x' are noted \"name`\" in Literal names.\n\
+    The absolute value of these variables will increase by shift_step\n\
+    in the next step.\n\
 \n\
 :param clause: a Clause object\n\
 :param var_code_table: Var code table from the model\n\
@@ -427,14 +428,15 @@ Dynamics initialisations. Set dynamic constraints for a forward one step: X1 = f
 \n\
 Numerically code clauses with the numeric codes found in\n\
 self.__var_code_table for a base variable x,\n\
-and numeric_code + shift_step for x' variable integer coding increases in future steps.\n\
+and numeric_code +/- shift_step (according to the sign) for x' variable.\n\
 \n\
 __dynamic_constraints is a list of lists of numeric clauses (lists of ints)\n\
 Each sublist of __dynamic_constraints corresponds to a step in the unfolder;\n\
 the last step is the last element.\n\
 \n\
-..note:: Future variables x' are noted \"name`\" in Literal names.\n\
-    Values of variables increases of __shift_step in future steps.\n\
+.. note:: Future variables x' are noted \"name`\" in Literal names.\n\
+    The absolute value of these variables will increase by shift_step\n\
+    in the next step.\n\
 \n\
 :param clauses: List of Clause objects\n\
 :param var_code_table: Var code table from the model\n\

library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py

@@ -61,8 +61,8 @@ 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
+    left depending on whether its sign is positive or negative
+    (addition vs soustraction of the shift_step value which is the number of
     variables in the system).
 
     Otherwise, the literal is a t literal and its value stays untouched.
@@ -233,7 +233,7 @@ class CLUnfolder(object):
         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
+        # 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.
@@ -386,7 +386,7 @@ class CLUnfolder(object):
         self.__dimacs_invariant = None    # list of DIMACS clauses
         self.__variant_property = None    # list<logic formulas>
         self.__dimacs_variant = None      # list<list<DIMACS clauses>>
-        # list of variant temporal constraints in Dimacs ground code
+        # list of variant temporal constraints in DIMACS ground code
         self.__precomputed_variant_constraints = None  # list<list<DIMACS clauses>>
 
         # If this function is called from the constructor,
@@ -678,12 +678,13 @@ class CLUnfolder(object):
     def __forward_code(self, clause):
         """(deprecated, directly included in C++ module: forward_init_dynamic())
 
-        Numerically code a clause with the numeric code found in
+        Numerically code a clause with the numeric codes found in
         self.__var_code_table for a base variable x,
-        and numeric_code + shift_step for x' variable
+        and numeric_code +/- shift_step (according to the sign) for x' variable.
 
         ..note:: Future variables x' are noted "name`" in Literal names.
-            Values of variables increases of __shift_step in future steps.
+            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
@@ -784,8 +785,7 @@ class CLUnfolder(object):
 
         Numerically code clauses with the numeric codes found in
         self.__var_code_table for a base variable x,
-        and numeric_code + shift_step for x' variable integer coding increases
-        in future steps.
+        and numeric_code +/- shift_step (according to the sign) for x' variable.
 
         __dynamic_constraints is a list of lists of numeric clauses (lists of ints)
         Each sublist of __dynamic_constraints corresponds to a step in the unfolder;
@@ -796,8 +796,8 @@ class CLUnfolder(object):
         .. note:: Called by init_forward_unfolding()
 
         .. note:: Future variables x' are noted "name`" in Literal names.
-
-        .. note:: Values of variables increases of __shift_step in future steps.
+            The absolute value of these variables will increase by shift_step
+            in the next step.
         """
         # New API via C++ module
         # TODO: take a look at __backward_init_dynamic & __backward_code
@@ -1374,6 +1374,8 @@ class CLUnfolder(object):
 
         # Now shifting is possible
         ## TODO: check shift_direction too (not urgent, backward is not usable)
+        # PS: no check if the system has changed with the same number of literals
+        # but different ones. This is assumed by init_with_query().
         if old_shift_step != self.__shift_step \
         or self.__include_aux_clauses_changed \
         or not self.__dynamic_constraints:

library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py

@@ -335,7 +335,7 @@ class MCLAnalyser(object):
         """Get the solution with the less number of activated frontier places
         among the given solutions.
 
-        ..note:: There is not constraint on the complexity of the trajectories;
+        .. note:: There is not constraint on the complexity of the trajectories;
             only on the number of activated frontier places.
 
         :param dimacs_solution_list: list of DimacsFrontierSol objects
@@ -469,7 +469,7 @@ class MCLAnalyser(object):
     def sq_is_satisfiable(self, query, max_step):
         """Check if the query is satisfiable.
 
-        ..warning::
+        .. warning::
             Many logical variables are auxiliary variables with no interest other
             than technical, we want different solutions to differ by their values
             on some set of significant variables.
@@ -477,7 +477,7 @@ class MCLAnalyser(object):
             **These variables of interest are not checked here!**
                 It is just a satisfiability test!
 
-        ..warning:: No frontier place is initialized to False in simple queries.
+        .. warning:: No frontier place is initialized to False in simple queries.
 
         :param query:
         :param max_step: Number of steps allowed in the unfolding;
@@ -537,21 +537,24 @@ class MCLAnalyser(object):
         because it returns FrontierSolutions.
 
 
-        @param query: MCLSimpleQuery
-        @param max_step: int - Number of steps allowed in the unfolding;
+        :param query: Query.
+        :param max_step: Number of steps allowed in the unfolding;
             the horizon on which the properties must be satisfied
         :param vvars: Variables for which solutions must differ.
             In practice, it is a list with the values (Dimacs code)
             of all frontier places of the system.
+        :type query: <MCLSimpleQuery>
+        :type max_step: <int>
         :type vvars: <list <int>>
         :return: a list of RawSolutions from the solver
         :rtype: <list <RawSolution>>
 
-        @warning:  no_frontier places are initialized to False in simple queries
+        .. warning:: no_frontier places are initialized to False in simple queries
             except if initial condition.
 
-        @warning: if the query includes variant constraints, the horizon (max_step) is
-            automatically adjusted to min(max_step, len(variant_constraints)).
+        .. warning:: if the query includes variant constraints,
+            the horizon (max_step) is automatically adjusted to
+            min(max_step, len(variant_constraints)).
         """
         # Initialise the unfolder with the given query
         # Following properties are used from the query:
@@ -827,7 +830,7 @@ class MCLAnalyser(object):
         """Wrapper for __mac_exhaustive_search(); return a generator of
         FrontierSolution objects.
 
-        ..note:: __mac_exhaustive_search() returns DimacsFrontierSols
+        .. note:: __mac_exhaustive_search() returns DimacsFrontierSols
 
         @param query: MCLSimpleQuery
         @param max_step: int - Number of steps allowed in the unfolding;
@@ -847,7 +850,7 @@ class MCLAnalyser(object):
     def is_strong_activator(self, act_sol, query):
         """Test if an activation condition is a strong one (independent of timing)
 
-        ..refactor note: Unclear function
+        .. refactor note: Unclear function
 
         final property becomes the invariant property
         => Ex: test if "C3 and C4" will never append if start property is "A1 and C1 and B1"
@@ -882,7 +885,7 @@ class MCLAnalyser(object):
 
     def next_inhibitor(self, mac, query):
         """
-        ..refactor note: Unclear function
+        .. refactor note: Unclear function
 
         if st_prop contains negation of mac conditions,
         return a different mac if any
@@ -920,7 +923,7 @@ class MCLAnalyser(object):
     def mac_inhibitor_search(self, mac, query, max_sol):
         """Search inhibitors for a mac scenario
 
-        ..refactor note: Unclear function
+        .. refactor note: Unclear function
 
         @param mac: the mac
         @param query: the property enforced by the mac
@@ -955,7 +958,7 @@ class MCLAnalyser(object):
         """Test if an activation condition inhibitor is a strong one
         (i.e independent of timing)
 
-        ..refactor note: Unclear function
+        .. refactor note: Unclear function
 
         @param in_sol: FrontierSolution with activation condition and inhibition
         @param query: the property which is inhibed

library/cadbiom/models/clause_constraints/mcl/MCLSolutions.py

@@ -214,7 +214,7 @@ class RawSolution(object):
         """Extracts frontier variables which are active in solution.
 
         :return: Set of activated frontier values.
-        :rtype: <set>
+        :rtype: <frozenset>
         """
         if self.shift_direction == 'FORWARD':
             # frontier_values: Set of frontier positive values only.

library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py

@@ -188,7 +188,7 @@ def create_unfolder(model):
 
 @pytest.fixture()
 def textual_properties():
-    """start, invariant, final"""
+    """start, invariant, final properties in textual form"""
     return (
         ("M", "L", "C"), # No solution (because inhibitor M is activated)
         ("", "L", "C and K"), # Solution: I E D F
@@ -197,7 +197,7 @@ def textual_properties():
 
 @pytest.fixture()
 def numeric_properties():
-
+    """start, invariant, final properties in DIMACS form"""
     return (
         # "M", "L", "C"
         ([[13]], [[12]], [[3]]),