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

monitor: add a few tests

Browse source 
* src/tgbatest/monitor.test: New file.
* src/tgbatest/Makefile.am: Add it.
* src/tgbaalgos/minimize.cc (minimize_monitor): Mark
the output automaton as state-based.
* src/tgba/tgbagraph.hh: Assume automata with 0 acceptance sets are also
state-based.
This commit is contained in:
Alexandre Duret-Lutz 2014-11-20 10:59:56 +01:00
parent 6eeb74e15f
commit 392c527d31
4 changed files with 80 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tgba/tgbagraph.hh
View file

@ -322,6 +322,8 @@ namespace spot
}
acc_.add_sets(num - acc_.num_sets());
prop_single_acc_set(num == 1);
if (num == 0)
prop_state_based_acc();
}
acc_cond::mark_t set_single_acceptance_set()
@ -430,7 +432,7 @@ namespace spot
bool state_is_accepting(unsigned s) const
{
assert(has_state_based_acc());
assert(has_state_based_acc() || acc_.num_sets() == 0);
for (auto& t: g_.out(s))
// Stop at the first transition, since the remaining should be
// labeled identically.