1#! /bin/sh 2# -*- coding: utf-8 -*- 3# Copyright (C) 2010-2012, 2015, 2017, 2019, 2021 Laboratoire de 4# Recherche et Développement de l'Epita (LRDE). 5# 6# This file is part of Spot, a model checking library. 7# 8# Spot is free software; you can redistribute it and/or modify it 9# under the terms of the GNU General Public License as published by 10# the Free Software Foundation; either version 3 of the License, or 11# (at your option) any later version. 12# 13# Spot is distributed in the hope that it will be useful, but WITHOUT 14# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 15# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 16# License for more details. 17# 18# You should have received a copy of the GNU General Public License 19# along with this program. If not, see <http://www.gnu.org/licenses/>. 20 21 22# Check for the constant_term visitor 23 24. ./defs || exit 1 25 26set -e 27 28cat >input<<EOF 29a,B&!xfLPSFsgopra 30a<->b,BxfLPSFsgopra 31!a,B&!xfLPSFsgopra 32!(a|b),B&xfLPSFsgopra 33F(a),&!xLPegopra 34G(a),&!xLPusopra 35a U b,&!xfLPgopra 36a U Fb,&!xLPegopra 37Ga U b,&!xLPopra 381 U a,&!xfLPegopra 39a W b,&!xfLPsopra 40a W 0,&!xfLPusopra 41a M b,&!xfLPgopra 42a M 1,&!xfLPegopra 43a R b,&!xfLPsopra 440 R b,&!xfLPusopra 45a R (b R (c R d)),&!xfLPsopra 46a U (b U (c U d)),&!xfLPgopra 47a W (b W (c W d)),&!xfLPsopra 48a M (b M (c M d)),&!xfLPgopra 49Fa -> Fb,xLPopra 50Ga -> Fb,xLPegopra 51Fa -> Gb,xLPusopra 52(Ga|Fc) -> Fb,xLPopra 53(Ga|Fa) -> Gb,xLPopra 54{a;c*;b}|->!Xb,&fPsopra 55{a;c*;b}|->X!b,&!fPsopra 56{a;c*;b}|->!Fb,&Psopra 57{a;c*;b}|->G!b,&!Psopra 58{a;c*;b}|->!Gb,&Pra 59{a;c*;b}|->F!b,&!Pra 60{a;c*;b}|->GFa,&!Pra 61{a;c*;b}|->FGa,&!Pa 62{a[+];c[+];b*}|->!Fb,&Psopra 63{a*;c[+];b*}|->!Fb,&xPsopra 64{a[+];c*;b[+]}|->G!b,&!Psopra 65{a*;c[+];b[+]}|->!Gb,&Pra 66{a[+];c*;b[+]}|->F!b,&!Pra 67{a[+];c[+];b*}|->GFa,&!Pra 68{a*;c[+];b[+]}|->FGa,&!Pa 69{a;c;b|(d;e)}|->!Xb,&fPFsgopra 70{a;c;b|(d;e)}|->X!b,&!fPFsgopra 71{a;c;b|(d;e)}|->!Fb,&Psopra 72{a;c;b|(d;e)}|->G!b,&!Psopra 73{a;c;b|(d;e)}|->!Gb,&Pgopra 74{a;c;b|(d;e)}|->F!b,&!Pgopra 75{a;c;b|(d;e)}|->GFa,&!Pra 76{a;c;b|(d;e)}|->FGa,&!Ppa 77{a[+] && c[+]}|->!Xb,&fPsopra 78{a[+] && c[+]}|->X!b,&!fPsopra 79{a[+] && c[+]}|->!Fb,&xPsopra 80{a[+] && c[+]}|->G!b,&!xPsopra 81{a[+] && c[+]}|->!Gb,&xPra 82{a[+] && c[+]}|->F!b,&!xPra 83{a[+] && c[+]}|->GFa,&!xPra 84{a[+] && c[+]}|->FGa,&!xPa 85{a;c*;b}<>->!Gb,&Pgopra 86{a;c*;b}<>->F!b,&!Pgopra 87{a;c*;b}<>->FGb,&!Ppa 88{a;c*;b}<>->!GFb,&Ppa 89{a;c*;b}<>->GFb,&!Pa 90{a;c*;b}<>->!FGb,&Pa 91{a*;c[+];b[+]}<>->!FGb,&Pa 92{a;c|d;b}<>->!Gb,&Pgopra 93{a;c|d;b}<>->G!b,&!Psopra 94{a;c|d;b}<>->FGb,&!Ppa 95{a;c|d;b}<>->!GFb,&Ppa 96{a;c|d;b}<>->GFb,&!Pra 97{a;c|d;_b}<>->!FGb,&Pr 98# Equivalent to a&b&c&d 99{a:b:c:d}!,B&!xfLPSFsgopra 100a&b&c&d,B&!xfLPSFsgopra 101(Xa <-> XXXc) U (b & Fe),LPgopra 102(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopra 103(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopra 104(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b)),LPeopra 105(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b)),LPuopra 106(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b)),LPpa 107(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b)),LPra 108(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b)),LPpa 109(!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b)),LPupa 110(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b)),LPra 111(!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b)),LPera 112(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb)),LPepa 113(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb)),LPa 114(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb)),LPura 115(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb)),LPa 116GFa M GFb,&!xLPeua 117FGa M FGb,&!xLPeupa 118Fa M GFb,&!xLPera 119GFa W GFb,&!xLPeura 120FGa W FGb,&!xLPeua 121Ga W FGb,&!xLPupa 122Ga W b,&!xLPsopra 123Fa M b,&!xLPgopra 124{a;b*;c},&!fPsopra 125{a;b*;c}!,&!fPgopra 126# The negative normal form is {a;b*;c}[]->1 127!{a;b*;c}!,&fPsopra 128{a;b*;p112}[]->0,&!fPsopra 129!{a;b*;c.2},&!fPgopr 130!{a[+];b*;c[+]},&!fPgopra 131!{a[+];b*;c*},&!xfPgopra 132{a[+];b*;c[+]},&!fPsopra 133{a[+] && b || c[+]},&!fPsopra 134{a[+] && b[+] || c[+]},&!xfPsopra 135{p[+]:p[+]},&!xfPsoprla 136(!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla 137{b[+][:*0..3]},&!fPsopra 138{a->c[*]},xfPsopra 139{(a[+];b*);c*}<>->d,&!xfPgopra 140{first_match(a[+];b*);c*}<>->d,&!fPgopra 141EOF 142 143run 0 ../kind input 144