1 2 21 package gov.nasa.ltl.trans; 26 27 import java.util.*; 28 29 30 33 public class Formula implements Comparable { 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; private BitSet rightOfWhichUntils; private String name; 57 private boolean has_been_visited; 58 59 private Formula (char c, boolean l, Formula sx, Formula dx, String 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 '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 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 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 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 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 int test = processRightUntils(0, acc_sets); 191 reset_visited(); 192 193 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()) { 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 str) throws ParseErrorException { 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 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 '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 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 '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 (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 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 '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 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 '/': case '&': case '\\': case '|': case 'U': case 'W': case 'V': case 'M': case ')': 612 throw new ParseErrorException("invalid character: " + ch); 613 614 case '!': i.skip(); 616 formula = Not(parse(i, P_NOT)); 617 618 break; 619 620 case 'X': i.skip(); 622 formula = Next(parse(i, P_NEXT)); 623 624 break; 625 626 case '[': 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 '<': 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 sb = new StringBuffer (); 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 sbf = new StringBuffer (); 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 } 695 696 String 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 '/': 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 '&': 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 '\\': 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 '|': 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': 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': 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': 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': 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 '-': 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 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 name) { 895 return (Formula) matches.get(name); 896 } 897 898 private void addMatch (String 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 ("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 ("code should not be reached"); 1005 } 1006 1007 1010 public static class EndOfInputException extends Exception { 1011 } 1012 1013 1016 private static class Input { 1017 private StringBuffer sb; 1018 1019 public Input (String str) { 1020 sb = new StringBuffer (str); 1021 } 1022 1023 public char get () throws EndOfInputException { 1024 try { 1025 return sb.charAt(0); 1026 } catch (StringIndexOutOfBoundsException e) { 1027 throw new EndOfInputException(); 1028 } 1029 } 1030 1031 public void skip () throws EndOfInputException { 1032 try { 1033 sb.deleteCharAt(0); 1034 } catch (StringIndexOutOfBoundsException e) { 1035 throw new EndOfInputException(); 1036 } 1037 } 1038 } 1039} | Popular Tags |