From 45db1c5fb9f83ed17f787fe7444b0a5ee4c91ed3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 8 Dec 2014 21:43:39 +0100 Subject: [PATCH] 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. --- src/bin/autfilt.cc | 14 +++- src/bin/randaut.cc | 1 + src/tgbatest/readsave.test | 148 ++++++++++++++++--------------------- 3 files changed, 76 insertions(+), 87 deletions(-) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index eefc76a1b..b5db0bfcb 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -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); diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index dc189b408..ebe88c6d5 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -315,4 +315,5 @@ main(int argc, char** argv) } flush_cout(); } + spot::ltl::destroy_atomic_prop_set(aprops); } diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 14311b65e..5fa3ce51e 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -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 +autfilt=../../bin/autfilt + cat >input <<\EOF -acc = c d; -s1, "s2", "a&!b", c d; -"s2", "state 3", "\"F\\G\"", c; -"state 3", s1,,; +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 -../ltl2tgba -b -X input > stdout - -cat >expected <<\EOF -acc = "0" "1"; -"0", "1", "a & !b", "0" "1"; -"1", "2", "\"F\\G\"", "0"; -"2", "0", "1",; -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 +run 0 ../../bin/randaut -S 20 a b -d 0.2 -a 0.2 -A 2 --hoa | tee 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 +run 0 $autfilt --hoa --merge-transitions input > stdout +# FIXME: use are-ismorphic +# diff input stdout + +# But this second output should be the same as the first +run 0 $autfilt --hoa stdout > 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 2 ../ltl2tgba -b -X input > stdout 2>stderr -cat stderr -grep input: stderr > stderrfilt - -cat >expected < stdout 2>stderr -cat stderr -grep input: stderr > stderrfilt -diff stderrfilt expected