diff --git a/NEWS b/NEWS index a6fbca306..5d4844a5e 100644 --- a/NEWS +++ b/NEWS @@ -1,11 +1,17 @@ New in spot 1.2.4a (not yet released) - * New feature: + * New features: - The online ltl2tgba translator will automatically attempt to parse a formula using LBT's syntax if it cannot parse it using the normal infix syntax. + - ltl2tgba and dstar2tgba have a new experimental option --hoaf to + output automata in the Hanoï Omega Automaton Format whose + current draft is at http://adl.github.io/hoaf/ + The corresponding C++ function is spot::hoaf_reachable() in + tgbaalgos/hoaf.hh. + * Documentation: - The man page for ltl2tgba has some new notes and references diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 1b4b92038..f877423c6 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -35,6 +35,7 @@ #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/hoaf.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" @@ -72,6 +73,10 @@ static const argp_option options[] = /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, + "Output the automaton in HOA format. Add letters to select " + "(s) state-based acceptance, (t) transition-based acceptance, " + "(m) mixed acceptance, (l) single-line output", 0 }, { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, "LBTT's format (add =t to force transition-based acceptance even" " on Büchi automata)", 0 }, @@ -122,9 +127,10 @@ const struct argp_child children[] = { 0, 0, 0, 0 } }; -enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats } format = Dot; +enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; bool utf8 = false; const char* stats = ""; +const char* hoaf_opt = 0; spot::option_map extra_options; static int @@ -142,6 +148,10 @@ parse_opt(int key, char* arg, struct argp_state*) case 'F': jobs.push_back(job(arg, true)); break; + case 'H': + format = Hoa; + hoaf_opt = arg; + break; case 'M': type = spot::postprocessor::Monitor; break; @@ -340,6 +350,9 @@ namespace case Lbtt_t: spot::lbtt_reachable(std::cout, aut, false); break; + case Hoa: + spot::hoaf_reachable(std::cout, aut, hoaf_opt) << '\n'; + break; case Spot: spot::tgba_save_reachable(std::cout, aut); break; diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index c81db4331..7e49cbedc 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -39,6 +39,7 @@ #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/save.hh" +#include "tgbaalgos/hoaf.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/translate.hh" #include "tgba/bddprint.hh" @@ -72,6 +73,10 @@ static const argp_option options[] = { "csv-escape", OPT_CSV, 0, 0, "quote formula output by %f in --format " "for use in CSV file", 0 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, + "Output the automaton in HOA format. Add letters to select " + "(s) state-based acceptance, (t) transition-based acceptance, " + "(m) mixed acceptance, (l) single-line output", 0 }, { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, "LBTT's format (add =t to force transition-based acceptance even" " on Büchi automata)", 0 }, @@ -118,9 +123,10 @@ const struct argp_child children[] = { 0, 0, 0, 0 } }; -enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats } format = Dot; +enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; bool utf8 = false; const char* stats = ""; +const char* hoaf_opt = 0; spot::option_map extra_options; static int @@ -136,6 +142,10 @@ parse_opt(int key, char* arg, struct argp_state*) case 'B': type = spot::postprocessor::BA; break; + case 'H': + format = Hoa; + hoaf_opt = arg; + break; case 'M': type = spot::postprocessor::Monitor; break; @@ -255,6 +265,9 @@ namespace case Lbtt_t: spot::lbtt_reachable(std::cout, aut, false); break; + case Hoa: + spot::hoaf_reachable(std::cout, aut, hoaf_opt, f) << '\n'; + break; case Spot: spot::tgba_save_reachable(std::cout, aut); break; diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index cb710ffc3..811165958 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de -## Recherche et Développement de l'Epita (LRDE). +## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire +## de Recherche et Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -44,6 +44,7 @@ tgbaalgos_HEADERS = \ emptiness.hh \ emptiness_stats.hh \ gv04.hh \ + hoaf.hh \ isdet.hh \ isweakscc.hh \ lbtt.hh \ @@ -92,6 +93,7 @@ libtgbaalgos_la_SOURCES = \ eltl2tgba_lacim.cc \ emptiness.cc \ gv04.cc \ + hoaf.cc \ isdet.cc \ isweakscc.cc \ lbtt.cc \ diff --git a/src/tgbaalgos/hoaf.cc b/src/tgbaalgos/hoaf.cc new file mode 100644 index 000000000..80eb8f3fe --- /dev/null +++ b/src/tgbaalgos/hoaf.cc @@ -0,0 +1,366 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et +// Developpement 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/tgba.hh" +#include "tgba/sba.hh" +#include "hoaf.hh" +#include "reachiter.hh" +#include "misc/escape.hh" +#include "misc/bddlt.hh" +#include "misc/minato.hh" +#include "tgba/formula2bdd.hh" +#include "ltlvisit/tostring.hh" + +namespace spot +{ + namespace + { + struct metadata + { + // Assign a number to each atomic proposition. + typedef std::map ap_map; + ap_map ap; + typedef std::vector vap_t; + vap_t vap; + + // Assign a number to each acceptance condition. + typedef std::map acc_map; + acc_map acc; + + // Map each state to a number. + typedef Sgi::hash_map state_map; + state_map sm; + // Map each number to its states. + typedef std::vector number_map; + number_map nm; + + std::vector common_acc; + bool state_acc; + bool is_complete; + bool is_deterministic; + + // Label support: the set of all conditions occurring in the + // automaton. + typedef std::map sup_map; + sup_map sup; + + metadata(const tgba* aut) + : state_acc(true), is_complete(true), is_deterministic(true) + { + number_all_acc(aut); + number_all_states_and_fill_sup(aut); + number_all_ap(); + } + + void number_all_acc(const tgba* aut) + { + bdd all_acc = aut->all_acceptance_conditions(); + unsigned count = 0; + while (all_acc != bddfalse) + { + bdd one = bdd_satone(all_acc); + all_acc -= one; + acc[one] = count++; + } + } + + std::ostream& + emit_acc(std::ostream& os, bdd b) + { + // FIXME: We could use a cache for this. + if (b == bddfalse) + return os; + os << " {"; + bool notfirst = false; + while (b != bddfalse) + { + bdd one = bdd_satone(b); + b -= one; + if (notfirst) + os << ' '; + else + notfirst = true; + os << acc[one]; + } + os << '}'; + return os; + } + + void number_all_states_and_fill_sup(const tgba* aut) + { + std::string empty; + + // Scan the whole automaton to number states. + std::deque todo; + + const state* init = aut->get_init_state(); + sm[init] = 0; + nm.push_back(init); + todo.push_back(init); + + while (!todo.empty()) + { + tgba_succ_iterator* i = aut->succ_iter(todo.front()); + todo.pop_front(); + bdd prev = bddtrue; + bool st_acc = true; + bdd sum = bddfalse; + bdd available = bddtrue; + for (i->first(); !i->done(); i->next()) + { + const state* dst = i->current_state(); + bdd cond = i->current_condition(); + if (is_complete) + sum |= cond; + if (is_deterministic) + { + if (!bdd_implies(cond, available)) + is_deterministic = false; + else + available -= cond; + } + sup.insert(std::make_pair(cond, empty)); + if (sm.insert(std::make_pair(dst, nm.size())).second) + { + nm.push_back(dst); + todo.push_back(dst); + } + else + { + dst->destroy(); + } + if (st_acc) + { + bdd acc = i->current_acceptance_conditions(); + if (prev != bddtrue && prev != acc) + st_acc = false; + else + prev = acc; + } + } + if (is_complete) + is_complete &= sum == bddtrue; + + common_acc.push_back(st_acc); + state_acc &= st_acc; + delete i; + } + } + + void number_all_ap() + { + sup_map::iterator i; + bdd all = bddtrue; + for (i = sup.begin(); i != sup.end(); ++i) + all &= bdd_support(i->first); + + while (all != bddtrue) + { + int v = bdd_var(all); + all = bdd_high(all); + ap.insert(std::make_pair(v, vap.size())); + vap.push_back(v); + } + + for (i = sup.begin(); i != sup.end(); ++i) + { + bdd cond = i->first; + if (cond == bddtrue) + { + i->second = "t"; + continue; + } + if (cond == bddfalse) + { + i->second = "f"; + continue; + } + std::ostringstream s; + bool notfirstor = false; + + minato_isop isop(cond); + bdd cube; + while ((cube = isop.next()) != bddfalse) + { + if (notfirstor) + s << " | "; + bool notfirstand = false; + while (cube != bddtrue) + { + if (notfirstand) + s << '&'; + else + notfirstand = true; + bdd h = bdd_high(cube); + if (h == bddfalse) + { + s << '!' << ap[bdd_var(cube)]; + cube = bdd_low(cube); + } + else + { + s << ap[bdd_var(cube)]; + cube = h; + } + } + notfirstor = true; + } + i->second = s.str(); + } + } + + }; + + } + + + std::ostream& + hoaf_reachable(std::ostream& os, + const tgba* aut, + const ltl::formula* f, + hoaf_acceptance acceptance, + hoaf_alias alias, + bool newline) + { + (void) alias; + + metadata md(aut); + + if (acceptance == Hoaf_Acceptance_States + && !md.state_acc) + acceptance = Hoaf_Acceptance_Transitions; + + unsigned num_states = md.nm.size(); + + const char nl = newline ? '\n' : ' '; + os << "HOA: v1" << nl; + if (f) + escape_str(os << "name: \"", to_string(f)) << '"' << nl; + os << "States: " << num_states << nl + << "Start: 0" << nl + << "AP: " << md.vap.size(); + bdd_dict* d = aut->get_dict(); + for (metadata::vap_t::const_iterator i = md.vap.begin(); + i != md.vap.end(); ++i) + escape_str(os << " \"", to_string(d->bdd_map[*i].f)) << '"'; + os << nl; + unsigned num_acc = md.acc.size(); + if (num_acc == 0) + os << "acc-name: all"; + else if (num_acc == 1) + os << "acc-name: Buchi"; + else + os << "acc-name: generalized-Buchi " << num_acc; + os << nl; + os << "Acceptance: " << num_acc; + if (num_acc > 0) + { + os << " I(0"; + for (unsigned i = 1; i < num_acc; ++i) + os << ")&I(" << i; + os << ')'; + } + else + { + os << " t"; + } + os << nl; + os << "properties: trans-labels explicit-labels"; + if (acceptance == Hoaf_Acceptance_States) + os << " state-acc"; + else if (acceptance == Hoaf_Acceptance_Transitions) + os << " trans-acc"; + if (md.is_complete) + os << " complete"; + if (md.is_deterministic) + os << " deterministic"; + os << nl; + os << "--BODY--" << nl; + for (unsigned i = 0; i < num_states; ++i) + { + hoaf_acceptance this_acc = acceptance; + if (this_acc == Hoaf_Acceptance_Mixed) + this_acc = (md.common_acc[i] ? + Hoaf_Acceptance_States : Hoaf_Acceptance_Transitions); + + tgba_succ_iterator* j = aut->succ_iter(md.nm[i]); + j->first(); + + os << "State: " << i; + if (this_acc == Hoaf_Acceptance_States && !j->done()) + md.emit_acc(os, j->current_acceptance_conditions()); + os << nl; + + for (; !j->done(); j->next()) + { + const state* dst = j->current_state(); + os << '[' << md.sup[j->current_condition()] << "] " << md.sm[dst]; + if (this_acc == Hoaf_Acceptance_Transitions) + md.emit_acc(os, j->current_acceptance_conditions()); + os << nl; + dst->destroy(); + } + delete j; + } + os << "--END--"; // No newline. Let the caller decide. + for (unsigned i = 0; i < num_states; ++i) + md.nm[i]->destroy(); + return os; + } + + std::ostream& + hoaf_reachable(std::ostream& os, + const tgba* aut, + const char* opt, + const ltl::formula* f) + { + bool newline = true; + hoaf_acceptance acceptance = Hoaf_Acceptance_States; + hoaf_alias alias = Hoaf_Alias_None; + + if (opt) + while (*opt) + { + switch (*opt++) + { + case 'l': + newline = false; + break; + case 'm': + acceptance = Hoaf_Acceptance_Mixed; + break; + case 's': + acceptance = Hoaf_Acceptance_States; + break; + case 't': + acceptance = Hoaf_Acceptance_Transitions; + break; + } + } + return hoaf_reachable(os, aut, f, acceptance, alias, newline); + } + +} diff --git a/src/tgbaalgos/hoaf.hh b/src/tgbaalgos/hoaf.hh new file mode 100644 index 000000000..4fe83cbc2 --- /dev/null +++ b/src/tgbaalgos/hoaf.hh @@ -0,0 +1,66 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 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_HOAF_HH +# define SPOT_TGBAALGOS_HOAF_HH + +#include +#include "ltlast/formula.hh" + +namespace spot +{ + class tgba; + enum hoaf_alias { Hoaf_Alias_None, Hoaf_Alias_Ap, Hoaf_Alias_Cond }; + enum hoaf_acceptance + { + Hoaf_Acceptance_States, /// state-based acceptance if + /// (globally) possible + /// transition-based acceptance + /// otherwise. + Hoaf_Acceptance_Transitions, /// transition-based acceptance globally + Hoaf_Acceptance_Mixed /// mix state-based and transition-based + }; + + /// \ingroup tgba_io + /// \brief Print reachable states in Hanoi Omega Automata format. + /// + /// \param os The output stream to print on. + /// \param g The automaton to output. + /// \param f The (optional) formula associated to the automaton. If given + /// it will be output as a comment. + /// \parama acceptance Force the type of acceptance mode used + /// in output. + /// \param alias Whether aliases should be used in output. + /// \param newslines Whether to use newlines in output. + SPOT_API std::ostream& + hoaf_reachable(std::ostream& os, + const tgba* g, + const ltl::formula* f = 0, + hoaf_acceptance acceptance = Hoaf_Acceptance_States, + hoaf_alias alias = Hoaf_Alias_None, + bool newlines = true); + + SPOT_API std::ostream& + hoaf_reachable(std::ostream& os, + const tgba* g, + const char* opt, + const ltl::formula* f = 0); +} + +#endif // SPOT_TGBAALGOS_HOAF_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 7ab4c93a0..4f6739d70 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014 +// Laboratoire de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis // Coopératifs (SRC), Université Pierre et Marie Curie. @@ -37,6 +37,7 @@ #include "tgbaalgos/save.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/hoaf.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbasgba.hh" #include "tgbaalgos/degen.hh" @@ -403,6 +404,7 @@ main(int argc, char** argv) bool containment = false; bool show_fc = false; bool spin_comments = false; + const char* hoaf_opt = 0; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; spot::tgba* system_aut = 0; @@ -581,6 +583,11 @@ main(int argc, char** argv) accepting_run = true; graph_run_tgba_opt = true; } + else if (!strncmp(argv[formula_index], "-H", 2)) + { + output = 17; + hoaf_opt = argv[formula_index] + 2; + } else if (!strcmp(argv[formula_index], "-k")) { output = 9; @@ -1883,7 +1890,11 @@ main(int argc, char** argv) } break; } - + case 17: + { + hoaf_reachable(std::cout, a, hoaf_opt, f) << '\n'; + break; + } default: assert(!"unknown output option"); }