#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# 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/>.

# While running some benchmark, Tomáš Babiak found that Spot took too
# much time (i.e. >1h) to translate those six formulae.  It turns out
# that the WDBA minimization was performed after the degeneralization
# algorithm, while this is not necessary (WDBA will produce a BA, so
# we may as well skip degeneralization).  Translating these formulae
# in the test-suite ensure that they don't take too much time (the
# buildfarm will timeout if it does).

. ./defs

set -e

run 0 ../tgbagraph | tee stdout

cat >expected <<EOF
p1
p2
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 0 [label="0"]
  0 -> 1 [label="p1"]
  0 -> 2 [label="p2\n{1}"]
  1 [label="1"]
  1 -> 2 [label="p1 & p2\n{0}"]
  2 [label="2"]
  2 -> 0 [label="p1 | p2\n{0,1}"]
  2 -> 1 [label="!p1 | p2"]
  2 -> 2 [label="1\n{0,1}"]
}
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 0 [label="0"]
  0 -> 1 [label="p1"]
  0 -> 2 [label="p2\n{1}"]
  1 [label="1"]
  1 -> 2 [label="p1 & p2\n{0}"]
  2 [label="2"]
  2 -> 0 [label="p1 | p2\n{0,1}"]
}
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 0 [label="0"]
  0 -> 1 [label="p1"]
  0 -> 2 [label="p2\n{1}"]
  1 [label="1"]
  1 -> 2 [label="p1 & p2\n{0}"]
  2 [label="2"]
}
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 0 [label="0"]
  0 -> 1 [label="p1"]
  0 -> 2 [label="p2\n{1}"]
  1 [label="1"]
  1 -> 2 [label="p1 & p2\n{0}"]
  2 [label="2"]
  2 -> 0 [label="p1 | p2\n{0,1}"]
  2 -> 1 [label="!p1 | p2"]
  2 -> 0 [label="1\n{0,1}"]
}
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 1 [label="p1"]
  0 -> 2 [label="p2\n{1}"]
  1 [label="1"]
  1 -> 2 [label="p1 & p2\n{0}"]
  2 [label="2"]
  2 -> 0 [label="1\n{0,1}"]
  2 -> 1 [label="!p1 | p2"]
}
digraph G {
  rankdir=LR
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 1 [label="p1"]
  0 -> 2 [label="p2\n{1}"]
  1 [label="1"]
  1 -> 2 [label="p1 & p2\n{0}"]
  2 [label="2"]
  2 -> 0 [label="1\n{0,1}"]
  2 -> 1 [label="!p1 | p2"]
  3 [label="3"]
  4 [label="4"]
  5 [label="5"]
  6 [label="6"]
  7 [label="7"]
  8 [label="8"]
  9 [label="9"]
  10 [label="10"]
  11 [label="11"]
  12 [label="12"]
  13 [label="13"]
  14 [label="14"]
  15 [label="15"]
  16 [label="16"]
  17 [label="17"]
  18 [label="18"]
  19 [label="19"]
  20 [label="20"]
  21 [label="21"]
  22 [label="22"]
  23 [label="23"]
  24 [label="24"]
  25 [label="25"]
  26 [label="26"]
  27 [label="27"]
  28 [label="28"]
  29 [label="29"]
  30 [label="30"]
  31 [label="31"]
  32 [label="32"]
  33 [label="33"]
  34 [label="34"]
  35 [label="35"]
  36 [label="36"]
  37 [label="37"]
  38 [label="38"]
  39 [label="39"]
  40 [label="40"]
  41 [label="41"]
  42 [label="42"]
  43 [label="43"]
  44 [label="44"]
  45 [label="45"]
  46 [label="46"]
  47 [label="47"]
  48 [label="48"]
  49 [label="49"]
  50 [label="50"]
  51 [label="51"]
  52 [label="52"]
  53 [label="53"]
  54 [label="54"]
  55 [label="55"]
  56 [label="56"]
  57 [label="57"]
  58 [label="58"]
  59 [label="59"]
  60 [label="60"]
  61 [label="61"]
  62 [label="62"]
  63 [label="63"]
  64 [label="64"]
  65 [label="65"]
  66 [label="66"]
  67 [label="67"]
  68 [label="68"]
  69 [label="69"]
  70 [label="70"]
  71 [label="71"]
  72 [label="72"]
  73 [label="73"]
  74 [label="74"]
  75 [label="75"]
  76 [label="76"]
  77 [label="77"]
  78 [label="78"]
  79 [label="79"]
  80 [label="80"]
  81 [label="81"]
  82 [label="82"]
  83 [label="83"]
  84 [label="84"]
  85 [label="85"]
  86 [label="86"]
  87 [label="87"]
  88 [label="88"]
  89 [label="89"]
  90 [label="90"]
  91 [label="91"]
  92 [label="92"]
  93 [label="93"]
  94 [label="94"]
  95 [label="95"]
  96 [label="96"]
  97 [label="97"]
  98 [label="98"]
  99 [label="99"]
  100 [label="100"]
  101 [label="101"]
  102 [label="102"]
}
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 2
  0 [label="s1"]
  1 [label="s2"]
  2 [label="s3"]
}
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="s3"]
}
EOF

diff stdout expected