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

Fix slight error in aiger

Browse source 
The negation of global equivalences for outputs
contained a slight error when the output corresponded
to a negated gate.

* spot/twaalgos/aiger.cc: Fix
* tests/core/ltlsynt.test: Test
This commit is contained in:
Philipp Schlehuber-Caissier 2025-01-05 13:18:35 +01:00 • committed by Alexandre Duret-Lutz
parent e4a49cda02
commit 480e5e999b
2 changed files with 16 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
spot/twaalgos/aiger.cc
View file

@ -2061,7 +2061,10 @@ namespace
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);
assert(outvar != -1u);
if (neg_repr)
outvar = circuit.aig_not(outvar);
circuit.set_output(i, outvar);
}
}
}

12
tests/core/ltlsynt.test
View file

@ -1304,3 +1304,15 @@ f2='G(i1->(o1|!o2)) & G(!i1->(o3|!o4)) & G(i2->(!o1|o2)) & G(!i2->(!o3|o4))&Go5'
ltlsynt -f "$f2" --polarity=before-decom --verbose 2>out 1>&2
sed 's/ [0-9.e-]* seconds/ X seconds/g;s/ -> /->/g;' out > outx
diff outx exp
# Additional test for global equivalences
# Specifically if the output is set to the negation of another output
ltlsynt -f "((G((p0)<->(!(p1))))&&(((F(a))||(G(b)))<->(G(F(p0)))))" \
--outs "p1, p0" \
--verify --aiger | tail -n 1 > out
cat > expected <<EOF
Circuit was verified
EOF
diff out expected