Commit 31504149 authored by Jaime Arias's avatar Jaime Arias
Browse files

fix formula generator

parent 0e4c2a2b
......@@ -127,15 +127,15 @@ def check_explored_states(model_name, model_instance, formula, time_out,
# timeout or error found
if (ltsmin_out is None):
return None
return False
match_regex_explored = re.search(r'Explored (\d+) states', ltsmin_out)
if match_regex_explored:
nb_explored_states = int(match_regex_explored.group(1))
return nb_explored_states
return nb_explored_states >= min_explored_states
return ltsmin_out
return False
def get_default_paths():
......@@ -205,10 +205,10 @@ def generate_formulas(model_name,
if (is_satisfied is None):
continue
print(
"# explored states: ",
check_explored_states(model_name, model_instance, f, timeout,
min_explored_states, paths))
# if number of explored states is not satisfied
if not check_explored_states(model_name, model_instance, f, timeout,
min_explored_states, paths):
continue
# add to formulas satisfied
if is_satisfied and len(true_formulas) < n:
......
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