tgba_digraph: Fix handling of initial state.
* src/tgba/tgbagraph.hh: Store the number of the initial state, not a pointer to it, because if the state vector is reallocated due to some later calls to new_state(), this pointer will be invalid. * src/graphtest/tgbagraph.cc, src/graphtest/tgbagraph.test: Test for this.
This commit is contained in:
parent
fd5fbda4dd
commit
ff83e92db4
3 changed files with 37 additions and 18 deletions
|
|
@ -82,6 +82,11 @@ void f1()
|
||||||
|
|
||||||
std::cerr << tg.num_transitions() << '\n';
|
std::cerr << tg.num_transitions() << '\n';
|
||||||
assert(tg.num_transitions() == 5);
|
assert(tg.num_transitions() == 5);
|
||||||
|
|
||||||
|
// Add enough states so that the state vector is reallocated.
|
||||||
|
for (unsigned i = 0; i < 100; ++i)
|
||||||
|
tg.new_state();
|
||||||
|
spot::dotty_reachable(std::cout, &tg);
|
||||||
}
|
}
|
||||||
|
|
||||||
int main()
|
int main()
|
||||||
|
|
|
||||||
|
|
@ -96,6 +96,18 @@ digraph G {
|
||||||
3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"]
|
3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"]
|
||||||
3 -> 2 [label="!p1 | p2\n"]
|
3 -> 2 [label="!p1 | p2\n"]
|
||||||
}
|
}
|
||||||
|
digraph G {
|
||||||
|
0 [label="", style=invis, height=0]
|
||||||
|
0 -> 1
|
||||||
|
1 [label="0"]
|
||||||
|
1 -> 2 [label="p1\n"]
|
||||||
|
1 -> 3 [label="p2\n{Acc[p2]}"]
|
||||||
|
2 [label="1"]
|
||||||
|
2 -> 3 [label="p1 & p2\n{Acc[p1]}"]
|
||||||
|
3 [label="2"]
|
||||||
|
3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"]
|
||||||
|
3 -> 2 [label="!p1 | p2\n"]
|
||||||
|
}
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
diff stdout expected
|
diff stdout expected
|
||||||
|
|
|
||||||
|
|
@ -33,6 +33,11 @@ namespace spot
|
||||||
struct SPOT_API tgba_graph_state: public spot::state
|
struct SPOT_API tgba_graph_state: public spot::state
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
|
tgba_graph_state():
|
||||||
|
spot::state()
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
virtual ~tgba_graph_state() noexcept
|
virtual ~tgba_graph_state() noexcept
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
@ -158,14 +163,14 @@ namespace spot
|
||||||
bdd_dict* dict_;
|
bdd_dict* dict_;
|
||||||
bdd all_acceptance_conditions_;
|
bdd all_acceptance_conditions_;
|
||||||
bdd neg_acceptance_conditions_;
|
bdd neg_acceptance_conditions_;
|
||||||
mutable const tgba_graph_state* init_;
|
mutable unsigned init_number_;
|
||||||
|
|
||||||
public:
|
public:
|
||||||
tgba_digraph(bdd_dict* dict)
|
tgba_digraph(bdd_dict* dict)
|
||||||
: dict_(dict),
|
: dict_(dict),
|
||||||
all_acceptance_conditions_(bddfalse),
|
all_acceptance_conditions_(bddfalse),
|
||||||
neg_acceptance_conditions_(bddtrue),
|
neg_acceptance_conditions_(bddtrue),
|
||||||
init_(nullptr)
|
init_number_(0)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -223,31 +228,28 @@ namespace spot
|
||||||
|
|
||||||
void set_init_state(graph_t::state s)
|
void set_init_state(graph_t::state s)
|
||||||
{
|
{
|
||||||
init_ = &g_.state_data(s);
|
assert(s < num_states());
|
||||||
|
init_number_ = s;
|
||||||
}
|
}
|
||||||
|
|
||||||
void set_init_state(const state* s)
|
void set_init_state(const state* s)
|
||||||
{
|
{
|
||||||
init_ = down_cast<const tgba_graph_state*>(s);
|
set_init_state(state_number(s));
|
||||||
assert(init_);
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual tgba_graph_state* get_init_state() const
|
|
||||||
{
|
|
||||||
if (num_states() == 0)
|
|
||||||
const_cast<graph_t&>(g_).new_state();
|
|
||||||
if (!init_)
|
|
||||||
init_ = &g_.state_data(0);
|
|
||||||
return const_cast<tgba_graph_state*>(init_);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual graph_t::state get_init_state_number() const
|
virtual graph_t::state get_init_state_number() const
|
||||||
{
|
{
|
||||||
if (num_states() == 0)
|
if (num_states() == 0)
|
||||||
const_cast<graph_t&>(g_).new_state();
|
const_cast<graph_t&>(g_).new_state();
|
||||||
if (!init_)
|
return init_number_;
|
||||||
return 0;
|
}
|
||||||
return state_number(init_);
|
|
||||||
|
// FIXME: The return type ought to be const.
|
||||||
|
virtual tgba_graph_state* get_init_state() const
|
||||||
|
{
|
||||||
|
if (num_states() == 0)
|
||||||
|
const_cast<graph_t&>(g_).new_state();
|
||||||
|
return const_cast<tgba_graph_state*>(state_from_number(init_number_));
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual tgba_succ_iterator*
|
virtual tgba_succ_iterator*
|
||||||
|
|
@ -276,7 +278,7 @@ namespace spot
|
||||||
return s - &g_.state_storage(0);
|
return s - &g_.state_storage(0);
|
||||||
}
|
}
|
||||||
|
|
||||||
const state*
|
const tgba_graph_state*
|
||||||
state_from_number(graph_t::state n) const
|
state_from_number(graph_t::state n) const
|
||||||
{
|
{
|
||||||
return &g_.state_data(n);
|
return &g_.state_data(n);
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue