61 lines
1.7 KiB
Bash
Executable file
61 lines
1.7 KiB
Bash
Executable file
#!/bin/sh
|
|
# -*- coding: utf-8 -*-
|
|
# Copyright (C) 2017 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/>.
|
|
|
|
set -e
|
|
|
|
# Skip this test if ltl2dstar is not installed.
|
|
(ltl2dstar --version) || exit 77
|
|
|
|
DIR=dca.dir
|
|
mkdir -p $DIR
|
|
|
|
cat >$DIR/ba_formulas << 'EOF'
|
|
FG((Xc & XXa) <-> !(b xor (c M b)))
|
|
F!FGFb
|
|
XF(b & Ga)
|
|
FG(F(b R Fc) R Gc)
|
|
(!c M F(b M Ga)) W (b U a)
|
|
(c xor Gb) M 1
|
|
X!Gc M ((Fb R a) M 1)
|
|
!a | F(b W 0)
|
|
F(!a -> Gb)
|
|
(Gb <-> X(b W Xb)) M (b xor !c)
|
|
(c R (X!c W Fb)) M 1
|
|
!a -> (FX!(0 R F(b | c)) W c)
|
|
XF((!c R a) W !Fb)
|
|
(!a <-> !(c <-> Gb)) M 1
|
|
((0 R a) M c) M ((b xor Fb) M F(b -> a))
|
|
EOF
|
|
cat >$DIR/dsa_formulas <<'EOF'
|
|
(!b U b) U X(!a -> Fb)
|
|
1 U (a xor b)
|
|
X(!(!b | (a M b)) -> XXa)
|
|
!Gb
|
|
F(XF!a & (Fb U !a))
|
|
EOF
|
|
while read ba_f; do
|
|
../run "$srcdir/dca.py" "$ba_f" > ba
|
|
while read dsa_f; do
|
|
ltldo -f "$dsa_f" "ltl2dstar --automata=streett\
|
|
--ltl2nba=spin:ltl2tgba@-Ds" -H | autfilt --product=ba > $DIR/input.hoa
|
|
autfilt --dca $DIR/input.hoa > $DIR/res.hoa
|
|
autfilt $DIR/input.hoa --equivalent-to $DIR/res.hoa
|
|
done <$DIR/dsa_formulas
|
|
done <$DIR/ba_formulas
|