Commit 579ab2ba authored by Jaime Arias's avatar Jaime Arias
Browse files

first version of formula sbatch generator

parent 3906293b
......@@ -140,7 +140,7 @@ def get_default_paths():
return paths
def write_formula(model_name, model_instance, formula, identifier):
def write_formula(model_name, model_instance, formula, identifier, paths):
"""write a formula into a file"""
base = os.path.join(paths['formulas'], model_name, model_instance)
create_folder(base)
......@@ -188,13 +188,13 @@ def generate_formulas(model_name,
# add to formulas satisfied
if is_satisfied and len(true_formulas) < n:
true_formulas.append(f)
write_formula(model_name, model_instance, f, formula_id)
write_formula(model_name, model_instance, f, formula_id, paths)
formula_id = formula_id + 1
# add to formulas violated
if not is_satisfied and len(false_formulas) < n:
false_formulas.append(f)
write_formula(model_name, model_instance, f, formula_id)
write_formula(model_name, model_instance, f, formula_id, paths)
formula_id = formula_id + 1
return {'satisfied': true_formulas, 'violated': true_formulas}
......
#!/usr/bin/env python3
import os
sbatch_header = """\
#!/bin/bash
#
#SBATCH --job-name={job_name}
#SBATCH --ntasks={nodes}
#SBATCH --cpus-per-task={threads}
#SBATCH --error={error}
#SBATCH --output={output}
# Formula generator
"""
def create_folder(path):
"""Creates a folder if it does not exist
Parameters
----------
path : str
Path of the new folder
Examples
--------
>>> create_folder('./results')
"""
if not os.path.exists(path):
os.makedirs(path)
def create_default_paths():
"""Create the default path for the project"""
base_folder = os.path.abspath(
os.path.join(os.path.dirname(os.path.realpath(__file__)), os.pardir))
paths = {
# Absolute path where are stored the formulas, models, and scripts
'project': base_folder,
# Folder where the formulas are saved
'formulas': os.path.join(base_folder, "formulas"),
# Folder where the models are saved
'models': os.path.join(base_folder, "models"),
# Folder where the results will be saved
'results': os.path.join(base_folder, "results"),
# Folder where the slurm batches will be saved
'slurm': os.path.join(base_folder, "slurm"),
# Folder where the scripts are saved
'scripts': os.path.join(base_folder, "scripts"),
# Folder where the tool are saved
'tools': os.path.join(base_folder, "tools")
}
# Create paths if they don't exist
for path in paths.values():
create_folder(path)
return paths
def command(model_name, model_instance, n_formulas, min_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}"
def generate_sbatch(model_name, model_instance, n_formulas, min_states,
timeout, threads, paths):
sbatch_folder = os.path.join(paths['slurm'], "formulas", model_name)
create_folder(sbatch_folder)
header = sbatch_header.format(job_name=f"f_gen_{model_instance}",
error=os.path.join(sbatch_folder,
f"{model_instance}.err"),
output=os.path.join(sbatch_folder,
f"{model_instance}.out"),
nodes=1,
threads=threads)
sbatch_name = f"{model_instance}.sbatch"
sbatch_file = os.path.join(sbatch_folder, sbatch_name)
with open(sbatch_file, 'w') as sbatch_file:
sbatch_file.write(header)
srun_command = command(model_name, model_instance, n_formulas,
min_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):
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)
if __name__ == '__main__':
# Default paths
paths = create_default_paths()
# Timeout: 5 minutes
timeout = 10
# Formulas to be verified
n_formulas = 200
# Minimum number of states in the generated state space
min_states = 1000
# Number of threads to run the model-checker
threads = 16
# Models to be run
models = [{
"name": "philo",
"instances": ["philo5", "philo10", "philo20"]
}, {
"name": "train",
"instances": ["train12", "train24", "train48", "train96"]
}, {
"name": "tring",
"instances": ["tring5", "tring10", "tring20"]
}, {
"name":
"robot",
"instances": ["robot2", "robot5", "robot10", "robot20", "robot50"]
}, {
"name": "spool",
"instances": ["spool1", "spool2", "spool3", "spool4", "spool5"]
}, {
"name": "kanban",
"instances": ["kanban5", "kanban10", "kanban20"]
}, {
"name":
"cloud",
"instances": ["cloud5by2", "cloud10by5", "cloud20by10", "cloud40by20"]
}]
generate_multiple_sbatchs(models, n_formulas, min_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