diff --git a/NEWS b/NEWS index cb130cf2c..181634834 100644 --- a/NEWS +++ b/NEWS @@ -54,6 +54,10 @@ New in spot 0.9.2a: files of formulas between different syntaxes, apply some simplifications, check whether to formulas are equivalent, ... + - ltl2tgba translate LTL/PSL formulas into Büchi automata. A + fondamental change to the interface is that you may + now specify the goal of the translation: do you + you favor deterministic or smaller automata? New in spot 0.9.2 (2012-07-02): diff --git a/bench/ltl2tgba/algorithms b/bench/ltl2tgba/algorithms index 745724b81..0f19b8891 100644 --- a/bench/ltl2tgba/algorithms +++ b/bench/ltl2tgba/algorithms @@ -77,100 +77,21 @@ Algorithm Path = "$LTL2NBA" Enabled = $HAVE_LTL2NBA } +EOF + +for type in tgba ba; do + for pref in any deterministic small; do + for level in high; do + cat >>$conffile < +#include +#include +#include + +#include +#include "progname.h" +#include "error.h" + +#include "common_r.hh" + +#include "misc/_config.h" +#include "ltlparse/public.hh" +#include "ltlvisit/simplify.hh" +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/neverclaim.hh" +#include "tgbaalgos/postproc.hh" +#include "tgbaalgos/save.hh" + +const char* argp_program_version = "\ +ltl2tgba (" 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 formulas (LTL/PSL) into Büchi automata.\n\n\ +The default is to take the time to apply all available optimization \ +to output the smallest Transition-based Generalized Büchi Automata, \ +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 + +static const argp_option options[] = + { + /**************************************************/ + { 0, 0, 0, 0, "Input options:", 1 }, + { "formula", 'f', "STRING", 0, "process the formula STRING", 0 }, + { "file", 'F', "FILENAME", 0, + "process each line of FILENAME as a formula", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Automaton type:", 2 }, + { "tgba", OPT_TGBA, 0, 0, + "Transition-based Generalized Büchi Automaton (default)", 0 }, + { "ba", 'B', 0, 0, "Büchi Automaton", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Output format:", 3 }, + { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "lbtt", OPT_LBTT, 0, 0, "LBTT's format", 0 }, + { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 }, + { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Translation intent:", 4 }, + { "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:", 5 }, + { "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 } + }; + +struct job +{ + const char* str; + bool file_p; // true if str is a filename, false if it is a formula + + job(const char* str, bool file_p) + : str(str), file_p(file_p) + { + } +}; + +typedef std::vector jobs_t; +static jobs_t jobs; + +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 } format = Dot; + + +static int +parse_opt(int key, char* arg, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + 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; + case 'F': + jobs.push_back(job(arg, true)); + break; + case 's': + 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; + case OPT_TGBA: + if (format == Spin) + error(2, 0, "--spin and --tgba are incompatible"); + type = spot::postprocessor::TGBA; + 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 = spot::ltl::parse(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); + + switch (format) + { + case Dot: + spot::dotty_reachable(std::cout, aut); + break; + case Lbtt: + spot::lbtt_reachable(std::cout, aut); + break; + case Spot: + spot::tgba_save_reachable(std::cout, aut); + break; + case Spin: + spot::never_claim_reachable(std::cout, aut, f); + break; + } + + delete aut; + 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, 0, 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 96bfa5fc5..21196b35d 100644 --- a/src/bin/man/Makefile.am +++ b/src/bin/man/Makefile.am @@ -22,12 +22,15 @@ common_dep = $(top_builddir)/configure.ac 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" + "$(PERL)" "$(top_srcdir)/tools/help2man -N -L 'en_US.UTF-8'" -dist_man1_MANS = ltlfilt.1 genltl.1 randltl.1 +dist_man1_MANS = ltlfilt.1 genltl.1 randltl.1 ltl2tgba.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 $@ + ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc $(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@ @@ -36,5 +39,3 @@ genltl.1: $(common_dep) $(srcdir)/genltl.x $(srcdir)/../genltl.cc randltl.1: $(common_dep) $(srcdir)/randltl.x $(srcdir)/../randltl.cc $(convman) ../randltl$(EXEEXT) $(srcdir)/randltl.x $@ - - diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x new file mode 100644 index 000000000..f7f660e42 --- /dev/null +++ b/src/bin/man/ltl2tgba.x @@ -0,0 +1,4 @@ +[NAME] +ltl2tgba \- translate LTL/PSL formulas into Büchi automata +[DESCRIPTION] +.\" Add any additional description here diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 15f665b09..8584b7fb9 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -48,6 +48,7 @@ tgbaalgos_HEADERS = \ magic.hh \ minimize.hh \ neverclaim.hh \ + postproc.hh \ powerset.hh \ projrun.hh \ randomgraph.hh \ @@ -87,6 +88,7 @@ libtgbaalgos_la_SOURCES = \ minimize.cc \ ndfs_result.hxx \ neverclaim.cc \ + postproc.cc \ powerset.cc \ projrun.cc \ randomgraph.cc \ diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc new file mode 100644 index 000000000..5469eed41 --- /dev/null +++ b/src/tgbaalgos/postproc.cc @@ -0,0 +1,119 @@ +// -*- 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 "postproc.hh" +#include "minimize.hh" +#include "simulation.hh" +#include "sccfilter.hh" +#include "degen.hh" +#include "stats.hh" + +namespace spot +{ + unsigned count_states(const tgba* a) + { + // FIXME: the number of states can be found more + // efficiently in explicit automata. + tgba_statistics st = stats_reachable(a); + return st.states; + } + + const tgba* postprocessor::run(const tgba* a, const ltl::formula* f) + { + if (type_ == TGBA && pref_ == Any && level_ == Low) + return a; + + // Remove useless SCCs. + { + const tgba* s = scc_filter(a, false); + delete a; + a = s; + } + + if (pref_ == Any) + { + if (type_ == BA) + { + const tgba* d = degeneralize(a); + delete a; + a = d; + } + return a; + } + + const tgba* wdba = 0; + const tgba* sim = 0; + + // (Small,Low) is the only configuration where we do not run + // WDBA-minimization. + if (pref_ != Small || level_ != Low) + { + bool reject_bigger = (pref_ == Small) && (level_ == Medium); + wdba = minimize_obligation(a, f, 0, reject_bigger); + if (wdba == a) // Minimization failed. + wdba = 0; + // The WDBA is a BA, so no degeneralization required. + } + + // Run a simulation when wdba failed (or was not run), or + // at hard levels if we want a small output. + if (!wdba || (level_ == High && pref_ == Small)) + { + if (level_ == Low) + sim = simulation(a); + else + sim = iterated_simulations(a); + + // Degeneralize the result of the simulation if needed. + if (type_ == BA) + { + const tgba* d = degeneralize(sim); + delete sim; + sim = d; + } + } + + delete a; + + if (wdba && sim) + { + if (count_states(wdba) > count_states(sim)) + { + delete wdba; + wdba = 0; + + if (type_ == TGBA && level_ == High) + { + const tgba* s = scc_filter(sim, true); + delete sim; + sim = s; + } + } + else + { + delete sim; + sim = 0; + } + } + + return wdba ? wdba : sim; + } +} diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh new file mode 100644 index 000000000..8adbc16ce --- /dev/null +++ b/src/tgbaalgos/postproc.hh @@ -0,0 +1,99 @@ +// -*- 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_TGBAALGOS_POSTPROC_HH +# define SPOT_TGBAALGOS_POSTPROC_HH + +#include "tgba/tgba.hh" + +namespace spot +{ + /// \addtogroup tgba_reduction + /// @{ + + /// \brief Wrap TGBA/BA post-processing algorithms in an easy interface. + /// + /// This class is a shell around scc_filter(), + /// minimize_obligation(), simulation(), iterated_simulations(), and + /// degeneralize(). These different algorithms will be combined + /// depending on the various options set with set_type(), + /// set_pref(), and set_level(). + /// + /// This helps hiding some of the logic required to combine these + /// simplifications efficiently (e.g., there is no point calling + /// degeneralize() or any simulation when minimize_obligation() + /// succeeded.) + /// + /// Use set_pref() method to specify whether you favor + /// deterministic automata or small automata. If you don't care, + /// less post processing will be done. + /// + /// The set_level() method let you set the optimization level. + /// Higher level enable more costly postprocessign. For instance + /// pref=Small,level=High will try two different postprocessings + /// (one with minimize_obligation(), and one with + /// iterated_simulations()) an keep the smallest result. + /// pref=Small,level=Medium will only try the iterated_simulations() + /// when minimized_obligation failed to produce an automaton smaller + /// than its input. pref=Small,level=Low will only run + /// simulation(). + class postprocessor + { + public: + postprocessor() + : type_(TGBA), pref_(Small), level_(High) + { + } + + enum output_type { TGBA, BA }; + void + set_type(output_type type) + { + type_ = type; + } + + enum output_pref { Any, Small, Deterministic }; + void + set_pref(output_pref pref) + { + pref_ = pref; + } + + + enum optimization_level { Low, Medium, High }; + void + set_level(optimization_level level) + { + level_ = level; + } + + /// Return the optimized automaton and delete \a input. + const tgba* run(const tgba* input, const ltl::formula* f); + + private: + output_type type_; + output_pref pref_; + optimization_level level_; + }; + /// @} +} + +#endif // SPOT_TGBAALGOS_POSTPROC_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index e1afe5c99..f0f0252c3 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -106,6 +106,7 @@ TESTS = \ emptchkr.test \ ltlcounter.test \ spotlbtt.test \ + spotlbtt2.test \ complementation.test \ randpsl.test diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index f264ae7bc..00a314102 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -95,30 +95,6 @@ Algorithm Enabled = yes } -Algorithm -{ - Name = "Spot (Couvreur -- FM), basic reduction of formula" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r1 -F -f -t'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM), reduction of formula using class of formula" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r2 -F -f -t'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM), reduction of formula using implies relation" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r3 -F -f -t'" - Enabled = no -} - Algorithm { Name = "Spot (Couvreur -- FM), reduction of formula (pre reduction)" @@ -249,7 +225,6 @@ Algorithm } - Algorithm { Name = "Spot (Couvreur -- FM), degeneralized on states" @@ -258,30 +233,6 @@ Algorithm Enabled = yes } -Algorithm -{ - Name = "Spot (Couvreur -- FM exprop)" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -x -t'" - Enabled = yes -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM exprop), without symb_merge" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -x -y -t'" - Enabled = yes -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM exprop), degeneralized" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -x -t -D'" - Enabled = yes -} - Algorithm { Name = "Spot (Couvreur -- FM post_branch + exprop)" @@ -314,14 +265,6 @@ Algorithm Enabled = yes } -Algorithm -{ - Name = "Spot (Couvreur -- FM), pre + post reduction, degeneralized on states" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -DS -R3 -r7 -t'" - Enabled = yes -} - Algorithm { Name = "Spot (Tauriainen -- TAA)" @@ -338,21 +281,6 @@ 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 = no -} GlobalOptions { diff --git a/src/tgbatest/spotlbtt2.test b/src/tgbatest/spotlbtt2.test new file mode 100755 index 000000000..04f29ee00 --- /dev/null +++ b/src/tgbatest/spotlbtt2.test @@ -0,0 +1,81 @@ +#!/bin/sh +# -*- 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. + + +. ./defs + +set -e + +rm -f config +for type in tgba ba; do + for pref in any deterministic small; do + for level in low medium high; do + cat >>config <>config <