Commit 1bb6e8ae authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[cmd] solutions_search; (re)Implementation of find_macs api; solutions search...

[cmd] solutions_search; (re)Implementation of find_macs api; solutions search is now 3-4x times more performant
parent 203c2390
......@@ -212,17 +212,29 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
current_start_prop = start_prop
i = len(previous_frontier_places)-1 if previous_frontier_places else 0
#with PyCallGraph(output=GraphvizOutput()):
while True:
LOGGER.info("%s:: START PROP: %s", final_prop, current_start_prop)
# Compute the number of previously computed frontier places
current_nb_sols = len(previous_frontier_places) if previous_frontier_places else 0
if current_nb_sols >= limit:
# EXIT
i += 1
if i > limit:
LOGGER.info("%s:: Reaching the limitation of the number of solutions!",
final_prop)
return
LOGGER.info("%s:: Reaching the limitation of the number of solutions!",
final_prop)
return
## Find macs in an optimized way with find_macs() (see the docstring for more info)
LOGGER.info("%s:: Start property: %s", final_prop, current_start_prop)
# with PyCallGraph(output=GraphvizOutput()):
find_macs(mcla,
mac_file, mac_step_file, mac_complete_file,
steps, final_prop, current_start_prop, inv_prop, limit, current_nb_sols)
return
## Alternative and deprecated way
## Find mac one by one with find_mac() (see the docstring for more info)
while True:
LOGGER.info("%s:: Start property: %s", final_prop, current_start_prop)
ret = \
find_mac(mcla,
......@@ -269,29 +281,42 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
def find_macs(mcla,
mac_file, mac_step_file, mac_complete_file,
steps, final_prop, start_prop, inv_prop):
"""__mac_exhaustive_search, on cherche d´abord des solutions non minimales
steps, final_prop, start_prop, inv_prop, limit, current_nb_sols):
"""Search for many solutions, save timings, and save frontiers.
For every new solution, the system is NOT reinitialized, and a satisfiability
test is made ONLY when there is no solution for the current step.
This test is made to evaluate the minimal number of steps for reachability.
Unlike find_mac(), this function is autonomous and takes into account the
limitation of the number of solutions.
.. TODO:: Handle all_macs flag like the old method with find_mac()
Not used very often but can be usefull sometimes...
__mac_exhaustive_search, on cherche d´abord des solutions non minimales
(lfsol = 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é
(current_mac = self.__prune_frontier_solution(small_sol, query, nb_step)).
Ce processus récursif 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,
cad contiennent beaucoup plus de places.
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 limit: Limit the number of solutions.
:param current_nb_sols: The current number of solutions already found.
This number is used to limit the number of searched solutions.
:type limit: <int>
:type current_nb_sols: <int>
:return: None
"""
# Build query
query = MCLSimpleQuery(start_prop, inv_prop, final_prop)
vmac_list = mcla.mac_search(query, steps)
# If yes, in how many steps ?
# min_step = mcla.unfolder.get_current_step()
for i, frontier_sol in enumerate(mcla.mac_search(query, steps)):
print("i", i)
# Iterate on solutions
for i, frontier_sol in enumerate(mcla.mac_search(query, steps), current_nb_sols):
LOGGER.info("%s:: Current solution n°%s", final_prop, i + 1)
LOGGER.debug("%s:: Next MAC object:\n%s", final_prop, frontier_sol)
......@@ -311,11 +336,14 @@ def find_macs(mcla,
# with open(mac_step_file, 'a') as file:
# file.write(str(min_step)+'\n')
# Save min steps
# min_step = mcla.unfolder.get_current_step() - 1 # Magic number !
# LOGGER.debug("%s:: Save minimal steps: %s", final_prop, min_step)
# with open(mac_step_file, 'a') as file:
# file.write(str(min_step)+'\n')
# Stop when limitation is reached
if i + 1 >= limit:
# EXIT
LOGGER.info("%s:: Reaching the limitation of the number of solutions!",
final_prop)
return
LOGGER.info("%s:: STOP the search! No more MAC.", final_prop)
def find_mac(mcla,
......
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