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

degen: Improve when initial state is accepting without self-loop.

Browse source 
* src/tgbaalgos/degen.cc: Choose the initial level according
to acceptance condition common to all outgoing transitions.
* src/tgbatest/degenid.test: Add test case.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2013-08-23 13:23:59 +02:00
parent 67a4833576
commit dfc5ff95e5
3 changed files with 51 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -14,6 +14,9 @@ New in spot 1.1.4a (not relased)
temporary files are created and if they should be erased. Read
the man page of ltlcross for detail.
* Degeneralization was not indempotant on automata with an accepting
initial state that was on a cycle, but without self-loop.
* Cleanup of exported symbols
All symbols in the library now have hidden visibility on ELF systems.

23
src/tgbaalgos/degen.cc
View file

@ -188,8 +188,7 @@ namespace spot
acc = temp;
unsigned next = slevel;
while (next < order_.size()
&& (acc & order_[next]) == order_[next])
while (next < order_.size() && bdd_implies(order_[next], acc))
++next;
return next;
}
@ -314,8 +313,8 @@ namespace spot
const state* s0 = uniq(a->get_init_state());
degen_state s(s0, 0);
// As an heuristic, if the initial state has accepting self-loops,
// start the degeneralization on the accepting level.
// As an heuristic, if the initial state at least one accepting
// self-loop, start the degeneralization on the accepting level.
{
bdd all = a->all_acceptance_conditions();
tgba_succ_iterator* it = a->succ_iter(s0);
@ -335,6 +334,18 @@ namespace spot
}
delete it;
}
// Otherwise, check for acceptance conditions common to all
// outgoing transitions, and assume we have already seen these and
// start on the associated level.
if (s.second == 0)
{
bdd acc = outgoing.common_acc(s.first);
if (use_cust_acc_orders)
s.second = orders.next_level(m.initial(), s.second, acc);
else
while (s.second < order.size() && bdd_implies(order[s.second], acc))
++s.second;
}
#ifdef DEGEN_DEBUG
std::map<const state*, int>names;
@ -426,7 +437,7 @@ namespace spot
// 1=>1, 1=>2, 2->2, 2->1 This is already an SBA,
// with 1 as accepting state. However if you try
// degeralize it without ignoring *prev, you'll get
// two copies of states 2, depending on whether we
// two copies of state 2, depending on whether we
// reach it using 1=>2 or from 2->2. If this
// example was not clear, uncomment the following
// "if" block, and play with the "degenid.test"
@ -495,7 +506,7 @@ namespace spot
// acceptance sets common to the outgoing transitions of
// the destination state.
while (next < order.size()
&& (acc & order[next]) == order[next])
&& bdd_implies(order[next], acc))
++next;
d.second = next;

31
src/tgbatest/degenid.test
View file

@ -1,5 +1,5 @@
#!/bin/sh
# Copyright (C) 2011 Laboratoire de Recherche et Développement
# Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -36,3 +36,32 @@ for f in 'FGa|GFb' 'GFa & GFb & GFc' 'GF(a->FGb)&GF(c->FGd)'; do
done
done
done
# This is another 6-state degeneralized automaton that
# we used the "redegeneralize" to a 8-state BA...
cat > bug <<EOF
acc = "1";
"1", "2", "!b | !a", "1";
"1", "5", "a & b", "1";
"2", "2", "b & !a", "1";
"2", "3", "!b & !a", "1";
"2", "4", "a", "1";
"5", "1", "a & !b",;
"5", "2", "!b & !a",;
"5", "5", "a & b",;
"5", "6", "b & !a",;
"3", "1", "a & b",;
"3", "2", "b & !a",;
"3", "3", "!b & !a",;
"3", "4", "a & !b",;
"4", "1", "b",;
"4", "5", "a & !b",;
"4", "6", "!b & !a",;
"6", "1", "!b",;
"6", "3", "b & !a",;
"6", "4", "a & b",;
EOF
run 0 ../ltl2tgba -ks -X -DS bug > out
grep 'states: 6' out