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

synthesis: fix handling of deadstates

Browse source 
* spot/twaalgos/synthesis.cc: Remove a debuging print
from the semisym code, and add an additional case
in the fullysym code.
* tests/core/ltlsynt.test: Add a some test case,
and remove some bashism.
This commit is contained in:
Alexandre Duret-Lutz 2024-09-12 14:00:08 +02:00
parent 90fb7b1cd9
commit 99a622059c
2 changed files with 10 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

14
spot/twaalgos/synthesis.cc
View file

@ -1386,6 +1386,8 @@ namespace spot
{ {
assert(std::holds_alternative<bdd>(ccondin)); assert(std::holds_alternative<bdd>(ccondin));
const bdd& ccond = std::get<bdd>(ccondin); const bdd& ccond = std::get<bdd>(ccondin);
if (ccond == bddfalse)
return;
int clvl = ccond == bddtrue ? inIdx : bdd_var(ccond); int clvl = ccond == bddtrue ? inIdx : bdd_var(ccond);
if (clvl >= inIdx) if (clvl >= inIdx)
{ {
@ -1468,17 +1470,11 @@ namespace spot
for (const auto &e: aut->out(s)) for (const auto &e: aut->out(s))
enc_out_s |= encode_edge(e); // Switch to new ins and outs enc_out_s |= encode_edge(e); // Switch to new ins and outs
// Can only be false if there is no outgoing edge
// In this case: Nothing to do
assert(enc_out_s != bddfalse
|| (!(aut->out(s).begin())));
if (enc_out_s == bddfalse) if (enc_out_s == bddfalse)
{ {
std::cerr << "Dead end state: " << s << '\n'; // Can only be false if there is no outgoing edge
#ifndef NDEBUG // In this case: Nothing to do
print_hoa(std::cerr, aut); assert(!(aut->out(s).begin()));
#endif
continue; continue;
} }

10
tests/core/ltlsynt.test
View file

@ -494,12 +494,12 @@ diff out exp
for splitt in expl semisym fullysym auto for splitt in expl semisym fullysym auto
do do
res=$(ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" \ # REALIZABLE
ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" \
--outs="o0,o1" --aiger=isop+ud --algo=lar --decompose=no \ --outs="o0,o1" --aiger=isop+ud --algo=lar --decompose=no \
--simpl=no --splittype="$splitt" --realizability) --simpl=no --splittype="$splitt" --realizability || exit 2
if [[ "$res" != "REALIZABLE" ]]; then # UNREALIZABLE
echo "Expected realizable" ltlsynt -f "Gi & Fo" --splittype="$splitt" --realizability && exit 2
fi
done done