Commit 788ab5dd authored by Jaime Arias's avatar Jaime Arias
Browse files

refactor: formula generator in python

parent d8b655bb
#!/usr/bin/env python3
import os
import xml.etree.ElementTree as etree
import subprocess
import re
def execute_command(command):
"""Run a command in the shell"""
output = None
output = subprocess.check_output(
command, shell=True, stderr=subprocess.STDOUT).decode("utf-8")
except Exception as e:
output = e.output.decode("utf-8")
except KeyboardInterrupt:
return output
def get_atomic_propositions(pnml_file):
"""Returns the atomic propositions from a PNML file"""
xml_tree = etree.parse(pnml_file)
root = xml_tree.getroot()
ns = {'pnml': root.tag[1:].split("}")[0]}
places = [p.get('id') for p in root.findall('.//pnml:place', ns)]
transitions = [t.get('id') for t in root.findall('.//pnml:transition', ns)]
return {'places': places, 'transitions': transitions}
def generate_spot_formulas(model_name, model_instance, n, paths):
"""Generates a number of formulas for a specific PNML model
model_name : str
Name of model
model_instance : str
Instance of the model
n : int
Number of formulas to be generated
paths : dict of str
Paths of the project
list of str
list with formulas
ignored_operators = "X=0,xor=0,W=0,M=0,R=0,U=0"
pnml_file = os.path.join(paths['models'], model_name,
atomic_propositions = get_atomic_propositions(pnml_file)
atomic_propositions = '==1 '.join(atomic_propositions['places'])
command = f'{paths["randltl"]} -L -s -p -n{n} --ltl-priorities="{ignored_operators}" {atomic_propositions}'
output = execute_command(command)
formulas = output.split('\n')[:-1]
return formulas
def check_formula(model_name, model_instance, formula, timeout, paths):
"""Check whether a property is satisfied or not"""
tool = paths['pnml2lts-mc']
model_file = os.path.join(paths['models'], model_name,
command = f'{tool} --strategy=ndfs --timeout={timeout} --ltl="{formula}" {model_file}'
ltsmin_out = execute_command(command)
# timeout or error found
if (ltsmin_out is None):
return None
match_false ='Accepting cycle FOUND', ltsmin_out)
match_time ='Total exploration time (\d+(\.\d+)?)', ltsmin_out)
# ignore formulas with time zero
if match_time:
time = float(
if (time > 0):
print("* property: {}\n - it is satisfied: {}\n - time: {} s".
format(formula, not match_false, time))
return not match_false
return None
def get_default_paths():
"""Returns the default path of the project"""
# Absolute path where are stored the formulas, models
base_folder = os.path.abspath(
os.path.join(os.path.dirname(os.path.realpath(__file__)), os.pardir))
paths = {
# randltl path: this tool generates random formulas
"randltl": "randltl",
# tool to verify the property
'pnml2lts-mc': os.path.join(base_folder, "tools", "pnml2lts-mc"),
# Folder where the models are saved
'models': os.path.join(base_folder, "models"),
# Folder where the formulas are saved
'formulas': os.path.join(base_folder, "formulas"),
return paths
def generate_formulas(model_name, model_instance, n, timeout, paths):
"""Generates N satified and N violated formulas"""
true_formulas = []
false_formulas = []
random_formulas = generate_spot_formulas(model_name, model_instance, 10000,
for f in random_formulas:
if len(true_formulas) == n and len(false_formulas) == n:
is_satisfied = check_formula(model_name, model_instance, f, timeout,
# if timeout or error during the verification
if (is_satisfied is None):
# add to formulas satisfied
if is_satisfied and len(true_formulas) < n:
# add to formulas violated
if not is_satisfied and len(false_formulas) < n:
return {'satisfied': true_formulas, 'violated': true_formulas}
if __name__ == '__main__':
# 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"]
}, {
"instances": ["robot2", "robot5", "robot10", "robot20", "robot50"]
}, {
"name": "spool",
"instances": ["spool1", "spool2", "spool3", "spool4", "spool5"]
}, {
"name": "kanban",
"instances": ["kanban5", "kanban10", "kanban20"]
}, {
"instances": ["cloud5by2", "cloud10by5", "cloud20by10", "cloud40by20"]
f = generate_formulas('philo', 'philo10', 2, timeout, paths)
# pmcsog_formulas = formulas.replace('==1', '').split('\n')[:-1]
......@@ -314,7 +314,7 @@ def create_default_paths():
paths = {
# Absolute path where are stored the formulas, models, and scripts
'project': base_folder,
# # Folder where the formulas are saved
# 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"),
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