From cee2819a4565671e6bee7fe6dafe192b73d4abe7 Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Wed, 29 Nov 2023 09:16:01 +0000 Subject: [PATCH] auts_to_aiger: Fix output name index * spot/twaalgos/aiger.cc: Correct the position of an output in a realizability_simplifier. * tests/core/ltlsynt.test: Add test. --- spot/twaalgos/aiger.cc | 10 +++++----- tests/core/ltlsynt.test | 4 ++++ 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index d41e2ae8a..8f3bfdcc7 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -2042,9 +2042,10 @@ namespace repr = repr[0]; } // is repr an input? + auto ap_name = repr.ap_name(); if (auto it2 = std::find(input_names_all.begin(), input_names_all.end(), - repr.ap_name()); + ap_name); it2 != input_names_all.end()) { unsigned ivar = @@ -2055,10 +2056,9 @@ namespace // is repr an output? else { - assert(std::find(output_names_all.begin(), - output_names_all.end(), - repr.ap_name()) == - output_names_all.end()); + it2 = std::find(output_names_all.begin(), + output_names_all.end(), ap_name); + assert(it2 != output_names_all.end()); unsigned outnum = it2 - output_names_all.begin(); unsigned outvar = circuit.output(outnum); circuit.set_output(i, outvar + neg_repr); diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 3944c2076..537872c23 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1106,3 +1106,7 @@ REALIZABLE REALIZABLE EOF 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 \ No newline at end of file