#! /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