alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twa_graph: add support for universal initial states

Browse source 
The only missing point is that the HOA parser cannot deal with multiple
universal initial states, as seen in parseaut.test.

* spot/graph/graph.hh (new_univ_dests): New function, extracted from...
(new_univ_edge): ... this one.
* spot/twa/twagraph.hh (set_univ_init_state): Implement using
new_univ_dests.
* spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc, python/spot/impl.i:
Add support for universal initial states.
* spot/parseaut/parseaut.yy: Add preliminary support for
universal initial states.  Multiple universal initial states
are still not supported.
* tests/core/alternating.test, tests/core/parseaut.test,
tests/python/alternating.py: Adjust tests and exercise this new feature.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-30 14:22:44 +01:00
parent d5c9c34514
commit 48c812a595
9 changed files with 193 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

5
python/spot/impl.i
View file

@ -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<unsigned>& v)
{
self->set_univ_init_state(v.begin(), v.end());
}
void report_univ_dest(unsigned src)
{
if (self->is_univ_dest(src))

31
spot/graph/graph.hh
View file

@ -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 <typename I>
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>(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>(args)...);
return new_edge(src, new_univ_dests(dst_begin, dst_end),
std::forward<Args>(args)...);
}
/// \brief Create a new universal edge

125
spot/parseaut/parseaut.yy
View file

@ -95,7 +95,8 @@ extern "C" int strverscmp(const char *s1, const char *s2);
std::vector<bdd>::const_iterator cur_guard;
map_t dest_map;
std::vector<state_info> info_states; // States declared and used.
std::vector<std::pair<spot::location, unsigned>> start; // Initial states;
std::vector<std::pair<spot::location,
std::vector<unsigned>>> start; // Initial states;
std::unordered_map<std::string, bdd> alias;
struct prop_info
{
@ -239,7 +240,7 @@ extern "C" int strverscmp(const char *s1, const char *s2);
%left '&'
%nonassoc '!'
%type <states> state-conj-2 state-conj-checked
%type <states> init-state-conj-2 state-conj-2 state-conj-checked
%type <num> checked-state-num state-num acc-set sign
%type <b> label-expr
%type <mark> 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<unsigned>{$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<unsigned>{$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<unsigned>{$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<unsigned>{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<unsigned>{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<unsigned> start;
std::vector<std::vector<unsigned>> 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<unsigned> 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<unsigned char> 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);
}
}
}

17
spot/twa/twagraph.hh
View file

@ -268,6 +268,23 @@ namespace spot
set_init_state(state_number(s));
}
template<class I>
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<class I>
void set_univ_init_state(const std::initializer_list<state_num>& 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.

37
spot/twaalgos/dot.cc
View file

@ -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)

30
spot/twaalgos/hoa.cc
View file

@ -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<std::vector<std::string>>("state-names");
for (unsigned i = 0; i < num_states; ++i)
{

13
tests/core/alternating.test
View file

@ -24,7 +24,7 @@ set -e
cat >alt.hoa <<EOF
HOA: v1.1
States: 7
Start: 0
Start: 0&2
acc-name: co-Buchi
Acceptance: 1 Fin(0)
AP: 2 "b" "a"
@ -62,14 +62,17 @@ digraph G {
label="Fin(⓿)"
labelloc="t"
I [label="", style=invis, width=0]
I -> 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⓿"]

3
tests/core/parseaut.test
View file

@ -1921,8 +1921,7 @@ State: 11 "t"
EOF
expecterr input <<EOF
input:4.8-12: alternation is not yet supported for initial states
autfilt: failed to read automaton from input
input:4.1-12: alternating automata only support a single initial state
EOF
# Some alternation errors

20
tests/python/alternating.py
View file

@ -74,3 +74,23 @@ aut2 = spot.automaton(h)
h2 = aut2.to_str('hoa')
print(h2)
assert h == h2
aut2.set_univ_init_state([0, 1])
h3 = aut2.to_str('hoa')
print(h3)
assert h3 == """HOA: v1
States: 3
Start: 0&1
AP: 2 "p1" "p2"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: univ-branch trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1&2 {0}
[1] 0&1
State: 1
[0&1] 0&2&1
State: 2
[0 | 1] 2
--END--"""