#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et Dévelopement to
# 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 .
# Check for the constant_term visitor
. ./defs || exit 1
set -e
t()
{
cat > tmp.$$
run 0 ../ltlrel "`head -n 1 tmp.$$`" > out.$$
sed 1d tmp.$$ > exp.$$
diff out.$$ exp.$$
}
t < a & c
p1 -> b
EOF
t < a
p1 -> b
p2 -> c
EOF
t < b
p1 -> a | c
EOF
t < h | i
p1 -> d & e
p2 -> !c
p3 -> f
EOF
t < b
p0
p0 -> a <-> b
EOF
t < b) & X(b -> c)
(p0 <-> p1) & X(p1 -> p2)
p0 -> a
p1 -> b
p2 -> c
EOF