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

complement: fix handling of output_aborter with postproc

Browse source 
Reported by Salomon Sickert.

* spot/twaalgos/complement.cc: Make sure the output of postproc
is deterministic.
* tests/core/ltlcross.test: Add test case.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2019-07-11 14:48:50 +02:00
parent 1f8a777e1f
commit e2fad2d7ae
3 changed files with 15 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
NEWS
View file

@ -1,6 +1,12 @@
New in spot 2.8.0.dev (not yet released) New in spot 2.8.0.dev (not yet released)
Nothing yet. Bugs fixed:
- When complement() was called with an output_aborter, it could
return an alternating automaton on large automata. This in turn
caused ltlcross to emit errors like "remove_alternation() only
works with weak alternating automata" or "product() does not
support alternating automata".
New in spot 2.8 (2019-07-10) New in spot 2.8 (2019-07-10)

2
spot/twaalgos/complement.cc
View file

@ -534,7 +534,7 @@ namespace spot
p.set_pref(spot::postprocessor::Deterministic); p.set_pref(spot::postprocessor::Deterministic);
p.set_level(spot::postprocessor::Low); p.set_level(spot::postprocessor::Low);
auto det = p.run(std::const_pointer_cast<twa_graph>(aut)); auto det = p.run(std::const_pointer_cast<twa_graph>(aut));
if (!det) if (!det || !is_universal(det))
return nullptr; return nullptr;
return dualize(det); return dualize(det);
} }

8
tests/core/ltlcross.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2012, 2013, 2014, 2016 Laboratoire de Recherche et # Copyright (C) 2012-2014, 2016, 2019 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -59,3 +59,9 @@ ltlcross -D \
"$ltl2tgba -t -taa -r4 %f > %T" \ "$ltl2tgba -t -taa -r4 %f > %T" \
"$ltl2tgba -t -taa -r4 -c %f > %T" \ "$ltl2tgba -t -taa -r4 -c %f > %T" \
"$ltl2tgba -t -taa -r4 -R3 -RDS %f > %T" "$ltl2tgba -t -taa -r4 -R3 -RDS %f > %T"
# This case, reported by Salomon Sickert, used to break ltlcross in
# Spot 2.8. We use ltl2tgba twice so ltlcross build cross-products.
ltlcross --verbose ltl2tgba ltl2tgba \
-f '(G(F((a1)&(X(X(b1))))))&(G(F((a2)&(X(X(b2))))))&(G(F((a3)&(X(X(b3))))))'