Commit 0e04b253 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltldo: preserve generic acceptance

* src/bin/ltldo.cc: Default to generic acceptance.
* src/tests/ltl2dstar.test: Add a test.
parent 3d1ccdc4
......@@ -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);
......
#!/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 <<EOF
HOA: v1
States: 5
Start: 3
AP: 2 "b" "a"
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
properties: implicit-labels state-acc complete deterministic
--BODY--
State: 0 {1 3}
2 0 4 1
State: 1 {0 3}
2 0 4 1
State: 2 {1}
2 0 4 1
State: 3 {0}
0 0 1 1
State: 4 {0}
2 0 4 1
--END--
EOF
diff out.hoa expected
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment