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

Fix computation of support_conditions in tgba_wdba_comp_proxy.

Browse source 
* src/tgba/wdbacomp.cc
(tgba_wdba_comp_proxy::compute_support_conditions): Fix.
* src/tgbatest/wdba2.test: Test a formula that used to be wrongly
minimized if translated by LaCIM, because the product of a
tgbabddconcrete automaton with another automaton (done during
WDBA-minimization) use the support conditions to speed things up.
This commit is contained in:
Alexandre Duret-Lutz 2012-06-07 22:34:00 +02:00
parent 03b13891e3
commit d7ff066513
2 changed files with 18 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/tgba/wdbacomp.cc
View file

@ -1,5 +1,6 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement de // -*- coding: utf-8 -*-
// l'Epita. // Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
// de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -250,15 +251,9 @@ namespace spot
protected: protected:
virtual bdd virtual bdd
compute_support_conditions(const state* ostate) const compute_support_conditions(const state*) const
{ {
const state_wdba_comp_proxy* s = // The automaton is complete, so we always support all variables.
down_cast<const state_wdba_comp_proxy*>(ostate);
assert(s);
const state* rs = s->real_state();
if (rs)
return a_->support_conditions(rs);
else
return bddtrue; return bddtrue;
} }

10
src/tgbatest/wdba2.test
View file

@ -1,4 +1,5 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2012 Laboratoire de Recherche et Développement # Copyright (C) 2012 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# #
@ -36,3 +37,12 @@ run 0 ../ltl2tgba -Rm -kt 'Fa | XGd' > out2
cmp out expected cmp out expected
cmp out2 expected cmp out2 expected
# This non-obligation formula used to be minimized by mistake when
# translated with lacim.
x=`../ltl2tgba -l -Rm 'F(Fa R (Gb & !a))' |
grep -v -- '->' |
sed -n 's/.*label="\(..*\)".*/\1/p' |
tr -d '0-9\n'`
test -n "$x"