Commit 80f8614d authored by Jaime Arias's avatar Jaime Arias
Browse files

update formula generator

parent c9e4a5ff
......@@ -110,6 +110,7 @@ def check_formula(model_name, model_instance, formula, timeout, min_states,
nb_states = int(match_states.group(1))
if (nb_states >= min_states):
print("# states (state space):", nb_states)
return not match_false
return None
......@@ -133,6 +134,7 @@ def check_explored_states(model_name, model_instance, formula, time_out,
if match_regex_explored:
nb_explored_states = int(match_regex_explored.group(1))
print("# explored states: ", nb_explored_states)
return nb_explored_states >= min_explored_states
return False
......@@ -191,7 +193,7 @@ def generate_formulas(model_name,
false_formulas = []
random_formulas = generate_spot_formulas(model_name, model_instance,
1000000, paths)
100000, paths)
formula_id = 1
for f in random_formulas:
......
......@@ -106,17 +106,17 @@ if __name__ == '__main__':
# Default paths
paths = create_default_paths()
# Timeout: 3 minutes
timeout = 3
# Timeout: 5 minutes
timeout = 5
# Formulas to be verified
n_formulas = 100
n_formulas = 1
# Minimum number of states in the generated state space
min_states = 1000
# Minimum number of states explored by the model checker
min_explored_states = 1500000000
min_explored_states = 500000000
# Number of threads to run the model-checker
threads = 16
......
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