From 1f0c765547a5ed4a1e6f6e74f4aa1035b531a54e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 24 Sep 2012 15:41:53 +0200 Subject: [PATCH] ltl2tgta: new tool * src/bin/common_post.cc, src/bin/common_post.hh: New files, extracted from ... * src/bin/ltl2tgba.cc: ... here. * src/bin/ltl2tgta.cc, src/bin/man/ltl2tgta.x: New files. * src/bin/Makefile.am, src/bin/man/Makefile.am: Adjust. * NEWS: Mention ltl2tgta. --- NEWS | 1 + src/bin/Makefile.am | 5 +- src/bin/common_post.cc | 85 +++++++++++ src/bin/common_post.hh | 35 +++++ src/bin/ltl2tgba.cc | 50 +----- src/bin/ltl2tgta.cc | 330 ++++++++++++++++++++++++++++++++++++++++ src/bin/man/Makefile.am | 5 +- src/bin/man/ltl2tgta.x | 4 + 8 files changed, 469 insertions(+), 46 deletions(-) create mode 100644 src/bin/common_post.cc create mode 100644 src/bin/common_post.hh create mode 100644 src/bin/ltl2tgta.cc create mode 100644 src/bin/man/ltl2tgta.x diff --git a/NEWS b/NEWS index 4ee4da650..a35cffd2d 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,7 @@ New in spot 0.9.2a: fondamental change to the interface is that you may now specify the goal of the translation: do you you favor deterministic or smaller automata? + - ltl2tgta translate LTL/PSL formulas into Testing Automata. These binaries are built in the src/bin/ directory. The former test versions of genltl and randltl have been removed from the diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 884b61045..d6f3d3018 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -34,14 +34,17 @@ libcommon_a_SOURCES = \ common_finput.hh \ common_output.cc \ common_output.hh \ + common_post.cc \ + common_post.hh \ common_range.cc \ common_range.hh \ common_r.cc \ common_r.hh \ common_sys.hh -bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba +bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlfilt_SOURCES = ltlfilt.cc genltl_SOURCES = genltl.cc randltl_SOURCES = randltl.cc ltl2tgba_SOURCES = ltl2tgba.cc +ltl2tgta_SOURCES = ltl2tgta.cc diff --git a/src/bin/common_post.cc b/src/bin/common_post.cc new file mode 100644 index 000000000..5f8cb2ff3 --- /dev/null +++ b/src/bin/common_post.cc @@ -0,0 +1,85 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement 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 "common_post.hh" +#include "common_r.hh" +#include "error.h" + +spot::postprocessor::output_type type = spot::postprocessor::TGBA; +spot::postprocessor::output_pref pref = spot::postprocessor::Small; +spot::postprocessor::optimization_level level = spot::postprocessor::High; + +#define OPT_SMALL 1 +#define OPT_LOW 2 +#define OPT_MEDIUM 3 +#define OPT_HIGH 4 + +static const argp_option options[] = + { + /**************************************************/ + { 0, 0, 0, 0, "Translation intent:", 20 }, + { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 }, + { "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 }, + { "any", 'a', 0, 0, "no preference", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Optimization level:", 21 }, + { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 }, + { "medium", OPT_MEDIUM, 0, 0, "moderate optimizations", 0 }, + { "high", OPT_HIGH, 0, 0, + "all available optimizations (slow, default)", 0 }, + { 0, 0, 0, 0, 0, 0 } + }; + +static int +parse_opt_post(int key, char*, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + case 'a': + pref = spot::postprocessor::Any; + break; + case 'D': + pref = spot::postprocessor::Deterministic; + break; + case OPT_HIGH: + level = spot::postprocessor::High; + simplification_level = 3; + break; + case OPT_LOW: + level = spot::postprocessor::Low; + simplification_level = 1; + break; + case OPT_MEDIUM: + level = spot::postprocessor::Medium; + simplification_level = 2; + break; + case OPT_SMALL: + pref = spot::postprocessor::Small; + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +const struct argp post_argp = { options, parse_opt_post, 0, 0, 0, 0, 0 }; + diff --git a/src/bin/common_post.hh b/src/bin/common_post.hh new file mode 100644 index 000000000..772021002 --- /dev/null +++ b/src/bin/common_post.hh @@ -0,0 +1,35 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement 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. + +#ifndef SPOT_BIN_COMMON_POST_HH +#define SPOT_BIN_COMMON_POST_HH + +#include "common_sys.hh" +#include "tgbaalgos/postproc.hh" +#include + +extern const struct argp post_argp; + +extern spot::postprocessor::output_type type; +extern spot::postprocessor::output_pref pref; +extern spot::postprocessor::optimization_level level; + +#endif // SPOT_BIN_COMMON_FINPUT_HH diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index a61d77eb2..5e61d3847 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -33,6 +33,7 @@ #include "common_r.hh" #include "common_cout.hh" #include "common_finput.hh" +#include "common_post.hh" #include "misc/_config.h" #include "ltlparse/public.hh" @@ -41,7 +42,6 @@ #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/neverclaim.hh" -#include "tgbaalgos/postproc.hh" #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" #include "tgba/bddprint.hh" @@ -64,14 +64,10 @@ in GraphViz's format.\n\ If multiple formulas are supplied, several automata will be output."; #define OPT_TGBA 1 -#define OPT_SMALL 2 -#define OPT_LOW 3 -#define OPT_MEDIUM 4 -#define OPT_HIGH 5 -#define OPT_DOT 6 -#define OPT_LBTT 7 -#define OPT_SPOT 8 -#define OPT_STATS 9 +#define OPT_DOT 2 +#define OPT_LBTT 3 +#define OPT_SPOT 4 +#define OPT_STATS 5 static const argp_option options[] = { @@ -108,17 +104,6 @@ static const argp_option options[] = { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, /**************************************************/ - { 0, 0, 0, 0, "Translation intent:", 5 }, - { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 }, - { "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 }, - { "any", 'a', 0, 0, "no preference", 0 }, - /**************************************************/ - { 0, 0, 0, 0, "Optimization level:", 6 }, - { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 }, - { "medium", OPT_MEDIUM, 0, 0, "moderate optimizations", 0 }, - { "high", OPT_HIGH, 0, 0, - "all available optimizations (slow, default)", 0 }, - /**************************************************/ { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { 0, 0, 0, 0, 0, 0 } }; @@ -126,12 +111,10 @@ static const argp_option options[] = const struct argp_child children[] = { { &finput_argp, 0, 0, 1 }, + { &post_argp, 0, 0, 20 }, { 0, 0, 0, 0 } }; -spot::postprocessor::output_type type = spot::postprocessor::TGBA; -spot::postprocessor::output_pref pref = spot::postprocessor::Small; -spot::postprocessor::optimization_level level = spot::postprocessor::High; enum output_format { Dot, Lbtt, Spin, Spot, Stats } format = Dot; bool utf8 = false; const char* stats = ""; @@ -145,15 +128,9 @@ parse_opt(int key, char* arg, struct argp_state*) case '8': spot::enable_utf8(); break; - case 'a': - pref = spot::postprocessor::Any; - break; case 'B': type = spot::postprocessor::BA; break; - case 'D': - pref = spot::postprocessor::Deterministic; - break; case 'f': jobs.push_back(job(arg, false)); break; @@ -164,27 +141,12 @@ parse_opt(int key, char* arg, struct argp_state*) format = Spin; type = spot::postprocessor::BA; break; - case OPT_HIGH: - level = spot::postprocessor::High; - simplification_level = 3; - break; case OPT_DOT: format = Dot; break; case OPT_LBTT: format = Lbtt; break; - case OPT_LOW: - level = spot::postprocessor::Low; - simplification_level = 1; - break; - case OPT_MEDIUM: - level = spot::postprocessor::Medium; - simplification_level = 2; - break; - case OPT_SMALL: - pref = spot::postprocessor::Small; - break; case OPT_SPOT: format = Spot; break; diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc new file mode 100644 index 000000000..359799931 --- /dev/null +++ b/src/bin/ltl2tgta.cc @@ -0,0 +1,330 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement 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 "common_sys.hh" + +#include +#include +#include +#include + +#include +#include "progname.h" +#include "error.h" + +#include "common_r.hh" +#include "common_cout.hh" +#include "common_finput.hh" +#include "common_post.hh" + +#include "misc/_config.h" +#include "ltlparse/public.hh" +#include "ltlvisit/simplify.hh" +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/postproc.hh" +#include "tgba/bddprint.hh" + +#include "taalgos/tgba2ta.hh" +#include "taalgos/dotty.hh" +#include "taalgos/minimize.hh" + +const char* argp_program_version = "\ +ltl2tgta (" SPOT_PACKAGE_STRING ")\n\ +\n\ +Copyright (C) 2012 Laboratoire de Recherche et Développement de l'Epita.\n\ +This is free software; see the source for copying conditions. There is NO\n\ +warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE,\n\ +to the extent permitted by law."; + +const char* argp_program_bug_address = "<" SPOT_PACKAGE_BUGREPORT ">"; + +const char argp_program_doc[] ="\ +Translate linear-time formulas (LTL/PSL) into Testing Automata.\n\n\ +By default it outputs a transition-based generalized Testing Automaton \ +the smallest Transition-based Generalized Büchi Automata, \ +in GraphViz's format. The input formula is assumed to be \ +stuttering-insensitive."; + +#define OPT_TGTA 1 +#define OPT_TA 2 +#define OPT_GTA 3 +#define OPT_SPLV 4 +#define OPT_SPNO 5 +#define OPT_INIT 6 + +static const argp_option options[] = + { + /**************************************************/ + { 0, 0, 0, 0, "Automaton type:", 1 }, + { "tgta", OPT_TGTA, 0, 0, + "Transition-based Generalized Testing Automaton (default)", 0 }, + { "ta", OPT_TA, 0, 0, "Testing Automaton", 0 }, + { "gta", OPT_GTA, 0, 0, "Generalized Testing Automaton", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Options for TA and GTA creation:", 3 }, + { "single-pass-lv", OPT_SPLV, 0, 0, + "add an artificial livelock state to obtain a single-pass (G)TA", 0 }, + { "single-pass", OPT_SPNO, 0, 0, + "create a single-pass (G)TA without artificial livelock state", 0 }, + { "multiple-init", OPT_INIT, 0, 0, + "do not create the fake initial state", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Output options:", 4 }, + { "utf8", '8', 0, 0, "enable UTF-8 characters in output", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Miscellaneous options:", -1 }, + { 0, 0, 0, 0, 0, 0 } + }; + +const struct argp_child children[] = + { + { &finput_argp, 0, 0, 1 }, + { &post_argp, 0, 0, 20 }, + { 0, 0, 0, 0 } + }; + +enum ta_types { TGTA, GTA, TA }; +ta_types ta_type = TGTA; + +bool utf8 = false; +const char* stats = ""; +bool opt_with_artificial_initial_state = true; +bool opt_single_pass_emptiness_check = false; +bool opt_with_artificial_livelock = false; + +static int +parse_opt(int key, char* arg, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + case '8': + spot::enable_utf8(); + break; + case 'B': + type = spot::postprocessor::BA; + break; + case 'f': + jobs.push_back(job(arg, false)); + break; + case 'F': + jobs.push_back(job(arg, true)); + break; + case OPT_TGTA: + ta_type = TGTA; + type = spot::postprocessor::TGBA; + break; + case OPT_GTA: + ta_type = GTA; + type = spot::postprocessor::TGBA; + break; + case OPT_TA: + ta_type = TA; + type = spot::postprocessor::BA; + break; + case OPT_INIT: + opt_with_artificial_initial_state = false; + break; + case OPT_SPLV: + opt_with_artificial_livelock = true; + break; + case OPT_SPNO: + opt_single_pass_emptiness_check = true; + break; + case ARGP_KEY_ARG: + // FIXME: use stat() to distinguish filename from string? + jobs.push_back(job(arg, false)); + break; + + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + + +namespace +{ + class trans_processor + { + public: + spot::ltl::ltl_simplifier& simpl; + spot::postprocessor& post; + + trans_processor(spot::ltl::ltl_simplifier& simpl, + spot::postprocessor& post) + : simpl(simpl), post(post) + { + } + + int + process_formula(const std::string& input, + const char* filename = 0, int linenum = 0) + { + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = parse_formula(input, pel); + + if (!f || pel.size() > 0) + { + if (filename) + error_at_line(0, 0, filename, linenum, "parse error:"); + spot::ltl::format_parse_errors(std::cerr, input, pel); + if (f) + f->destroy(); + return 1; + } + + const spot::ltl::formula* res = simpl.simplify(f); + f->destroy(); + f = res; + + // This helps ltl_to_tgba_fm() to order BDD variables in a more + // natural way (improving the degeneralization). + simpl.clear_as_bdd_cache(); + + bool exprop = level == spot::postprocessor::High; + const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop); + aut = post.run(aut, f); + + if (utf8) + { + spot::tgba* a = const_cast(aut); + if (spot::tgba_explicit_formula* tef = + dynamic_cast(a)) + tef->enable_utf8(); + else if (spot::sba_explicit_formula* sef = + dynamic_cast(a)) + sef->enable_utf8(); + } + + bdd ap_set = atomic_prop_collect_as_bdd(f, aut); + + if (ta_type != TGTA) + { + spot::ta* testing_automaton = 0; + testing_automaton = tgba_to_ta(aut, ap_set, + type == spot::postprocessor::BA, + opt_with_artificial_initial_state, + opt_single_pass_emptiness_check, + opt_with_artificial_livelock); + if (level != spot::postprocessor::Low) + { + spot::ta* testing_automaton_nm = testing_automaton; + testing_automaton = spot::minimize_ta(testing_automaton); + delete testing_automaton_nm; + } + spot::dotty_reachable(std::cout, testing_automaton); + delete testing_automaton; + } + else + { + spot::tgta_explicit* tgta = tgba_to_tgta(aut, ap_set); + if (level != spot::postprocessor::Low) + { + spot::tgta_explicit* a = spot::minimize_tgta(tgta); + delete tgta; + tgta = a; + } + spot::dotty_reachable(std::cout, + dynamic_cast(tgta) + ->get_ta()); + delete tgta; + } + + delete aut; + flush_cout(); + return 0; + } + + int + process_stream(std::istream& is, const char* filename) + { + int error = 0; + int linenum = 0; + std::string line; + while (std::getline(is, line)) + error |= process_formula(line, filename, ++linenum); + return error; + } + + int + process_file(const char* filename) + { + // Special case for stdin. + if (filename[0] == '-' && filename[1] == 0) + return process_stream(std::cin, filename); + + errno = 0; + std::ifstream input(filename); + if (!input) + error(2, errno, "cannot open '%s'", filename); + return process_stream(input, filename); + } + }; +} + +static int +run_jobs() +{ + spot::ltl::ltl_simplifier simpl(simplifier_options()); + + spot::postprocessor postproc; + postproc.set_pref(pref); + postproc.set_type(type); + postproc.set_level(level); + + trans_processor processor(simpl, postproc); + + int error = 0; + jobs_t::const_iterator i; + for (i = jobs.begin(); i != jobs.end(); ++i) + { + if (!i->file_p) + error |= processor.process_formula(i->str); + else + error |= processor.process_file(i->str); + } + if (error) + return 2; + return 0; +} + +int +main(int argc, char** argv) +{ + set_program_name(argv[0]); + // Simplify the program name, because argp() uses it to report errors + // and display help text. + argv[0] = const_cast(program_name); + + const argp ap = { options, parse_opt, "[FORMULA...]", + argp_program_doc, children, 0, 0 }; + + if (int err = argp_parse(&ap, argc, argv, 0, 0, 0)) + exit(err); + + if (jobs.empty()) + error(2, 0, "No formula to translate? Run '%s --help' for usage.", + program_name); + + return run_jobs(); +} diff --git a/src/bin/man/Makefile.am b/src/bin/man/Makefile.am index 21196b35d..31aa70433 100644 --- a/src/bin/man/Makefile.am +++ b/src/bin/man/Makefile.am @@ -24,13 +24,16 @@ x_to_1 = $(top_builddir)/tools/x-to-1 convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \ "$(PERL)" "$(top_srcdir)/tools/help2man -N -L 'en_US.UTF-8'" -dist_man1_MANS = ltlfilt.1 genltl.1 randltl.1 ltl2tgba.1 +dist_man1_MANS = ltlfilt.1 genltl.1 randltl.1 ltl2tgba.1 ltl2tgta.1 MAINTAINERCLEANFILES = $(dist_man1_MANS) EXTRA_DIST = $(dist_man1_MANS:.1=.x) ltl2tgba.1: $(common_dep) $(srcdir)/ltl2tgba.x $(srcdir)/../ltl2tgba.cc $(convman) ../ltl2tgba$(EXEEXT) $(srcdir)/ltl2tgba.x $@ +ltl2tgta.1: $(common_dep) $(srcdir)/ltl2tgta.x $(srcdir)/../ltl2tgta.cc + $(convman) ../ltl2tgta$(EXEEXT) $(srcdir)/ltl2tgta.x $@ + ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc $(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@ diff --git a/src/bin/man/ltl2tgta.x b/src/bin/man/ltl2tgta.x new file mode 100644 index 000000000..e52ed1aed --- /dev/null +++ b/src/bin/man/ltl2tgta.x @@ -0,0 +1,4 @@ +[NAME] +ltl2tgta \- translate LTL/PSL formulas into Testing Automata +[DESCRIPTION] +.\" Add any additional description here