00001 package edu.ksu.cis.bandera.specification.nnf.ltl;
00002
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004 * Bandera, a Java(TM) analysis and transformation toolkit *
00005 * Copyright (C) 1998-2001 SAnToS Laboratories (santos@cis.ksu.edu) *
00006
00007 * All rights reserved. *
00008 * *
00009 * This work was done as a project in the SAnToS Laboratory, *
00010 * Department of Computing and Information Sciences, Kansas State *
00011 * University, USA (http://www.cis.ksu.edu/santos). *
00012 * It is understood that any modification not identified as such is *
00013 * not covered by the preceding statement. *
00014 * *
00015 * This work is free software; you can redistribute it and/or *
00016 * modify it under the terms of the GNU Library General Public *
00017 * License as published by the Free Software Foundation; either *
00018 * version 2 of the License, or (at your option) any later version. *
00019 * *
00020 * This work is distributed in the hope that it will be useful, *
00021 * but WITHOUT ANY WARRANTY; without even the implied warranty of *
00022 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU *
00023 * Library General Public License for more details. *
00024 * *
00025 * You should have received a copy of the GNU Library General Public *
00026 * License along with this toolkit; if not, write to the *
00027 * Free Software Foundation, Inc., 59 Temple Place - Suite 330, *
00028 * Boston, MA 02111-1307, USA. *
00029 * *
00030 * Java is a trademark of Sun Microsystems, Inc. *
00031 * *
00032 * To submit a bug report, send a comment, or get the latest news on *
00033 * this project and other SAnToS projects, please visit the web-site *
00034 * http://www.cis.ksu.edu/santos *
00035 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
00036 //package NNF;
00037 import java.io.*;
00038
00039 public class Node {
00040 int token;
00041 String atom_value;
00042 Node left=null;
00043 Node right=null;
00044
00045
00046
00047 public Node(int t, Node n) {
00048 token=t;
00049 left=n;
00050 }
00051 public Node(int t, Node l,Node r) {
00052 token=t;
00053 left=l;
00054 right=r;
00055 }
00056 public Node(int t, String s) {
00057 token=t;
00058 atom_value=s;
00059 }
00060 /* print ltl tree */
00061 public void ltlprint(StringWriter sw) {
00062 switch (token)
00063 {
00064 case sym.ATOM: sw.write(atom_value);break;
00065 case sym.OR: sw.write("(");left.ltlprint(sw);
00066 sw.write(" || ");right.ltlprint(sw);
00067 sw.write(")");break;
00068 case sym.AND: sw.write("(");left.ltlprint(sw);
00069 sw.write(" && ");right.ltlprint(sw);
00070 sw.write(")");break;
00071 case sym.NOT: sw.write("!");left.ltlprint(sw);
00072 sw.write("");break;
00073 case sym.F: sw.write("<>(");left.ltlprint(sw);
00074 sw.write(")");break;
00075 case sym.X: sw.write("X(");left.ltlprint(sw);
00076 sw.write(")");break;
00077 case sym.G: sw.write("[](");left.ltlprint(sw);
00078 sw.write(")");break;
00079 case sym.UNTIL:sw.write("(");left.ltlprint(sw);
00080 sw.write(" U");
00081 right.ltlprint(sw);sw.write(")");break;
00082 default: sw.write("Error : bad node type");break;
00083 }
00084 return;
00085 }
00086 public void nnf()
00087 {
00088 Node tmp_left, tmp_right;
00089 switch (token)
00090 {
00091 case sym.E :
00092 case sym.A :
00093 case sym.F :
00094 case sym.X :
00095 case sym.G :
00096 left.nnf();
00097 break;
00098 case sym.UNTIL :
00099 case sym.OR :
00100 case sym.AND :
00101 left.nnf();
00102 right.nnf();
00103 break;
00104 case sym.NOT :
00105 /* All of the real work happens here */
00106 switch (left.token)
00107 {
00108 case sym.E :
00109 /* !Ep => A!p */
00110 token = sym.A;
00111 left.token = sym.NOT;
00112 nnf();
00113 break;
00114 case sym.A :
00115 /* !Ap => E!p */
00116 token = sym.E;
00117 left.token = sym.NOT;
00118 nnf();
00119 break;
00120 case sym.F :
00121 /* !Fp => G!p */
00122 token = sym.G;
00123 left.token = sym.NOT;
00124 nnf();
00125 break;
00126 case sym.X :
00127 /* !Xp => X!p */
00128 token = sym.X;
00129 left.token = sym.NOT;
00130 nnf();
00131 break;
00132 case sym.G :
00133 /* !Gp => F!p */
00134 token = sym.F;
00135 left.token = sym.NOT;
00136 nnf();
00137 break;
00138 case sym.UNTIL :
00139 /* ![pUq] => [!q U (!p & !q)] | G!q */
00140 /* what about V? */
00141 /* ![pUq] => [!p V !q] */
00142 token = sym.OR;
00143 tmp_left = new Node(sym.UNTIL, new Node(sym.NOT, left.right), new Node(sym.AND, new Node(sym.NOT, left.left), new Node(sym.NOT, left.right)));
00144 tmp_right = new Node(sym.G, new Node(sym.NOT, left.right));
00145 left = tmp_left;
00146 right = tmp_right;
00147 nnf();
00148 break;
00149 case sym.OR :
00150 /* !(p | q) => (!p & !q) */
00151 token = sym.AND;
00152 tmp_left = new Node(sym.NOT, left.left);
00153 tmp_right = new Node(sym.NOT, left.right);
00154 left = tmp_left;
00155 right = tmp_right;
00156 nnf();
00157 break;
00158 case sym.AND :
00159 /* !(p & q) => (!p | !q) */
00160 token = sym.OR;
00161 tmp_left = new Node(sym.NOT, left.left);
00162 tmp_right = new Node(sym.NOT, left.right);
00163 left = tmp_left;
00164 right = tmp_right;
00165 nnf();
00166 break;
00167 case sym.NOT :
00168 /* !!p == p */
00169 token = left.left.token;
00170 tmp_left = left.left.left;
00171 tmp_right = left.left.right;
00172 atom_value = left.left.atom_value;
00173 left = tmp_left;
00174 right = tmp_right;
00175 nnf();
00176 break;
00177 case sym.ATOM :
00178 /* !a == !a */
00179 break;
00180 }
00181 break;
00182 case sym.ATOM :
00183 break;
00184 default :
00185 System.out.println("Error : bad node type encountered in nnf");
00186 }
00187 }
00188 /* print tree */
00189 public void print() {
00190 switch (token)
00191 {
00192 case sym.ATOM: System.out.print(atom_value);break;
00193 case sym.OR: System.out.print("(");left.print();
00194 System.out.print(" | ");right.print();
00195 System.out.print(")");break;
00196 case sym.AND: System.out.print("(");left.print();
00197 System.out.print(" & ");right.print();
00198 System.out.print(")");break;
00199 case sym.NOT: System.out.print("!(");left.print();
00200 System.out.print(")");break;
00201 case sym.E: System.out.print("E(");left.print();
00202 System.out.print(")");break;
00203 case sym.A: System.out.print("A(");left.print();
00204 System.out.print(")");break;
00205 case sym.F: System.out.print("F(");left.print();
00206 System.out.print(")");break;
00207 case sym.X: System.out.print("X(");left.print();
00208 System.out.print(")");break;
00209 case sym.G: System.out.print("G(");left.print();
00210 System.out.print(")");break;
00211 case sym.UNTIL:System.out.print("[");left.print();
00212 System.out.print(" U");
00213 right.print();System.out.print("]");break;
00214 default: System.out.print("Error : bad node type");break;
00215 }
00216 return;
00217 }
00218 }
1.2.10 written by Dimitri van Heesch,
© 1997-2001