diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 077921c70..fee74e9a0 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -597,8 +597,6 @@ namespace spot all_acceptance_conditions_computed_ = false; } - protected: - bdd get_acceptance_condition(const ltl::formula* f) { bdd_dict::fv_map::iterator i = this->dict_->acc_map.find(f); @@ -609,6 +607,8 @@ namespace spot return v; } + protected: + virtual bdd compute_support_conditions(const spot::state* in) const { const State* s = down_cast(in); diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 88849b482..5d6af97cf 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -25,8 +26,10 @@ #include #include #include "tgba/bddprint.hh" +#include "tgba/tgbaexplicit.hh" #include "reachiter.hh" #include "misc/bddlt.hh" +#include "ltlparse/public.hh" namespace spot { @@ -150,4 +153,111 @@ namespace spot b.run(); return os; } + + const tgba* + lbtt_read_tgba(unsigned num_states, unsigned num_acc, + std::istream& is, std::string& error, + bdd_dict* dict, + ltl::environment& env, ltl::environment& envacc) + { + tgba_explicit_number* aut = new tgba_explicit_number(dict); + std::vector acc_f(num_acc); + for (unsigned n = 0; n < num_acc; ++n) + { + std::ostringstream s; + s << n; + const ltl::formula* af = acc_f[n] = envacc.require(s.str()); + aut->declare_acceptance_condition(af->clone()); + } + std::vector acc_b(num_acc); + for (unsigned n = 0; n < num_acc; ++n) + acc_b[n] = aut->get_acceptance_condition(acc_f[n]); + + for (unsigned n = 0; n < num_states; ++n) + { + int src_state = 0; + int initial = 0; + is >> src_state >> initial; + if (initial) + aut->set_init_state(src_state); + + // Read the transitions. + for (;;) + { + int dst_state = 0; + is >> dst_state; + if (dst_state == -1) + break; + + // Read the acceptance conditions. + bdd acc = bddfalse; + for (;;) + { + int acc_n = 0; + is >> acc_n; + if (acc_n == -1) + break; + if (acc_n < 0 || (unsigned)acc_n >= num_acc) + { + error += "invalid acceptance set"; + goto fail; + } + acc |= acc_b[acc_n]; + } + std::string guard; + std::getline(is, guard); + ltl::parse_error_list pel; + const ltl::formula* f = parse_lbt(guard, pel, env); + if (!f || pel.size() > 0) + { + error += "failed to parse guard: " + guard; + if (f) + f->destroy(); + goto fail; + } + state_explicit_number::transition* t + = aut->create_transition(src_state, dst_state); + aut->add_condition(t, f); + t->acceptance_conditions |= acc; + } + } + return aut; + fail: + delete aut; + return 0; + } + + const tgba* + lbtt_parse(std::istream& is, std::string& error, bdd_dict* dict, + ltl::environment& env, ltl::environment& envacc) + { + is >> std::skipws; + + unsigned num_states = 0; + is >> num_states; + if (!is) + { + error += "failed to read the number of states"; + return 0; + } + + // No states? Read the rest of the line and return an empty automaton. + if (num_states == 0) + { + std::string header; + std::getline(is, header); + return new sba_explicit_number(dict); + } + + unsigned num_acc = 0; + is >> num_acc; + std::string rest; + std::getline(is, rest); + if (rest[0] == 't' || rest[0] == 'T') + return lbtt_read_tgba(num_states, num_acc, is, error, dict, + env, envacc); + else + assert(!"unsupported format"); + return 0; + } } diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index b38125567..a206a3c1b 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -22,6 +25,7 @@ #include "tgba/tgba.hh" #include +#include "ltlenv/defaultenv.hh" namespace spot { @@ -31,6 +35,24 @@ namespace spot /// \param g The automata to print. /// \param os Where to print. std::ostream& lbtt_reachable(std::ostream& os, const tgba* g); + + + /// \brief Read an automaton in LBTT's format + /// \ingroup tgba_io + /// + /// \param is The stream on which the automaton should be input. + /// \param error A string in which to write any error message. + /// \param env The environment of atomic proposition into which parsing + /// should take place. + /// \param envacc The environment of acceptance conditions into which parsing + /// should take place. + /// \return the read tgba or 0 on error. + const tgba* lbtt_parse(std::istream& is, std::string& error, + bdd_dict* dict, + ltl::environment& env + = ltl::default_environment::instance(), + ltl::environment& envacc + = ltl::default_environment::instance()); } #endif // SPOT_TGBAALGOS_LBTT_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index c5c3356c5..22fbe1c75 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -93,6 +93,7 @@ TESTS = \ degendet.test \ degenid.test \ kv.test \ + lbttparse.test \ scc.test \ sccsimpl.test \ obligation.test \ diff --git a/src/tgbatest/lbttparse.test b/src/tgbatest/lbttparse.test new file mode 100755 index 000000000..25a1eba3d --- /dev/null +++ b/src/tgbatest/lbttparse.test @@ -0,0 +1,41 @@ +#!/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 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 . + +. ./defs + +set -e + +for f in 'p0 U p1 U p2' 'Gp00 | Gp13 | Gp42' '{(1;1)*}[]->p1' +do + # Make sure Spot can read the LBTT it produces + run 0 ../ltl2tgba -t "$f" > out + s=`wc -l < out` + run 0 ../ltl2tgba -t -XL out > out2 + s2=`wc -l < out2` + test "$s" -eq "$s2" + + # The LBTT output use 2 lines par state, one line per transition, + # and one extra line for header. + run 0 ../ltl2tgba -ks "$f" > size + st=`cat size | sed -n 's/states: //p'` + tr=`cat size | sed -n 's/transitions: //p'` + l=`expr $st \* 2 + $tr + 1` + test "$s" -eq "$l" +done diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index c93a4a532..934b20602 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -118,6 +118,8 @@ syntax(char* prog) << std::endl << " -X do not compute an automaton, read it from a file" << std::endl + << " -XL do not compute an automaton, read it from an" + << " LBTT file" << std::endl << " -XN do not compute an automaton, read it from a" << " neverclaim file" << std::endl << " -Pfile multiply the formula automaton with the TGBA read" @@ -334,6 +336,7 @@ main(int argc, char** argv) bool accepting_run_replay = false; bool from_file = false; bool read_neverclaim = false; + bool read_lbtt = false; bool scc_filter = false; bool simpltl = false; spot::ltl::ltl_simplifier_options redopt(false, false, false, false, @@ -782,6 +785,11 @@ main(int argc, char** argv) from_file = true; read_neverclaim = true; } + else if (!strcmp(argv[formula_index], "-XL")) + { + from_file = true; + read_lbtt = true; + } else if (!strcmp(argv[formula_index], "-y")) { translation = TransFM; @@ -887,8 +895,8 @@ main(int argc, char** argv) if (from_file) { - spot::tgba_explicit_string* e; - if (!read_neverclaim) + spot::tgba_explicit_string* e = 0; + if (!read_neverclaim && !read_lbtt) { spot::tgba_parse_error_list pel; tm.start("parsing automaton"); @@ -902,7 +910,7 @@ main(int argc, char** argv) return 2; } } - else + else if (read_neverclaim) { spot::neverclaim_parse_error_list pel; tm.start("parsing neverclaim"); @@ -917,7 +925,30 @@ main(int argc, char** argv) } assume_sba = true; } - e->merge_transitions(); + else + { + std::string error; + std::fstream f(input.c_str()); + if (!f) + { + std::cerr << "cannot open " << input << std::endl; + delete dict; + return 2; + } + tm.start("parsing lbtt"); + to_free = a = + const_cast(spot::lbtt_parse(f, error, dict, + env, env)); + tm.stop("parsing lbtt"); + if (!to_free) + { + std::cerr << error << std::endl; + delete dict; + return 2; + } + } + if (e) + e->merge_transitions(); } else {