From 76787b23c07f08e75d57387568335fa1f1f1c242 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 20 Oct 2012 20:18:01 +0200 Subject: [PATCH] postproc: add the possibility to output a monitor * src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add a Monitor output option. * src/bin/ltl2tgba.cc: Add a --monitor/-M option. * NEWS: Mention monitors. * src/tgba/tgbaexplicit.hh (is_accepting_state): Fix for the case where the automaton has no acceptance set. --- NEWS | 20 +++++++------ src/bin/ltl2tgba.cc | 13 ++++++-- src/tgba/tgbaexplicit.hh | 3 +- src/tgbaalgos/Makefile.am | 2 ++ src/tgbaalgos/postproc.cc | 44 +++++++++++++++++++++++++++ src/tgbaalgos/postproc.hh | 5 ++-- src/tgbaalgos/stripacc.cc | 63 +++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/stripacc.hh | 34 +++++++++++++++++++++ 8 files changed, 169 insertions(+), 15 deletions(-) create mode 100644 src/tgbaalgos/stripacc.cc create mode 100644 src/tgbaalgos/stripacc.hh diff --git a/NEWS b/NEWS index aa42b4414..8d53f9ce9 100644 --- a/NEWS +++ b/NEWS @@ -25,17 +25,19 @@ New in spot 0.9.2a: 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? + - ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA, + BA, or Monitor). 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? - ltl2tgta: Translate LTL/PSL formulas into Testing Automata. - - ltlcheck: A tool to find bugs in translators from LTL/PSL to - Büchi automata. This is essentially a Spot-based - reimplementation of LBTT that supports PSL in addition - to LTL, and that can output more statistics. + - ltlcheck: Compare the output of translators from LTL/PSL to + Büchi automata, to find bug or for benchmarking. This + is essentially a Spot-based reimplementation of LBTT + that supports PSL in addition to LTL, and that can + output more statistics. These binaries are built in the src/bin/ directory. The former test versions of genltl and randltl have been removed from the @@ -113,7 +115,7 @@ New in spot 0.9.2a: automata generated with the web interface.) - A new class, "postprocessor", makes it easier to apply - all availlable simplification algorithms on a TGBA. + all availlable simplification algorithms on a TGBA/BA/Monitors. * Minor changes: diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 252e344e5..0507c96b6 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -56,10 +56,12 @@ If multiple formulas are supplied, several automata will be output."; static const argp_option options[] = { /**************************************************/ - { 0, 0, 0, 0, "Automaton type:", 2 }, + { 0, 0, 0, 0, "Output automaton type:", 2 }, { "tgba", OPT_TGBA, 0, 0, "Transition-based Generalized Büchi Automaton (default)", 0 }, { "ba", 'B', 0, 0, "Büchi Automaton", 0 }, + { "monitor", 'M', 0, 0, "Monitor (accepts all finite prefixes " + "of the given formula)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, @@ -116,9 +118,13 @@ parse_opt(int key, char* arg, struct argp_state*) case 'B': type = spot::postprocessor::BA; break; + case 'M': + type = spot::postprocessor::Monitor; + break; case 's': format = Spin; - type = spot::postprocessor::BA; + if (type != spot::postprocessor::Monitor) + type = spot::postprocessor::BA; break; case OPT_DOT: format = Dot; @@ -209,7 +215,8 @@ namespace { case Dot: spot::dotty_reachable(std::cout, aut, - type == spot::postprocessor::BA); + (type == spot::postprocessor::BA) + || (type == spot::postprocessor::Monitor)); break; case Lbtt: spot::lbtt_reachable(std::cout, aut); diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 633c12610..674da38a0 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -710,7 +710,8 @@ namespace spot // So we need only to check one to decide if (st->successors.empty()) return false; - return st->successors.front().acceptance_conditions != bddfalse; + return (st->successors.front().acceptance_conditions + == this->all_acceptance_conditions_); } private: diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 963ec4a18..92b48797b 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -63,6 +63,7 @@ tgbaalgos_HEADERS = \ se05.hh \ simulation.hh \ stats.hh \ + stripacc.hh \ tau03.hh \ tau03opt.hh \ reductgba_sim.hh \ @@ -105,6 +106,7 @@ libtgbaalgos_la_SOURCES = \ se05.cc \ simulation.cc \ stats.cc \ + stripacc.cc \ tau03.cc \ tau03opt.cc \ reductgba_sim.cc \ diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 31ffb658e..53e5589cf 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -23,6 +23,7 @@ #include "sccfilter.hh" #include "degen.hh" #include "stats.hh" +#include "stripacc.hh" namespace spot { @@ -46,6 +47,49 @@ namespace spot a = s; } + if (type_ == Monitor) + { + if (pref_ == Deterministic) + { + const tgba* m = minimize_monitor(a); + delete a; + return m; + } + else + { + const tgba* m = strip_acceptance(a); + delete a; + a = m; + } + if (pref_ == Any) + return a; + + const tgba* sim; + if (level_ == Low) + sim = simulation(a); + else + sim = iterated_simulations(a); + if (level_ != High) + { + delete a; + return sim; + } + // For Small,High we return the smallest between the output of + // the simulation, and that of the deterministic minimization. + const tgba* m = minimize_monitor(a); + delete a; + if (count_states(m) > count_states(sim)) + { + delete m; + return sim; + } + else + { + delete sim; + return m; + } + } + if (pref_ == Any) { if (type_ == BA) diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index 8c8f1093f..3bc6d684f 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -27,7 +27,8 @@ namespace spot /// \addtogroup tgba_reduction /// @{ - /// \brief Wrap TGBA/BA post-processing algorithms in an easy interface. + /// \brief Wrap TGBA/BA/Monitor post-processing algorithms in an + /// easy interface. /// /// This class is a shell around scc_filter(), /// minimize_obligation(), simulation(), iterated_simulations(), and @@ -61,7 +62,7 @@ namespace spot { } - enum output_type { TGBA, BA }; + enum output_type { TGBA, BA, Monitor }; void set_type(output_type type) { diff --git a/src/tgbaalgos/stripacc.cc b/src/tgbaalgos/stripacc.cc new file mode 100644 index 000000000..da7e31c67 --- /dev/null +++ b/src/tgbaalgos/stripacc.cc @@ -0,0 +1,63 @@ +// -*- 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 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 "stripacc.hh" +#include "reachiter.hh" + +namespace spot +{ + namespace + { + class strip_iter: public tgba_reachable_iterator_depth_first + { + public: + strip_iter(const tgba* a) + : tgba_reachable_iterator_depth_first(a), + out_(new sba_explicit_number(a->get_dict())) + { + } + + sba_explicit_number* + result() + { + return out_; + } + + void + process_link(const state*, int in, + const state*, int out, + const tgba_succ_iterator* si) + { + state_explicit_number::transition* t = out_->create_transition(in, out); + out_->add_conditions(t, si->current_condition()); + } + + private: + sba_explicit_number* out_; + }; + } + + sba_explicit_number* + strip_acceptance(const tgba* a) + { + strip_iter si(a); + si.run(); + return si.result(); + } +} diff --git a/src/tgbaalgos/stripacc.hh b/src/tgbaalgos/stripacc.hh new file mode 100644 index 000000000..93eccbd55 --- /dev/null +++ b/src/tgbaalgos/stripacc.hh @@ -0,0 +1,34 @@ +// -*- 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 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 . + +#ifndef SPOT_TGBAALGOS_STRIPACC_HH +# define SPOT_TGBAALGOS_STRIPACC_HH + +# include "tgba/tgbaexplicit.hh" + +namespace spot +{ + /// \brief Duplicate automaton \a a, removing all acceptance sets. + /// + /// This is equivalent to marking all states/transitions as accepting. + /// \ingroup tgba_misc + sba_explicit_number* strip_acceptance(const tgba* a); +} + +#endif // SPOT_TGBAALGOS_STRIPACC_HH