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

fix a bug in aiger printer

Browse source 
* spot/twaalgos/aiger.cc: here
* tests/core/ltlsynt.test: add a non-regression test
This commit is contained in:
Maximilien Colange 2018-06-07 15:11:16 +02:00
parent 9489a65bc6
commit 1183a935c7
2 changed files with 29 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/aiger.cc
View file

@ -319,7 +319,7 @@ namespace spot
int bddvar = aut->get_dict()->has_registered_proposition(ap, aut); int bddvar = aut->get_dict()->has_registered_proposition(ap, aut);
assert(bddvar >= 0); assert(bddvar >= 0);
bdd b = bdd_ithvar(bddvar); bdd b = bdd_ithvar(bddvar);
if (bdd_implies(b, all_outputs)) // ap is an output AP if (bdd_implies(all_outputs, b)) // ap is an output AP
{ {
bddvar_to_outputnum[bddvar] = output_names.size(); bddvar_to_outputnum[bddvar] = output_names.size();
output_names.emplace_back(ap.ap_name()); output_names.emplace_back(ap.ap_name());

28
tests/core/ltlsynt.test
View file

@ -73,6 +73,34 @@ EOF
ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --aiger > out ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --aiger > out
diff out exp diff out exp
cat >exp <<EOF
REALIZABLE
aag 16 1 2 2 13
2
4 29
6 33
31
31
8 5 7
10 3 8
12 2 8
14 4 7
16 3 14
18 2 14
20 5 6
22 2 20
24 3 20
26 17 25
28 11 26
30 19 23
32 13 30
i0 a
o0 b
o1 c
EOF
ltlsynt --ins='a' --outs='b,c' -f 'GFa <-> (GFb & GFc)' --aiger > out
diff out exp
cat >exp <<EOF cat >exp <<EOF
translating formula done translating formula done
split inputs and outputs done split inputs and outputs done