diff --git a/library/_cadbiom/cadbiom.c b/library/_cadbiom/cadbiom.c
index b19d5a32f404d0ee3d9f763aa09a22a7937ca86a..77d6b2e6141447aad0483bcacf2e34bff673cbf7 100644
--- a/library/_cadbiom/cadbiom.c
+++ b/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\
diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index e97a122a644db33cde1c17b0f1dfcd01c16a60c6..40796b945c2730054b90480c6846f223c64f6a67 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/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:
diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
index e0bee74f3c45744bcb32cf6c201aaf9335e93d26..ece3473929cf765f5e27e1633570b2d303da5198 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
+++ b/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
diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLSolutions.py b/library/cadbiom/models/clause_constraints/mcl/MCLSolutions.py
index 527360f50b962d55712637ce2f1fd3a198034328..5d8c8c70627544fdcdc181adffa1b2663afd723a 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLSolutions.py
+++ b/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.
diff --git a/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py
index 66c9e8aecd20e7f69f63e9e87437f48ff27b935e..b156c5fb87ddf8f0a4967500e2eae8c639303de1 100644
--- a/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py
+++ b/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]]),