#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) by the Spot authors, see the AUTHORS file for details.
#
# 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/>.


# More checks for ltlfilt

. ./defs || exit 1

set -e

cat >formulas.ltl <<EOF
G(i1 <-> Xo1)
F(i1 xor i2) <-> F(o1)
i1 <-> F(o1 xor o2)
F(i1) <-> G(o2)
EOF

ltlsynt --ins=i1,i2 -F formulas.ltl -f 'o1 & F(i1 <-> o2)' -q \
        --csv-with-formula=out.csv &&\
    exit 2
test $? -eq 1 || exit 2

test -z "$PYTHON" && exit 77

cat >test.py <<EOF
import sys
try:
  import pandas
  import numpy as np
except ImportError:
  sys.exit(77)

x = pandas.read_csv("out.csv")
x.to_csv('filtered.csv',
         columns=('source', 'formula', 'algo',
                  'realizable', 'sum_strat_states'),
         index=False)
EOF

# will exit 77 if panda is not installed
$PYTHON test.py

cat >expected <<EOF
source,formula,algo,realizable,sum_strat_states
formulas.ltl:1,G(i1 <-> Xo1),lar,1,3
formulas.ltl:2,F(i1 xor i2) <-> Fo1,lar,1,2
formulas.ltl:3,i1 <-> F(o1 xor o2),lar,1,3
formulas.ltl:4,Fi1 <-> Go2,lar,0,0
,o1 & F(i1 <-> o2),lar,1,2
EOF

diff filtered.csv expected

# ltlfilt should be able to read the second column
mv filtered.csv input.csv
ltlsynt --ins=i1,i2 -F input.csv/-2 --csv-with-formula=out.csv -q && exit 2
test $? -eq 1
$PYTHON test.py
cat >expected <<EOF
source,formula,algo,realizable,sum_strat_states
input.csv:2,G(i1 <-> Xo1),lar,1,3
input.csv:3,F(i1 xor i2) <-> Fo1,lar,1,2
input.csv:4,i1 <-> F(o1 xor o2),lar,1,3
input.csv:5,Fi1 <-> Go2,lar,0,0
input.csv:6,o1 & F(i1 <-> o2),lar,1,2
EOF
diff filtered.csv expected

grep -v 0,0 filtered.csv >input.csv
ltlsynt -F input.csv/-2 --csv-with-formula=out.csv -q
$PYTHON test.py
cat >expected <<EOF
source,formula,algo,realizable,sum_strat_states
input.csv:2,G(i1 <-> Xo1),lar,1,3
input.csv:3,F(i1 xor i2) <-> Fo1,lar,1,2
input.csv:4,i1 <-> F(o1 xor o2),lar,1,3
input.csv:5,o1 & F(i1 <-> o2),lar,1,2
EOF
diff filtered.csv expected

ltlsynt -F input.csv/-2 --csv=out.csv -q
cut out.csv -d, -f1,2,3 >filtered.csv
cat >expected <<EOF
source,subspecs,algo
"input.csv:2",1,lar
"input.csv:3",1,lar
"input.csv:4",1,lar
"input.csv:5",1,lar
EOF
diff filtered.csv expected