Commit 6eedb8fe authored by Jaime Arias's avatar Jaime Arias
Browse files

add min number of explored states

parent 7e7e88b8
......@@ -107,18 +107,37 @@ def check_formula(model_name, model_instance, formula, timeout, min_states,
# ignore formulas with time zero
if match_time:
# time = float(match_time.group(1))
nb_states = int(match_states.group(1))
if (nb_states >= min_states):
# print("* property: {}\n - it is satisfied: {}\n - time: {} s".
# format(formula, not match_false, time))
return not match_false
return None
def check_explored_states(model_name, model_instance, formula, time_out,
min_explored_states, paths):
"""Checks the number of states visited by the model checker"""
tool = paths['pnml2lts-mc']
model_file = os.path.join(paths['models'], model_name,
f"{model_instance}.pnml")
command = f'{tool} --strategy=dfs --timeout={timeout*60} --ltl="{formula}" {model_file}'
ltsmin_out = execute_command(command)
# timeout or error found
if (ltsmin_out is None):
return None
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 ltsmin_out
def get_default_paths():
"""Returns the default path of the project"""
......@@ -164,6 +183,7 @@ def generate_formulas(model_name,
n,
timeout,
min_states,
min_explored_states,
paths,
save=True):
"""Generates N satisfied and N violated formulas"""
......@@ -171,7 +191,7 @@ def generate_formulas(model_name,
false_formulas = []
random_formulas = generate_spot_formulas(model_name, model_instance,
100000, paths)
1000000, paths)
formula_id = 1
for f in random_formulas:
......@@ -185,6 +205,11 @@ 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))
# add to formulas satisfied
if is_satisfied and len(true_formulas) < n:
true_formulas.append(f)
......@@ -205,11 +230,13 @@ def generate_all_formulas(model_name,
n,
timeout,
min_states,
min_explored_states,
paths,
save=True):
for model_instance in model_instances:
formulas = generate_formulas(model_name, model_instance, n, timeout,
min_states, paths, save)
min_states, min_explored_states, paths,
save)
print(model_instance, formulas)
......@@ -228,7 +255,7 @@ def parse_arguments():
type=int,
nargs=1,
required=True,
help='timeout of verification')
help='timeout of verification (s)')
parser.add_argument('--min_states',
type=int,
......@@ -236,6 +263,12 @@ def parse_arguments():
required=True,
help='minimum number of states')
parser.add_argument('--min_explored_states',
type=int,
nargs=1,
required=True,
help='minimum number of explored states')
parser.add_argument('--model-name',
type=str,
nargs=1,
......@@ -260,8 +293,9 @@ if __name__ == '__main__':
n_formulas = args.n[0]
timeout = args.timeout[0]
min_states = args.min_states[0]
min_explored_states = args.min_explored_states[0]
model_name = args.model_name[0]
model_instances = args.model_instance
generate_all_formulas(model_name, model_instances, n_formulas, timeout,
min_states, paths)
min_states, min_explored_states, paths)
......@@ -62,14 +62,14 @@ def create_default_paths():
return paths
def command(model_name, model_instance, n_formulas, min_states, timeout,
paths):
def command(model_name, model_instance, n_formulas, min_states,
min_explored_states, timeout, paths):
command = os.path.join(paths["scripts"], "formula_generator.py")
return f"{command} --n {n_formulas} --timeout {timeout} --min_states {min_states} --model-name {model_name} --model-instance {model_instance}"
return f"{command} --n {n_formulas} --timeout {timeout} --min_states {min_states} --min_explored_states {min_explored_states} --model-name {model_name} --model-instance {model_instance}"
def generate_sbatch(model_name, model_instance, n_formulas, min_states,
timeout, threads, paths):
min_explored_states, timeout, threads, paths):
sbatch_folder = os.path.join(paths['slurm'], "formulas", model_name)
create_folder(sbatch_folder)
......@@ -88,18 +88,18 @@ def generate_sbatch(model_name, model_instance, n_formulas, min_states,
sbatch_file.write(header)
srun_command = command(model_name, model_instance, n_formulas,
min_states, timeout, paths)
min_states, min_explored_states, timeout, paths)
sbatch_file.write(srun_command)
sbatch_file.write("\n\n")
def generate_multiple_sbatchs(models, n_formulas, min_states, timeout, threads,
paths):
def generate_multiple_sbatchs(models, n_formulas, min_states,
min_explored_states, timeout, threads, paths):
for model_object in models:
model_name = model_object["name"]
for model_instance in model_object["instances"]:
generate_sbatch(model_name, model_instance, n_formulas, min_states,
timeout, threads, paths)
min_explored_states, timeout, threads, paths)
if __name__ == '__main__':
......@@ -115,6 +115,9 @@ if __name__ == '__main__':
# 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
# Number of threads to run the model-checker
threads = 16
......@@ -137,5 +140,5 @@ if __name__ == '__main__':
"instances": ["spool1", "spool2", "spool3", "spool4", "spool5"]
}]
generate_multiple_sbatchs(models, n_formulas, min_states, timeout, threads,
paths)
generate_multiple_sbatchs(models, n_formulas, min_states,
min_explored_states, timeout, threads, paths)
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