diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh index 9791642ff..a8212f9ca 100644 --- a/src/priv/accmap.hh +++ b/src/priv/accmap.hh @@ -28,33 +28,51 @@ namespace spot { - class acc_mapper + class acc_mapper_common { + protected: bdd_dict* dict_; tgba_digraph* aut_; ltl::environment& env_; - std::unordered_map map_; bdd neg_; - public: - acc_mapper(tgba_digraph *aut, - ltl::environment& env = ltl::default_environment::instance()) + acc_mapper_common(tgba_digraph *aut, ltl::environment& env) : dict_(aut->get_dict()), aut_(aut), env_(env), neg_(bddtrue) { } + public: const ltl::environment& get_env() const { return env_; } + // Commit all acceptance set to the automaton. + void commit() + { + aut_->set_acceptance_conditions(neg_); + } + }; + + class acc_mapper_string: public acc_mapper_common + { + std::unordered_map map_; + + public: + acc_mapper_string(tgba_digraph *aut, + ltl::environment& env + = ltl::default_environment::instance()) + : acc_mapper_common(aut, env) + { + } + // Declare an acceptance name. bool declare(const std::string& name) { auto i = map_.find(name); if (i != map_.end()) return true; - const ltl::formula* f = env_.require(name); + auto f = env_.require(name); if (!f) return false; int v = dict_->register_acceptance_variable(f, aut_); @@ -64,12 +82,6 @@ namespace spot return true; } - // Commit all acceptance set to the automaton. - void commit() - { - aut_->set_acceptance_conditions(neg_); - } - std::pair lookup(std::string name) const { auto p = map_.find(name); @@ -79,7 +91,54 @@ namespace spot bdd_nithvar(p->second), p->second)); } + }; + // The acceptance sets are named using count integers, but we do not + // assume the numbers are necessarily consecutive. + class acc_mapper_int: public acc_mapper_common + { + std::vector usable_; + unsigned used_; + std::map map_; + + public: + acc_mapper_int(tgba_digraph *aut, + unsigned count, + ltl::environment& env = ltl::default_environment::instance()) + : acc_mapper_common(aut, env), usable_(count), used_(0) + { + std::vector vmap(count); + for (unsigned n = 0; n < count; ++n) + { + std::ostringstream s; + s << n; + auto f = env.require(s.str()); + int v = dict_->register_acceptance_variable(f, aut_); + f->destroy(); + vmap[n] = v; + neg_ &= bdd_nithvar(v); + } + for (unsigned n = 0; n < count; ++n) + { + int v = vmap[n]; + usable_[n] = bdd_compose(neg_, bdd_nithvar(v), v); + } + commit(); + } + + std::pair lookup(unsigned n) + { + auto p = map_.find(n); + if (p != map_.end()) + return std::make_pair(true, p->second); + if (used_ < usable_.size()) + { + bdd res = usable_[used_++]; + map_[n] = res; + return std::make_pair(true, res); + } + return std::make_pair(false, bddfalse); + } }; } diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 2b5f64e49..67844b2d4 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -24,10 +24,12 @@ #include #include #include -#include +#include #include "tgba/tgbaexplicit.hh" +#include "tgba/formula2bdd.hh" #include "reachiter.hh" #include "misc/bddlt.hh" +#include "priv/accmap.hh" #include "ltlvisit/lbt.hh" #include "ltlparse/public.hh" @@ -166,8 +168,142 @@ namespace spot const sba* sba_; }; + static + const tgba_digraph* + lbtt_read_tgba(unsigned num_states, unsigned num_acc, + std::istream& is, std::string& error, + bdd_dict* dict, + ltl::environment& env, ltl::environment& envacc) + { + auto aut = std::unique_ptr(new tgba_digraph(dict)); + acc_mapper_int acc_b(aut.get(), num_acc, envacc); + auto& g = aut->get_graph(); + g.new_states(num_states); + + 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; + auto p = acc_b.lookup(acc_n); + if (p.first) + { + acc |= p.second; + } + else + { + error += "more acceptance sets used than declared"; + return nullptr; + } + } + + std::string guard; + std::getline(is, guard); + ltl::parse_error_list pel; + const ltl::formula* f = parse_lbt(guard, pel, env); + if (!f || !pel.empty()) + { + error += "failed to parse guard: " + guard; + if (f) + f->destroy(); + return nullptr; + } + bdd cond = formula_to_bdd(f, dict, aut.get()); + f->destroy(); + g.new_transition(src_state, dst_state, cond, acc); + } + } + return aut.release(); + } + + const tgba_digraph* + lbtt_read_gba(unsigned num_states, unsigned num_acc, + std::istream& is, std::string& error, + bdd_dict* dict, + ltl::environment& env, ltl::environment& envacc) + { + auto aut = std::unique_ptr(new tgba_digraph(dict)); + acc_mapper_int acc_b(aut.get(), num_acc, envacc); + auto& g = aut->get_graph(); + g.new_states(num_states); + + 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 acceptance conditions. + bdd acc = bddfalse; + for (;;) + { + int acc_n = 0; + is >> acc_n; + if (acc_n == -1) + break; + auto p = acc_b.lookup(acc_n); + if (p.first) + { + acc |= p.second; + } + else + { + error += "more acceptance sets used than declared"; + return nullptr; + } + } + + // Read the transitions. + for (;;) + { + int dst_state = 0; + is >> dst_state; + if (dst_state == -1) + break; + + std::string guard; + std::getline(is, guard); + ltl::parse_error_list pel; + const ltl::formula* f = parse_lbt(guard, pel, env); + if (!f || !pel.empty()) + { + error += "failed to parse guard: " + guard; + if (f) + f->destroy(); + return nullptr; + } + bdd cond = formula_to_bdd(f, dict, aut.get()); + f->destroy(); + g.new_transition(src_state, dst_state, cond, acc); + } + } + return aut.release(); + } + } // anonymous + std::ostream& lbtt_reachable(std::ostream& os, const tgba* g, bool sba) { @@ -176,173 +312,8 @@ namespace spot 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::map acc_b; - 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; - std::map::const_iterator i = acc_b.find(acc_n); - if (i != acc_b.end()) - { - acc |= i->second; - } - else - { - size_t s = acc_b.size(); - if (s >= num_acc) - { - error += "more acceptance sets used than declared"; - goto fail; - } - bdd a = aut->get_acceptance_condition(acc_f[s]); - acc_b[acc_n] = a; - acc |= a; - } - } - - std::string guard; - std::getline(is, guard); - ltl::parse_error_list pel; - const ltl::formula* f = parse_lbt(guard, pel, env); - if (!f || !pel.empty()) - { - 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_read_gba(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::map acc_b; - - 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 acceptance conditions. - bdd acc = bddfalse; - for (;;) - { - int acc_n = 0; - is >> acc_n; - if (acc_n == -1) - break; - std::map::const_iterator i = acc_b.find(acc_n); - if (i != acc_b.end()) - { - acc |= i->second; - } - else - { - size_t s = acc_b.size(); - if (s >= num_acc) - { - error += "more acceptance sets used than declared"; - goto fail; - } - bdd a = aut->get_acceptance_condition(acc_f[s]); - acc_b[acc_n] = a; - acc |= a; - } - } - - // Read the transitions. - for (;;) - { - int dst_state = 0; - is >> dst_state; - if (dst_state == -1) - break; - - std::string guard; - std::getline(is, guard); - ltl::parse_error_list pel; - const ltl::formula* f = parse_lbt(guard, pel, env); - if (!f || !pel.empty()) - { - 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* + const tgba_digraph* lbtt_parse(std::istream& is, std::string& error, bdd_dict* dict, ltl::environment& env, ltl::environment& envacc) { @@ -361,7 +332,7 @@ namespace spot { std::string header; std::getline(is, header); - return new sba_explicit_number(dict); + return new tgba_digraph(dict); } unsigned num_acc = 0; @@ -378,6 +349,5 @@ namespace spot else return lbtt_read_gba(num_states, num_acc, is, error, dict, env, envacc); - return 0; } } diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index af5dd0b7e..fe8e3a3a6 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de +// Copyright (C) 2012, 2013, 2014 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 @@ -23,7 +23,7 @@ #ifndef SPOT_TGBAALGOS_LBTT_HH # define SPOT_TGBAALGOS_LBTT_HH -#include "tgba/tgba.hh" +#include "tgba/tgbagraph.hh" #include #include "ltlenv/defaultenv.hh" @@ -51,7 +51,7 @@ namespace spot /// \param envacc The environment of acceptance conditions into which parsing /// should take place. /// \return the read tgba or 0 on error. - SPOT_API const tgba* + SPOT_API const tgba_digraph* lbtt_parse(std::istream& is, std::string& error, bdd_dict* dict, ltl::environment& env = ltl::default_environment::instance(), diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 2459fde6c..b284ec157 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -45,7 +45,7 @@ %parse-param {spot::tgba_parse_error_list& error_list} %parse-param {spot::ltl::environment& parse_environment} -%parse-param {spot::acc_mapper& acc_map} +%parse-param {spot::acc_mapper_string& acc_map} %parse-param {spot::tgba_digraph*& result} %parse-param {named_tgba_t*& namer} %parse-param {formula_cache& fcache} @@ -233,7 +233,7 @@ namespace spot formula_cache fcache; tgba_digraph* result = new tgba_digraph(dict); auto namer = result->create_namer(); - spot::acc_mapper acc_map(result, envacc); + spot::acc_mapper_string acc_map(result, envacc); tgbayy::parser parser(error_list, env, acc_map, result, namer, fcache); parser.set_debug_level(debug); parser.parse(); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index a532adafe..ba84bc276 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1144,8 +1144,9 @@ main(int argc, char** argv) } tm.start("parsing lbtt"); to_free = a = - const_cast(spot::lbtt_parse(*in, error, dict, - env, env)); + const_cast(spot::lbtt_parse(*in, + error, dict, + env, env)); tm.stop("parsing lbtt"); delete f; if (!to_free)