From ed94a35bea5b7c337a1d7891dc66f77ed3662e34 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 5 Aug 2014 10:49:03 +0200 Subject: [PATCH] dstarparse: Build a tgba_digraph instead of tgba_explicit_number. * src/dstarparse/dstarparse.yy, src/dstarparse/public.hh: Adjust the parser to build a tgba_digraph. * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc: Temporarily adjust these functions to the new type until they are rewritten. --- src/dstarparse/dra2ba.cc | 11 ++++++----- src/dstarparse/dstarparse.yy | 17 ++++++++--------- src/dstarparse/nra2nba.cc | 5 +++-- src/dstarparse/nsa2tgba.cc | 9 +++++---- src/dstarparse/public.hh | 6 +++--- 5 files changed, 25 insertions(+), 23 deletions(-) diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index 43d41faa3..504f065fb 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -19,6 +19,7 @@ #include "public.hh" #include "tgba/tgbamask.hh" +#include "tgba/tgbaexplicit.hh" #include "tgbaalgos/scc.hh" #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/gtec/gtec.hh" @@ -121,12 +122,12 @@ namespace spot // u=[u₁,u₂,...] be bitvectors where bit lᵢ (resp. uᵢ) // indicates that Lᵢ (resp. Uᵢ) has been visited in the SCC. state_list::const_iterator it = sl.begin(); - int num = dra->aut->get_label(*it++); + int num = dra->aut->state_number(*it++); bitvect* l = dra->accsets->at(num * 2).clone(); bitvect* u = dra->accsets->at(num * 2 + 1).clone(); for (; it != sl.end(); ++it) { - num = dra->aut->get_label(*it); + num = dra->aut->state_number(*it); *l |= dra->accsets->at(num * 2); *u |= dra->accsets->at(num * 2 + 1); } @@ -177,7 +178,7 @@ namespace spot state_set unknown; for (it = sl.begin(); it != sl.end(); ++it) { - num = dra->aut->get_label(*it); + num = dra->aut->state_number(*it); bitvect* l2 = dra->accsets->at(num * 2).clone(); *l2 &= *l; if (!l2->is_fully_clear()) @@ -258,8 +259,8 @@ namespace spot const state* sout, int, const tgba_succ_iterator* si) { - int in = in_->aut->get_label(sin); - int out = in_->aut->get_label(sout); + int in = in_->aut->state_number(sin); + int out = in_->aut->state_number(sout); unsigned in_scc = sm_.scc_of_state(sin); typedef state_explicit_number::transition trans; diff --git a/src/dstarparse/dstarparse.yy b/src/dstarparse/dstarparse.yy index c0285d0cb..dded9fdf9 100644 --- a/src/dstarparse/dstarparse.yy +++ b/src/dstarparse/dstarparse.yy @@ -45,7 +45,8 @@ map_t dest_map; int cur_state; - unsigned state_count; + unsigned state_count = 0; + unsigned start_state = 0; std::vector aps; bool state_count_seen:1; @@ -53,7 +54,7 @@ bool start_state_seen:1; bool aps_seen:1; - result_() : + result_(): state_count_seen(false), accpair_count_seen(false), start_state_seen(false), @@ -146,6 +147,8 @@ header: auttype opt_eols V2 opt_eols EXPLICIT opt_eols sizes result.d->aut = 0; YYABORT; } + result.d->aut->new_states(result.state_count);; + result.d->aut->set_init_state(result.start_state); fill_guards(result); } @@ -173,7 +176,7 @@ sizes: } | sizes START opt_eols NUMBER opt_eols { - result.d->aut->set_init_state($4); + result.start_state = $4; result.start_state_seen = true; } | sizes AP opt_eols NUMBER opt_eols aps @@ -270,11 +273,7 @@ states: { for (map_t::const_iterator i = result.dest_map.begin(); i != result.dest_map.end(); ++i) - { - spot::tgba_explicit_number::transition* t = - result.d->aut->create_transition(result.cur_state, i->first); - t->condition = i->second; - } + result.d->aut->new_transition(result.cur_state, i->first, i->second); } %% @@ -329,7 +328,7 @@ namespace spot } result_ r; r.d = new dstar_aut; - r.d->aut = new tgba_explicit_number(dict); + r.d->aut = new tgba_digraph(dict); r.d->accsets = 0; r.env = &env; dstaryy::parser parser(error_list, r); diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index 06ef6cdd0..e7ae0c410 100644 --- a/src/dstarparse/nra2nba.cc +++ b/src/dstarparse/nra2nba.cc @@ -21,6 +21,7 @@ #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/sccfilter.hh" #include "ltlast/constant.hh" +#include "tgba/tgbaexplicit.hh" namespace spot { @@ -67,8 +68,8 @@ namespace spot const state* sout, int, const tgba_succ_iterator* si) { - int in = d_->aut->get_label(sin); - int out = d_->aut->get_label(sout); + int in = d_->aut->state_number(sin); + int out = d_->aut->state_number(sout); typedef state_explicit_number::transition trans; trans* t = out_->create_transition(in, out); diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc index 003a781e2..80ebdd678 100644 --- a/src/dstarparse/nsa2tgba.cc +++ b/src/dstarparse/nsa2tgba.cc @@ -22,6 +22,7 @@ #include "public.hh" #include "tgbaalgos/sccfilter.hh" #include "ltlenv/defaultenv.hh" +#include "tgba/tgbaexplicit.hh" namespace spot { @@ -99,9 +100,9 @@ namespace spot } - int label(const tgba_explicit_number* aut, state* s) + int label(const tgba_digraph* aut, state* s) { - int label = aut->get_label(s); + int label = aut->state_number(s); s->destroy(); return label; } @@ -110,7 +111,7 @@ namespace spot tgba* nsa_to_tgba(const dstar_aut* nsa) { assert(nsa->type == Streett); - tgba_explicit_number* a = nsa->aut; + tgba_digraph* a = nsa->aut; bdd_dict* dict = a->get_dict(); tgba_explicit_number* res = new tgba_explicit_number(dict); @@ -154,7 +155,7 @@ namespace spot todo.pop_front(); int src = bs2num[s]; - for (auto i: a->succ(a->get_state(s.s))) + for (auto i: a->succ(a->state_from_number(s.s))) { int dlabel = label(a, i->current_state()); diff --git a/src/dstarparse/public.hh b/src/dstarparse/public.hh index 4b4a41245..749217a88 100644 --- a/src/dstarparse/public.hh +++ b/src/dstarparse/public.hh @@ -20,7 +20,7 @@ #ifndef SPOT_DSTARPARSE_PUBLIC_HH # define SPOT_DSTARPARSE_PUBLIC_HH -# include "tgba/tgbaexplicit.hh" +# include "tgba/tgbagraph.hh" # include "misc/location.hh" # include "ltlenv/defaultenv.hh" # include @@ -47,7 +47,7 @@ namespace spot { // Transition structure of the automaton. // This is encoded as a TGBA without acceptance condition. - tgba_explicit_number* aut; + tgba_digraph* aut; /// Type of the acceptance. dstar_type type; /// Number of acceptance pairs. @@ -68,7 +68,7 @@ namespace spot }; - /// \brief Build a spot::tgba_explicit from ltl2dstar's output. + /// \brief Build a spot::tgba_digraph from ltl2dstar's output. /// \param filename The name of the file to parse. /// \param error_list A list that will be filled with /// parse errors that occured during parsing.