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

lbttparse: allow acceptance sets that are not consecutive integers.

Browse source 
* src/tgbaalgos/lbtt.cc: Renumber acceptance sets as they are read.
* src/tgbatest/lbttparse.test: Add a test cases.
This commit is contained in:
Alexandre Duret-Lutz 2012-10-19 15:56:42 +02:00
parent 89b9cc5fd5
commit e426c63550
2 changed files with 51 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

47
src/tgbaalgos/lbtt.cc
View file

@ -169,9 +169,7 @@ namespace spot
const ltl::formula* af = acc_f[n] = envacc.require(s.str());
aut->declare_acceptance_condition(af->clone());
}
std::vector<bdd> acc_b(num_acc);
for (unsigned n = 0; n < num_acc; ++n)
acc_b[n] = aut->get_acceptance_condition(acc_f[n]);
std::map<int, bdd> acc_b;
for (unsigned n = 0; n < num_states; ++n)
{
@ -197,13 +195,25 @@ namespace spot
is >> acc_n;
if (acc_n == -1)
break;
if (acc_n < 0 || (unsigned)acc_n >= num_acc)
std::map<int, bdd>::const_iterator i = acc_b.find(acc_n);
if (i != acc_b.end())
{
error += "invalid acceptance set";
goto fail;
acc |= i->second;
}
else
{
size_t s = acc_b.size();
if (s >= num_acc)
{
error += "more acceptance sets used than declared";
goto fail;
}
bdd a = aut->get_acceptance_condition(acc_f[s]);
acc_b[acc_n] = a;
acc |= a;
}
acc |= acc_b[acc_n];
}
std::string guard;
std::getline(is, guard);
ltl::parse_error_list pel;
@ -242,9 +252,7 @@ namespace spot
const ltl::formula* af = acc_f[n] = envacc.require(s.str());
aut->declare_acceptance_condition(af->clone());
}
std::vector<bdd> acc_b(num_acc);
for (unsigned n = 0; n < num_acc; ++n)
acc_b[n] = aut->get_acceptance_condition(acc_f[n]);
std::map<int, bdd> acc_b;
for (unsigned n = 0; n < num_states; ++n)
{
@ -262,12 +270,23 @@ namespace spot
is >> acc_n;
if (acc_n == -1)
break;
if (acc_n < 0 || (unsigned)acc_n >= num_acc)
std::map<int, bdd>::const_iterator i = acc_b.find(acc_n);
if (i != acc_b.end())
{
error += "invalid acceptance set";
goto fail;
acc |= i->second;
}
else
{
size_t s = acc_b.size();
if (s >= num_acc)
{
error += "more acceptance sets used than declared";
goto fail;
}
bdd a = aut->get_acceptance_condition(acc_f[s]);
acc_b[acc_n] = a;
acc |= a;
}
acc |= acc_b[acc_n];
}
// Read the transitions.

18
src/tgbatest/lbttparse.test
View file

@ -81,3 +81,21 @@ run 0 ../ltl2tgba -ks -XL wring2lbtt > size
test "`cat size | sed -n 's/states: //p'`" = 4
test "`cat size | sed -n 's/transitions: //p'`" = 6
# Another example from wring2lbtt (or modella), showing that the
# acceptance set of the state is not always numbered from 0.
cat >wring2lbtt2 <<EOF
6 1 0 1 -1 1 | & ! p0 ! p1 & p0 ! p1
2 & ! p0 ! p1
3 | & p0 p1 & ! p0 p1
-1 1 0 -1 4 ! p1
-1 2 0 -1 2 & ! p0 ! p1
3 | & p0 p1 & ! p0 p1
-1 3 0 -1 5 t
-1 4 0 1 -1 4 ! p1
-1 5 0 1 -1 5 t
-1
EOF
run 0 ../ltl2tgba -ks -XL wring2lbtt2 > size
test "`cat size | sed -n 's/states: //p'`" = 6
test "`cat size | sed -n 's/transitions: //p'`" = 9