KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > ltl > trans > Formula


1
2 //
3
// Copyright (C) 2005 United States Government as represented by the
4
// Administrator of the National Aeronautics and Space Administration
5
// (NASA). All Rights Reserved.
6
//
7
// This software is distributed under the NASA Open Source Agreement
8
// (NOSA), version 1.3. The NOSA has been approved by the Open Source
9
// Initiative. See the file NOSA-1.3-JPF at the top of the distribution
10
// directory tree for the complete NOSA document.
11
//
12
// THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
13
// KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
14
// LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
15
// SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
16
// A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
17
// THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
18
// DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
19
//
20

21 // Written by Dimitra Giannakopoulou, 19 Jan 2001
22
// Parser by Flavio Lerda, 8 Feb 2001
23
// Parser extended by Flavio Lerda, 21 Mar 2001
24
// Modified to accept && and || by Roby Joehanes 15 Jul 2002
25
package gov.nasa.ltl.trans;
26
27 import java.util.*;
28
29
30 /**
31  * DOCUMENT ME!
32  */

33 public class Formula implements Comparable JavaDoc {
34   private static int nId = 0;
35   private static final int P_ALL = 0;
36   private static final int P_IMPLIES = 1;
37   private static final int P_OR = 2;
38   private static final int P_AND = 3;
39   private static final int P_UNTIL = 4;
40   private static final int P_WUNTIL = 4;
41   private static final int P_RELEASE = 5;
42   private static final int P_WRELEASE = 5;
43   private static final int P_NOT = 6;
44   private static final int P_NEXT = 6;
45   private static final int P_ALWAYS = 6;
46   private static final int P_EVENTUALLY = 6;
47   private static Hashtable ht = new Hashtable();
48   private static Hashtable matches = new Hashtable();
49   private char content;
50   private boolean literal;
51   private Formula left;
52   private Formula right;
53   private int id;
54   private int untils_index; // index to the untils vector
55
private BitSet rightOfWhichUntils; // for bug fix - formula can be right of >1 untils
56
private String JavaDoc name;
57   private boolean has_been_visited;
58
59   private Formula (char c, boolean l, Formula sx, Formula dx, String JavaDoc n) {
60     id = nId++;
61     content = c;
62     literal = l;
63     left = sx;
64     right = dx;
65     name = n;
66     rightOfWhichUntils = null;
67     untils_index = -1;
68     has_been_visited = false;
69   }
70
71   public static boolean is_reserved_char (char ch) {
72     switch (ch) {
73     // case 't':
74
// case 'f':
75
case 'U':
76     case 'V':
77     case 'W':
78     case 'M':
79     case 'X':
80     case ' ':
81     case '<':
82     case '>':
83     case '(':
84     case ')':
85     case '[':
86     case ']':
87     case '-':
88
89       // ! not allowed by Java identifiers anyway - maybe some above neither?
90
return true;
91
92     default:
93       return false;
94     }
95   }
96
97   public static void reset_static () {
98     clearMatches();
99     clearHT();
100   }
101
102   public char getContent () {
103     return content;
104   }
105
106   public String JavaDoc getName () {
107     return name;
108   }
109
110   public Formula getNext () {
111     switch (content) {
112     case 'U':
113     case 'W':
114       return this;
115
116     case 'V':
117       return this;
118
119     case 'O':
120       return null;
121
122     default:
123
124       // System.out.println(content + " Switch did not find a relevant case...");
125
return null;
126     }
127   }
128
129   public Formula getSub1 () {
130     if (content == 'V') {
131       return right;
132     } else {
133       return left;
134     }
135   }
136
137   public Formula getSub2 () {
138     if (content == 'V') {
139       return left;
140     } else {
141       return right;
142     }
143   }
144
145   public void addLeft (Formula l) {
146     left = l;
147   }
148
149   public void addRight (Formula r) {
150     right = r;
151   }
152
153   public int compareTo (Object JavaDoc f) {
154     Formula ff = (Formula) f;
155
156     return (this.id - ff.id);
157   }
158
159   public int countUntils (int acc_sets) {
160     has_been_visited = true;
161
162     if (getContent() == 'U') {
163       acc_sets++;
164     }
165
166     if ((left != null) && (!left.has_been_visited)) {
167       acc_sets = left.countUntils(acc_sets);
168     }
169
170     if ((right != null) && (!right.has_been_visited)) {
171       acc_sets = right.countUntils(acc_sets);
172     }
173
174     return acc_sets;
175   }
176
177   public BitSet get_rightOfWhichUntils () {
178     return rightOfWhichUntils;
179   }
180
181   public int get_untils_index () {
182     return untils_index;
183   }
184
185   public int initialize () {
186     int acc_sets = countUntils(0);
187     reset_visited();
188
189     // System.out.println("Number of Us is: " + acc_sets);
190
int test = processRightUntils(0, acc_sets);
191     reset_visited();
192
193     // System.out.println("Number of Us is: " + test);
194
return acc_sets;
195   }
196
197   public boolean is_literal () {
198     return literal;
199   }
200
201   public boolean is_right_of_until (int size) {
202     return (rightOfWhichUntils != null);
203   }
204
205   public boolean is_special_case_of_V (TreeSet check_against) {
206     Formula form = (Release(False(), this));
207
208     if (check_against.contains(form)) {
209       return true;
210     } else {
211       return false;
212     }
213   }
214
215   public boolean is_synt_implied (TreeSet old, TreeSet next) {
216     if (this.getContent() == 't') {
217       return true;
218     }
219
220     if (old.contains(this)) {
221       return true;
222     }
223
224     if (!is_literal()) // non-elementary formula
225
{
226       Formula form1 = this.getSub1();
227       Formula form2 = this.getSub2();
228       Formula form3 = this.getNext();
229
230       boolean condition1;
231       boolean condition2;
232       boolean condition3;
233
234       if (form2 != null) {
235         condition2 = form2.is_synt_implied(old, next);
236       } else {
237         condition2 = true;
238       }
239
240       if (form1 != null) {
241         condition1 = form1.is_synt_implied(old, next);
242       } else {
243         condition1 = true;
244       }
245
246       if (form3 != null) {
247         if (next != null) {
248           condition3 = next.contains(form3);
249         } else {
250           condition3 = false;
251         }
252       } else {
253         condition3 = true;
254       }
255
256       switch (getContent()) {
257       case 'U':
258       case 'W':
259       case 'O':
260         return (condition2 || (condition1 && condition3));
261
262       case 'V':
263         return ((condition1 && condition2) || (condition1 && condition3));
264
265       case 'X':
266
267         if (form1 != null) {
268           if (next != null) {
269             return (next.contains(form1));
270           } else {
271             return false;
272           }
273         } else {
274           return true;
275         }
276
277       case 'A':
278         return (condition2 && condition1);
279
280       default:
281         System.out.println("Default case of switch at Form.synt_implied");
282
283         return false;
284       }
285     } else {
286       return false;
287     }
288   }
289
290   public Formula negate () {
291     return Not(this);
292   }
293
294   public static Formula parse (String JavaDoc str) throws ParseErrorException { // "aObAc"
295

296     Input i = new Input(str);
297
298     return parse(i, P_ALL);
299   }
300
301   public int processRightUntils (int current_index, int acc_sets) {
302     has_been_visited = true;
303
304     if (getContent() == 'U') {
305       this.untils_index = current_index;
306
307       if (right.rightOfWhichUntils == null) {
308         right.rightOfWhichUntils = new BitSet(acc_sets);
309       }
310
311       right.rightOfWhichUntils.set(current_index);
312       current_index++;
313     }
314
315     if ((left != null) && (!left.has_been_visited)) {
316       current_index = left.processRightUntils(current_index, acc_sets);
317     }
318
319     if ((right != null) && (!right.has_been_visited)) {
320       current_index = right.processRightUntils(current_index, acc_sets);
321     }
322
323     return current_index;
324   }
325
326   public void reset_visited () {
327     has_been_visited = false;
328
329     if (left != null) {
330       left.reset_visited();
331     }
332
333     if (right != null) {
334       right.reset_visited();
335     }
336   }
337
338   public Formula rewrite (Formula rule, Formula rewritten) {
339     switch (content) {
340     case 'A':
341     case 'O':
342     case 'U':
343     case 'V':
344     case 'W':
345       left = left.rewrite(rule, rewritten);
346       right = right.rewrite(rule, rewritten);
347
348       break;
349
350     case 'X':
351     case 'N':
352       left = left.rewrite(rule, rewritten);
353
354       break;
355
356     case 't':
357     case 'f':
358     case 'p':
359       break;
360     }
361
362     if (match(rule)) {
363       Formula expr = rewritten.rewrite();
364
365       clearMatches();
366
367       return expr;
368     }
369
370     clearMatches();
371
372     return this;
373   }
374
375   public int size () {
376     switch (content) {
377     case 'A':
378     case 'O':
379     case 'U':
380     case 'V':
381     case 'W':
382       return left.size() + right.size() + 1;
383
384     case 'X':
385     case 'N':
386       return left.size() + 1;
387
388     default:
389       return 0;
390     }
391   }
392
393   public String JavaDoc toString (boolean exprId) {
394     if (!exprId) {
395       return toString();
396     }
397
398     switch (content) {
399     case 'A':
400       return "( " + left.toString(true) + " /\\ " + right.toString(true) +
401              " )[" + id + "]";
402
403     case 'O':
404       return "( " + left.toString(true) + " \\/ " + right.toString(true) +
405              " )[" + id + "]";
406
407     case 'U':
408       return "( " + left.toString(true) + " U " + right.toString(true) +
409              " )[" + id + "]";
410
411     case 'V':
412       return "( " + left.toString(true) + " V " + right.toString(true) +
413              " )[" + id + "]";
414
415     case 'W':
416       return "( " + left.toString(true) + " W " + right.toString(true) +
417              " )[" + id + "]";
418
419     //case 'M': return "( " + left.toString(true) + " M " + right.toString(true) + " )[" + id + "]";
420
case 'X':
421       return "( X " + left.toString(true) + " )[" + id + "]";
422
423     case 'N':
424       return "( ! " + left.toString(true) + " )[" + id + "]";
425
426     case 't':
427       return "( true )[" + id + "]";
428
429     case 'f':
430       return "( false )[" + id + "]";
431
432     case 'p':
433       return "( \"" + name + "\" )[" + id + "]";
434
435     default:
436       return "( " + content + " )[" + id + "]";
437     }
438   }
439
440   public String JavaDoc toString () {
441     switch (content) {
442     case 'A':
443       return "( " + left.toString() + " /\\ " + right.toString() + " )";
444
445     case 'O':
446       return "( " + left.toString() + " \\/ " + right.toString() + " )";
447
448     case 'U':
449       return "( " + left.toString() + " U " + right.toString() + " )";
450
451     case 'V':
452       return "( " + left.toString() + " V " + right.toString() + " )";
453
454     case 'W':
455       return "( " + left.toString() + " W " + right.toString() + " )";
456
457     //case 'M': return "( " + left.toString() + " M " + right.toString() + " )";
458
case 'X':
459       return "( X " + left.toString() + " )";
460
461     case 'N':
462       return "( ! " + left.toString() + " )";
463
464     case 't':
465       return "( true )";
466
467     case 'f':
468       return "( false )";
469
470     case 'p':
471       return "( \"" + name + "\" )";
472
473     default:
474       return new Character JavaDoc(content).toString();
475     }
476   }
477
478   private static Formula Always (Formula f) {
479     return unique(new Formula('V', false, False(), f, null));
480   }
481
482   private static Formula And (Formula sx, Formula dx) {
483     if (sx.id < dx.id) {
484       return unique(new Formula('A', false, sx, dx, null));
485     } else {
486       return unique(new Formula('A', false, dx, sx, null));
487     }
488   }
489
490   private static Formula Eventually (Formula f) {
491     return unique(new Formula('U', false, True(), f, null));
492   }
493
494   private static Formula False () {
495     return unique(new Formula('f', true, null, null, null));
496   }
497
498   private static Formula Implies (Formula sx, Formula dx) {
499     return Or(Not(sx), dx);
500   }
501
502   private static Formula Next (Formula f) {
503     return unique(new Formula('X', false, f, null, null));
504   }
505
506   private static Formula Not (Formula f) {
507     if (f.literal) {
508       switch (f.content) {
509       case 't':
510         return False();
511
512       case 'f':
513         return True();
514
515       case 'N':
516         return f.left;
517
518       default:
519         return unique(new Formula('N', true, f, null, null));
520       }
521     }
522
523     // f is not a literal, so go on...
524
switch (f.content) {
525     case 'A':
526       return Or(Not(f.left), Not(f.right));
527
528     case 'O':
529       return And(Not(f.left), Not(f.right));
530
531     case 'U':
532       return Release(Not(f.left), Not(f.right));
533
534     case 'V':
535       return Until(Not(f.left), Not(f.right));
536
537     case 'W':
538       return WRelease(Not(f.left), Not(f.right));
539
540     //case 'M': return WUntil(Not(f.left), Not(f.right));
541
case 'N':
542       return f.left;
543
544     case 'X':
545       return Next(Not(f.left));
546
547     default:
548       throw new ParserInternalError();
549     }
550   }
551
552   private static Formula Or (Formula sx, Formula dx) {
553     if (sx.id < dx.id) {
554       return unique(new Formula('O', false, sx, dx, null));
555     } else {
556       return unique(new Formula('O', false, dx, sx, null));
557     }
558   }
559
560   private static Formula Proposition (String JavaDoc name) {
561     return unique(new Formula('p', true, null, null, name));
562   }
563
564   private static Formula Release (Formula sx, Formula dx) {
565     return unique(new Formula('V', false, sx, dx, null));
566   }
567
568   private static Formula True () {
569     return unique(new Formula('t', true, null, null, null));
570   }
571
572   private static Formula Until (Formula sx, Formula dx) {
573     return unique(new Formula('U', false, sx, dx, null));
574   }
575
576   private static Formula WRelease (Formula sx, Formula dx) {
577     return unique(new Formula('U', false, dx, And(sx, dx), null));
578   }
579
580   private static Formula WUntil (Formula sx, Formula dx) {
581     return unique(new Formula('W', false, sx, dx, null));
582   }
583
584   private static void clearHT () {
585     ht = new Hashtable();
586   }
587
588   private static void clearMatches () {
589     matches = new Hashtable();
590   }
591
592   private static Formula parse (Input i, int precedence)
593                          throws ParseErrorException {
594     try {
595       Formula formula;
596       char ch;
597
598       while (i.get() == ' ') {
599         i.skip();
600       }
601
602       switch (ch = i.get()) {
603       case '/': // and
604
case '&': // robbyjo's and
605
case '\\': // or
606
case '|': // robbyjo's or
607
case 'U': // until
608
case 'W': // weak until
609
case 'V': // release
610
case 'M': // dual of W - weak release
611
case ')':
612         throw new ParseErrorException("invalid character: " + ch);
613
614       case '!': // not
615
i.skip();
616         formula = Not(parse(i, P_NOT));
617
618         break;
619
620       case 'X': // next
621
i.skip();
622         formula = Next(parse(i, P_NEXT));
623
624         break;
625
626       case '[': // always
627
i.skip();
628
629         if (i.get() != ']') {
630           throw new ParseErrorException("expected ]");
631         }
632
633         i.skip();
634         formula = Always(parse(i, P_ALWAYS));
635
636         break;
637
638       case '<': // eventually
639
i.skip();
640
641         if (i.get() != '>') {
642           throw new ParseErrorException("expected >");
643         }
644
645         i.skip();
646         formula = Eventually(parse(i, P_EVENTUALLY));
647
648         break;
649
650       case '(':
651         i.skip();
652         formula = parse(i, P_ALL);
653
654         if (i.get() != ')') {
655           throw new ParseErrorException("invalid character: " + ch);
656         }
657
658         i.skip();
659
660         break;
661
662       case '"':
663
664         StringBuffer JavaDoc sb = new StringBuffer JavaDoc();
665         i.skip();
666
667         while ((ch = i.get()) != '"') {
668           sb.append(ch);
669           i.skip();
670         }
671
672         i.skip();
673
674         formula = Proposition(sb.toString());
675
676         break;
677
678       default:
679
680         if (Character.isJavaIdentifierStart(ch)) {
681           StringBuffer JavaDoc sbf = new StringBuffer JavaDoc();
682
683           sbf.append(ch);
684           i.skip();
685
686           try {
687             while (Character.isJavaIdentifierPart(ch = i.get()) &&
688                    (!Formula.is_reserved_char(ch))) {
689               sbf.append(ch);
690               i.skip();
691             }
692           } catch (EndOfInputException e) {
693             // return Proposition(sbf.toString());
694
}
695
696           String JavaDoc id = sbf.toString();
697
698           if (id.equals("true")) {
699             formula = True();
700           } else if (id.equals("false")) {
701             formula = False();
702           } else {
703             formula = Proposition(sbf.toString());
704           }
705         } else {
706           throw new ParseErrorException("invalid character: " + ch);
707         }
708
709         break;
710       }
711
712       try {
713         while (i.get() == ' ') {
714           i.skip();
715         }
716
717         ch = i.get();
718       } catch (EndOfInputException e) {
719         return formula;
720       }
721
722       while (true) {
723         switch (ch) {
724         case '/': // and
725

726           if (precedence > P_AND) {
727             return formula;
728           }
729
730           i.skip();
731
732           if (i.get() != '\\') {
733             throw new ParseErrorException("expected \\");
734           }
735
736           i.skip();
737           formula = And(formula, parse(i, P_AND));
738
739           break;
740
741         case '&': // robbyjo's and
742

743           if (precedence > P_AND) {
744             return formula;
745           }
746
747           i.skip();
748
749           if (i.get() != '&') {
750             throw new ParseErrorException("expected &&");
751           }
752
753           i.skip();
754           formula = And(formula, parse(i, P_AND));
755
756           break;
757
758         case '\\': // or
759

760           if (precedence > P_OR) {
761             return formula;
762           }
763
764           i.skip();
765
766           if (i.get() != '/') {
767             throw new ParseErrorException("expected /");
768           }
769
770           i.skip();
771           formula = Or(formula, parse(i, P_OR));
772
773           break;
774
775         case '|': // robbyjo's or
776

777           if (precedence > P_OR) {
778             return formula;
779           }
780
781           i.skip();
782
783           if (i.get() != '|') {
784             throw new ParseErrorException("expected ||");
785           }
786
787           i.skip();
788           formula = Or(formula, parse(i, P_OR));
789
790           break;
791
792         case 'U': // until
793

794           if (precedence > P_UNTIL) {
795             return formula;
796           }
797
798           i.skip();
799           formula = Until(formula, parse(i, P_UNTIL));
800
801           break;
802
803         case 'W': // weak until
804

805           if (precedence > P_WUNTIL) {
806             return formula;
807           }
808
809           i.skip();
810           formula = WUntil(formula, parse(i, P_WUNTIL));
811
812           break;
813
814         case 'V': // release
815

816           if (precedence > P_RELEASE) {
817             return formula;
818           }
819
820           i.skip();
821           formula = Release(formula, parse(i, P_RELEASE));
822
823           break;
824
825         case 'M': // weak_release
826

827           if (precedence > P_WRELEASE) {
828             return formula;
829           }
830
831           i.skip();
832           formula = WRelease(formula, parse(i, P_WRELEASE));
833
834           break;
835
836         case '-': // implies
837

838           if (precedence > P_IMPLIES) {
839             return formula;
840           }
841
842           i.skip();
843
844           if (i.get() != '>') {
845             throw new ParseErrorException("expected >");
846           }
847
848           i.skip();
849           formula = Implies(formula, parse(i, P_IMPLIES));
850
851           break;
852
853         case ')':
854           return formula;
855
856         case '!':
857         case 'X':
858         case '[':
859         case '<':
860         case '(':
861         default:
862           throw new ParseErrorException("invalid character: " + ch);
863         }
864
865         try {
866           while (i.get() == ' ') {
867             i.skip();
868           }
869
870           ch = i.get();
871         } catch (EndOfInputException e) {
872           break;
873         }
874       }
875
876       return formula;
877     } catch (EndOfInputException e) {
878       throw new ParseErrorException("unexpected end of input");
879     }
880   }
881
882   private static Formula unique (Formula f) {
883     String JavaDoc s = f.toString();
884
885     if (ht.containsKey(s)) {
886       return (Formula) ht.get(s);
887     }
888
889     ht.put(s, f);
890
891     return f;
892   }
893
894   private Formula getMatch (String JavaDoc name) {
895     return (Formula) matches.get(name);
896   }
897
898   private void addMatch (String JavaDoc name, Formula expr) {
899     matches.put(name, expr);
900   }
901
902   private boolean match (Formula rule) {
903     if (rule.content == 'p') {
904       Formula match = getMatch(rule.name);
905
906       if (match == null) {
907         addMatch(rule.name, this);
908
909         return true;
910       }
911
912       return match == this;
913     }
914
915     if (rule.content != content) {
916       return false;
917     }
918
919     Hashtable saved = (Hashtable) matches.clone();
920
921     switch (content) {
922     case 'A':
923     case 'O':
924
925       if (left.match(rule.left) && right.match(rule.right)) {
926         return true;
927       }
928
929       matches = saved;
930
931       if (right.match(rule.left) && left.match(rule.right)) {
932         return true;
933       }
934
935       matches = saved;
936
937       return false;
938
939     case 'U':
940     case 'V':
941     case 'W':
942
943       if (left.match(rule.left) && right.match(rule.right)) {
944         return true;
945       }
946
947       matches = saved;
948
949       return false;
950
951     case 'X':
952     case 'N':
953
954       if (left.match(rule.left)) {
955         return true;
956       }
957
958       matches = saved;
959
960       return false;
961
962     case 't':
963     case 'f':
964       return true;
965     }
966
967     throw new RuntimeException JavaDoc("code should not be reached");
968   }
969
970   private Formula rewrite () {
971     if (content == 'p') {
972       return getMatch(name);
973     }
974
975     switch (content) {
976     case 'A':
977       return And(left.rewrite(), right.rewrite());
978
979     case 'O':
980       return Or(left.rewrite(), right.rewrite());
981
982     case 'U':
983       return Until(left.rewrite(), right.rewrite());
984
985     case 'V':
986       return Release(left.rewrite(), right.rewrite());
987
988     case 'W':
989       return WUntil(left.rewrite(), right.rewrite());
990
991     case 'X':
992       return Next(left.rewrite());
993
994     case 'N':
995       return Not(left.rewrite());
996
997     case 't':
998       return True();
999
1000    case 'f':
1001      return False();
1002    }
1003
1004    throw new RuntimeException JavaDoc("code should not be reached");
1005  }
1006
1007  /**
1008   * DOCUMENT ME!
1009   */

1010  public static class EndOfInputException extends Exception JavaDoc {
1011  }
1012
1013  /**
1014   * DOCUMENT ME!
1015   */

1016  private static class Input {
1017    private StringBuffer JavaDoc sb;
1018
1019    public Input (String JavaDoc str) {
1020      sb = new StringBuffer JavaDoc(str);
1021    }
1022
1023    public char get () throws EndOfInputException {
1024      try {
1025        return sb.charAt(0);
1026      } catch (StringIndexOutOfBoundsException JavaDoc e) {
1027        throw new EndOfInputException();
1028      }
1029    }
1030
1031    public void skip () throws EndOfInputException {
1032      try {
1033        sb.deleteCharAt(0);
1034      } catch (StringIndexOutOfBoundsException JavaDoc e) {
1035        throw new EndOfInputException();
1036      }
1037    }
1038  }
1039}
Popular Tags