Commit 0288aaa3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

determinize: add tests for the bug Alexandre L fixed

* tests/core/safra.test: More tests.
parent 0d9019ea
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement # Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
...@@ -171,9 +171,14 @@ Fa W Gb ...@@ -171,9 +171,14 @@ Fa W Gb
Ga | GFb Ga | GFb
a M G(F!b | X!a) a M G(F!b | X!a)
G!a R XFb G!a R XFb
F(G((a) | (F(b))))
FG(!p1 | (p1 M XX!p1))
EOF EOF
run 0 ../safra --hoa double_b.hoa -H > out.hoa run 0 ../safra --hoa double_b.hoa -H > out.hoa
ltl2tgba=ltl2tgba
ltlcross -F formulae \ ltlcross -F formulae \
"../safra -f %f -H > %O" \ "../safra -f %f -H > %O" \
"$ltl2tgba -f %f -H > %O" "../safra --scc_opt -f %f -H > %O" \
"../safra --bisim_opt -f %f -H > %O" \
"../safra --stutter -f %f -H > %O" \
"../safra --scc_opt --bisim_opt --stutter -f %f -H > %O" \
"ltl2tgba"
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