#! /bin/sh
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# 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 2 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 Spot; see the file COPYING.  If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.


# Check LTL reductions

. ./defs || exit 1

for x in ../reduccmp ../reductaustr; do

  # No reduction
  run 0 $x 'a U b' 'a U b'
  run 0 $x 'a R b' 'a R b'
  run 0 $x 'a & b' 'a & b'
  run 0 $x 'a | b' 'a | b'
  run 0 $x 'a & (a U b)' 'a & (a U b)'
  run 0 $x 'a | (a U b)' 'a | (a U b)'

  # Syntactic reduction
  run 0 $x 'a & (!b R !a)' 'false'
  run 0 $x '(!b R !a) & a' 'false'
  run 0 $x 'a & (!b R !a) & c' 'false'
  run 0 $x 'c & (!b R !a) & a' 'false'

  run 0 $x 'a & (!b M !a)' 'false'
  run 0 $x '(!b M !a) & a' 'false'
  run 0 $x 'a & (!b M !a) & c' 'false'
  run 0 $x 'c & (!b M !a) & a' 'false'

  run 0 $x 'a & (b U a)' 'a'
  run 0 $x '(b U a) & a' 'a'
  run 0 $x 'a | (b U a)' '(b U a)'
  run 0 $x '(b U a) | a' '(b U a)'
  run 0 $x 'a U (b U a)' '(b U a)'

  run 0 $x 'a & (b W a)' 'a'
  run 0 $x '(b W a) & a' 'a'
  run 0 $x 'a | (b W a)' '(b W a)'
  run 0 $x '(b W a) | a' '(b W a)'
  run 0 $x 'a W (b W a)' '(b W a)'

  run 0 $x 'a & (b U a) & a' 'a'
  run 0 $x 'a & (b U a) & a' 'a'
  run 0 $x 'a | (b U a) | a' '(b U a)'
  run 0 $x 'a | (b U a) | a' '(b U a)'
  run 0 $x 'a U (b U a)' '(b U a)'


  # Basics reduction
  run 0 $x 'X(true)' 'true'
  run 0 $x 'X(false)' 'false'
  run 0 $x 'F(true)' 'true'
  run 0 $x 'F(false)' 'false'
  run 0 $x 'G(true)' 'true'
  run 0 $x 'G(false)' 'false'

  run 0 $x 'XGF(f)' 'GF(f)'

  case $x in
   *tau*);;
   *)
     run 0 $x 'G(a R b)' 'G(b)'

     run 0 $x 'FX(a)' 'XF(a)'
     run 0 $x 'GX(a)' 'XG(a)'

     run 0 $x 'X(a) U X(b)' 'X(a U b)'
     run 0 $x 'X(a) R X(b)' 'X(a R b)'
     run 0 $x 'Xa & Xb' 'X(a & b)'
     run 0 $x 'Xa | Xb' 'X(a | b)'

     run 0 $x '(a U b) & (c U b)' '(a & c) U b'
     run 0 $x '(a R b) & (a R c)' 'a R (b & c)'
     run 0 $x '(a U b) | (a U c)' 'a U (b | c)'
     run 0 $x '(a R b) | (c R b)' '(a | c) R b'

     run 0 $x 'X(a & GFb)' 'Xa & GFb'
     run 0 $x 'X(a | GFb)' 'Xa | GFb'
     # The following is not reduced to F(a) & GFb.  because
     # (1) is does not help the translate the formula into a
     #     smaller automaton, and ...
     run 0 $x 'F(a & GFb)' 'F(a & GFb)'
     # (2) ... it would hinder this useful reduction (that helps to
     #     produce a smaller automaton)
     run 0 $x 'F(f1 & GF(f2)) | F(a & GF(b))' 'F((f1&GFf2)|(a&GFb))'
     run 0 $x 'G(a | GFb)' 'Ga | GFb'

     run 0 $x 'X(a & GFb & c)' 'X(a & c) & GFb'
     run 0 $x 'X(a | GFb | c)' 'X(a | c) | GFb'
     # The following is not reduced to F(a & c) & GF(b) for the same
     # reason as above.
     run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)'
     run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb'

     run 0 $x 'Gb W a' 'Gb|a'
     run 0 $x 'Fb M Fa' 'Fa & Fb'

     run 0 $x 'a U (b | G(a) | c)' 'a W (b | c)'
     run 0 $x 'a U (G(a))' 'Ga'
     run 0 $x '(a U b) | (a W c)' 'a W (b | c)'
     run 0 $x '(a U b) | Ga' 'a W b'

     run 0 $x 'a R (b & F(a) & c)' 'a M (b & c)'
     run 0 $x 'a R (F(a))' 'Fa'
     run 0 $x '(a R b) & (a M c)' 'a M (b & c)'
     run 0 $x '(a R b) & Fa' 'a M b'

     run 0 $x '(a U b) & (c W b)' '(a & c) U b'
     run 0 $x '(a W b) & (c W b)' '(a & c) W b'
     run 0 $x '(a R b) | (c M b)' '(a | c) R b'
     run 0 $x '(a M b) | (c M b)' '(a | c) M b'

     run 0 $x '(a R b) | Gb' 'a R b'
     run 0 $x '(a M b) | Gb' 'a R b'
     run 0 $x '(a U b) & Fb' 'a U b'
     run 0 $x '(a W b) & Fb' 'a U b'
     run 0 $x '(a M b) | Gb | (c M b)' '(a | c) R b'
     ;;
  esac

  # Eventuality and universality class reduction
  run 0 $x 'FFa' 'Fa'
  run 0 $x 'FGFa' 'GFa'
  run 0 $x 'b U Fa' 'Fa'
  run 0 $x 'b U GFa' 'GFa'
  run 0 $x 'Ga' 'Ga'
  run 0 $x 'GFGa' 'FGa'
  run 0 $x 'b R Ga' 'Ga'
  run 0 $x 'b R FGa' 'FGa'
done