0001: //
0002: // Copyright (C) 2005 United States Government as represented by the
0003: // Administrator of the National Aeronautics and Space Administration
0004: // (NASA). All Rights Reserved.
0005: //
0006: // This software is distributed under the NASA Open Source Agreement
0007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
0008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
0009: // directory tree for the complete NOSA document.
0010: //
0011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
0012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
0013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
0014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
0015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
0016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
0017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
0018: //
0019:
0020: // Written by Dimitra Giannakopoulou, 19 Jan 2001
0021: // Parser by Flavio Lerda, 8 Feb 2001
0022: // Parser extended by Flavio Lerda, 21 Mar 2001
0023: // Modified to accept && and || by Roby Joehanes 15 Jul 2002
0024: package gov.nasa.ltl.trans;
0025:
0026: import java.util.*;
0027:
0028: /**
0029: * DOCUMENT ME!
0030: */
0031: public class Formula implements Comparable {
0032: private static int nId = 0;
0033: private static final int P_ALL = 0;
0034: private static final int P_IMPLIES = 1;
0035: private static final int P_OR = 2;
0036: private static final int P_AND = 3;
0037: private static final int P_UNTIL = 4;
0038: private static final int P_WUNTIL = 4;
0039: private static final int P_RELEASE = 5;
0040: private static final int P_WRELEASE = 5;
0041: private static final int P_NOT = 6;
0042: private static final int P_NEXT = 6;
0043: private static final int P_ALWAYS = 6;
0044: private static final int P_EVENTUALLY = 6;
0045: private static Hashtable ht = new Hashtable();
0046: private static Hashtable matches = new Hashtable();
0047: private char content;
0048: private boolean literal;
0049: private Formula left;
0050: private Formula right;
0051: private int id;
0052: private int untils_index; // index to the untils vector
0053: private BitSet rightOfWhichUntils; // for bug fix - formula can be right of >1 untils
0054: private String name;
0055: private boolean has_been_visited;
0056:
0057: private Formula(char c, boolean l, Formula sx, Formula dx, String n) {
0058: id = nId++;
0059: content = c;
0060: literal = l;
0061: left = sx;
0062: right = dx;
0063: name = n;
0064: rightOfWhichUntils = null;
0065: untils_index = -1;
0066: has_been_visited = false;
0067: }
0068:
0069: public static boolean is_reserved_char(char ch) {
0070: switch (ch) {
0071: // case 't':
0072: // case 'f':
0073: case 'U':
0074: case 'V':
0075: case 'W':
0076: case 'M':
0077: case 'X':
0078: case ' ':
0079: case '<':
0080: case '>':
0081: case '(':
0082: case ')':
0083: case '[':
0084: case ']':
0085: case '-':
0086:
0087: // ! not allowed by Java identifiers anyway - maybe some above neither?
0088: return true;
0089:
0090: default:
0091: return false;
0092: }
0093: }
0094:
0095: public static void reset_static() {
0096: clearMatches();
0097: clearHT();
0098: }
0099:
0100: public char getContent() {
0101: return content;
0102: }
0103:
0104: public String getName() {
0105: return name;
0106: }
0107:
0108: public Formula getNext() {
0109: switch (content) {
0110: case 'U':
0111: case 'W':
0112: return this ;
0113:
0114: case 'V':
0115: return this ;
0116:
0117: case 'O':
0118: return null;
0119:
0120: default:
0121:
0122: // System.out.println(content + " Switch did not find a relevant case...");
0123: return null;
0124: }
0125: }
0126:
0127: public Formula getSub1() {
0128: if (content == 'V') {
0129: return right;
0130: } else {
0131: return left;
0132: }
0133: }
0134:
0135: public Formula getSub2() {
0136: if (content == 'V') {
0137: return left;
0138: } else {
0139: return right;
0140: }
0141: }
0142:
0143: public void addLeft(Formula l) {
0144: left = l;
0145: }
0146:
0147: public void addRight(Formula r) {
0148: right = r;
0149: }
0150:
0151: public int compareTo(Object f) {
0152: Formula ff = (Formula) f;
0153:
0154: return (this .id - ff.id);
0155: }
0156:
0157: public int countUntils(int acc_sets) {
0158: has_been_visited = true;
0159:
0160: if (getContent() == 'U') {
0161: acc_sets++;
0162: }
0163:
0164: if ((left != null) && (!left.has_been_visited)) {
0165: acc_sets = left.countUntils(acc_sets);
0166: }
0167:
0168: if ((right != null) && (!right.has_been_visited)) {
0169: acc_sets = right.countUntils(acc_sets);
0170: }
0171:
0172: return acc_sets;
0173: }
0174:
0175: public BitSet get_rightOfWhichUntils() {
0176: return rightOfWhichUntils;
0177: }
0178:
0179: public int get_untils_index() {
0180: return untils_index;
0181: }
0182:
0183: public int initialize() {
0184: int acc_sets = countUntils(0);
0185: reset_visited();
0186:
0187: // System.out.println("Number of Us is: " + acc_sets);
0188: int test = processRightUntils(0, acc_sets);
0189: reset_visited();
0190:
0191: // System.out.println("Number of Us is: " + test);
0192: return acc_sets;
0193: }
0194:
0195: public boolean is_literal() {
0196: return literal;
0197: }
0198:
0199: public boolean is_right_of_until(int size) {
0200: return (rightOfWhichUntils != null);
0201: }
0202:
0203: public boolean is_special_case_of_V(TreeSet check_against) {
0204: Formula form = (Release(False(), this ));
0205:
0206: if (check_against.contains(form)) {
0207: return true;
0208: } else {
0209: return false;
0210: }
0211: }
0212:
0213: public boolean is_synt_implied(TreeSet old, TreeSet next) {
0214: if (this .getContent() == 't') {
0215: return true;
0216: }
0217:
0218: if (old.contains(this )) {
0219: return true;
0220: }
0221:
0222: if (!is_literal()) // non-elementary formula
0223: {
0224: Formula form1 = this .getSub1();
0225: Formula form2 = this .getSub2();
0226: Formula form3 = this .getNext();
0227:
0228: boolean condition1;
0229: boolean condition2;
0230: boolean condition3;
0231:
0232: if (form2 != null) {
0233: condition2 = form2.is_synt_implied(old, next);
0234: } else {
0235: condition2 = true;
0236: }
0237:
0238: if (form1 != null) {
0239: condition1 = form1.is_synt_implied(old, next);
0240: } else {
0241: condition1 = true;
0242: }
0243:
0244: if (form3 != null) {
0245: if (next != null) {
0246: condition3 = next.contains(form3);
0247: } else {
0248: condition3 = false;
0249: }
0250: } else {
0251: condition3 = true;
0252: }
0253:
0254: switch (getContent()) {
0255: case 'U':
0256: case 'W':
0257: case 'O':
0258: return (condition2 || (condition1 && condition3));
0259:
0260: case 'V':
0261: return ((condition1 && condition2) || (condition1 && condition3));
0262:
0263: case 'X':
0264:
0265: if (form1 != null) {
0266: if (next != null) {
0267: return (next.contains(form1));
0268: } else {
0269: return false;
0270: }
0271: } else {
0272: return true;
0273: }
0274:
0275: case 'A':
0276: return (condition2 && condition1);
0277:
0278: default:
0279: System.out
0280: .println("Default case of switch at Form.synt_implied");
0281:
0282: return false;
0283: }
0284: } else {
0285: return false;
0286: }
0287: }
0288:
0289: public Formula negate() {
0290: return Not(this );
0291: }
0292:
0293: public static Formula parse(String str) throws ParseErrorException { // "aObAc"
0294:
0295: Input i = new Input(str);
0296:
0297: return parse(i, P_ALL);
0298: }
0299:
0300: public int processRightUntils(int current_index, int acc_sets) {
0301: has_been_visited = true;
0302:
0303: if (getContent() == 'U') {
0304: this .untils_index = current_index;
0305:
0306: if (right.rightOfWhichUntils == null) {
0307: right.rightOfWhichUntils = new BitSet(acc_sets);
0308: }
0309:
0310: right.rightOfWhichUntils.set(current_index);
0311: current_index++;
0312: }
0313:
0314: if ((left != null) && (!left.has_been_visited)) {
0315: current_index = left.processRightUntils(current_index,
0316: acc_sets);
0317: }
0318:
0319: if ((right != null) && (!right.has_been_visited)) {
0320: current_index = right.processRightUntils(current_index,
0321: acc_sets);
0322: }
0323:
0324: return current_index;
0325: }
0326:
0327: public void reset_visited() {
0328: has_been_visited = false;
0329:
0330: if (left != null) {
0331: left.reset_visited();
0332: }
0333:
0334: if (right != null) {
0335: right.reset_visited();
0336: }
0337: }
0338:
0339: public Formula rewrite(Formula rule, Formula rewritten) {
0340: switch (content) {
0341: case 'A':
0342: case 'O':
0343: case 'U':
0344: case 'V':
0345: case 'W':
0346: left = left.rewrite(rule, rewritten);
0347: right = right.rewrite(rule, rewritten);
0348:
0349: break;
0350:
0351: case 'X':
0352: case 'N':
0353: left = left.rewrite(rule, rewritten);
0354:
0355: break;
0356:
0357: case 't':
0358: case 'f':
0359: case 'p':
0360: break;
0361: }
0362:
0363: if (match(rule)) {
0364: Formula expr = rewritten.rewrite();
0365:
0366: clearMatches();
0367:
0368: return expr;
0369: }
0370:
0371: clearMatches();
0372:
0373: return this ;
0374: }
0375:
0376: public int size() {
0377: switch (content) {
0378: case 'A':
0379: case 'O':
0380: case 'U':
0381: case 'V':
0382: case 'W':
0383: return left.size() + right.size() + 1;
0384:
0385: case 'X':
0386: case 'N':
0387: return left.size() + 1;
0388:
0389: default:
0390: return 0;
0391: }
0392: }
0393:
0394: public String toString(boolean exprId) {
0395: if (!exprId) {
0396: return toString();
0397: }
0398:
0399: switch (content) {
0400: case 'A':
0401: return "( " + left.toString(true) + " /\\ "
0402: + right.toString(true) + " )[" + id + "]";
0403:
0404: case 'O':
0405: return "( " + left.toString(true) + " \\/ "
0406: + right.toString(true) + " )[" + id + "]";
0407:
0408: case 'U':
0409: return "( " + left.toString(true) + " U "
0410: + right.toString(true) + " )[" + id + "]";
0411:
0412: case 'V':
0413: return "( " + left.toString(true) + " V "
0414: + right.toString(true) + " )[" + id + "]";
0415:
0416: case 'W':
0417: return "( " + left.toString(true) + " W "
0418: + right.toString(true) + " )[" + id + "]";
0419:
0420: //case 'M': return "( " + left.toString(true) + " M " + right.toString(true) + " )[" + id + "]";
0421: case 'X':
0422: return "( X " + left.toString(true) + " )[" + id + "]";
0423:
0424: case 'N':
0425: return "( ! " + left.toString(true) + " )[" + id + "]";
0426:
0427: case 't':
0428: return "( true )[" + id + "]";
0429:
0430: case 'f':
0431: return "( false )[" + id + "]";
0432:
0433: case 'p':
0434: return "( \"" + name + "\" )[" + id + "]";
0435:
0436: default:
0437: return "( " + content + " )[" + id + "]";
0438: }
0439: }
0440:
0441: public String toString() {
0442: switch (content) {
0443: case 'A':
0444: return "( " + left.toString() + " /\\ " + right.toString()
0445: + " )";
0446:
0447: case 'O':
0448: return "( " + left.toString() + " \\/ " + right.toString()
0449: + " )";
0450:
0451: case 'U':
0452: return "( " + left.toString() + " U " + right.toString()
0453: + " )";
0454:
0455: case 'V':
0456: return "( " + left.toString() + " V " + right.toString()
0457: + " )";
0458:
0459: case 'W':
0460: return "( " + left.toString() + " W " + right.toString()
0461: + " )";
0462:
0463: //case 'M': return "( " + left.toString() + " M " + right.toString() + " )";
0464: case 'X':
0465: return "( X " + left.toString() + " )";
0466:
0467: case 'N':
0468: return "( ! " + left.toString() + " )";
0469:
0470: case 't':
0471: return "( true )";
0472:
0473: case 'f':
0474: return "( false )";
0475:
0476: case 'p':
0477: return "( \"" + name + "\" )";
0478:
0479: default:
0480: return new Character(content).toString();
0481: }
0482: }
0483:
0484: private static Formula Always(Formula f) {
0485: return unique(new Formula('V', false, False(), f, null));
0486: }
0487:
0488: private static Formula And(Formula sx, Formula dx) {
0489: if (sx.id < dx.id) {
0490: return unique(new Formula('A', false, sx, dx, null));
0491: } else {
0492: return unique(new Formula('A', false, dx, sx, null));
0493: }
0494: }
0495:
0496: private static Formula Eventually(Formula f) {
0497: return unique(new Formula('U', false, True(), f, null));
0498: }
0499:
0500: private static Formula False() {
0501: return unique(new Formula('f', true, null, null, null));
0502: }
0503:
0504: private static Formula Implies(Formula sx, Formula dx) {
0505: return Or(Not(sx), dx);
0506: }
0507:
0508: private static Formula Next(Formula f) {
0509: return unique(new Formula('X', false, f, null, null));
0510: }
0511:
0512: private static Formula Not(Formula f) {
0513: if (f.literal) {
0514: switch (f.content) {
0515: case 't':
0516: return False();
0517:
0518: case 'f':
0519: return True();
0520:
0521: case 'N':
0522: return f.left;
0523:
0524: default:
0525: return unique(new Formula('N', true, f, null, null));
0526: }
0527: }
0528:
0529: // f is not a literal, so go on...
0530: switch (f.content) {
0531: case 'A':
0532: return Or(Not(f.left), Not(f.right));
0533:
0534: case 'O':
0535: return And(Not(f.left), Not(f.right));
0536:
0537: case 'U':
0538: return Release(Not(f.left), Not(f.right));
0539:
0540: case 'V':
0541: return Until(Not(f.left), Not(f.right));
0542:
0543: case 'W':
0544: return WRelease(Not(f.left), Not(f.right));
0545:
0546: //case 'M': return WUntil(Not(f.left), Not(f.right));
0547: case 'N':
0548: return f.left;
0549:
0550: case 'X':
0551: return Next(Not(f.left));
0552:
0553: default:
0554: throw new ParserInternalError();
0555: }
0556: }
0557:
0558: private static Formula Or(Formula sx, Formula dx) {
0559: if (sx.id < dx.id) {
0560: return unique(new Formula('O', false, sx, dx, null));
0561: } else {
0562: return unique(new Formula('O', false, dx, sx, null));
0563: }
0564: }
0565:
0566: private static Formula Proposition(String name) {
0567: return unique(new Formula('p', true, null, null, name));
0568: }
0569:
0570: private static Formula Release(Formula sx, Formula dx) {
0571: return unique(new Formula('V', false, sx, dx, null));
0572: }
0573:
0574: private static Formula True() {
0575: return unique(new Formula('t', true, null, null, null));
0576: }
0577:
0578: private static Formula Until(Formula sx, Formula dx) {
0579: return unique(new Formula('U', false, sx, dx, null));
0580: }
0581:
0582: private static Formula WRelease(Formula sx, Formula dx) {
0583: return unique(new Formula('U', false, dx, And(sx, dx), null));
0584: }
0585:
0586: private static Formula WUntil(Formula sx, Formula dx) {
0587: return unique(new Formula('W', false, sx, dx, null));
0588: }
0589:
0590: private static void clearHT() {
0591: ht = new Hashtable();
0592: }
0593:
0594: private static void clearMatches() {
0595: matches = new Hashtable();
0596: }
0597:
0598: private static Formula parse(Input i, int precedence)
0599: throws ParseErrorException {
0600: try {
0601: Formula formula;
0602: char ch;
0603:
0604: while (i.get() == ' ') {
0605: i.skip();
0606: }
0607:
0608: switch (ch = i.get()) {
0609: case '/': // and
0610: case '&': // robbyjo's and
0611: case '\\': // or
0612: case '|': // robbyjo's or
0613: case 'U': // until
0614: case 'W': // weak until
0615: case 'V': // release
0616: case 'M': // dual of W - weak release
0617: case ')':
0618: throw new ParseErrorException("invalid character: "
0619: + ch);
0620:
0621: case '!': // not
0622: i.skip();
0623: formula = Not(parse(i, P_NOT));
0624:
0625: break;
0626:
0627: case 'X': // next
0628: i.skip();
0629: formula = Next(parse(i, P_NEXT));
0630:
0631: break;
0632:
0633: case '[': // always
0634: i.skip();
0635:
0636: if (i.get() != ']') {
0637: throw new ParseErrorException("expected ]");
0638: }
0639:
0640: i.skip();
0641: formula = Always(parse(i, P_ALWAYS));
0642:
0643: break;
0644:
0645: case '<': // eventually
0646: i.skip();
0647:
0648: if (i.get() != '>') {
0649: throw new ParseErrorException("expected >");
0650: }
0651:
0652: i.skip();
0653: formula = Eventually(parse(i, P_EVENTUALLY));
0654:
0655: break;
0656:
0657: case '(':
0658: i.skip();
0659: formula = parse(i, P_ALL);
0660:
0661: if (i.get() != ')') {
0662: throw new ParseErrorException("invalid character: "
0663: + ch);
0664: }
0665:
0666: i.skip();
0667:
0668: break;
0669:
0670: case '"':
0671:
0672: StringBuffer sb = new StringBuffer();
0673: i.skip();
0674:
0675: while ((ch = i.get()) != '"') {
0676: sb.append(ch);
0677: i.skip();
0678: }
0679:
0680: i.skip();
0681:
0682: formula = Proposition(sb.toString());
0683:
0684: break;
0685:
0686: default:
0687:
0688: if (Character.isJavaIdentifierStart(ch)) {
0689: StringBuffer sbf = new StringBuffer();
0690:
0691: sbf.append(ch);
0692: i.skip();
0693:
0694: try {
0695: while (Character.isJavaIdentifierPart(ch = i
0696: .get())
0697: && (!Formula.is_reserved_char(ch))) {
0698: sbf.append(ch);
0699: i.skip();
0700: }
0701: } catch (EndOfInputException e) {
0702: // return Proposition(sbf.toString());
0703: }
0704:
0705: String id = sbf.toString();
0706:
0707: if (id.equals("true")) {
0708: formula = True();
0709: } else if (id.equals("false")) {
0710: formula = False();
0711: } else {
0712: formula = Proposition(sbf.toString());
0713: }
0714: } else {
0715: throw new ParseErrorException("invalid character: "
0716: + ch);
0717: }
0718:
0719: break;
0720: }
0721:
0722: try {
0723: while (i.get() == ' ') {
0724: i.skip();
0725: }
0726:
0727: ch = i.get();
0728: } catch (EndOfInputException e) {
0729: return formula;
0730: }
0731:
0732: while (true) {
0733: switch (ch) {
0734: case '/': // and
0735:
0736: if (precedence > P_AND) {
0737: return formula;
0738: }
0739:
0740: i.skip();
0741:
0742: if (i.get() != '\\') {
0743: throw new ParseErrorException("expected \\");
0744: }
0745:
0746: i.skip();
0747: formula = And(formula, parse(i, P_AND));
0748:
0749: break;
0750:
0751: case '&': // robbyjo's and
0752:
0753: if (precedence > P_AND) {
0754: return formula;
0755: }
0756:
0757: i.skip();
0758:
0759: if (i.get() != '&') {
0760: throw new ParseErrorException("expected &&");
0761: }
0762:
0763: i.skip();
0764: formula = And(formula, parse(i, P_AND));
0765:
0766: break;
0767:
0768: case '\\': // or
0769:
0770: if (precedence > P_OR) {
0771: return formula;
0772: }
0773:
0774: i.skip();
0775:
0776: if (i.get() != '/') {
0777: throw new ParseErrorException("expected /");
0778: }
0779:
0780: i.skip();
0781: formula = Or(formula, parse(i, P_OR));
0782:
0783: break;
0784:
0785: case '|': // robbyjo's or
0786:
0787: if (precedence > P_OR) {
0788: return formula;
0789: }
0790:
0791: i.skip();
0792:
0793: if (i.get() != '|') {
0794: throw new ParseErrorException("expected ||");
0795: }
0796:
0797: i.skip();
0798: formula = Or(formula, parse(i, P_OR));
0799:
0800: break;
0801:
0802: case 'U': // until
0803:
0804: if (precedence > P_UNTIL) {
0805: return formula;
0806: }
0807:
0808: i.skip();
0809: formula = Until(formula, parse(i, P_UNTIL));
0810:
0811: break;
0812:
0813: case 'W': // weak until
0814:
0815: if (precedence > P_WUNTIL) {
0816: return formula;
0817: }
0818:
0819: i.skip();
0820: formula = WUntil(formula, parse(i, P_WUNTIL));
0821:
0822: break;
0823:
0824: case 'V': // release
0825:
0826: if (precedence > P_RELEASE) {
0827: return formula;
0828: }
0829:
0830: i.skip();
0831: formula = Release(formula, parse(i, P_RELEASE));
0832:
0833: break;
0834:
0835: case 'M': // weak_release
0836:
0837: if (precedence > P_WRELEASE) {
0838: return formula;
0839: }
0840:
0841: i.skip();
0842: formula = WRelease(formula, parse(i, P_WRELEASE));
0843:
0844: break;
0845:
0846: case '-': // implies
0847:
0848: if (precedence > P_IMPLIES) {
0849: return formula;
0850: }
0851:
0852: i.skip();
0853:
0854: if (i.get() != '>') {
0855: throw new ParseErrorException("expected >");
0856: }
0857:
0858: i.skip();
0859: formula = Implies(formula, parse(i, P_IMPLIES));
0860:
0861: break;
0862:
0863: case ')':
0864: return formula;
0865:
0866: case '!':
0867: case 'X':
0868: case '[':
0869: case '<':
0870: case '(':
0871: default:
0872: throw new ParseErrorException("invalid character: "
0873: + ch);
0874: }
0875:
0876: try {
0877: while (i.get() == ' ') {
0878: i.skip();
0879: }
0880:
0881: ch = i.get();
0882: } catch (EndOfInputException e) {
0883: break;
0884: }
0885: }
0886:
0887: return formula;
0888: } catch (EndOfInputException e) {
0889: throw new ParseErrorException("unexpected end of input");
0890: }
0891: }
0892:
0893: private static Formula unique(Formula f) {
0894: String s = f.toString();
0895:
0896: if (ht.containsKey(s)) {
0897: return (Formula) ht.get(s);
0898: }
0899:
0900: ht.put(s, f);
0901:
0902: return f;
0903: }
0904:
0905: private Formula getMatch(String name) {
0906: return (Formula) matches.get(name);
0907: }
0908:
0909: private void addMatch(String name, Formula expr) {
0910: matches.put(name, expr);
0911: }
0912:
0913: private boolean match(Formula rule) {
0914: if (rule.content == 'p') {
0915: Formula match = getMatch(rule.name);
0916:
0917: if (match == null) {
0918: addMatch(rule.name, this );
0919:
0920: return true;
0921: }
0922:
0923: return match == this ;
0924: }
0925:
0926: if (rule.content != content) {
0927: return false;
0928: }
0929:
0930: Hashtable saved = (Hashtable) matches.clone();
0931:
0932: switch (content) {
0933: case 'A':
0934: case 'O':
0935:
0936: if (left.match(rule.left) && right.match(rule.right)) {
0937: return true;
0938: }
0939:
0940: matches = saved;
0941:
0942: if (right.match(rule.left) && left.match(rule.right)) {
0943: return true;
0944: }
0945:
0946: matches = saved;
0947:
0948: return false;
0949:
0950: case 'U':
0951: case 'V':
0952: case 'W':
0953:
0954: if (left.match(rule.left) && right.match(rule.right)) {
0955: return true;
0956: }
0957:
0958: matches = saved;
0959:
0960: return false;
0961:
0962: case 'X':
0963: case 'N':
0964:
0965: if (left.match(rule.left)) {
0966: return true;
0967: }
0968:
0969: matches = saved;
0970:
0971: return false;
0972:
0973: case 't':
0974: case 'f':
0975: return true;
0976: }
0977:
0978: throw new RuntimeException("code should not be reached");
0979: }
0980:
0981: private Formula rewrite() {
0982: if (content == 'p') {
0983: return getMatch(name);
0984: }
0985:
0986: switch (content) {
0987: case 'A':
0988: return And(left.rewrite(), right.rewrite());
0989:
0990: case 'O':
0991: return Or(left.rewrite(), right.rewrite());
0992:
0993: case 'U':
0994: return Until(left.rewrite(), right.rewrite());
0995:
0996: case 'V':
0997: return Release(left.rewrite(), right.rewrite());
0998:
0999: case 'W':
1000: return WUntil(left.rewrite(), right.rewrite());
1001:
1002: case 'X':
1003: return Next(left.rewrite());
1004:
1005: case 'N':
1006: return Not(left.rewrite());
1007:
1008: case 't':
1009: return True();
1010:
1011: case 'f':
1012: return False();
1013: }
1014:
1015: throw new RuntimeException("code should not be reached");
1016: }
1017:
1018: /**
1019: * DOCUMENT ME!
1020: */
1021: public static class EndOfInputException extends Exception {
1022: }
1023:
1024: /**
1025: * DOCUMENT ME!
1026: */
1027: private static class Input {
1028: private StringBuffer sb;
1029:
1030: public Input(String str) {
1031: sb = new StringBuffer(str);
1032: }
1033:
1034: public char get() throws EndOfInputException {
1035: try {
1036: return sb.charAt(0);
1037: } catch (StringIndexOutOfBoundsException e) {
1038: throw new EndOfInputException();
1039: }
1040: }
1041:
1042: public void skip() throws EndOfInputException {
1043: try {
1044: sb.deleteCharAt(0);
1045: } catch (StringIndexOutOfBoundsException e) {
1046: throw new EndOfInputException();
1047: }
1048: }
1049: }
1050: }
|