Commit 41f415af authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

Add not used, exhaustive method to find MACs (more time consuming than find_mac)

parent 9a8d98d9
......@@ -168,12 +168,64 @@ def main2(chart_file, cam_file, cam_step_file, cam_complete_file, cam_strong_fil
# Compute the formula of the next start_property
start_prop = make_logical_formula(previous_frontier_places,
start_prop)
steps = min_steps
# If all_macs flag is not set (to True),
# search allways macs with less or equal steps than previous,
# by limiting steps.
# If all_macs == True: The limit is always the maximal number given
# in 'step' setting.
if not all_macs:
steps = min_steps
LOGGER.debug(
final_prop +
":: Next start_prop formula: {} in {} steps".format(start_prop, steps)
)
def find_macs(mcla,
cam_file, cam_step_file, cam_complete_file,
steps, final_prop, start_prop, inv_prop):
"""__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 supprimer 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 control sur les solutions fournies par SAT et les solutions non minimale
sont en générales tres éloignées de la solution minimale,
cad contiennent beaucoup plus de places.
: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 next_mac_object in vmac_list:
LOGGER.debug(final_prop + ":: Next MAC object:\n{}".format(next_mac_object))
# Save MAC and timings
LOGGER.debug(final_prop + ":: Save MAC and timings...")
with open(cam_complete_file, 'a') as file:
next_mac_object.save(file)
# Save MAC
next_mac = next_mac_object.activated_frontier
LOGGER.debug(final_prop + ":: Save next MAC: {}".format(next_mac))
with open(cam_file, 'a') as file:
file.write('\t'.join(next_mac) + '\n')
# Save min steps
min_step = mcla.unfolder.get_current_step() - 1 # Magic number !
LOGGER.debug(final_prop + ":: Save minimal steps: {}".format(min_step))
with open(cam_step_file, 'a') as file:
file.write(str(min_step)+'\n')
def find_mac(mcla,
cam_file, cam_step_file, cam_complete_file,
......
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