Commit 1a6f72a8 authored by Jaime Arias's avatar Jaime Arias
Browse files

feature: generate all formulas for a list of models

parent 8a6f4927
......@@ -3,6 +3,7 @@
import os
import argparse
from scripts import sbatch_generator as utils
import sys
def parse_arguments():
......@@ -69,6 +70,10 @@ if __name__ == '__main__':
# Parse tool parameters
tool = {"name": args.tool[0], "parameters": {}}
if (args.parameters is None):
print('tool parameters are missing')
for parameter in args.parameters:
k, v = parameter[0].split('=')
tool["parameters"][k] = v
......@@ -6,6 +6,23 @@ import subprocess
import re
def create_folder(path):
"""Creates a folder if it does not exist
path : str
Path of the new folder
>>> create_folder('./results')
if not os.path.exists(path):
def execute_command(command):
"""Run a command in the shell"""
output = None
......@@ -116,11 +133,11 @@ def get_default_paths():
return paths
def write_formula(model_name, model_instance, formula, identifier,
def write_formula(model_name, model_instance, formula, identifier):
"""write a formula into a file"""
base = os.path.join(paths['formulas'], model_name, model_instance)
filename_ltsmin = f"{model_instance}-{verification}-{identifier}.ltl"
filename_ltsmin = f"{model_instance}-{identifier}.ltl"
filename_pmcsog = f"{filename_ltsmin}.reduced"
with open(os.path.join(base, filename_ltsmin), 'w') as ltsmin, \
......@@ -165,15 +182,25 @@ def generate_formulas(model_name,
if save:
for i, f in enumerate(true_formulas):
write_formula(model_name, model_instance, f, i + 1, 'T')
write_formula(model_name, model_instance, f, i + 1)
offset = len(true_formulas) + 1
for i, f in enumerate(false_formulas):
write_formula(model_name, model_instance, f, offset + i, 'F')
write_formula(model_name, model_instance, f, offset + i)
return {'satisfied': true_formulas, 'violated': true_formulas}
def generate_all_formulas(models, n, timeout, paths, save=True):
for model_obj in models:
model_name = model_obj['name']
model_instances = model_obj['instances']
for model_instance in model_instances:
generate_formulas(model_name, model_instance, n, timeout, paths,
if __name__ == '__main__':
# default paths of the project
paths = get_default_paths()
......@@ -210,5 +237,4 @@ if __name__ == '__main__':
"instances": ["cloud5by2", "cloud10by5", "cloud20by10", "cloud40by20"]
f = generate_formulas('philo', 'philo10', 2, timeout, paths)
generate_all_formulas(models, n_formulas, timeout, 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