Commit 548a35ad authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

adjust test case to work with ltl2dstar 0.5.4

* tests/core/ltl2dstar.test: Here.
parent f1924430
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013-2017 Laboratoire de Recherche et Développement de
# Copyright (C) 2013-2018 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -78,28 +78,13 @@ test `grep -c 'info: check_empty.*Comp' err` = 2
ltldo \
"ltl2dstar --ltl2nba=spin:ltl2tgba@-s --output-format=hoa %L %O" \
-f 'GFa -> GFb' -Hi > out.hoa
grep 'acc-name:\|Acceptance:' out.hoa > out2
cat >expected <<EOF
HOA: v1
States: 5
Start: 3
AP: 2 "a" "b"
acc-name: Rabin 2
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
properties: implicit-labels state-acc complete deterministic
--BODY--
State: 0 {1 3}
2 4 0 1
State: 1 {0 3}
2 4 0 1
State: 2 {1}
2 4 0 1
State: 3 {0}
0 1 0 1
State: 4 {0}
2 4 0 1
--END--
EOF
diff out.hoa expected
diff out2 expected
# Test the stutter-invariant check on Rabin
autfilt --trust-hoa=no --check=stutter out.hoa -H1.1 |
......
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