Commit 8a6f4927 authored by Jaime Arias's avatar Jaime Arias
Browse files

feature: write formulas into files

parent 788ab5dd
......@@ -87,9 +87,9 @@ def check_formula(model_name, model_instance, formula, timeout, paths):
# ignore formulas with time zero
if match_time:
time = float(match_time.group(1))
if (time > 0):
print("* property: {}\n - it is satisfied: {}\n - time: {} s".
format(formula, not match_false, time))
if (time > 0.0):
# print("* property: {}\n - it is satisfied: {}\n - time: {} s".
# format(formula, not match_false, time))
return not match_false
return None
......@@ -116,13 +116,33 @@ def get_default_paths():
return paths
def generate_formulas(model_name, model_instance, n, timeout, paths):
def write_formula(model_name, model_instance, formula, identifier,
verification):
"""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_pmcsog = f"{filename_ltsmin}.reduced"
with open(os.path.join(base, filename_ltsmin), 'w') as ltsmin, \
open(os.path.join(base, filename_pmcsog), 'w') as pmcsog:
pmcsog_formula = formula.replace('==1', '')
ltsmin.write(formula)
pmcsog.write(pmcsog_formula)
def generate_formulas(model_name,
model_instance,
n,
timeout,
paths,
save=True):
"""Generates N satified and N violated formulas"""
true_formulas = []
false_formulas = []
random_formulas = generate_spot_formulas(model_name, model_instance, 10000,
paths)
random_formulas = generate_spot_formulas(model_name, model_instance,
100000, paths)
for f in random_formulas:
if len(true_formulas) == n and len(false_formulas) == n:
......@@ -143,6 +163,14 @@ def generate_formulas(model_name, model_instance, n, timeout, paths):
if not is_satisfied and len(false_formulas) < n:
false_formulas.append(f)
if save:
for i, f in enumerate(true_formulas):
write_formula(model_name, model_instance, f, i + 1, 'T')
offset = len(true_formulas) + 1
for i, f in enumerate(false_formulas):
write_formula(model_name, model_instance, f, offset + i, 'F')
return {'satisfied': true_formulas, 'violated': true_formulas}
......@@ -184,5 +212,3 @@ if __name__ == '__main__':
f = generate_formulas('philo', 'philo10', 2, timeout, paths)
print(f)
# pmcsog_formulas = formulas.replace('==1', '').split('\n')[:-1]
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