Commit 4e672293 authored by Jaime Arias's avatar Jaime Arias
Browse files

feature: add CLI for formula generator

parent e6097ac7
......@@ -4,6 +4,7 @@ import os
import xml.etree.ElementTree as etree
import subprocess
import re
import argparse
def create_folder(path):
......@@ -188,51 +189,60 @@ def generate_formulas(model_name,
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']
def generate_all_formulas(model_name,
model_instances,
n,
timeout,
paths,
save=True):
for model_instance in model_instances:
formulas = generate_formulas(model_name, model_instance, n, timeout,
paths, save)
print(model_instance, formulas)
for model_instance in model_instances:
formulas = generate_formulas(model_name, model_instance, n,
timeout, paths, save)
print(model_instance, formulas)
def parse_arguments():
"""Creates the command line interface"""
parser = argparse.ArgumentParser(
description='Generates formulas for a model')
parser.add_argument('--n',
type=int,
nargs=1,
required=True,
help='number of formulas')
parser.add_argument('--timeout',
type=int,
nargs=1,
required=True,
help='timeout of verification')
parser.add_argument('--model-name',
type=str,
nargs=1,
required=True,
help='Name of the model (e.g. philo)')
parser.add_argument('--model-instance',
type=str,
nargs='+',
required=True,
help='Instances of the model (e.g. philo10)')
return parser.parse_args()
if __name__ == '__main__':
args = parse_arguments()
# default paths of the project
paths = get_default_paths()
# number of formulas generated
n_formulas = 100
# timeout of verification (seconds)
timeout = 180
# Models to generate formulas
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_all_formulas(models, n_formulas, timeout, paths)
n_formulas = args.n[0]
timeout = args.timeout[0]
model_name = args.model_name[0]
model_instances = args.model_instance
generate_all_formulas(model_name, model_instances, 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