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

auts_to_aiger: Fix output name index

Browse source 
* spot/twaalgos/aiger.cc: Correct the position of an output in
  a realizability_simplifier.
* tests/core/ltlsynt.test: Add test.
This commit is contained in:
Florian Renkin 2023-11-29 09:16:01 +00:00
parent 234ba2bb84
commit cee2819a45
2 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
spot/twaalgos/aiger.cc
View file

@ -2042,9 +2042,10 @@ namespace
repr = repr[0]; repr = repr[0];
} }
// is repr an input? // is repr an input?
auto ap_name = repr.ap_name();
if (auto it2 = std::find(input_names_all.begin(), if (auto it2 = std::find(input_names_all.begin(),
input_names_all.end(), input_names_all.end(),
repr.ap_name()); ap_name);
it2 != input_names_all.end()) it2 != input_names_all.end())
{ {
unsigned ivar = unsigned ivar =
@ -2055,10 +2056,9 @@ namespace
// is repr an output? // is repr an output?
else else
{ {
assert(std::find(output_names_all.begin(), it2 = std::find(output_names_all.begin(),
output_names_all.end(), output_names_all.end(), ap_name);
repr.ap_name()) == assert(it2 != output_names_all.end());
output_names_all.end());
unsigned outnum = it2 - output_names_all.begin(); unsigned outnum = it2 - output_names_all.begin();
unsigned outvar = circuit.output(outnum); unsigned outvar = circuit.output(outnum);
circuit.set_output(i, outvar + neg_repr); circuit.set_output(i, outvar + neg_repr);

4
tests/core/ltlsynt.test
View file

@ -1106,3 +1106,7 @@ REALIZABLE
REALIZABLE REALIZABLE
EOF EOF
diff out expected diff out expected
f1="((G ((p0) <-> (! (p1)))) && (((((F ((b) && (G (F (a))))) ||\
(F ((c) && (G (F (! (a))))))) && (F (b))) && (F (c))) <-> (G (F (p0)))))"
ltlsynt -f "$f1" --outs="p1, p0" --aiger > /dev/null