diff --git a/python/spot/impl.i b/python/spot/impl.i index 6affd03f8..d723a70f1 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -761,6 +761,11 @@ def state_is_accepting(self, src) -> "bool": return self->new_univ_edge(src, v.begin(), v.end(), cond, acc); } + void set_univ_init_state(const std::vector& v) + { + self->set_univ_init_state(v.begin(), v.end()); + } + void report_univ_dest(unsigned src) { if (self->is_univ_dest(src)) diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 88a3b7feb..d5940028e 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -766,6 +766,27 @@ namespace spot return t; } + /// \brief Create a new universal destination group + /// + /// The resulting state number can be used as the destination of + /// an edge. + /// + /// \param dst_begin start of a non-empty container of destination states + /// \param dst_end end of a non-empty container of destination states + template + state + new_univ_dests(I dst_begin, I dst_end) + { + unsigned sz = std::distance(dst_begin, dst_end); + if (sz == 1) + return *dst_begin; + SPOT_ASSERT(sz > 1); + unsigned d = dests_.size(); + dests_.emplace_back(sz); + dests_.insert(dests_.end(), dst_begin, dst_end); + return ~d; + } + /// \brief Create a new universal edge /// /// \param src the source state @@ -776,14 +797,8 @@ namespace spot edge new_univ_edge(state src, I dst_begin, I dst_end, Args&&... args) { - unsigned sz = std::distance(dst_begin, dst_end); - if (sz == 1) - return new_edge(src, *dst_begin, std::forward(args)...); - SPOT_ASSERT(sz > 1); - unsigned d = dests_.size(); - dests_.emplace_back(sz); - dests_.insert(dests_.end(), dst_begin, dst_end); - return new_edge(src, ~d, std::forward(args)...); + return new_edge(src, new_univ_dests(dst_begin, dst_end), + std::forward(args)...); } /// \brief Create a new universal edge diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 1db58e981..8b6e64ebc 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -95,7 +95,8 @@ extern "C" int strverscmp(const char *s1, const char *s2); std::vector::const_iterator cur_guard; map_t dest_map; std::vector info_states; // States declared and used. - std::vector> start; // Initial states; + std::vector>> start; // Initial states; std::unordered_map alias; struct prop_info { @@ -239,7 +240,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); %left '&' %nonassoc '!' -%type state-conj-2 state-conj-checked +%type init-state-conj-2 state-conj-2 state-conj-checked %type checked-state-num state-num acc-set sign %type label-expr %type acc-sig acc-sets trans-acc_opt state-acc_opt @@ -348,13 +349,14 @@ header: format-version header-items { unsigned states = res.states; for (auto& p : res.start) - if ((unsigned) res.states <= p.second) - { - error(p.first, - "initial state number is larger than state count..."); - error(res.states_loc, "... declared here."); - states = std::max(states, p.second + 1); - } + for (unsigned s: p.second) + if ((unsigned) res.states <= s) + { + error(p.first, "initial state number is larger " + "than state count..."); + error(res.states_loc, "... declared here."); + states = std::max(states, s + 1); + } if (res.opts.want_kripke) res.h->ks->new_states(states, bddfalse); else @@ -631,12 +633,12 @@ header-item: "States:" INT } | "Start:" init-state-conj-2 { - error(@2, "alternation is not yet supported for initial states"); - YYABORT; + res.start.emplace_back(@$, *$2); + delete $2; } | "Start:" state-num { - res.start.emplace_back(@$, $2); + res.start.emplace_back(@$, std::vector{$2}); } | aps | "Alias:" ANAME label-expr @@ -819,10 +821,17 @@ state-conj-2: checked-state-num '&' checked-state-num $$->emplace_back($3); } - // Currently we do not check the number of these states - // since we do not support alternation for initial states. +// Same as state-conj-2 except we cannot check the state numbers +// against a number of state that may not have been declared yet. init-state-conj-2: state-num '&' state-num + { + $$ = new std::vector{$1, $3}; + } | init-state-conj-2 '&' state-num + { + $$ = $1; + $$->emplace_back($3); + } label-expr: 't' { @@ -983,17 +992,16 @@ acceptance-cond: IDENTIFIER '(' acc-set ')' body: states { for (auto& p: res.start) - if (p.second >= res.info_states.size() - || !res.info_states[p.second].declared) - { - error(p.first, - "initial state " + std::to_string(p.second) + - " has no definition"); - // Pretend that the state is declared so we do not - // mention it in the next loop. - if (p.second < res.info_states.size()) - res.info_states[p.second].declared = true; - } + for (unsigned s: p.second) + if (s >= res.info_states.size() || !res.info_states[s].declared) + { + error(p.first, "initial state " + std::to_string(s) + + " has no definition"); + // Pretend that the state is declared so we do not + // mention it in the next loop. + if (s < res.info_states.size()) + res.info_states[s].declared = true; + } unsigned n = res.info_states.size(); // States with number above res.states have already caused a // diagnostic, so let not add another one. @@ -1498,7 +1506,7 @@ dstar_sizes: } | dstar_sizes "Start:" INT { - res.start.emplace_back(@3, $3); + res.start.emplace_back(@3, std::vector{$3}); } | dstar_sizes aps @@ -1654,7 +1662,7 @@ nc-ident-list: nc-one-ident if (res.start.empty()) { // The first state is initial. - res.start.emplace_back(@$, n); + res.start.emplace_back(@$, std::vector{n}); } $$ = $1; } @@ -1843,7 +1851,7 @@ lbtt: lbtt-header lbtt-body ENDAUT rename[i.second] = s++; assert(s == (unsigned) res.states); for (auto& i: res.start) - i.second = rename[i.second]; + i.second.front() = rename[i.second.front()]; res.h->aut->get_graph().defrag_states(std::move(rename), s); } res.info_states.resize(res.h->aut->num_states()); @@ -1899,7 +1907,8 @@ lbtt-state: STATE_NUM INT lbtt-acc res.cur_state = $1; } if ($2) - res.start.emplace_back(@1 + @2, res.cur_state); + res.start.emplace_back(@1 + @2, + std::vector{res.cur_state}); res.acc_state = $3; } lbtt-acc: { $$ = 0U; } @@ -2121,13 +2130,20 @@ static void fix_acceptance(result_& r) static void fix_initial_state(result_& r) { - std::vector start; + std::vector> start; start.reserve(r.start.size()); + unsigned ssz = r.info_states.size(); for (auto& p : r.start) - // Ignore initial states without declaration - if (p.second < r.info_states.size() - && r.info_states[p.second].declared) - start.push_back(p.second); + { + std::vector v; + v.reserve(p.second.size()); + for (unsigned s: p.second) + // Ignore initial states without declaration + if (s < ssz && r.info_states[s].declared) + v.emplace_back(s); + if (!v.empty()) + start.push_back(v); + } if (start.empty()) { @@ -2149,9 +2165,10 @@ static void fix_initial_state(result_& r) if (start.size() == 1) { if (r.opts.want_kripke) - r.h->ks->set_init_state(start.front()); + r.h->ks->set_init_state(start.front().front()); else - r.h->aut->set_init_state(start.front()); + r.h->aut->set_univ_init_state(start.front().begin(), + start.front().end()); } else { @@ -2167,24 +2184,38 @@ static void fix_initial_state(result_& r) auto& aut = r.h->aut; std::vector has_incoming(aut->num_states(), 0); for (auto& t: aut->edges()) - has_incoming[t.dst] = 1; + for (unsigned ud: aut->univ_dests(t)) + has_incoming[ud] = 1; bool found = false; unsigned init = 0; - for (auto p: start) - if (!has_incoming[p]) - { - init = p; - found = true; - } + for (auto& pp: start) + { + if (pp.size() != 1) + { + r.h->errors.emplace_front(r.start.front().first, + "alternating automata only support " + "a single initial state"); + return; + } + unsigned p = pp.front(); + if (!has_incoming[p]) + { + init = p; + found = true; + } + } if (!found) // We do need a fake initial state init = aut->new_state(); aut->set_init_state(init); - for (auto p: start) - if (p != init) - for (auto& t: aut->out(p)) - aut->new_edge(init, t.dst, t.cond); + for (auto& pp: start) + { + unsigned p = pp.front(); + if (p != init) + for (auto& t: aut->out(p)) + aut->new_edge(init, t.dst, t.cond); + } } } diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index c1963ca56..b4960939c 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -268,6 +268,23 @@ namespace spot set_init_state(state_number(s)); } + template + void set_univ_init_state(I dst_begin, I dst_end) + { + auto ns = num_states(); + for (I i = dst_begin; i != dst_end; ++i) + if (SPOT_UNLIKELY(*i >= ns)) + throw std::invalid_argument + ("set_univ_init_state() called with nonexisiting state"); + init_number_ = g_.new_univ_dests(dst_begin, dst_end); + } + + template + void set_univ_init_state(const std::initializer_list& il) + { + set_univ_init_state(il.begin(), il.end()); + } + state_num get_init_state_number() const { // If the automaton has no state, it has no initial state. diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 0cd3c8f23..15ee5bd08 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -360,6 +360,19 @@ namespace spot return bdd_format_formula(aut_->get_dict(), label); } + void + print_dst(int dst, const char* style = nullptr) + { + os_ << " " << dst << " [label=<>,width=0,height=0,shape=none]\n"; + for (unsigned d: aut_->univ_dests(dst)) + { + os_ << " " << dst << " -> " << d; + if (style && *style) + os_ << " [" << style << ']'; + os_ << '\n'; + } + } + void start() { @@ -444,7 +457,17 @@ namespace spot os_ << " " << extra << '\n'; os_ << " I [label=\"\", style=invis, "; os_ << (opt_vertical_ ? "height" : "width"); - os_ << "=0]\n I -> " << aut_->get_init_state_number() << '\n'; + int init = (int) aut_->get_init_state_number(); + os_ << "=0]\n I -> " << init; + if (init >= 0) + { + os_ << '\n'; + } + else + { + os_ << " [dir=none]\n"; + print_dst(init); + } } void @@ -608,17 +631,7 @@ namespace spot os_ << ", dir=none"; os_ << "]\n"; if ((int)t.dst < 0) // Universal destination - { - os_ << " " << (int)t.dst - << "[label=<>,width=0,height=0,shape=none]\n"; - for (unsigned d: aut_->univ_dests(t)) - { - os_ << " " << (int)t.dst << " -> " << d; - if (!highlight.empty()) - os_ << " [" << highlight << ']'; - os_ << '\n'; - } - } + print_dst(t.dst, highlight.c_str()); } void print(const const_twa_graph_ptr& aut) diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 1bd1a332f..49f984e17 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -317,6 +317,19 @@ namespace spot if (acceptance == Hoa_Acceptance_States && !md.has_state_acc) acceptance = Hoa_Acceptance_Transitions; + auto print_dst = [&os, &aut](unsigned dst) + { + bool notfirst = false; + for (unsigned d: aut->univ_dests(dst)) + { + if (notfirst) + os << '&'; + else + notfirst = true; + os << d; + } + }; + unsigned num_states = aut->num_states(); unsigned init = aut->get_init_state_number(); @@ -327,7 +340,9 @@ namespace spot escape_str(os << "name: \"", *n) << '"' << nl; unsigned nap = md.vap.size(); os << "States: " << num_states << nl - << "Start: " << init << nl + << "Start: "; + print_dst(init); + os << nl << "AP: " << nap; auto d = aut->get_dict(); for (auto& i: md.vap) @@ -548,19 +563,6 @@ namespace spot os << "--BODY--" << nl; - auto print_dst = [&](unsigned dst) - { - bool notfirst = false; - for (unsigned d: aut->univ_dests(dst)) - { - if (notfirst) - os << '&'; - else - notfirst = true; - os << d; - } - }; - auto sn = aut->get_named_prop>("state-names"); for (unsigned i = 0; i < num_states; ++i) { diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 49d55afe3..718f77351 100644 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -24,7 +24,7 @@ set -e cat >alt.hoa < 0 + I -> -11 [dir=none] + -11 [label=<>,width=0,height=0,shape=none] + -11 -> 0 + -11 -> 2 0 [label="((((a) U (b)) && GF(b)) && FG(a))"] 0 -> -1 [label="b", dir=none] - -1[label=<>,width=0,height=0,shape=none] + -1 [label=<>,width=0,height=0,shape=none] -1 -> 3 -1 -> 1 0 -> -4 [label="a & !b", style=bold, color="#F15854", dir=none] - -4[label=<>,width=0,height=0,shape=none] + -4 [label=<>,width=0,height=0,shape=none] -4 -> 5 [style=bold, color="#F15854"] -4 -> 3 [style=bold, color="#F15854"] -4 -> 1 [style=bold, color="#F15854"] @@ -81,7 +84,7 @@ digraph G { 3 [label="GF(b)"] 3 -> 3 [label="b"] 3 -> -8 [label="!b", style=bold, color="#FAA43A", dir=none] - -8[label=<>,width=0,height=0,shape=none] + -8 [label=<>,width=0,height=0,shape=none] -8 -> 4 [style=bold, color="#FAA43A"] -8 -> 3 [style=bold, color="#FAA43A"] 4 [label="F(b)\n⓿"] diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index a0abda2dc..fb17a50b9 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1921,8 +1921,7 @@ State: 11 "t" EOF expecterr input <