MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 88fbb30e authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLUnfolder: Partial refactor & rewriting; have fun; more changes to come

parent 73ec45cd
......@@ -81,12 +81,17 @@ class CLUnfolder(object):
- trajectory: list of state_vectors
"""
def __init__(self, sys):
self.__dyn_sys = sys # symbolic clause dynamic system
def __init__(self, dynamic_system):
"""
:param dynamic_system: Describe a dynamic system in clause form.
:type dynamic_system: <CLDynSys>
"""
self.__dyn_sys = dynamic_system # symbolic clause dynamic system
# shift_step equal to the total number of coded variables
self.__shift_step_init = sys.get_var_number() # shift step of system
self.__shift_step = self.__shift_step_init # current shift/step
# shift_step_init: the shift step ss (if n is X_0 code, n+ss is X_1 code)
self.shift_step_init = dynamic_system.get_var_number() # shift step of system
self.__shift_step = self.shift_step_init # current shift/step
self.__locked = False
self.__current_step = 1
self.__steps_before_check = 0
......@@ -96,12 +101,19 @@ class CLUnfolder(object):
self.__lit_cpt = self.__shift_step +1 # counter for aux. var. coding
self.__var_code_table = dict() # name -> DIMACS code
self.__var_list = ['##'] # DIMACS code -> name - != 0
cpt = 1
for svar in sys.base_var_set:
self.__var_list.append(svar)
self.__var_code_table[svar] = cpt
cpt += 1
assert(cpt == self.__shift_step + 1)
# Create mappings between names and variables of the system
# dynamic_system.base_var_set : set of variables of the dynamic system
# (including aux vars)
# Fix order of variables names with a list:
# indexes of __var_list are the values of the variables at these indexes
# keys of __var_code_table are the names of the variables, and the values theirvalues
base_var_set = list(dynamic_system.base_var_set)
self.__var_list += base_var_set
self.__var_code_table = {var_name: var_num for var_num, var_name in enumerate(base_var_set, 1)}
assert len(self.__var_code_table) == self.__shift_step
# same tools for auxiliary variables from property compilation
self.__aux_code_table = dict() # name 2 code
......@@ -110,38 +122,36 @@ class CLUnfolder(object):
# list no_frontier place DIMACS codes
self.__no_frontier_init = [[-self.__var_code_table[nfp]] for nfp in self.__dyn_sys.no_frontier]
# ordered list of frontier place DIMACS codes for extraction (inv)
self.__frontier = [self.__var_code_table[frp] for frp in self.__dyn_sys.frontier]
self.__frontier.sort()
# ordered list of DIMACS code of the frontier place variables
self.frontier_values = [self.__var_code_table[frp] for frp in self.__dyn_sys.frontier]
self.frontier_values.sort() ## TODO: sort utile ici ???? si non passer en frozenset et supprimer les casts partout ailleurs
# Convenient attribute for RawSolution.extract_frontier_values()
# all frontiers and their opposite version
# Set of frontier positive and negative values.
# operations with sets are much faster
self._frontiers_pos_and_neg = \
frozenset(-frontier for frontier in self.__frontier) | frozenset(self.__frontier)
# ordered list of input places DIMACS code for extraction (inv)
## plus forcément nécessaire... ou passer avec une @property et un lrucache dessus
## ou mieux juste un attr avec les frontières négatives,
## utilisé dans RawSolution.extract_frontier_values() avec l'union des frontieres positives self.frontier_values
## utilisé dans MCLAnalyser.__solve_with_inact_fsolution directement en utilisant l'objet unfolder
self.frontiers_negative_values = frozenset(-frontier for frontier in self.frontier_values)
self.frontiers_pos_and_neg = \
self.frontiers_negative_values | frozenset(self.frontier_values)
# DIMACS codes of the input variables/places for extraction (inv)
self.__inputs = frozenset(self.__var_code_table[inp] for inp in self.__dyn_sys.inputs)
# ordered list of free clocks DIMACS code for extraction (invariant)
# DIMACS codes of the free_clocks variables/places for extraction (invariant)
self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.__dyn_sys.free_clocks)
# Binding for a merged version of __inputs and __free_clocks
# Convenient attribute for RawSolution.extract_frontier_values()
self.__inputs_and_free_clocks = self.__inputs | self.__free_clocks
# DIMACS codes of the input and free_clocks variables
self.inputs_and_free_clocks = self.__inputs | self.__free_clocks
# properties to be checked
self.__initial_property = None # string
self.__dim_initial = None # list of dimacs clauses
self.__final_property = None # idem
self.__dim_final = None
self.__invariant_property = None # idem
self.__dim_invariant = None
self.__variant_property = None # list<logic formulas>
self.__dim_variant = None # list<list<dimacs clauses>>
# list of variant temporal constraints in Dimacs ground code
self.__list_variant_constraints = None # list<list<dimacs clauses>>
# Properties to be checked
self.reset()
# constraints - logical constraints
# Logical constraints
# result from unfolding of base constraints
# Boolean vectors signification:
# X: Current state of places (activated/unactivated)
......@@ -153,7 +163,7 @@ class CLUnfolder(object):
# Simple temporal properties
# SP(X0): Initial property/start property; Never change at each step.
# IP(X): Invariant property
# VP(X): Variant property;
# VP(X): Variant property
# List of logical formulas of properties forced at each step
# FP(X): Final property
......@@ -161,7 +171,7 @@ class CLUnfolder(object):
self.__final_constraints = [] # idem: C(X_n)
self.__invariant_constraints = [] # DIMACS clauses: C(X_i))
self.__variant_constraints = [] # variant constraints along traj.
self.__shift_direction = None # forward or backward
self.__shift_direction = None # FORWARD or BACKWARD
# statistics on solver
self.__stats = False
......@@ -169,24 +179,51 @@ class CLUnfolder(object):
self.__nb_clauses = 0
def reset(self):
"""Reset the unfolder before a new query
This function is called from the constructor and during
MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions() with the
call of init_with_query().
"""
Reset the unfolder before a new query
"""
self.__initial_property = None
self.__dim_initial = None
self.__final_property = None
# Properties to be checked
self.__initial_property = None # string
self.__dim_initial = None # list of dimacs clauses
self.__final_property = None # idem
self.__dim_final = None
self.__invariant_property = None
self.__invariant_property = None # idem
self.__dim_invariant = None
self.__variant_property = None
self.__dim_variant = None
self.list_variant_constraints = None
self.__variant_property = None # list<logic formulas>
self.__dim_variant = None # list<list<dimacs clauses>>
# list of variant temporal constraints in Dimacs ground code
self.__list_variant_constraints = None # list<list<dimacs clauses>>
# If called from the constructor, for now these variables are just redefined here
self.__steps_before_check = 0
self.__shift_direction = None
self.__shift_direction = None # FORWARD or BACKWARD
self.__locked = False
def init_with_query(self, query):
"""Initialise the unfolder with the given query
Following properties are used from the query:
start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
variant_prop, dim_variant_prop, steps_before_reach
"""
# Reset the unfolder before a new query
self.reset()
# Init with properties
self.set_initial_property(query.start_prop)
self.set_dim_initial_property(query.dim_start)
self.set_current_property(query.inv_prop)
self.set_dim_current_property(query.dim_inv)
self.set_final_property(query.final_prop)
self.set_dim_final_property(query.dim_final)
self.set_variant_property(query.variant_prop)
self.set_dim_variant_property(query.dim_variant_prop)
self.set_minimal_steps(query.steps_before_reach) ## TODO check this value
def set_stats(self):
"""
Enable solver statistics
......@@ -278,10 +315,12 @@ class CLUnfolder(object):
@return: name of the variable
"""
var_code = (abs(var_num) - 1) % self.__shift_step + 1
if var_code <= self.__shift_step_init: # variable from initial system
if var_code <= self.shift_step_init:
# variable from initial system
return self.__var_list[var_code]
else: # auxiliary variable introduced by properties compilation
return self.__aux_list[var_code - self.__shift_step_init -1]
else:
# auxiliary variable introduced by properties compilation
return self.__aux_list[var_code - self.shift_step_init -1]
#raise MCLException("Not a DIMACS code of an initial variable")
def get_var_indexed_name(self, var_num):
......@@ -292,29 +331,12 @@ class CLUnfolder(object):
varnum1 = abs(var_num)
var_code = (varnum1 - 1) % self.__shift_step + 1
var_step = (varnum1 - var_code)/self.__shift_step
if var_code <= self.__shift_step_init:
if var_code <= self.shift_step_init:
return self.__var_list[var_code] + '_%s'% var_step
else:
index = var_code - self.__shift_step_init -1
index = var_code - self.shift_step_init -1
return self.__aux_list[index] + '_%s'% var_step
def get_frontier(self):
"""
@return: the DIMACS code of the frontier variables
"""
return self.__frontier
def get_frontiers_pos_and_neg(self):
"""
Convenient attribute for RawSolution.extract_frontier_values()
all frontiers and their opposite version
operations with sets are much faster
:return: Set of frontier positive and negative values.
:rtype: <frozenset>
"""
return self._frontiers_pos_and_neg
def get_free_clocks(self):
"""
@return: the DIMACS code of the free_clocks variables
......@@ -327,15 +349,6 @@ class CLUnfolder(object):
"""
return self.__inputs
def get_inputs_and_free_clocks(self):
"""Binding for a merged version of __inputs and __free_clocks
Convenient attribute for RawSolution.extract_frontier_values()
:return: the DIMACS code of the input and free_clocks variables
:rtype: <frozenset>
"""
return self.__inputs_and_free_clocks
def get_shift_direction(self):
"""
@return: string "FORWARD" or "BACKWARD"
......@@ -348,12 +361,6 @@ class CLUnfolder(object):
"""
return self.__shift_step
def get_shift_step_init(self):
"""
@return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
"""
return self.__shift_step_init
def get_current_step(self):
"""
@return: the current number of unfolding
......@@ -844,9 +851,9 @@ class CLUnfolder(object):
"""
self.__shift_direction = 'FORWARD'
self.__current_step = 1
self.__shift_step = self.__shift_step_init # back to basic!
self.__aux_code_table = dict() # flush auxiliary variables
self.__aux_list = [] # idem
self.__shift_step = self.shift_step_init # back to basic!
self.__aux_code_table = dict() # flush auxiliary variables
self.__aux_list = [] # idem
# init properties to generate all variable num codes
self.__init_initial_constraint_0()
......@@ -866,9 +873,9 @@ class CLUnfolder(object):
"""
self.__shift_direction = 'BACKWARD'
self.__current_step = 0
self.__shift_step = self.__shift_step_init # back to basic!
self.__aux_code_table = dict() # flush auxiliary variables
self.__aux_list = [] # idem
self.__shift_step = self.shift_step_init # back to basic!
self.__aux_code_table = dict() # flush auxiliary variables
self.__aux_list = [] # idem
# init properties to generate all variable num codes
self.__init_initial_constraint_0()
......@@ -975,10 +982,14 @@ class CLUnfolder(object):
def __msolve_constraints(self, max_sol, vvars):
"""
"""Get solutions from the solver
@param max_sol: int - the max number of solution returned
@param vvars: variables for which the solver must find different solutions(dimacs code)
@return: a tuple of RawSolution
:return: A tuple of RawSolution objects
RawSolution objects contain a solution got from SAT solver with all
variable parameters from the unfolder
:rtype: <tuple <RawSolution>>
"""
solver = CryptoMS()
self.__load_solver(solver)
......@@ -993,8 +1004,10 @@ class CLUnfolder(object):
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)
# Make a RawSolution for each solution (tuple of literals)
return [RawSolution(solint, self) for solint in lintsol]
return tuple(RawSolution(solint, self)
......@@ -1002,9 +1015,8 @@ class CLUnfolder(object):
# dynamic properties
def squery_is_satisfied(self, max_step):
"""
Ask the SAT solver
@param max_step: int - the horizon
"""Ask the SAT solver if the query/unfolding is satisfiable
@param max_step: int - the horizon on which the properties must be satisfied
"""
# initialization
self.init_forward_unfolding()
......
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