diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index 12d31bb21ad62c558eac48b83db379502cf12874..cefeced73119d0a18fb6c3bc2b6e06afa2478087 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
@@ -70,16 +70,17 @@ About shifting clauses and variables:
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.
+ Shifting 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.
- *constraints attributes are shifted at every step and submitted to the solver.
+ *constraints unfolder attributes are shifted at every step and submitted to
+ the solver.
---
init_with_query(query):
- Copy of the query attributes to temporary attributes internal to the CLUnfolder.
+ Copy of the query attributes to temporary attributes of the CLUnfolder.
Textual properties of query are compiled into numeric clauses in
init_forward_unfolding(), just at the beginning of squery_is_satisfied()
@@ -115,22 +116,23 @@ init_forward_unfolding():
Shift dynamic_system.list_clauses + dynamic_system.aux_list_clauses + init
- __shift_final(): __final_constraints:
Shift + replace __final_constraints
- - __shift_invariant(): _invariant_constraints:
+ - __shift_invariant(): __invariant_constraints:
Shift + append of the last element of __invariant_constraints
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()).
- The following functions decompile textual properties or events and code them
- into DIMACS clauses constraints via __code_clause().
__code_clause() is susceptible to add new auxiliary numerical variables
during this process if a variable is not found in __var_code_table and in
__aux_code_table.
- __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0
- __code_clause + __compile_property
+ Call __code_clause + __compile_property
- __init_variant_constraints_0
- __code_clause + __compile_event
+ Call __code_clause + __compile_event
shift():
@@ -211,11 +213,11 @@ class CLUnfolder(object):
__*_property: Logical formulas in text format from the current query.
__dimacs_*: Clauses in DIMACS format from the current query.
- __*_constraints: CLUnfolder attributes for unfolding and shift initialised
- from the query attributes.
+ __*_constraints: CLUnfolder attributes for unfolding and shift;
+ initialized from the query attributes.
- :param dynamical_system: dynamical system in clause constraint form
- :type dynamical_system: <CLDynSys>
+ :param dynamical_system: dynamical system in clause constraint form
+ :type dynamical_system: <CLDynSys>
"""
def __init__(self, dynamic_system, debug=False):
@@ -351,11 +353,11 @@ class CLUnfolder(object):
# It's the trajectory of events of a solution.
# FP(X): Final property
- self.__initial_constraints = [] # DIMACS clauses: C(X_0) <list <list <int>>>
- self.__final_constraints = [] # idem: C(X_n)
- self.__invariant_constraints = [] # DIMACS clauses: C(X_i))
- self.__variant_constraints = [] # variant constraints along trajectory
- self.__shift_direction = None # FORWARD or BACKWARD
+ self.__initial_constraints = [] # DIMACS clauses: C(X_0) <list <list <int>>>
+ self.__final_constraints = [] # idem: C(X_n)
+ self.__invariant_constraints = [] # DIMACS clauses: C(X_i))
+ self.__variant_constraints = [] # variant constraints along trajectory
+ self.__shift_direction = None # FORWARD or BACKWARD
# statistics on solver
self.__stats = False
@@ -378,14 +380,14 @@ class CLUnfolder(object):
following the call of init_with_query().
"""
# Properties to be checked
- self.__initial_property = None # logical formula - literal boolean expression
- self.__dimacs_initial = None # list of DIMACS clauses
- self.__final_property = None # logical formula
- self.__dimacs_final = None # list of DIMACS clauses
- self.__invariant_property = None # logical formula
- self.__dimacs_invariant = None # list of DIMACS clauses
- self.__variant_property = None # list<logic formulas>
- self.__dimacs_variant = None # list<list<DIMACS clauses>>
+ self.__initial_property = None # logical formula - literal boolean expression
+ self.__dimacs_initial = None # list of DIMACS clauses
+ self.__final_property = None # logical formula
+ self.__dimacs_final = None # list of DIMACS clauses
+ self.__invariant_property = None # logical formula
+ 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
self.__precomputed_variant_constraints = None # list<list<DIMACS clauses>>
@@ -395,7 +397,7 @@ class CLUnfolder(object):
# For reachability optimisation. Number of shifts before checking
# the final property
self.__steps_before_check = 0
- self.__shift_direction = None # FORWARD or BACKWARD
+ self.__shift_direction = None # FORWARD or BACKWARD
self.__locked = False
def init_with_query(self, query):
@@ -1142,6 +1144,12 @@ class CLUnfolder(object):
Initialisation of self.__invariant_constraints:
List of lists of DIMACS clauses (lists of values).
+ .. 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
+ 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)
@@ -1279,9 +1287,9 @@ class CLUnfolder(object):
__aux_code_table.
- __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0
- __code_clause + __compile_property
+ Call __code_clause + __compile_property
- __init_variant_constraints_0
- __code_clause + __compile_event
+ Call __code_clause + __compile_event
Called at the begining of squery_is_satisfied() and squery_solve()
"""
@@ -1454,11 +1462,12 @@ class CLUnfolder(object):
self.__sync_stats(solver)
if LOGGER.getEffectiveLevel() == DEBUG:
- LOGGER.debug("__msolve_constraints :: vvars : %s", vvars)
- LOGGER.debug("__msolve_constraints :: max_sol : %s", max_sol)
# Get List of solutions (list of tuples of literals)
lintsol = solver.msolve_selected(max_sol, vvars)
- LOGGER.debug("__msolve_constraints :: lintsol : %s", lintsol)
+
+ LOGGER.info("__msolve_constraints :: max_sol : %s", max_sol)
+ LOGGER.info("__msolve_constraints :: lintsol : %s", [len(sol) for sol in lintsol])
+
# Make a RawSolution for each solution (tuple of literals)
return [RawSolution(solint, self) for solint in lintsol]
@@ -1595,6 +1604,12 @@ class CLUnfolder(object):
# ... to max_step excluded.
# Ex: __steps_before_check = 3, __current_step = 3, max_step = 4
# => we search solutions only for 1 step (step 4)
+ #
+ # When __steps_before_check is 0 by default, or less than
+ # (max_step - 1), we need to search solutions for every steps
+ # until max_step is reached.
+ # Otherwise, __steps_before_check is set to (maxstep - 1) only
+ # to allow us to search solutions for the last step (max_step).
raw_solutions = list()
while self.__current_step < max_step:
self.shift()
@@ -1606,14 +1621,8 @@ class CLUnfolder(object):
"current_step", self.__current_step
)
#raw_input("pause")
- # When __steps_before_check is 0 by default, or less than
- # (max_step - 1), we need to search solutions for every steps
- # until max_step is reached.
- # Otherwise, __steps_before_check is set to (maxstep - 1) only
- # to allow us to search solutions for the last step (max_step).
-
- if temp_raw_solutions:
- raw_solutions += temp_raw_solutions
+
+ raw_solutions += temp_raw_solutions
return raw_solutions