diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index d62ff063f..eefc76a1b 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -34,6 +34,7 @@ #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/hoa.hh" #include "tgbaalgos/neverclaim.hh" +#include "tgbaalgos/product.hh" #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" #include "tgba/bddprint.hh" @@ -57,6 +58,7 @@ Convert, transform, and filter Büchi automata.\n\ #define OPT_STATS 5 #define OPT_RANDOMIZE 6 #define OPT_SEED 7 +#define OPT_PRODUCT 8 static const argp_option options[] = { @@ -116,6 +118,8 @@ static const argp_option options[] = "a single %", 0 }, /**************************************************/ { 0, 0, 0, 0, "Transformation:", -1 }, + { "product", OPT_PRODUCT, "FILENAME", 0, + "build the product with FILENAME", 0 }, { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL, "randomize states and transitions (specify 's' or 't' to" "randomize only states or transitions)", 0 }, @@ -143,6 +147,8 @@ static spot::option_map extra_options; static bool randomize_st = false; 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 int to_int(const char* s) @@ -204,6 +210,20 @@ parse_opt(int key, char* arg, struct argp_state*) format = Lbtt; } break; + case OPT_PRODUCT: + { + spot::hoa_parse_error_list pel; + auto p = hoa_parse(arg, pel, dict); + if (spot::format_hoa_parse_errors(std::cerr, arg, pel) + || !p || p->aborted) + error(2, 0, "failed to read automaton from %s", arg); + if (!opt_product) + opt_product = std::move(p->aut); + else + opt_product = spot::product(std::move(opt_product), + std::move(p->aut)); + } + break; case OPT_RANDOMIZE: if (arg) { @@ -347,12 +367,19 @@ namespace { spot::stopwatch sw; sw.start(); - auto aut = post.run(haut->aut, nullptr); - const double conversion_time = sw.stop(); + + auto aut = haut->aut; + + if (opt_product) + aut = spot::product(std::move(aut), opt_product); + + aut = post.run(aut, nullptr); if (randomize_st || randomize_tr) spot::randomize(aut, randomize_st, randomize_tr); + const double conversion_time = sw.stop(); + switch (format) { case Dot: @@ -394,7 +421,6 @@ namespace process_file(const char* filename) { spot::hoa_parse_error_list pel; - auto b = spot::make_bdd_dict(); auto hp = spot::hoa_stream_parser(filename); int err = 0; @@ -402,7 +428,7 @@ namespace for (;;) { pel.clear(); - auto haut = hp.parse(pel, b); + auto haut = hp.parse(pel, dict); if (!haut && pel.empty()) break; if (spot::format_hoa_parse_errors(std::cerr, filename, pel)) diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index ffb54416b..aa357cf84 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -38,7 +38,6 @@ check_PROGRAMS = \ checkta \ emptchk \ expldot \ - explprod \ intvcomp \ intvcmp2 \ ltlprod \ @@ -46,8 +45,7 @@ check_PROGRAMS = \ powerset \ readsat \ taatgba \ - tgbaread \ - tripprod + tgbaread # Keep this sorted alphabetically. acc_SOURCES = acc.cc @@ -58,7 +56,6 @@ complement_SOURCES = complementation.cc emptchk_SOURCES = emptchk.cc expldot_SOURCES = powerset.cc expldot_CXXFLAGS = -DDOTTY -explprod_SOURCES = explprod.cc intvcomp_SOURCES = intvcomp.cc intvcmp2_SOURCES = intvcmp2.cc ltl2tgba_SOURCES = ltl2tgba.cc @@ -69,7 +66,6 @@ randtgba_SOURCES = randtgba.cc readsat_SOURCES = readsat.cc taatgba_SOURCES = taatgba.cc tgbaread_SOURCES = tgbaread.cc -tripprod_SOURCES = tripprod.cc # Keep this sorted by STRENGTH. Test basic things first, # because such failures will be easier to diagnose and fix. diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test index 3635b3819..8691e99cd 100755 --- a/src/tgbatest/explpro2.test +++ b/src/tgbatest/explpro2.test @@ -27,23 +27,58 @@ set -e cat >input1 <input2 <expected <<'EOF' -acc = "0" "1" "2" "3"; -"0 * 0", "1 * 1", "!a & b", "0" "2"; -"0 * 0", "2 * 2", "a & !b", "1" "3"; +HOA: v1 +States: 3 +Start: 0 +AP: 2 "b" "a" +acc-name: generalized-Buchi 4 +Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3) +properties: trans-labels explicit-labels trans-acc deterministic +--BODY-- +State: 0 +[0&!1] 1 {0 2} +[!0&1] 2 {1 3} +State: 1 +State: 2 +--END-- EOF -run 0 ../explprod input1 input2 | tee stdout +run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout +# FIXME: Use are-isomorphic diff stdout expected + rm input1 input2 stdout expected diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test index 18b69e0a8..045069d52 100755 --- a/src/tgbatest/explpro3.test +++ b/src/tgbatest/explpro3.test @@ -27,24 +27,57 @@ set -e cat >input1 <input2 <expected <input1 <input2 <expected <<'EOF' -acc = "0" "1"; -"0 * 0", "0 * 0", "a", "0"; -"0 * 0", "0 * 0", "!a", "1"; +HOA: v1 +States: 1 +Start: 0 +AP: 1 "a" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc complete deterministic +--BODY-- +State: 0 +[!0] 0 {1} +[0] 0 {0} +--END-- EOF -run 0 ../explprod input1 input2 > stdout -cat stdout +run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout +# FIXME: Use are-isomorphic diff stdout expected + rm input1 input2 stdout expected diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc deleted file mode 100644 index f9219cf0b..000000000 --- a/src/tgbatest/explprod.cc +++ /dev/null @@ -1,66 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 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 -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include -#include -#include "tgba/tgbaproduct.hh" -#include "tgbaparse/public.hh" -#include "tgbaalgos/save.hh" -#include "ltlast/allnodes.hh" - -void -syntax(char* prog) -{ - std::cerr << prog << " file1 file2" << std::endl; - exit(2); -} - -int -main(int argc, char** argv) -{ - int exit_code = 0; - - if (argc != 3) - syntax(argv[0]); - - { - auto dict = spot::make_bdd_dict(); - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::tgba_parse_error_list pel1; - auto a1 = spot::tgba_parse(argv[1], pel1, dict, env); - if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1)) - return 2; - spot::tgba_parse_error_list pel2; - auto a2 = spot::tgba_parse(argv[2], pel2, dict, env); - if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2)) - return 2; - - spot::tgba_save_reachable(std::cout, product(a1, a2)); - } - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); - assert(spot::ltl::atomic_prop::instance_count() == 0); - return exit_code; -} diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test index e54436786..9385ec6e5 100755 --- a/src/tgbatest/explprod.test +++ b/src/tgbatest/explprod.test @@ -27,26 +27,77 @@ set -e cat >input1 <input2 <expected <expected <. - -#include -#include -#include -#include "tgba/tgbaproduct.hh" -#include "tgbaparse/public.hh" -#include "tgbaalgos/save.hh" -#include "ltlast/allnodes.hh" - -void -syntax(char* prog) -{ - std::cerr << prog << " file1 file2 file3" << std::endl; - exit(2); -} - -int -main(int argc, char** argv) -{ - int exit_code = 0; - - if (argc != 4) - syntax(argv[0]); - { - auto dict = spot::make_bdd_dict(); - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::tgba_parse_error_list pel1; - auto a1 = spot::tgba_parse(argv[1], pel1, dict, env); - if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1)) - return 2; - spot::tgba_parse_error_list pel2; - auto a2 = spot::tgba_parse(argv[2], pel2, dict, env); - if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2)) - return 2; - spot::tgba_parse_error_list pel3; - auto a3 = spot::tgba_parse(argv[3], pel3, dict, env); - if (spot::format_tgba_parse_errors(std::cerr, argv[3], pel3)) - return 2; - - spot::tgba_save_reachable(std::cout, product(product(a1, a2), a3)); - } - - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); - assert(spot::ltl::atomic_prop::instance_count() == 0); - return exit_code; -} diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test index 3b53e209b..a37abdfd3 100755 --- a/src/tgbatest/tripprod.test +++ b/src/tgbatest/tripprod.test @@ -26,37 +26,88 @@ set -e cat >input1 <input2 <input3 <expected <