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 5ee8833c authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Big Opti: Do not shift the whole system (invariable) at each query: Just once per new step

parent 70efd855
...@@ -272,6 +272,7 @@ class CLUnfolder(object): ...@@ -272,6 +272,7 @@ class CLUnfolder(object):
# If A->B has clock h, an aux constraint added is h included in h when A # If A->B has clock h, an aux constraint added is h included in h when A
# Must be set to False for inhibitors computations # Must be set to False for inhibitors computations
self.__include_aux_clauses = True self.__include_aux_clauses = True
self.__include_aux_clauses_changed = False
self.__lit_cpt = self.__shift_step + 1 # counter for aux. var. coding self.__lit_cpt = self.__shift_step + 1 # counter for aux. var. coding
# Same mapping tools for auxiliary variables introduced by properties # Same mapping tools for auxiliary variables introduced by properties
...@@ -331,6 +332,7 @@ class CLUnfolder(object): ...@@ -331,6 +332,7 @@ class CLUnfolder(object):
# H: Current 'free' events (present/not present) => ? # H: Current 'free' events (present/not present) => ?
# I: Current inputs => ? # I: Current inputs => ?
self.__dynamic_constraints = [] # DIMACS clauses: X' = f(X,H,I) self.__dynamic_constraints = [] # DIMACS clauses: X' = f(X,H,I)
self.__precomputed_dynamic_constraints = []
# Simple temporal properties: # Simple temporal properties:
# SP(X0): Initial property/start property; Never change at each step. # SP(X0): Initial property/start property; Never change at each step.
...@@ -438,12 +440,19 @@ class CLUnfolder(object): ...@@ -438,12 +440,19 @@ class CLUnfolder(object):
print("NB Clauses in solver:", self.__nb_clauses) print("NB Clauses in solver:", self.__nb_clauses)
def set_include_aux_clauses(self, val): def set_include_aux_clauses(self, val):
""" """Flag to include auxiliary clause to eliminate undesirable solutions.
Include auxiliary clause to eliminate undesirable solutions
If A->B has clock h, an aux constraint added is h included in h when A If A->B has clock h, an aux constraint added is h included in h when A
Must be set to False for inhibitors computations Must be set to False for inhibitors computations.
.. warning:: This function impacts the shift_step number.
Tested in by:
- __forward_init_dynamic
- __backward_init_dynamic
""" """
self.__include_aux_clauses = val self.__include_aux_clauses = val
self.__include_aux_clauses_changed = True
## Internal variable access for tests (never used) ######################### ## Internal variable access for tests (never used) #########################
@property @property
...@@ -727,6 +736,10 @@ class CLUnfolder(object): ...@@ -727,6 +736,10 @@ class CLUnfolder(object):
self.__var_code_table, self.__var_code_table,
self.__shift_step) self.__shift_step)
# __dynamic_constraints is initialized and
# has now taken into account the auxiliary clauses flag
self.__include_aux_clauses_changed = False
def __backward_init_dynamic(self): def __backward_init_dynamic(self):
"""Dynamics initialisations. (never used, backward is partially implemented) """Dynamics initialisations. (never used, backward is partially implemented)
Set dynamic constraints for a forward one step: X0 = f(X1) Set dynamic constraints for a forward one step: X0 = f(X1)
...@@ -812,6 +825,27 @@ class CLUnfolder(object): ...@@ -812,6 +825,27 @@ class CLUnfolder(object):
.. note:: Called by shift() .. note:: Called by shift()
""" """
if len(self.__precomputed_dynamic_constraints) > self.__current_step:
# Recall the saved state of the system for the next step
self.__dynamic_constraints.append(
self.__precomputed_dynamic_constraints[self.__current_step]
)
LOGGER.info(
"__shift_dynamic:: OPTI-DO NOT SHIFT; "
"Reload dynamic constraints; step: %s",
self.__current_step
)
return
# System has not been shifted for this step until now
LOGGER.info(
"__shift_dynamic:: SHIFT; "
"Set dynamic constraints; step: %s; dyn consts len: %s",
self.__current_step,
len(self.__dynamic_constraints)
)
# Old API # Old API
# self.__dynamic_constraints.append( # self.__dynamic_constraints.append(
# [self.__shift_clause(clause) # [self.__shift_clause(clause)
...@@ -1235,6 +1269,7 @@ class CLUnfolder(object): ...@@ -1235,6 +1269,7 @@ class CLUnfolder(object):
Called at the begining of squery_is_satisfied() and squery_solve() Called at the begining of squery_is_satisfied() and squery_solve()
""" """
old_shift_step = self.__shift_step
self.__shift_direction = 'FORWARD' self.__shift_direction = 'FORWARD'
self.__current_step = 1 self.__current_step = 1
self.__shift_step = self.shift_step_init # back to basic! self.__shift_step = self.shift_step_init # back to basic!
...@@ -1248,7 +1283,23 @@ class CLUnfolder(object): ...@@ -1248,7 +1283,23 @@ class CLUnfolder(object):
self.__init_variant_constraints_0() self.__init_variant_constraints_0()
# Now shifting is possible # Now shifting is possible
self.__forward_init_dynamic() if old_shift_step != self.__shift_step \
or self.__include_aux_clauses_changed \
or not self.__dynamic_constraints:
# The size of the system has changed,
# or aux_clauses flag has been updated (so the system has changed),
# or the system has never been initialized before.
LOGGER.info("init_forward_unfolding:: New dynamic constraints")
self.__forward_init_dynamic()
self.__precomputed_dynamic_constraints = []
else:
# Main settings of the unfolder haven't changed and the system
# was initialized before.
LOGGER.info("init_forward_unfolding:: Reload dynamic constraints")
# Save the whole system
self.__precomputed_dynamic_constraints = self.__dynamic_constraints
# Recall the initial state of the system
self.__dynamic_constraints = [self.__dynamic_constraints[0]]
self.__shift_final() self.__shift_final()
self.__shift_invariant() self.__shift_invariant()
......
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