Commit e6097ac7 authored by Jaime Arias's avatar Jaime Arias
Browse files

fix: save formula into file when it is found

parent 91ed2c05
#!/bin/bash
###################################################################
#Title : formula-generator.sh
#Description : Generates LTL formulas without the X operator
#Authors : Hiba Ouni, Jaime Arias
#Date : 22-12-2019
#Usage : ./formula-generator.sh
###################################################################
# Check for model
if [ -z "$1" ]; then
echo "No model supplied"
exit 1
fi
# randltl path: this tool generates random formulas
RANDLTL="randltl";
# Absolute path where are stored the formulas, models
BASE_FOLDER="${PWD}";
# folder containing the models (.net files)
MODELS_FOLDER="${BASE_FOLDER}/models";
# folder where the formulas will be stored
OUTPUT_BASE_FOLDER="${BASE_FOLDER}/formulas";
# tool to verify the property
TOOL="${BASE_FOLDER}/tools/pnml2lts-mc";
# timeout of verification (seconds)
TIMEOUT=180;
# list with the models' name (separated by spaces)
MODELS="$1";
# number of formulas generated
N_FORMULAS=100;
# ignored operators
OPERATORS="X=0,xor=0,W=0,M=0,R=0,U=0";
# Flag: keep old formulas
KEEP_OLDS=true;
# Make backup of all formulas
if ${KEEP_OLDS} ; then find ${OUTPUT_BASE_FOLDER} -type f -name "*.ltl*" -print0 -exec mv {} {}_bk \; &>/dev/null; fi
for model in ${MODELS}; do
for model_file in ${MODELS_FOLDER}/${model}/*.net; do
model_name=`basename $model_file .net`;
# create output folder if it does not exist
output_folder="${OUTPUT_BASE_FOLDER}/${model}/${model_name}";
[[ -d ${output_folder} ]] || mkdir -p ${output_folder};
atomic_props=`awk '/place/{ print $2"==1"}' ${model_file}`;
# Generate a pool of formulas
all_formulas_file="${output_folder}/${model_name}-all.ltl";
${RANDLTL} -L -s -n 10000 --ltl-priorities ${OPERATORS} -o ${all_formulas_file} ${atomic_props};
nb_true_formulas=0;
nb_false_formulas=0;
id_formula=1;
while IFS= read -r formula; do
# Check property
tmp_file="tmp.txt";
${TOOL} --strategy=ndfs --timeout=${TIMEOUT} --ltl="${formula}" ${model_file%.*}.pnml &> ${tmp_file};
is_false_formula=`grep -c "Accepting cycle FOUND" ${tmp_file}`;
is_true_formula=`grep -c "Empty product with LTL" ${tmp_file}`;
rm ${tmp_file};
# false formula
if [ $is_false_formula -gt 0 ] && [ $nb_false_formulas -lt $N_FORMULAS ]; then
echo $formula >> ${output_folder}/${model_name}-${id_formula}.ltl;
((nb_false_formulas++))
((id_formula++))
fi
# true formula
if [ $is_true_formula -gt 0 ] && [ $nb_true_formulas -lt $N_FORMULAS ]; then
# true formula
echo $formula >> ${output_folder}/${model_name}-${id_formula}.ltl;
((nb_true_formulas++))
((id_formula++))
fi
# exit loop
if [ $nb_false_formulas -eq $N_FORMULAS ] && [ $nb_true_formulas -eq $N_FORMULAS ]; then
break;
fi
done < "${all_formulas_file}"
rm ${all_formulas_file};
# Translate into pmc-sog syntax of formulas
for formula_file in ${output_folder}/*.ltl; do
sed -e "s/==1//g" ${formula_file} > "${formula_file}.reduced";
done;
done;
done;
if ${KEEP_OLDS} ; then find ${OUTPUT_BASE_FOLDER} -type f -name "*_bk" -print0 -exec rename.ul "_bk" "" {} \; &>/dev/null; fi
...@@ -161,6 +161,7 @@ def generate_formulas(model_name, ...@@ -161,6 +161,7 @@ def generate_formulas(model_name,
random_formulas = generate_spot_formulas(model_name, model_instance, random_formulas = generate_spot_formulas(model_name, model_instance,
100000, paths) 100000, paths)
formula_id = 1
for f in random_formulas: for f in random_formulas:
if len(true_formulas) == n and len(false_formulas) == n: if len(true_formulas) == n and len(false_formulas) == n:
break break
...@@ -175,18 +176,14 @@ def generate_formulas(model_name, ...@@ -175,18 +176,14 @@ def generate_formulas(model_name,
# add to formulas satisfied # add to formulas satisfied
if is_satisfied and len(true_formulas) < n: if is_satisfied and len(true_formulas) < n:
true_formulas.append(f) true_formulas.append(f)
write_formula(model_name, model_instance, f, formula_id)
formula_id = formula_id + 1
# add to formulas violated # add to formulas violated
if not is_satisfied and len(false_formulas) < n: if not is_satisfied and len(false_formulas) < n:
false_formulas.append(f) false_formulas.append(f)
write_formula(model_name, model_instance, f, formula_id)
if save: formula_id = formula_id + 1
for i, f in enumerate(true_formulas):
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)
return {'satisfied': true_formulas, 'violated': true_formulas} return {'satisfied': true_formulas, 'violated': true_formulas}
......
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