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

[lib] CLUnfolder: Full audit for squery_solve() and squery_is_satisfied()

parent f9abea5c
......@@ -1057,69 +1057,161 @@ class CLUnfolder(object):
# dynamic properties
def squery_is_satisfied(self, max_step):
"""Ask the SAT solver if the query/unfolding is satisfiable
@param max_step: int - the horizon on which the properties must be satisfied
"""Ask the SAT solver if the query/unfolding is satisfiable in the given
number of steps.
If __invariant_property is set and __final_property is not set,
1 satisfiability test is made only after all shift() calls for each
remaining step from the current step.
Otherwise, 1 test is made for each remaining step after each shift() call.
.. warning:: vvars (frontier values) are not tested. Thus the satisfiability
is not tested for interesting variables like in squery_solve().
:param max_step: The horizon on which the properties must be satisfied.
:type max_step: <int>
"""
# initialization
# Initialization
self.init_forward_unfolding()
# horizon adjustment
# Horizon adjustment
if self.__list_variant_constraints:
max_step = min(max_step, len(self.__list_variant_constraints)-1)
# loop
if self.__invariant_property and not self.__final_property :
max_step = min(max_step, len(self.__list_variant_constraints)-1) ## TODO: -1 ?
if self.__invariant_property and not self.__final_property:
# 1 satisfiability test is made only after all shift() calls for each step
# Shift all remaining steps
while self.__current_step <= max_step:
self.shift()
return self.__constraints_satisfied()
else :
while self.__current_step <= max_step:
if self.__constraints_satisfied():
return True
else:
# 1 test is made for each remaining step after each shift()
# Check and correct for incoherent data on step number
# __steps_before_check can't be >= max_step, otherwise
# __current_step could be > max_step due to shift() of "auto shift loop"
# and this function will not search any solution,
# and will return an empty list.
if self.__steps_before_check >= max_step:
self.__steps_before_check = max_step - 1
# Auto shift loop: Shift without checking (optimization)
# Do not search solutions before the specified limit
while self.__current_step < self.__steps_before_check:
print("SATIS TEST AUTO SHIFT opti")
self.shift()
return self.__constraints_satisfied()
satisfiability_test = False
while self.__current_step < max_step:
# Shift the system
self.shift()
# Test satisfiability
satisfiability_test = self.__constraints_satisfied()
print("SATIS TEST done, current_step", self.__current_step)
if satisfiability_test:
return True
# Return the satisfiability status in all cases
return satisfiability_test
def squery_solve(self, vvars, max_step, max_sol):
"""
"""Search max_sol number of solutions with max_step steps, involving vvars
(frontiers) variables of interest.
Assert a query is loaded (start_condition, inv_condition, final_condition)
@param vvars: variables on which different solutions must differ
@param max_step: bounded horizon for computations
@param max_sol: max number of solutions to be computed
@return: list of RawSolution objects
If __invariant_property is set and __final_property is not set,
1 unique solution search is made only after all shift() calls for each
remaining step from the current step.
Otherwise, 1 test is made for each remaining step after each shift() call.
:param max_step: bounded horizon for computations
:param max_sol: The maximum number of solutions to be returned
: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 max_step: <int>
:type max_sol: <int>
:type vvars: <list <int>>
:return: RawSolution objects
RawSolution objects contain a solution got from SAT solver with all
variable parameters from the unfolder
:rtype: <tuple <RawSolution>>
"""
if LOGGER.getEffectiveLevel() == DEBUG:
LOGGER.debug("squery_solve :: vvars : %s", vvars)
# initialization
# Initialization
self.init_forward_unfolding()
# horizon adjustment
# Horizon adjustment
if self.__list_variant_constraints:
max_step = min(max_step, len(self.__list_variant_constraints)-1)
max_step = min(max_step, len(self.__list_variant_constraints)-1) ## TODO: -1 ?
if self.__invariant_property and not self.__final_property:
# loop
# Shift all remaining steps
while self.__current_step <= max_step:
self.shift()
# return l_rawsol
# Solve the problem
return self.__msolve_constraints(max_sol, vvars)
else : # reachability
l_rawsol = []
# check and correct for incoherent data on step number
if self.__steps_before_check > max_step:
else:
# Check and correct for incoherent data on step number
# __steps_before_check can't be >= max_step, otherwise
# __current_step could be > max_step due to shift() of "auto shift loop"
# and this function will not search any solution,
# and will return an empty list.
if self.__steps_before_check >= max_step:
self.__steps_before_check = max_step - 1
# shift without checking (optimization)
while self.__current_step <= self.__steps_before_check:
# Auto shift loop: Shift without checking (optimization)
# Do not search solutions before the specified limit
print("squery_solve: begining; current_step:", self.__current_step, "max_step:", max_step)
while self.__current_step < self.__steps_before_check:
print("AUTO SHIFT opti")
self.shift()
# search for solutions at each step
while self.__current_step <= max_step:
lsol = self.__msolve_constraints(max_sol, vvars)
if lsol:
l_rawsol.extend(lsol)
# Search for solutions for each remaining step
# from __current_step = __steps_before_check
# (__current_step is incremented by the last shift() above)...
# ... to max_step excluded.
# Ex: __steps_before_check = 3, __current_step = 3, max_step = 4
# => we search solutions only for 1 step (step 4)
raw_solutions = list()
while self.__current_step < max_step:
self.shift()
return l_rawsol
temp_raw_solutions = self.__msolve_constraints(max_sol, vvars)
print("Nb raw_solutions:", len(temp_raw_solutions),
"steps_before_check", self.__steps_before_check,
"max_step", max_step,
"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).
# Thus, as we know the current loop is for the
# last step only, we do not need to make merge temp_raw_solutions
# with raw_solutions
# => The while loop is stopped now and we return solutions
# or an empty list
## NOTE: this optimization is questionable
if self.__steps_before_check == max_step - 1:
if temp_raw_solutions:
return temp_raw_solutions
return []
if 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