diff --git a/ChangeLog b/ChangeLog index ba3172a58..27a6a6297 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2010-01-05 Damien Lefortier + + Merge eltl2tgba.cc into ltl2tgba.cc. + + * src/tgbatest/eltl2tgba.cc: Remove. + * src/tgbatest/Makefile.am: Adjust. + * src/tgbatest/ltl2tgba.cc: New option: -xltl to translate an + extended LTL instead of an LTL, a feature previously offered by + eltl2tgba.cc. Also: -R3b to use delete_unaccepting_scc. + * src/tgbatest/spotlbtt.test: Adjust. + 2009-11-10 Damien Lefortier * src/tgba/tgbabddcoredata.cc (delete_unaccepting_scc): Fix a bug. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 913c9a7a9..17731347a 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -25,7 +25,7 @@ LDADD = ../libspot.la # These are the most used test programs, and they are also useful # to run manually outside the test suite. Always build them. -noinst_PROGRAMS = eltl2tgba ltl2tgba randtgba +noinst_PROGRAMS = ltl2tgba randtgba check_SCRIPTS = defs # Keep this sorted alphabetically. @@ -49,7 +49,6 @@ check_PROGRAMS = \ bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT complement_SOURCES = complementation.cc -eltl2tgba_SOURCES = eltl2tgba.cc explicit_SOURCES = explicit.cc expldot_SOURCES = powerset.cc expldot_CXXFLAGS = -DDOTTY diff --git a/src/tgbatest/eltl2tgba.cc b/src/tgbatest/eltl2tgba.cc deleted file mode 100644 index 22b4b0ccb..000000000 --- a/src/tgbatest/eltl2tgba.cc +++ /dev/null @@ -1,151 +0,0 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE) -// -// 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 2 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 Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include -#include -#include -#include -#include -#include "ltlparse/public.hh" -#include "eltlparse/public.hh" -#include "tgbaalgos/eltl2tgba_lacim.hh" -#include "tgbaalgos/dotty.hh" -#include "tgbaalgos/lbtt.hh" -#include "tgbaalgos/save.hh" -#include "ltlvisit/tostring.hh" -#include "ltlast/allnodes.hh" - -void -syntax(char* prog) -{ - std::cerr << "Usage: " << prog << " [OPTIONS...] formula [file]" << std::endl - << " " << prog << " -F [OPTIONS...] file [file]" << std::endl - << " " << prog << " -L [OPTIONS...] file [file]" << std::endl - << " " << prog << " -LW [OPTIONS...] file [file]" << std::endl - << std::endl - << "Options:" << std::endl - << " -F read the formula from the file (extended input format)" - << std::endl - << " -L read the formula from an LBTT-compatible file" - << std::endl - << " -LW read the formula from an LBTT-compatible file" - << " (with no reduction)" - << std::endl; -} - -std::string -ltl_defs() -{ - std::string s = "\ -X=(0 1 true \ - 1 2 $0 \ - accept 2) \ -U=(0 0 $0 \ - 0 1 $1 \ - accept 1) \ -G=(0 0 $0) \ -F=U(true, $0) \ -R=!U(!$0, !$1)"; - return s; -} - -int -main(int argc, char** argv) -{ - if (argc < 2) - { - syntax(argv[0]); - return 1; - } - - spot::eltl::parse_error_list p; - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::ltl::formula* f = 0; - int formula_index = 0; - int reduce = 1; - - if (strcmp(argv[1], "-F") == 0) - { - f = spot::eltl::parse_file(argv[2], p, env, false); - formula_index = 2; - } - if (strcmp(argv[1], "-L") == 0 || strcmp(argv[1], "-LW") == 0) - { - reduce = strcmp(argv[1], "-LW") == 0 ? 0 : 1; - std::string input; - std::ifstream ifs(argv[2]); - std::getline(ifs, input, '\0'); - - spot::ltl::parse_error_list p_; - f = spot::ltl::parse(input, p_, env, false); - input = ltl_defs(); - input += "%"; - input += spot::ltl::to_string(f, true); - f->destroy(); - - f = spot::eltl::parse_string(input, p, env, false); - formula_index = 2; - } - if (formula_index == 0) - { - std::stringstream oss; - oss << ltl_defs() << "%" << argv[1]; - f = spot::eltl::parse_string(oss.str(), p, env, false); - formula_index = 1; - } - - if (spot::eltl::format_parse_errors(std::cerr, p)) - { - if (f != 0) - std::cout << f->dump() << std::endl; - return 1; - } - - assert(f != 0); - std::cerr << f->dump() << std::endl; - - spot::bdd_dict* dict = new spot::bdd_dict(); - spot::tgba_bdd_concrete* concrete = spot::eltl_to_tgba_lacim(f, dict); - if (reduce == 1) - concrete->delete_unaccepting_scc(); - - if (strcmp(argv[1], "-L") == 0 || strcmp(argv[1], "-LW") == 0) - spot::lbtt_reachable(std::cout, concrete); - else - { - spot::dotty_reachable(std::cout, concrete); - if (formula_index + 1 < argc) - { - std::ofstream ofs(argv[formula_index + 1]); - spot::tgba_save_reachable(ofs, concrete); - ofs.close(); - } - } - - f->destroy(); - delete concrete; - - assert(spot::ltl::atomic_prop::instance_count() == 0); - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); - assert(spot::ltl::automatop::instance_count() == 0); - delete dict; -} diff --git a/src/tgbatest/eltl2tgba.test b/src/tgbatest/eltl2tgba.test index ddf845942..cafa4511d 100755 --- a/src/tgbatest/eltl2tgba.test +++ b/src/tgbatest/eltl2tgba.test @@ -6,7 +6,7 @@ set -e # Check if the TGBA was corretly constructed. check_construct() { - run 0 ../eltl2tgba -F "$1" input + run 0 ../ltl2tgba -F -l -xltl -b "$1" > output } # Check if the TGBA behaves correctly by doing an emptiness check on @@ -14,11 +14,11 @@ check_construct() # translated using FM. check_true() { - run 0 ../ltl2tgba -e -Pinput -f "$1" + run 0 ../ltl2tgba -e -Poutput -f "$1" } check_false() { - run 1 ../ltl2tgba -e -Pinput -f "$1" + run 1 ../ltl2tgba -e -Poutput -f "$1" } # Create the prelude file. diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 2b9dd5d29..127c9e10f 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -49,12 +49,30 @@ #include "tgbaalgos/replayrun.hh" #include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/sccfilter.hh" +#include "tgbaalgos/eltl2tgba_lacim.hh" +#include "eltlparse/public.hh" #include "misc/timer.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/scc.hh" #include "tgbaalgos/emptiness_stats.hh" +std::string +ltl_defs() +{ + std::string s = "\ +X=(0 1 true \ + 1 2 $0 \ + accept 2) \ +U=(0 0 $0 \ + 0 1 $1 \ + accept 1) \ +G=(0 0 $0) \ +F=U(true, $0) \ +R=!U(!$0, !$1)"; + return s; +} + void syntax(char* prog) { @@ -125,6 +143,7 @@ syntax(char* prog) << "reachability graph" << std::endl << " -A same as -a, but as a set" << std::endl + << " -xltl translate an extended LTL, not an LTL" << std::endl << " -r display the relation BDD, not the reachability graph" << std::endl << " -R same as -r, but as a set" << std::endl @@ -170,6 +189,7 @@ syntax(char* prog) << " -R2t remove transitions using delayed simulation" << std::endl << " -R3 use SCC to reduce the automata" << std::endl + << " -R3b delete unaccepting SCC directly on the BDD" << std::endl << " -Rd display the simulation relation" << std::endl << " -RD display the parity game (dot format)" << std::endl << std::endl @@ -254,6 +274,8 @@ main(int argc, char** argv) bool from_file = false; int reduc_aut = spot::Reduce_None; int redopt = spot::ltl::Reduce_None; + bool eltl = false; + bool delete_unaccepting_scc = false; bool display_reduce_form = false; bool display_rel_sim = false; bool display_parity_game = false; @@ -351,6 +373,10 @@ main(int argc, char** argv) expect_counter_example = false; output = -1; } + else if (!strcmp(argv[formula_index], "-xltl")) + { + eltl = true; + } else if (!strcmp(argv[formula_index], "-taa")) { translation = TransTAA; @@ -528,6 +554,10 @@ main(int argc, char** argv) { reduc_aut |= spot::Reduce_Scc; } + else if (!strcmp(argv[formula_index], "-R3b")) + { + delete_unaccepting_scc = true; + } else if (!strcmp(argv[formula_index], "-rd")) { display_reduce_form = true; @@ -634,11 +664,40 @@ main(int argc, char** argv) spot::ltl::formula* f = 0; if (!from_file) { - spot::ltl::parse_error_list pel; - tm.start("parsing formula"); - f = spot::ltl::parse(input, pel, env, debug_opt); - tm.stop("parsing formula"); - exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel); + if (!eltl) + { + spot::ltl::parse_error_list pel; + tm.start("parsing formula"); + f = spot::ltl::parse(input, pel, env, debug_opt); + tm.stop("parsing formula"); + exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel); + } + else if (!file_opt || output == 6) + { + // Call the LTL parser first to handle abbreviations such as + // [] when the formula is not given in a file or when the + // output in done in LBTT's format. The ELTL parser is then + // called with usual LTL operators. + spot::ltl::parse_error_list pel; + tm.start("parsing formula"); + f = spot::ltl::parse(input, pel, env, debug_opt); + input = ltl_defs(); + input += "%"; + input += spot::ltl::to_string(f, true); + f->destroy(); + spot::eltl::parse_error_list p; + f = spot::eltl::parse_string(input, p, env, debug_opt); + tm.stop("parsing formula"); + exit_code = spot::eltl::format_parse_errors(std::cerr, p); + } + else + { + spot::eltl::parse_error_list p; + tm.start("parsing formula"); + f = spot::eltl::parse_string(input, p, env, false); + tm.stop("parsing formula"); + exit_code = spot::eltl::format_parse_errors(std::cerr, p); + } } if (f || from_file) { @@ -690,7 +749,10 @@ main(int argc, char** argv) a = spot::ltl_to_taa(f, dict, containment); break; case TransLaCIM: - a = concrete = spot::ltl_to_tgba_lacim(f, dict); + if (!eltl) + a = concrete = spot::ltl_to_tgba_lacim(f, dict); + else + a = concrete = spot::eltl_to_tgba_lacim(f, dict); break; } tm.stop("translating formula"); @@ -727,6 +789,15 @@ main(int argc, char** argv) tm.stop("reducing A_f w/ SCC"); } + if (delete_unaccepting_scc) + { + tm.start("reducing A_f w/ SCC on BDD"); + if (spot::tgba_bdd_concrete* bc = + dynamic_cast(a)) + bc->delete_unaccepting_scc(); + tm.stop("reducing A_f w/ SCC on BDD"); + } + if (reduc_aut & ~spot::Reduce_Scc) { tm.start("reducing A_f w/ sim."); diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index ae7a85211..dec20ac7f 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -32,7 +32,7 @@ Algorithm { Name = "Spot (Couvreur -- LaCIM)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -l -t'" + Parameters = "--spot '../ltl2tgba -l -F -t'" Enabled = yes } @@ -40,7 +40,7 @@ Algorithm { Name = "Spot (Couvreur -- LaCIM), reduction of formula" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r4 -l -F -t'" + Parameters = "--spot '../ltl2tgba -l -F -t -r4'" Enabled = yes } @@ -49,7 +49,7 @@ Algorithm Name = "Spot (Couvreur -- LaCIM), degeneralized" Path = "${LBTT_TRANSLATE}" Parameters = "--spot '../ltl2tgba -l -F -t -D'" - Enabled = yes + Enabled = no } Algorithm @@ -64,7 +64,7 @@ Algorithm { Name = "Spot (Couvreur -- LaCIM), eltl" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../eltl2tgba -LW'" + Parameters = "--spot '../ltl2tgba -F -l -t -xltl'" Enabled = yes } @@ -72,10 +72,18 @@ Algorithm { Name = "Spot (Couvreur -- LaCIM), eltl + delete_unaccepting_scc" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../eltl2tgba -L'" + Parameters = "--spot '../ltl2tgba -F -l -t -xltl -R3b'" Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- LaCIM), eltl + post reduction with scc" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../ltl2tgba -F -l -t -xltl -R3'" + Enabled = no +} + Algorithm { Name = "Spot (Couvreur -- FM)" @@ -276,12 +284,20 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Tauriainen -- TAA), refined rules + post reduction with scc" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../ltl2tgba -F -taa -t -c -R3'" + Enabled = yes +} + Algorithm { Name = "Spot (Tauriainen -- TAA) refined rules + pre + post reduction" Path = "${LBTT_TRANSLATE}" Parameters = "--spot '../ltl2tgba -F -taa -t -c -r7 -R3'" - Enabled = yes + Enabled = no } GlobalOptions