Commit 203c2390 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[cmd] solutions_search; Doc for find_mac; prepare code for the new find_macs api

parent bb954cc9
......@@ -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)
......
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