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