#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
# et Developpement 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 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/>.


# 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)'

  run 0 $x 'a <-> !a' '0'
  run 0 $x 'a <-> a' '1'
  run 0 $x 'a ^ a' '0'
  run 0 $x 'a ^ !a' '1'

  run 0 $x 'GFa | FGa' 'GFa'
  run 0 $x 'XXGa | GFa' 'GFa'
  run 0 $x 'GFa & FGa' 'FGa'
  run 0 $x 'XXGa & GFa' 'XXGa'

  # Basic reductions
  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 'XGF(f)' 'GF(f)'

  case $x in
   *tau*);;
   *)
     run 0 $x 'G(true)' 'true'
     run 0 $x 'G(false)' 'false'

     run 0 $x 'a M 1' 'Fa'
     run 0 $x 'a W 0' 'Ga'
     run 0 $x '1 U a' 'Fa'
     run 0 $x '0 R a' 'Ga'

     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 'GF(a | Xb)' 'GF(a | b)'
     run 0 $x 'GF(a | Fb)' 'GF(a | b)'
     run 0 $x 'GF(Xa | Fb)' 'GF(a | b)'
     run 0 $x 'FG(a & Xb)' 'FG(a & b)'
     run 0 $x 'FG(a & Gb)' 'FG(a & b)'
     run 0 $x 'FG(Xa & Gb)' 'FG(a & b)'

     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 'X(a) M X(b)' 'X(a M b)'
     run 0 $x 'X(a) W X(b)' 'X(a W b)'
     run 0 $x 'X(a) M b' 'b & X(b U a)'
     run 0 $x 'X(a) R b' 'b & X(b W a)'
     run 0 $x 'X(a) U b' 'b | X(b M a)'
     run 0 $x 'X(a) W b' 'b | X(b R a)'

     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 'Xa & FGb' 'X(a & FGb)'
     run 0 $x 'Xa | FGb' 'X(a | FGb)'
     run 0 $x 'Xa & GFb' 'X(a & GFb)'
     run 0 $x 'Xa | GFb' 'X(a | 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))'
     # FIXME: Don't we want the opposite rewriting?
     # rewriting Fa & GFb as  F(a & GFb) seems better, but
     # it not clear how that scales to Fa & Fb & GFc...
     run 0 $x 'Fa & GFb' 'Fa & GFb'
     run 0 $x 'G(a | GFb)' 'Ga | 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 'GFa <=> GFb' 'G(Fa&Fb)|FG(!a&!b)'

     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'

     run 0 $x 'GFGa' 'FGa'
     run 0 $x 'b R Ga' 'Ga'
     run 0 $x 'b R FGa' 'FGa'

     run 0 $x 'G(!a M a) M 1' '0'
     run 0 $x 'G(!a M a) U 1' '1'
     run 0 $x 'a R (!a M a)' '0'
     run 0 $x 'a W (!a M a)' 'Ga'

     run 0 $x 'F(a U b)' 'Fb'
     run 0 $x 'F(a M b)' 'F(a & b)'
     run 0 $x 'G(a R b)' 'Gb'
     run 0 $x 'G(a W b)' 'G(a | b)'

     run 0 $x 'Fa W Fb' 'F(GFa | b)'
     run 0 $x 'Ga M Gb' 'FGa & Gb'

     run 0 $x 'a & XGa' 'Ga'
     run 0 $x 'a & XG(a&b)' '(XGb)&(Ga)'
     run 0 $x 'a & b & XG(a&b)'  'G(a&b)'
     run 0 $x 'a & b & X(Ga&Gb)'  'G(a&b)'
     run 0 $x 'a & b & XGa &XG(b)'  'G(a&b)'
     run 0 $x 'a & b & XGa & XGc' 'b & Ga & XGc'
     run 0 $x 'a & b & X(G(a&d) & b) & X(Gc)' 'b & Ga & X(b & G(c&d))'
     run 0 $x 'a|b|c|X(F(a|b)|F(c)|Gd)' 'F(a|b|c)|XGd'
     run 0 $x 'b|c|X(F(a|b)|F(c)|Gd)' 'b|c|X(F(a|b|c)|Gd)'

     run 0 $x 'a | (Xa R b) | c' '(b W a) | c'
     run 0 $x 'a | (Xa M b) | c' '(b U a) | c'
     run 0 $x 'a | (Xa M b) | (Xa R c)' '(b U a) | (c W a)'
     run 0 $x 'a | (Xa M b) | XF(a)' 'Fa'
     run 0 $x 'a | (Xa R b) | XF(a)' '(b W a) | Fa' # Gb | Fa ?
     run 0 $x 'a & (Xa W b) & c' '(b R a) & c'
     run 0 $x 'a & (Xa U b) & c' '(b M a) & c'
     run 0 $x 'a & (Xa W b) & (Xa U c)' '(b R a) & (c M a)'
     run 0 $x 'a & (Xa W b) & XGa' 'Ga'
     run 0 $x 'a & (Xa U b) & XGa' '(b M a) & Ga'  # Fb & Ga ?
     run 0 $x 'a|(c&b&X((b&c) U a))|d' '((b&c) U a)|d'
     run 0 $x 'a|(c&X((b&c) W a)&b)|d' '((b&c) W a)|d'
     run 0 $x 'a&(c|b|X((b|c) M a))&d' '((b|c) M a)&d'
     run 0 $x 'a&(c|X((b|c) R a)|b)&d' '((b|c) R a)&d'
     run 0 $x 'g R (f|g|h)' '(f|h) W g'
     run 0 $x 'g M (f|g|h)' '(f|h) U g'
     run 0 $x 'g U (f&g&h)' '(f&h) M g'
     run 0 $x 'g W (f&g&h)' '(f&h) R g'

     # Syntactic implication
     run 0 $x '(a & b) R (a R c)' '(a & b)R c'
     run 0 $x 'a R ((a & b) R c)' '(a & b)R c'
     run 0 $x 'a R ((a & b) M c)' '(a & b)M c'
     run 0 $x 'a M ((a & b) M c)' '(a & b)M c'
     run 0 $x '(a & b) M (a R c)' '(a & b)M c'
     run 0 $x '(a & b) M (a M c)' '(a & b)M c'

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

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

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

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

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

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


     # Eventuality and universality class reductions
     run 0 $x 'Fa M b' 'Fa & b'
     run 0 $x 'GFa M b' 'GFa & b'

     run 0 $x 'Fa|Xb|GFc' 'Fa | X(b|GFc)'
     run 0 $x 'Fa|GFc' 'F(a|GFc)'
     run 0 $x 'FGa|GFc' 'F(Ga|GFc)'
     run 0 $x 'Ga&Xb&FGc' 'Ga & X(b&FGc)'
     run 0 $x 'Ga&Xb&GFc' 'Ga & X(b&GFc)'
     run 0 $x 'Ga&GFc' 'G(a&Fc)'
     run 0 $x 'G(a|b|GFc|GFd|FGe|FGf)' 'G(a|b)|GF(c|d)|F(Ge|Gf)'
     run 0 $x 'G(a|b)|GFc|GFd|FGe|FGf' 'G(a|b)|GF(c|d)|F(Ge|Gf)'
     run 0 $x 'X(a|b)|GFc|GFd|FGe|FGf' 'X(a|b|GF(c|d)|F(Ge|Gf))'
     run 0 $x 'Xa&Xb&GFc&GFd&Ge' 'X(a&b&G(Fc&Fd))&Ge'

     # F comes in front when possible...
     run 0 $x 'GFc|GFd|FGe|FGf' 'F(GF(c|d)|Ge|Gf)'
     run 0 $x 'G(GFc|GFd|FGe|FGf)' 'F(GF(c|d)|Ge|Gf)'

     # Because reduccmp will translate the formula,
     # this also check for an old bug in ltl2tgba_fm.
     run 0 $x '{(c&!c)[->0..1]}!' '0'

     # Tricky case that used to break the translator,
     # because it was translating closer on-the-fly
     # without pruning the rational automaton.
     run 0 $x '{(c&!c)[=2]}' '0'

     run 0 $x '{a && b && c*} <>-> d' 'a&b&c&d'
     run 0 $x '{a && b && c[*1..3]} <>-> d' 'a&b&c&d'
     run 0 $x '{a && b && c[->0..2]} <>-> d' 'a&b&c&d'
     run 0 $x '{a && b && c[+]} <>-> d' 'a&b&c&d'
     run 0 $x '{a && b && c[=1]} <>-> d' 'a&b&c&d'
     run 0 $x '{a && b && d[=2]} <>-> d' '0'
     run 0 $x '{a && b && d[*2..]} <>-> d' '0'
     run 0 $x '{a && b && d[->2..4]} <>-> d' '0'
     run 0 $x '{a && { c* : b* : (g|h)*}} <>-> d' 'a & c & b & (g | h) & d'
     run 0 $x '{a && {b;c}} <>-> d' '0'
     run 0 $x '{a && {(b;c):e}} <>-> d' '0'
     run 0 $x '{a && {b*;c*}} <>-> d' '{a && {b*|c*}} <>-> d' # until better
     run 0 $x '{a && {(b*;c*):e}} <>-> d' '{a && {b*|c*} && e} <>-> d' # idem
     run 0 $x '{a && {b*;c}} <>-> d' 'a & c & d'
     run 0 $x '{a && {(b*;c):e}} <>-> d' 'a & c & d & e'
     run 0 $x '{a && {b;c*}} <>-> d' 'a & b & d'
     run 0 $x '{a && {(b;c*):e}} <>-> d' 'a & b & d & e'
     run 0 $x '{{{b1;r1*}&&{b2;r2*}};c}' 'b1&b2&X{{r1*&&r2*};c}'
     run 0 $x '{{b1:r1*}&&{b2:r2*}}' '{{b1&&b2}:{r1*&&r2*}}'
     run 0 $x '{{r1*;b1}&&{r2*;b2}}' '{{r1*&&r2*};{b1&&b2}}'
     run 0 $x '{{r1*:b1}&&{r2*:b2}}' '{{r1*&&r2*}:{b1&&b2}}'
     run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \
              '{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}'
     run 0 $x '{{{b1;r1*}&{b2;r2*}};c}' 'b1&b2&X{{r1*&r2*};c}'
     run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1&&b2}:{r1*&r2*}}'
     run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*&r2*};{b1&&b2}}'
     run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*&r2*}:{b1&&b2}}'
     run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}}' \
              '{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}'
     run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'
     run 0 $x '{a&b&c*}|->!Xb' '(X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))'
     run 0 $x '{[*]}[]->b' 'Gb'
     run 0 $x '{a;[*]}[]->b' 'Gb | !a'
     run 0 $x '{[*];a}[]->b' 'G(b | !a)'
     run 0 $x '{a;b;[*]}[]->c' '!a | X(!b | Gc)'
     run 0 $x '{a;a;[*]}[]->c' '!a | X(!a | Gc)'
     run 0 $x '{s[*]}[]->b' 'b W !s'
     run 0 $x '{s[+]}[]->b' 'b W !s'
     run 0 $x '{s[*2..]}[]->b' '!s | X(b W !s)'
     run 0 $x '{a;b*;c;d*}[]->e' '!a | X(!b R ((e & X(e W !d)) | !c))'
     run 0 $x '{a:b*:c:d*}[]->e' '!a | ((!c | (e W !d)) W !b)'
     run 0 $x '{a|b*|c|d*}[]->e' '(e | !(a | c)) & (e W !b) & (e W !d)'
     run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} []-> f' \
	      '{{[*0] | a};b;{[*0] | a}} []-> X((f & X(f W !e)) | !c)'

     run 0 $x '{a&b&c*}<>->!Xb' '(a & b & X!b) | (a & b & c & X(c U !b))'
     run 0 $x '{[*]}<>->b' 'Fb'
     run 0 $x '{a;[*]}<>->b' 'Fb & a'
     run 0 $x '{[*];a}<>->b' 'F(a & b)'
     run 0 $x '{a;b;[*]}<>->c' 'a & X(b & Fc)'
     run 0 $x '{a;a;[*]}<>->c' 'a & X(a & Fc)'
     run 0 $x '{s[*]}<>->b' 'b M s'
     run 0 $x '{s[+]}<>->b' 'b M s'
     run 0 $x '{s[*2..]}<>->b' 's & X(b M s)'
     run 0 $x '{a;b*;c;d*}<>->e' 'a & X(b U (c & (e | X(e M d))))'
     run 0 $x '{a:b*:c:d*}<>->e' 'a & ((c & (e M d)) M b)'
     run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)'
     run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} <>-> f' \
	      '{{[*0] | a};b;{[*0] | a}} <>-> X(c & (f | X(f M e)))'
     run 0 $x '{a;b[*];c[*];e;f*}' 'a & X(b W (c W e))'
     run 0 $x '{a;b*;(a* && (b;c));c*}' 'a & X(b W {a[*] && {b;c}})'
     run 0 $x '{a;a;b[*2..];b}' 'a & X(a & X(b & X(b & Xb)))'
     run 0 $x '!{a;a;b[*2..];b}' '!a | X(!a | X(!b | X(!b | X!b)))'
     run 0 $x '!{a;b[*];c[*];e;f*}' '!a | X(!b M (!c M !e))'
     run 0 $x '!{a;b*;(a* && (b;c));c*}' '!a | X(!b M !{a[*] && {b;c}})'
     run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)'
     run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)'
     run 0 $x '(Xc R b) & (Xc W 0)' 'b & XGc'

     # not reduced
     run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \
              '{a;(b[*2..4];c*;([*0]+{d;e}))*}!'
     run 0 $x '{((a*;b)+[*0])[*4..6]}!' '{((a*;b))[*0..6]}!'
     run 0 $x '{c[*];e[*]}[]-> a' '{c[*];e[*]}[]-> a'
     ;;
  esac

  run 0 $x 'a R (b W G(c))' 'a R (b W G(c))' #not reduced

  run 0 $x 'a M ((a&b) R c)' 'a M ((a&b) R c)' #not reduced.
  run 0 $x '(a&b) W (a U c)' '(a&b) W (a U c)' #not reduced.

  # Eventuality and universality class reductions
  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 'a U XXXFb' 'XXXFb'
done