7a65bdf6bc
This is adapted from a proposition in a paper by J. Esparza, J. Křentínský, and S. Sickert, submitted to LICS'18. We should add proper references to the code and documentation once that paper is accepted. * spot/twaalgos/gfguarantee.cc, spot/twaalgos/gfguarantee.hh: New files. * spot/twaalgos/Makefile.am, python/spot/impl.i: Add them. * spot/twa/fwd.hh: Add a forward declaration of bdd_dict_ptr. * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Make it possible to call finalize() from the translator subclass. Constify all the do_* functions while we are there. * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add a "gf-guarantee" option to decide whether to use the new translation. * bin/spot-x.cc: Document it. * tests/core/dca2.test, tests/core/genltl.test, tests/core/ltl2tgba2.test, tests/core/parity2.test, tests/core/satmin.test, tests/python/automata.ipynb, tests/python/sbacc.py: Adjust test cases. * tests/python/except.py: Add a couple more tests.
76 lines
2.5 KiB
Bash
Executable file
76 lines
2.5 KiB
Bash
Executable file
#!/bin/sh
|
|
# -*- coding: utf-8 -*-
|
|
# Copyright (C) 2017, 2018 Laboratoire de Recherche et
|
|
# Développement de l'EPITA.
|
|
#
|
|
# This file is part of Spot, a model checking library.
|
|
#
|
|
# Spot is free software; you can redistribute it and/or modify it
|
|
# under the terms of the GNU General Public License as published by
|
|
# the Free Software Foundation; either version 3 of the License, or
|
|
# (at your option) any later version.
|
|
#
|
|
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
|
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
|
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
|
# License for more details.
|
|
#
|
|
# You should have received a copy of the GNU General Public License
|
|
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
. ./defs
|
|
set -e
|
|
|
|
cat >l_formulas <<'EOF'
|
|
FG!b
|
|
FGc
|
|
F(a | Gb)
|
|
XF(b & Ga)
|
|
a | c | FG(!b & !c)
|
|
!a | FGb
|
|
F((!a & ((c & F!b) | (!c & Gb))) | (a & ((c & Gb) | (!c & F!b))))
|
|
F((c & F!b) | (!c & Gb))
|
|
F((!c R a) W G!b)
|
|
FG(((!b | (c M b)) & X(c & Xa)) | (b & (!c W !b) & X(!c | X!a)))
|
|
(Ga M c) M ((!b & Fb) M F(a | !b))
|
|
(Gb | X(!b M X!b)) M ((b & c) | (!b & !c))
|
|
F(c R (X!c W Fb))
|
|
XF!c & F(Fb R a)
|
|
(!c M F(b & Ga)) W (b U a)
|
|
EOF
|
|
|
|
cat >r_formulas <<'EOF'
|
|
GF(b | GF!c)
|
|
!b & G(G!c | XFc)
|
|
GF(b | c | (!c & XFb))
|
|
GFc | G(!b | !c)
|
|
G(Gb | Fc)
|
|
G(c | (c R Xc) | XF(b & !c))
|
|
Gc R XFb
|
|
G(c | (!b M (GFc | G!c)))
|
|
F(((c W Xb) & F(b R !c)) | ((!c M X!b) & G(!b U c)))
|
|
EOF
|
|
|
|
while read l_f; do
|
|
ltl2tgba --parity='max odd' "$l_f" > l.hoa
|
|
autfilt -q --acceptance-is='Fin(0) | Inf(1)' l.hoa ||
|
|
autfilt -q --acceptance-is='Fin(0)' l.hoa
|
|
while read r_f; do
|
|
# Dualizing a deterministic transition-based parity automaton
|
|
# to obtain a transition-based deterministic streett
|
|
# automaton. What we want to avoid as much as possible is
|
|
# weak automata, because l.hoa is already weak and that would
|
|
# make the sum/product weak as well.
|
|
ltl2tgba "$r_f" -D --parity='min odd' | autfilt --dualize --gsa > r.hoa
|
|
# Streett & Streett
|
|
autfilt r.hoa --name="($l_f)&!($r_f)" --product=l.hoa -S > and.hoa
|
|
autfilt -q --acceptance-is=Streett-like and.hoa
|
|
# Streett | Streett
|
|
autfilt r.hoa --name="($l_f)|!($r_f)" --product-or=l.hoa -S > or.hoa
|
|
autfilt -q -v --acceptance-is=Streett-like or.hoa
|
|
|
|
autcross --language-preserved --verbose -F or.hoa -F and.hoa \
|
|
'autfilt %H --stats=%M | ltl2tgba >%O' \
|
|
'autfilt --cobuchi' 'autfilt --cobuchi -D'
|
|
done <r_formulas
|
|
done <l_formulas
|