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

DVE2: Do not display state variables with only one possible value.

Browse source 
* iface/dve2/dve2.cc (dve2_kripke::dve2_kripke): Fill
a format_filter_ array with boolean indicating whether each
variable should be printed.  Ignore variable with only one
possible value.
(dve2_kripke::~dve2_kripke): Destroy it.
(dve2_kripke::format_state): Use it.
* iface/dve2/finite.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2011-06-06 18:19:11 +02:00
parent 866af2a715
commit d47aa1d8b2
3 changed files with 32 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

12
ChangeLog
View file

@ -1,3 +1,15 @@
2011-06-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
DVE2: Do not display state variables with only one possible value.
* iface/dve2/dve2.cc (dve2_kripke::dve2_kripke): Fill
a format_filter_ array with boolean indicating whether each
variable should be printed. Ignore variable with only one
possible value.
(dve2_kripke::~dve2_kripke): Destroy it.
(dve2_kripke::format_state): Use it.
* iface/dve2/finite.test: Adjust.
2011-06-06 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-06-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Remove Kristin Rozier's LTLcounter.pl scripts, now that we can Remove Kristin Rozier's LTLcounter.pl scripts, now that we can

18
iface/dve2/dve2.cc
View file

@ -612,8 +612,17 @@ namespace spot
state_condition_last_state_(0), state_condition_last_cc_(0) state_condition_last_state_(0), state_condition_last_cc_(0)
{ {
vname_ = new const char*[state_size_]; vname_ = new const char*[state_size_];
format_filter_ = new bool[state_size_];
for (int i = 0; i < state_size_; ++i) for (int i = 0; i < state_size_; ++i)
vname_[i] = d_->get_state_variable_name(i); {
vname_[i] = d_->get_state_variable_name(i);
// We don't want to print variables that can take a single
// value (e.g. process with a single state) to shorten the
// output.
int type = d->get_state_variable_type(i);
format_filter_[i] =
(d->get_state_variable_type_value_count(type) != 1);
}
// Register the "dead" proposition. There are three cases to // Register the "dead" proposition. There are three cases to
// consider: // consider:
@ -648,6 +657,7 @@ namespace spot
~dve2_kripke() ~dve2_kripke()
{ {
delete[] format_filter_;
delete[] vname_; delete[] vname_;
if (compress_) if (compress_)
{ {
@ -866,6 +876,11 @@ namespace spot
int i = 0; int i = 0;
for (;;) for (;;)
{ {
if (!format_filter_[i])
{
++i;
continue;
}
res << vname_[i] << "=" << vars[i]; res << vname_[i] << "=" << vars[i];
++i; ++i;
if (i == state_size_) if (i == state_size_)
@ -886,6 +901,7 @@ namespace spot
int state_size_; int state_size_;
bdd_dict* dict_; bdd_dict* dict_;
const char** vname_; const char** vname_;
bool* format_filter_;
const prop_set* ps_; const prop_set* ps_;
bdd alive_prop; bdd alive_prop;
bdd dead_prop; bdd dead_prop;

6
iface/dve2/finite.test
View file

@ -34,19 +34,19 @@ fi
set -e set -e
run 0 ../dve2check -gm $srcdir/finite.dve '"P.a < 10"' > stdout run 0 ../dve2check -gm $srcdir/finite.dve '"P.a < 10"' > stdout
test "`grep ' -> ' stdout | wc -l`" = 25 test "`grep ' -> ' stdout | wc -l`" = 25
test "`grep 'P=0' stdout | wc -l`" = 15 test "`grep 'P.a=' stdout | wc -l`" = 15
run 0 ../dve2check -dtrue -gm $srcdir/finite.dve '"P.a < 10"' > stdout2 run 0 ../dve2check -dtrue -gm $srcdir/finite.dve '"P.a < 10"' > stdout2
cmp stdout stdout2 cmp stdout stdout2
run 0 ../dve2check -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout run 0 ../dve2check -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout
test "`grep ' -> ' stdout | wc -l`" = 19 test "`grep ' -> ' stdout | wc -l`" = 19
test "`grep 'P=0' stdout | wc -l`" = 15 test "`grep 'P.a=' stdout | wc -l`" = 15
# the same with compressed states # the same with compressed states
run 0 ../dve2check -z -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout run 0 ../dve2check -z -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout
test "`grep ' -> ' stdout | wc -l`" = 19 test "`grep ' -> ' stdout | wc -l`" = 19
test "`grep 'P=0' stdout | wc -l`" = 15 test "`grep 'P.a=' stdout | wc -l`" = 15
run 0 ../dve2check -ddead -e $srcdir/finite.dve \ run 0 ../dve2check -ddead -e $srcdir/finite.dve \
'!(G(dead -> ("P.a==3" | "P.b==3")))' '!(G(dead -> ("P.a==3" | "P.b==3")))'