Commit 45db1c5f authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

autfilt: add a --merge-transitions option

* src/bin/randaut.cc: Fix memory leak.
* src/bin/autfilt.cc: Add a --merge-transitions option.
* src/tgbatest/readsave.test: Rewrite using randaut and autfilt.
parent fbbf584b
......@@ -59,6 +59,7 @@ Convert, transform, and filter Büchi automata.\n\
#define OPT_RANDOMIZE 6
#define OPT_SEED 7
#define OPT_PRODUCT 8
#define OPT_MERGE 9
static const argp_option options[] =
{
......@@ -117,7 +118,9 @@ static const argp_option options[] =
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Transformation:", -1 },
{ 0, 0, 0, 0, "Transformations:", 5 },
{ "merge-transitions", OPT_MERGE, 0, 0,
"merge transitions with same destination and acceptance", 0 },
{ "product", OPT_PRODUCT, "FILENAME", 0,
"build the product with FILENAME", 0 },
{ "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
......@@ -149,6 +152,7 @@ static bool randomize_tr = false;
static int opt_seed = 0;
static auto dict = spot::make_bdd_dict();
static spot::tgba_digraph_ptr opt_product = nullptr;
static bool opt_merge = false;
static int
to_int(const char* s)
......@@ -210,6 +214,9 @@ parse_opt(int key, char* arg, struct argp_state*)
format = Lbtt;
}
break;
case OPT_MERGE:
opt_merge = true;
break;
case OPT_PRODUCT:
{
spot::hoa_parse_error_list pel;
......@@ -370,6 +377,11 @@ namespace
auto aut = haut->aut;
// Do this first, because it is cheap and will help most
// algorithms.
if (opt_merge)
aut->merge_transitions();
if (opt_product)
aut = spot::product(std::move(aut), opt_product);
......
......@@ -315,4 +315,5 @@ main(int argc, char** argv)
}
flush_cout();
}
spot::ltl::destroy_atomic_prop_set(aprops);
}
......@@ -3,7 +3,7 @@
# Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
......@@ -26,105 +26,81 @@
set -e
cat >input <<\EOF
acc = c d;
s1, "s2", "a&!b", c d;
"s2", "state 3", "\"F\\G\"", c;
"state 3", s1,,;
EOF
../ltl2tgba -b -X input > stdout
autfilt=../../bin/autfilt
cat >expected <<\EOF
acc = "0" "1";
"0", "1", "a & !b", "0" "1";
"1", "2", "\"F\\G\"", "0";
"2", "0", "1",;
cat >input <<\EOF
HOA: v1
States: 3
Start: 0
AP: 3 "a" "b" "F\\G"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {0 1}
[0&!1] 1
State: 1 {0}
[2] 2
State: 2
[t] 0
--END--
EOF
# Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.)
sed 's/"d" "c"/"c" "d"/g;s/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout
diff stdout expected
mv stdout input
run 0 ../ltl2tgba -b -X input > stdout
# Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.)
sed 's/"d" "c"/"c" "d"/g;s/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout
diff input stdout
rm -f input stdout expected
run 0 $autfilt --hoa input > stdout
diff stdout input
# Transition merging
cat >input <<\EOF
acc = c;
s1, s2, "a&!b", c;
s1, s2, "b&a", c;
s1, s2, "!b", ;
s2, s1, "!b", ;
s2, s1, "a&!b", c;
s2, s1, "b&a", c;
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0&1] 1 {0}
[!1] 1
[0&!1] 1 {0}
State: 1
[!1] 0
[1&0] 0 {0}
[0&!1] 0 {0}
--END--
EOF
cat >expected <<\EOF
acc = "0";
"0", "1", "!b",;
"0", "1", "a", "0";
"1", "0", "!b",;
"1", "0", "a", "0";
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[!1] 1
[0] 1 {0}
State: 1
[!1] 0
[0] 0 {0}
--END--
EOF
run 0 ../ltl2tgba -b -X input > stdout
run 0 ../../bin/autfilt --merge-transitions --hoa input > stdout
# FIXME: use are-isomorphic once it is available
cat stdout
diff stdout expected
# Likewise, with a randomly generated TGBA.
run 0 ../randtgba -t 1 -n 20 -d 0.2 a b -a 2 0.1 >input
sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' input > tmp_ &&
mv tmp_ input
cat input
# the first read-write can renumber the states
run 0 ../ltl2tgba -b -X input > stdout
sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' stdout > tmp_ &&
mv tmp_ stdout
test `wc -l < input` = `wc -l < stdout`
# But this second shout output the same as the first
run 0 ../ltl2tgba -b -X input > stdout2
sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' stdout2 > tmp_ &&
mv tmp_ stdout2
diff stdout stdout2
rm -f input stdout stdout2
# Check the position of syntax errors in the diagnostics:
cat >input <<\EOF
acc = "c" "d";
"s1", "s2", "a & !b", "c" "d";
"s2", "state 3", "a &&", "c";
"state 3", "s1", "1)",;
EOF
run 0 ../../bin/randaut -S 20 a b -d 0.2 -a 0.2 -A 2 --hoa | tee input
run 2 ../ltl2tgba -b -X input > stdout 2>stderr
cat stderr
grep input: stderr > stderrfilt
cat >expected <<EOF
input:3.23-22: syntax error, unexpected end of formula
input:3.21-22: missing right operand for "and operator"
input:4.20: syntax error, unexpected closing parenthesis
input:4.20: ignoring trailing garbage
EOF
diff stderrfilt expected
# the first read-write can renumber the states
run 0 $autfilt --hoa --merge-transitions input > stdout
# FIXME: use are-ismorphic
# diff input stdout
# The diagnostic should be the same with DOS input
perl -pi -e 's/$/\r/' input
run 2 ../ltl2tgba -b -X input > stdout 2>stderr
cat stderr
grep input: stderr > stderrfilt
diff stderrfilt expected
# But this second output should be the same as the first
run 0 $autfilt --hoa stdout > stdout2
diff stdout stdout2
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