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

[lib] MCLAnalyser: Rewrite __mac_exhaustive_search; Auto-adjust steps; search optimisation

parent 598ef37f
......@@ -193,6 +193,9 @@ from cadbiom.models.guard_transitions.chart_model import ChartModel
from cadbiom.models.clause_constraints.mcl.MCLSolutions import FrontierSolution, DimacsFrontierSol
from cadbiom.models.clause_constraints.mcl.MCLQuery import MCLSimpleQuery
from cadbiom import commons as cm
LOGGER = cm.logger()
class MCLAnalyser(object):
"""Query a UCL dynamical system and analyse solutions
......@@ -608,24 +611,62 @@ class MCLAnalyser(object):
return dimacfrontsol
def __mac_exhaustive_search(self, query, max_step):
"""
@param query: MCLQuery
@param max_step: int - Number of steps allowed in the unfolding;
def __mac_exhaustive_search(self, query, max_user_step):
"""Return a generator of FrontierSolution objects.
This is a function very similar to next_mac(), but it returns
many solutions.
The satisfiability tests and the banishment of the previous solutions
are done internally in an optimal way.
There is also a self adjustment of the number of minimum steps during
which to find solutions until reaching the maximum number set by the user.
---
On cherche ensuite d'abord des solutions non minimales (actuellement 2) via:
self.__sq_dimacs_frontier_solutions(query, nb_step, 2)
Pour ensuite les élaguer en supprimant les places non essentielles à la
satisfiabilité de la propriété via:
small_fsol = self.less_activated_solution(lfsol)
current_mac = self.__prune_frontier_solution(small_sol, query, nb_step)
Ce processus itératif est le plus "time-consuming" car nous n'avons pas
le controle sur les solutions fournies par SAT et les solutions non minimales
sont en général très éloignées de la solution minimale, c.-à-d. contiennent
beaucoup plus de places (ces places excédentaires sont dispensables).
:param query: Current query.
:param max_user_step: Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
@return: <generator <FrontierSolution>>
:type query: <MCLSimpleQuery>
:type max_user_step: <int>
:return: A generator of FrontierSolution objects which are a wrapper of
a symbolic representation of frontier values and timings from
a raw solution.
:rtype: <generator <FrontierSolution>>
"""
# list of timed minimal activation conditions on frontier (dimacs code)
# i.e list<DimacsFrontierSol>
mac_list = []
# mac_list = [] # Not used anymore
forbidden_frontier_values = []
## TODO: parser les properties au format DIMACS une bonne fois pour toutes
## et les ajouter dans forbidden_frontier_values
## Lors du rechargement des places précédentes, le problème du parsing va réapparaitre
# Satisfiability test
reachable = self.sq_is_satisfiable(query, max_user_step)
# get the minimum number of steps for reachability
# set number of shifts before testing final prop
min_step = self.unfolder.get_current_step() - 1
query.set_steps_before_reach(min_step)
# Get the minimum number of steps for reachability
min_step = self.unfolder.get_current_step()
# Adjust the number of useless shifts needed before finding a solution
# (i.e. testing final prop).
# __steps_before_check can't be >= max_user_step
# (see squery_is_satisfied() and squery_solve())
query.steps_before_check = min_step - 1
LOGGER.info("Solution reachable in min_step: %s", min_step)
while reachable:
# Forbidden solutions: already discovered macs (see at the end of the while loop)
......@@ -633,36 +674,71 @@ class MCLAnalyser(object):
# Equivalent of wrapping each previous solution with a logical OR:
# OR( not (frontier places))
## TODO: check in unfolder: dim_start elements joined by OR or AND operator ?
print("forbidden_frontier_values", forbidden_frontier_values)
query.dim_start = forbidden_frontier_values
## TODO: keep previous dim_start à la première itération (mettre le contenu dans forbidden values)
query.dim_start = list(forbidden_frontier_values)
print("query variant prop", query.variant_prop)
## TODO: equivaut à mettre à jour le start_prop ou __initial_property avec l'ancienne méthode ??
## si non, faudrait ptetre éviter de recompiler ça à chaque fois dans __init_initial_constraint_0
#### redondance code next_mac()
# Solutions differ on frontiers: Search only 2 different solutions
# to avoid all activated solutions
# Get <tuple <DimacsFrontierSol>>
lfsol = self.__sq_dimacs_frontier_solutions(query, max_step, 2)
if not lfsol:
break
dimacs_front_sol = self.__sq_dimacs_frontier_solutions(query, min_step, 2)
if not dimacs_front_sol:
# If we do not want to self-adjust steps, just break the loop
# break
print("NOT FOUND - current step ?", self.unfolder.get_current_step())
if self.unfolder.get_current_step() + 1 > max_user_step:
# Cosmetic break, avoid to do useless test
break
## TEST
## Make autoadjustment... of max_steps during the solving
## Juste appeler squery_solve avec les memes parametres mais
## min_step augmenté de 1
## en restant inférieur au nb d'étapes demandées à l'origine
## => on bénéficie des shifts précédents et on évite de reconstruire le problème...
# Hack: reuse the current Unfolder (without init with query)
# => do not do this at home!
self.unfolder._CLUnfolder__locked = False
# Avoid a new test of satisfiability on the same current_step
# (we already know that there is no more solution for it)
# => increment __steps_before_check
self.unfolder._CLUnfolder__steps_before_check += 1
ret = self.unfolder.squery_is_satisfied(max_user_step)
if not ret:
# The problem is definitly not satisfiable in the given
# number of steps
break
# __steps_before_check can't be >= min_step
# (see squery_is_satisfied() and squery_solve())
min_step = self.unfolder.get_current_step()
query.steps_before_check = min_step - 1
print("testing AUTO CORRECT max step:", min_step)
continue
# Get the solution with the less number of activated states
small_fsol = self.less_activated_solution(lfsol)
small_fsol = self.less_activated_solution(dimacs_front_sol)
# Prune non essential places for the satisfiability of the property
# => reduce the number of activated variables
current_mac = self.__prune_frontier_solution(small_fsol, query, max_step)
current_mac = self.__prune_frontier_solution(small_fsol, query, min_step)
## TEST
print("final current step ?", self.unfolder.get_current_step())
print("__mac_exhaustive_search:: final current step ?", self.unfolder.get_current_step())
if current_mac.nb_activated_frontiers == 0:
# Condition that seems to be never reached..
print("NOT REACHABLE")
reachable = False
else:
yield current_mac
mac_list.append(current_mac)
# mac_list.append(current_mac)
# Keep a list of frontier values to be banned in the next search
# - Get all activated frontiers on the current DimacsFrontierSol
......@@ -671,7 +747,6 @@ class MCLAnalyser(object):
[-var for var in current_mac.activated_frontier_values]
)
def next_mac(self, query, max_step):
"""Search a Minimal Access Condition for the given query.
......
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