diff --git a/command_line/cadbiom_cmd/solution_search.py b/command_line/cadbiom_cmd/solution_search.py index a7e9b3c3b0f5686025433d00650b05a3a2c4033e..810a4da5c8959f1dc2222359b99ff7e282737231 100644 --- a/command_line/cadbiom_cmd/solution_search.py +++ b/command_line/cadbiom_cmd/solution_search.py @@ -138,10 +138,23 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil :param mac_strong_file: ??? :param steps: Maximal steps to reach the solutions. :param final_prop: Formula: Property that the solver looks for. - :param start_prop: Formula: Original property (constraint) for the solver. - :param inv_prop: Formula: ??? + :param start_prop: Formula: Original property (constraint) for the solver. ## TODO + :param inv_prop: Formula: ???## TODO :param all_macs: If set to True (not default), search all macs with - less or equal steps than previous, by limiting steps. + less or equal the maxium of steps defined with the argument `steps`. + If set to False: The solver will search all solutions with the minimum + of steps found in the first returned solution. + Example: + all_macs = False, steps = 10; + First solution found with 4 steps; + The next solution will be searched with a maximum of 4 steps; + + all_macs = True, steps = 10; + First solution found with 4 steps; + The next solution is not reachable with 4 steps but with 5 steps + (which is still less than 10 steps); + Get the solution for 5 steps; + :param continue_run: If set to True (not default), previous macs from a previous run, will be reloaded. :param limit: Limit the number of solutions. @@ -170,8 +183,6 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil # sert pas: # final_prop = "not ("+final_prop+" and "+inv_prop+")" """ - - # Build MCLA with Error Reporter mcla = MCLAnalyser(ErrorRep()) @@ -235,14 +246,21 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil current_start_prop = make_logical_formula(previous_frontier_places, start_prop) - # If all_macs flag is not set (to True), - # search allways macs with less or equal steps than previous, - # by limiting steps. + # If set to True (not default), search all macs with + # less or equal the maxium of steps defined with the argument `steps`. # If all_macs == True: The limit is always the maximal number given - # in 'step' setting. + # in 'steps' argument. if not all_macs: steps = min_steps + # Stop when limitation is reached + current_nb_sols += 1 + if current_nb_sols >= limit: + # EXIT + LOGGER.info("%s:: Reaching the limitation of the number of solutions!", + final_prop) + return + LOGGER.debug("%s:: Next start_prop formula: %s in %s steps", final_prop, current_start_prop, @@ -303,10 +321,20 @@ def find_macs(mcla, def find_mac(mcla, mac_file, mac_step_file, mac_complete_file, steps, final_prop, start_prop, inv_prop): - """ - list, min step + """Search for 1 solution, save timings, save frontiers, and return it with + the current step. + + For every new solution, the system is reinitialized, and a satisfiability + test is made on a new query to evaluate the minimal number of steps for + reachability. + + The side effect is that this process is expensive in a general way, + and that parsing the properties (logical formulas of the frontier places of + the previous solutions for example) in text format is very expensive because + realized by the grammar ANTLR. - :return: None if there is no new Solution or if problem is not satisfiable. + :return: A tuple of activated frontiers and the current step. + None if there is no new Solution or if problem is not satisfiable. """ # Build query query = MCLSimpleQuery(start_prop, inv_prop, final_prop)