diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index 6ea37fc51..3b23687f6 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -344,6 +344,7 @@ main(int argc, char** argv) // Disable post-processing as much as possible by default. level = spot::postprocessor::Low; pref = spot::postprocessor::Any; + type = spot::postprocessor::Generic; if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) exit(err); diff --git a/src/tests/ltl2dstar.test b/src/tests/ltl2dstar.test index 640c3fd23..348e567a4 100755 --- a/src/tests/ltl2dstar.test +++ b/src/tests/ltl2dstar.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2014 Laboratoire de Recherche et +# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -75,3 +75,30 @@ $ltlcross -f 'FGa' --verbose \ "ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \ "ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err test `grep -c 'info: check_empty.*Comp' err` = 1 + + +# Make sure ltldo preserve the Rabin acceptance by default +../../bin/ltldo \ + "ltl2dstar --ltl2nba=spin:$ltl2tgba@-s --output-format=hoa %L %O" \ + -f 'GFa -> GFb' -Hi > out.hoa +cat >expected <