Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit fd001e42 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Fix typos/doc

parent b2c20ecd
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment