00001 package edu.ksu.cis.bandera.abstraction.lib.integral;
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037 import edu.ksu.cis.bandera.abstraction.*;
00038 public class Range04 extends IntegralAbstraction {
00039 private static final Range04 v = new Range04();
00040 public static final int R0 = 0;
00041 public static final int LT0 = 1;
00042 public static final int R1 = 2;
00043 public static final int R2 = 3;
00044 public static final int R3 = 4;
00045 public static final int R4 = 5;
00046 public static final int GT4 = 6;
00047 private Range04() {
00048 }
00049 public static int abs(long n) {
00050 if (n < 0) return LT0;
00051 if (n == 0) return R0;
00052 if (n == 1) return R1;
00053 if (n == 2) return R2;
00054 if (n == 3) return R3;
00055 if (n == 4) return R4;
00056 if (n > 4) return GT4;
00057 throw new RuntimeException("Range04 cannot abstract value '" + n + "'");
00058 }
00059 public static int add(int left$, int right$) {
00060 if (left$ == LT0 && right$ == LT0) return LT0;
00061 if (left$ == LT0 && right$ == R0) return LT0;
00062 if (left$ == LT0 && right$ == R1) return Abstraction.choose((1 << R0) | (1 << LT0));
00063 if (left$ == LT0 && right$ == R2) return Abstraction.choose((1 << R1) | (1 << R0) | (1 << LT0));
00064 if (left$ == LT0 && right$ == R3) return Abstraction.choose((1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00065 if (left$ == LT0 && right$ == R4) return Abstraction.choose((1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00066 if (left$ == LT0 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00067 if (left$ == R0 && right$ == LT0) return LT0;
00068 if (left$ == R0 && right$ == R0) return R0;
00069 if (left$ == R0 && right$ == R1) return R1;
00070 if (left$ == R0 && right$ == R2) return R2;
00071 if (left$ == R0 && right$ == R3) return R3;
00072 if (left$ == R0 && right$ == R4) return R4;
00073 if (left$ == R0 && right$ == GT4) return GT4;
00074 if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << R0) | (1 << LT0));
00075 if (left$ == R1 && right$ == R0) return R1;
00076 if (left$ == R1 && right$ == R1) return R2;
00077 if (left$ == R1 && right$ == R2) return R3;
00078 if (left$ == R1 && right$ == R3) return R4;
00079 if (left$ == R1 && right$ == R4) return GT4;
00080 if (left$ == R1 && right$ == GT4) return GT4;
00081 if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << R1) | (1 << R0) | (1 << LT0));
00082 if (left$ == R2 && right$ == R0) return R2;
00083 if (left$ == R2 && right$ == R1) return R3;
00084 if (left$ == R2 && right$ == R2) return R4;
00085 if (left$ == R2 && right$ == R3) return GT4;
00086 if (left$ == R2 && right$ == R4) return GT4;
00087 if (left$ == R2 && right$ == GT4) return GT4;
00088 if (left$ == R3 && right$ == LT0) return Abstraction.choose((1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00089 if (left$ == R3 && right$ == R0) return R3;
00090 if (left$ == R3 && right$ == R1) return R4;
00091 if (left$ == R3 && right$ == R2) return GT4;
00092 if (left$ == R3 && right$ == R3) return GT4;
00093 if (left$ == R3 && right$ == R4) return GT4;
00094 if (left$ == R3 && right$ == GT4) return GT4;
00095 if (left$ == R4 && right$ == LT0) return Abstraction.choose((1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00096 if (left$ == R4 && right$ == R0) return R4;
00097 if (left$ == R4 && right$ == R1) return GT4;
00098 if (left$ == R4 && right$ == R2) return GT4;
00099 if (left$ == R4 && right$ == R3) return GT4;
00100 if (left$ == R4 && right$ == R4) return GT4;
00101 if (left$ == R4 && right$ == GT4) return GT4;
00102 if (left$ == GT4 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00103 if (left$ == GT4 && right$ == R0) return GT4;
00104 if (left$ == GT4 && right$ == R1) return GT4;
00105 if (left$ == GT4 && right$ == R2) return GT4;
00106 if (left$ == GT4 && right$ == R3) return GT4;
00107 if (left$ == GT4 && right$ == R4) return GT4;
00108 if (left$ == GT4 && right$ == GT4) return GT4;
00109 throw new RuntimeException("Range04.add(" + left$ + ", " + right$ + ") is undefined");
00110 }
00111 private static int addNoChoose(int left, int right) {
00112 int result = 0;
00113 switch (left) {
00114 case 0:
00115 switch (right) {
00116 case 0:
00117 result = 1;
00118 break;
00119 case 1:
00120 result = 2;
00121 break;
00122 case 2:
00123 result = 4;
00124 break;
00125 case 3:
00126 result = 8;
00127 break;
00128 case 4:
00129 result = 16;
00130 break;
00131 case 5:
00132 result = 32;
00133 break;
00134 case 6:
00135 result = 64;
00136 break;
00137 }
00138 break;
00139 case 1:
00140 switch (right) {
00141 case 0:
00142 result = 2;
00143 break;
00144 case 1:
00145 result = 2;
00146 break;
00147 case 2:
00148 result = 3;
00149 break;
00150 case 3:
00151 result = 7;
00152 break;
00153 case 4:
00154 result = 15;
00155 break;
00156 case 5:
00157 result = 31;
00158 break;
00159 case 6:
00160 result = 127;
00161 break;
00162 }
00163 break;
00164 case 2:
00165 switch (right) {
00166 case 0:
00167 result = 4;
00168 break;
00169 case 1:
00170 result = 3;
00171 break;
00172 case 2:
00173 result = 8;
00174 break;
00175 case 3:
00176 result = 16;
00177 break;
00178 case 4:
00179 result = 32;
00180 break;
00181 case 5:
00182 result = 64;
00183 break;
00184 case 6:
00185 result = 64;
00186 break;
00187 }
00188 break;
00189 case 3:
00190 switch (right) {
00191 case 0:
00192 result = 8;
00193 break;
00194 case 1:
00195 result = 7;
00196 break;
00197 case 2:
00198 result = 16;
00199 break;
00200 case 3:
00201 result = 32;
00202 break;
00203 case 4:
00204 result = 64;
00205 break;
00206 case 5:
00207 result = 64;
00208 break;
00209 case 6:
00210 result = 64;
00211 break;
00212 }
00213 break;
00214 case 4:
00215 switch (right) {
00216 case 0:
00217 result = 16;
00218 break;
00219 case 1:
00220 result = 15;
00221 break;
00222 case 2:
00223 result = 32;
00224 break;
00225 case 3:
00226 result = 64;
00227 break;
00228 case 4:
00229 result = 64;
00230 break;
00231 case 5:
00232 result = 64;
00233 break;
00234 case 6:
00235 result = 64;
00236 break;
00237 }
00238 break;
00239 case 5:
00240 switch (right) {
00241 case 0:
00242 result = 32;
00243 break;
00244 case 1:
00245 result = 31;
00246 break;
00247 case 2:
00248 result = 64;
00249 break;
00250 case 3:
00251 result = 64;
00252 break;
00253 case 4:
00254 result = 64;
00255 break;
00256 case 5:
00257 result = 64;
00258 break;
00259 case 6:
00260 result = 64;
00261 break;
00262 }
00263 break;
00264 case 6:
00265 switch (right) {
00266 case 0:
00267 result = 64;
00268 break;
00269 case 1:
00270 result = 127;
00271 break;
00272 case 2:
00273 result = 64;
00274 break;
00275 case 3:
00276 result = 64;
00277 break;
00278 case 4:
00279 result = 64;
00280 break;
00281 case 5:
00282 result = 64;
00283 break;
00284 case 6:
00285 result = 64;
00286 break;
00287 }
00288 break;
00289 }
00290 if (result == 0) throw new RuntimeException("Range04.addNoChoose(" + left + ", " + right + ") is undefined");
00291 return result;
00292 }
00293 public static int addSet(int leftTokens, int rightTokens) {
00294 int result = -1;
00295 for (int left = 0; (1 << left) <= leftTokens; left++) {
00296 if ((leftTokens & (1 << left)) == 0) continue;
00297 for (int right = 0; (1 << right) <= rightTokens; right++) {
00298 if ((rightTokens & (1 << right)) != 0) {
00299 if (result == -1) result = addNoChoose(left, right);
00300 else result = Abstraction.meetArith(result, addNoChoose(left, right));
00301 }
00302 }
00303 }
00304 return result;
00305 }
00306 public static int div(int left$, int right$) {
00307 if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00308 if (left$ == LT0 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00309 if (left$ == LT0 && right$ == R1) return LT0;
00310 if (left$ == LT0 && right$ == R2) return LT0;
00311 if (left$ == LT0 && right$ == R3) return LT0;
00312 if (left$ == LT0 && right$ == R4) return LT0;
00313 if (left$ == LT0 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00314 if (left$ == R0 && right$ == LT0) return R0;
00315 if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00316 if (left$ == R0 && right$ == R1) return R0;
00317 if (left$ == R0 && right$ == R2) return R0;
00318 if (left$ == R0 && right$ == R3) return R0;
00319 if (left$ == R0 && right$ == R4) return R0;
00320 if (left$ == R0 && right$ == GT4) return R0;
00321 if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00322 if (left$ == R1 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00323 if (left$ == R1 && right$ == R1) return R1;
00324 if (left$ == R1 && right$ == R2) return R0;
00325 if (left$ == R1 && right$ == R3) return R0;
00326 if (left$ == R1 && right$ == R4) return R0;
00327 if (left$ == R1 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00328 if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00329 if (left$ == R2 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00330 if (left$ == R2 && right$ == R1) return R2;
00331 if (left$ == R2 && right$ == R2) return R1;
00332 if (left$ == R2 && right$ == R3) return R0;
00333 if (left$ == R2 && right$ == R4) return R0;
00334 if (left$ == R2 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00335 if (left$ == R3 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00336 if (left$ == R3 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00337 if (left$ == R3 && right$ == R1) return R3;
00338 if (left$ == R3 && right$ == R2) return R1;
00339 if (left$ == R3 && right$ == R3) return R1;
00340 if (left$ == R3 && right$ == R4) return R0;
00341 if (left$ == R3 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00342 if (left$ == R4 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00343 if (left$ == R4 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00344 if (left$ == R4 && right$ == R1) return R4;
00345 if (left$ == R4 && right$ == R2) return R2;
00346 if (left$ == R4 && right$ == R3) return R1;
00347 if (left$ == R4 && right$ == R4) return R1;
00348 if (left$ == R4 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00349 if (left$ == GT4 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00350 if (left$ == GT4 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00351 if (left$ == GT4 && right$ == R1) return GT4;
00352 if (left$ == GT4 && right$ == R2) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2));
00353 if (left$ == GT4 && right$ == R3) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1));
00354 if (left$ == GT4 && right$ == R4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1));
00355 if (left$ == GT4 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00356 throw new RuntimeException("Range04.div(" + left$ + ", " + right$ + ") is undefined");
00357 }
00358 private static int divNoChoose(int left, int right) {
00359 int result = 0;
00360 switch (left) {
00361 case 0:
00362 switch (right) {
00363 case 0:
00364 result = 127;
00365 break;
00366 case 1:
00367 result = 1;
00368 break;
00369 case 2:
00370 result = 1;
00371 break;
00372 case 3:
00373 result = 1;
00374 break;
00375 case 4:
00376 result = 1;
00377 break;
00378 case 5:
00379 result = 1;
00380 break;
00381 case 6:
00382 result = 1;
00383 break;
00384 }
00385 break;
00386 case 1:
00387 switch (right) {
00388 case 0:
00389 result = 127;
00390 break;
00391 case 1:
00392 result = 127;
00393 break;
00394 case 2:
00395 result = 2;
00396 break;
00397 case 3:
00398 result = 2;
00399 break;
00400 case 4:
00401 result = 2;
00402 break;
00403 case 5:
00404 result = 2;
00405 break;
00406 case 6:
00407 result = 127;
00408 break;
00409 }
00410 break;
00411 case 2:
00412 switch (right) {
00413 case 0:
00414 result = 127;
00415 break;
00416 case 1:
00417 result = 127;
00418 break;
00419 case 2:
00420 result = 4;
00421 break;
00422 case 3:
00423 result = 1;
00424 break;
00425 case 4:
00426 result = 1;
00427 break;
00428 case 5:
00429 result = 1;
00430 break;
00431 case 6:
00432 result = 127;
00433 break;
00434 }
00435 break;
00436 case 3:
00437 switch (right) {
00438 case 0:
00439 result = 127;
00440 break;
00441 case 1:
00442 result = 127;
00443 break;
00444 case 2:
00445 result = 8;
00446 break;
00447 case 3:
00448 result = 4;
00449 break;
00450 case 4:
00451 result = 1;
00452 break;
00453 case 5:
00454 result = 1;
00455 break;
00456 case 6:
00457 result = 127;
00458 break;
00459 }
00460 break;
00461 case 4:
00462 switch (right) {
00463 case 0:
00464 result = 127;
00465 break;
00466 case 1:
00467 result = 127;
00468 break;
00469 case 2:
00470 result = 16;
00471 break;
00472 case 3:
00473 result = 4;
00474 break;
00475 case 4:
00476 result = 4;
00477 break;
00478 case 5:
00479 result = 1;
00480 break;
00481 case 6:
00482 result = 127;
00483 break;
00484 }
00485 break;
00486 case 5:
00487 switch (right) {
00488 case 0:
00489 result = 127;
00490 break;
00491 case 1:
00492 result = 127;
00493 break;
00494 case 2:
00495 result = 32;
00496 break;
00497 case 3:
00498 result = 8;
00499 break;
00500 case 4:
00501 result = 4;
00502 break;
00503 case 5:
00504 result = 4;
00505 break;
00506 case 6:
00507 result = 127;
00508 break;
00509 }
00510 break;
00511 case 6:
00512 switch (right) {
00513 case 0:
00514 result = 127;
00515 break;
00516 case 1:
00517 result = 127;
00518 break;
00519 case 2:
00520 result = 64;
00521 break;
00522 case 3:
00523 result = 120;
00524 break;
00525 case 4:
00526 result = 124;
00527 break;
00528 case 5:
00529 result = 124;
00530 break;
00531 case 6:
00532 result = 127;
00533 break;
00534 }
00535 break;
00536 }
00537 if (result == 0) throw new RuntimeException("Range04.divNoChoose(" + left + ", " + right + ") is undefined");
00538 return result;
00539 }
00540 public static int divSet(int leftTokens, int rightTokens) {
00541 int result = -1;
00542 for (int left = 0; (1 << left) <= leftTokens; left++) {
00543 if ((leftTokens & (1 << left)) == 0) continue;
00544 for (int right = 0; (1 << right) <= rightTokens; right++) {
00545 if ((rightTokens & (1 << right)) != 0) {
00546 if (result == -1) result = divNoChoose(left, right);
00547 else result = Abstraction.meetArith(result, divNoChoose(left, right));
00548 }
00549 }
00550 }
00551 return result;
00552 }
00553 public static boolean eq(int left$, int right$) {
00554 if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00555 if (left$ == LT0 && right$ == R0) return false;
00556 if (left$ == LT0 && right$ == R1) return false;
00557 if (left$ == LT0 && right$ == R2) return false;
00558 if (left$ == LT0 && right$ == R3) return false;
00559 if (left$ == LT0 && right$ == R4) return false;
00560 if (left$ == LT0 && right$ == GT4) return false;
00561 if (left$ == R0 && right$ == LT0) return false;
00562 if (left$ == R0 && right$ == R0) return true;
00563 if (left$ == R0 && right$ == R1) return false;
00564 if (left$ == R0 && right$ == R2) return false;
00565 if (left$ == R0 && right$ == R3) return false;
00566 if (left$ == R0 && right$ == R4) return false;
00567 if (left$ == R0 && right$ == GT4) return false;
00568 if (left$ == R1 && right$ == LT0) return false;
00569 if (left$ == R1 && right$ == R0) return false;
00570 if (left$ == R1 && right$ == R1) return true;
00571 if (left$ == R1 && right$ == R2) return false;
00572 if (left$ == R1 && right$ == R3) return false;
00573 if (left$ == R1 && right$ == R4) return false;
00574 if (left$ == R1 && right$ == GT4) return false;
00575 if (left$ == R2 && right$ == LT0) return false;
00576 if (left$ == R2 && right$ == R0) return false;
00577 if (left$ == R2 && right$ == R1) return false;
00578 if (left$ == R2 && right$ == R2) return true;
00579 if (left$ == R2 && right$ == R3) return false;
00580 if (left$ == R2 && right$ == R4) return false;
00581 if (left$ == R2 && right$ == GT4) return false;
00582 if (left$ == R3 && right$ == LT0) return false;
00583 if (left$ == R3 && right$ == R0) return false;
00584 if (left$ == R3 && right$ == R1) return false;
00585 if (left$ == R3 && right$ == R2) return false;
00586 if (left$ == R3 && right$ == R3) return true;
00587 if (left$ == R3 && right$ == R4) return false;
00588 if (left$ == R3 && right$ == GT4) return false;
00589 if (left$ == R4 && right$ == LT0) return false;
00590 if (left$ == R4 && right$ == R0) return false;
00591 if (left$ == R4 && right$ == R1) return false;
00592 if (left$ == R4 && right$ == R2) return false;
00593 if (left$ == R4 && right$ == R3) return false;
00594 if (left$ == R4 && right$ == R4) return true;
00595 if (left$ == R4 && right$ == GT4) return false;
00596 if (left$ == GT4 && right$ == LT0) return false;
00597 if (left$ == GT4 && right$ == R0) return false;
00598 if (left$ == GT4 && right$ == R1) return false;
00599 if (left$ == GT4 && right$ == R2) return false;
00600 if (left$ == GT4 && right$ == R3) return false;
00601 if (left$ == GT4 && right$ == R4) return false;
00602 if (left$ == GT4 && right$ == GT4) return Abstraction.choose();
00603 throw new RuntimeException("Range04.eq(" + left$ + ", " + right$ + ") is undefined");
00604 }
00605 private static byte eqNoChoose(int left, int right) {
00606 byte result = -1;
00607 switch (left) {
00608 case 0:
00609 switch (right) {
00610 case 0:
00611 result = 1;
00612 break;
00613 case 1:
00614 result = 0;
00615 break;
00616 case 2:
00617 result = 0;
00618 break;
00619 case 3:
00620 result = 0;
00621 break;
00622 case 4:
00623 result = 0;
00624 break;
00625 case 5:
00626 result = 0;
00627 break;
00628 case 6:
00629 result = 0;
00630 break;
00631 }
00632 break;
00633 case 1:
00634 switch (right) {
00635 case 0:
00636 result = 0;
00637 break;
00638 case 1:
00639 result = 2;
00640 break;
00641 case 2:
00642 result = 0;
00643 break;
00644 case 3:
00645 result = 0;
00646 break;
00647 case 4:
00648 result = 0;
00649 break;
00650 case 5:
00651 result = 0;
00652 break;
00653 case 6:
00654 result = 0;
00655 break;
00656 }
00657 break;
00658 case 2:
00659 switch (right) {
00660 case 0:
00661 result = 0;
00662 break;
00663 case 1:
00664 result = 0;
00665 break;
00666 case 2:
00667 result = 1;
00668 break;
00669 case 3:
00670 result = 0;
00671 break;
00672 case 4:
00673 result = 0;
00674 break;
00675 case 5:
00676 result = 0;
00677 break;
00678 case 6:
00679 result = 0;
00680 break;
00681 }
00682 break;
00683 case 3:
00684 switch (right) {
00685 case 0:
00686 result = 0;
00687 break;
00688 case 1:
00689 result = 0;
00690 break;
00691 case 2:
00692 result = 0;
00693 break;
00694 case 3:
00695 result = 1;
00696 break;
00697 case 4:
00698 result = 0;
00699 break;
00700 case 5:
00701 result = 0;
00702 break;
00703 case 6:
00704 result = 0;
00705 break;
00706 }
00707 break;
00708 case 4:
00709 switch (right) {
00710 case 0:
00711 result = 0;
00712 break;
00713 case 1:
00714 result = 0;
00715 break;
00716 case 2:
00717 result = 0;
00718 break;
00719 case 3:
00720 result = 0;
00721 break;
00722 case 4:
00723 result = 1;
00724 break;
00725 case 5:
00726 result = 0;
00727 break;
00728 case 6:
00729 result = 0;
00730 break;
00731 }
00732 break;
00733 case 5:
00734 switch (right) {
00735 case 0:
00736 result = 0;
00737 break;
00738 case 1:
00739 result = 0;
00740 break;
00741 case 2:
00742 result = 0;
00743 break;
00744 case 3:
00745 result = 0;
00746 break;
00747 case 4:
00748 result = 0;
00749 break;
00750 case 5:
00751 result = 1;
00752 break;
00753 case 6:
00754 result = 0;
00755 break;
00756 }
00757 break;
00758 case 6:
00759 switch (right) {
00760 case 0:
00761 result = 0;
00762 break;
00763 case 1:
00764 result = 0;
00765 break;
00766 case 2:
00767 result = 0;
00768 break;
00769 case 3:
00770 result = 0;
00771 break;
00772 case 4:
00773 result = 0;
00774 break;
00775 case 5:
00776 result = 0;
00777 break;
00778 case 6:
00779 result = 2;
00780 break;
00781 }
00782 break;
00783 }
00784 if (result == -1) throw new RuntimeException("Range04.eqNoChoose(" + left + ", " + right + ") is undefined");
00785 return result;
00786 }
00787 public static byte eqSet(int leftTokens, int rightTokens) {
00788 byte result = -1;
00789 for (int left = 0; (1 << left) <= leftTokens; left++) {
00790 if ((leftTokens & (1 << left)) == 0) continue;
00791 for (int right = 0; (1 << right) <= rightTokens; right++) {
00792 if ((rightTokens & (1 << right)) != 0) {
00793 if (result == -1) result = eqNoChoose(left, right);
00794 else result = Abstraction.meetTest(result, eqNoChoose(left, right));
00795 }
00796 }
00797 }
00798 return result;
00799 }
00800 public static boolean ge(int left$, int right$) {
00801 if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00802 if (left$ == LT0 && right$ == R0) return false;
00803 if (left$ == LT0 && right$ == R1) return false;
00804 if (left$ == LT0 && right$ == R2) return false;
00805 if (left$ == LT0 && right$ == R3) return false;
00806 if (left$ == LT0 && right$ == R4) return false;
00807 if (left$ == LT0 && right$ == GT4) return false;
00808 if (left$ == R0 && right$ == LT0) return true;
00809 if (left$ == R0 && right$ == R0) return true;
00810 if (left$ == R0 && right$ == R1) return false;
00811 if (left$ == R0 && right$ == R2) return false;
00812 if (left$ == R0 && right$ == R3) return false;
00813 if (left$ == R0 && right$ == R4) return false;
00814 if (left$ == R0 && right$ == GT4) return false;
00815 if (left$ == R1 && right$ == LT0) return true;
00816 if (left$ == R1 && right$ == R0) return true;
00817 if (left$ == R1 && right$ == R1) return true;
00818 if (left$ == R1 && right$ == R2) return false;
00819 if (left$ == R1 && right$ == R3) return false;
00820 if (left$ == R1 && right$ == R4) return false;
00821 if (left$ == R1 && right$ == GT4) return false;
00822 if (left$ == R2 && right$ == LT0) return true;
00823 if (left$ == R2 && right$ == R0) return true;
00824 if (left$ == R2 && right$ == R1) return true;
00825 if (left$ == R2 && right$ == R2) return true;
00826 if (left$ == R2 && right$ == R3) return false;
00827 if (left$ == R2 && right$ == R4) return false;
00828 if (left$ == R2 && right$ == GT4) return false;
00829 if (left$ == R3 && right$ == LT0) return true;
00830 if (left$ == R3 && right$ == R0) return true;
00831 if (left$ == R3 && right$ == R1) return true;
00832 if (left$ == R3 && right$ == R2) return true;
00833 if (left$ == R3 && right$ == R3) return true;
00834 if (left$ == R3 && right$ == R4) return false;
00835 if (left$ == R3 && right$ == GT4) return false;
00836 if (left$ == R4 && right$ == LT0) return true;
00837 if (left$ == R4 && right$ == R0) return true;
00838 if (left$ == R4 && right$ == R1) return true;
00839 if (left$ == R4 && right$ == R2) return true;
00840 if (left$ == R4 && right$ == R3) return true;
00841 if (left$ == R4 && right$ == R4) return true;
00842 if (left$ == R4 && right$ == GT4) return false;
00843 if (left$ == GT4 && right$ == LT0) return true;
00844 if (left$ == GT4 && right$ == R0) return true;
00845 if (left$ == GT4 && right$ == R1) return true;
00846 if (left$ == GT4 && right$ == R2) return true;
00847 if (left$ == GT4 && right$ == R3) return true;
00848 if (left$ == GT4 && right$ == R4) return true;
00849 if (left$ == GT4 && right$ == GT4) return Abstraction.choose();
00850 throw new RuntimeException("Range04.ge(" + left$ + ", " + right$ + ") is undefined");
00851 }
00852 private static byte geNoChoose(int left, int right) {
00853 byte result = -1;
00854 switch (left) {
00855 case 0:
00856 switch (right) {
00857 case 0:
00858 result = 1;
00859 break;
00860 case 1:
00861 result = 1;
00862 break;
00863 case 2:
00864 result = 0;
00865 break;
00866 case 3:
00867 result = 0;
00868 break;
00869 case 4:
00870 result = 0;
00871 break;
00872 case 5:
00873 result = 0;
00874 break;
00875 case 6:
00876 result = 0;
00877 break;
00878 }
00879 break;
00880 case 1:
00881 switch (right) {
00882 case 0:
00883 result = 0;
00884 break;
00885 case 1:
00886 result = 2;
00887 break;
00888 case 2:
00889 result = 0;
00890 break;
00891 case 3:
00892 result = 0;
00893 break;
00894 case 4:
00895 result = 0;
00896 break;
00897 case 5:
00898 result = 0;
00899 break;
00900 case 6:
00901 result = 0;
00902 break;
00903 }
00904 break;
00905 case 2:
00906 switch (right) {
00907 case 0:
00908 result = 1;
00909 break;
00910 case 1:
00911 result = 1;
00912 break;
00913 case 2:
00914 result = 1;
00915 break;
00916 case 3:
00917 result = 0;
00918 break;
00919 case 4:
00920 result = 0;
00921 break;
00922 case 5:
00923 result = 0;
00924 break;
00925 case 6:
00926 result = 0;
00927 break;
00928 }
00929 break;
00930 case 3:
00931 switch (right) {
00932 case 0:
00933 result = 1;
00934 break;
00935 case 1:
00936 result = 1;
00937 break;
00938 case 2:
00939 result = 1;
00940 break;
00941 case 3:
00942 result = 1;
00943 break;
00944 case 4:
00945 result = 0;
00946 break;
00947 case 5:
00948 result = 0;
00949 break;
00950 case 6:
00951 result = 0;
00952 break;
00953 }
00954 break;
00955 case 4:
00956 switch (right) {
00957 case 0:
00958 result = 1;
00959 break;
00960 case 1:
00961 result = 1;
00962 break;
00963 case 2:
00964 result = 1;
00965 break;
00966 case 3:
00967 result = 1;
00968 break;
00969 case 4:
00970 result = 1;
00971 break;
00972 case 5:
00973 result = 0;
00974 break;
00975 case 6:
00976 result = 0;
00977 break;
00978 }
00979 break;
00980 case 5:
00981 switch (right) {
00982 case 0:
00983 result = 1;
00984 break;
00985 case 1:
00986 result = 1;
00987 break;
00988 case 2:
00989 result = 1;
00990 break;
00991 case 3:
00992 result = 1;
00993 break;
00994 case 4:
00995 result = 1;
00996 break;
00997 case 5:
00998 result = 1;
00999 break;
01000 case 6:
01001 result = 0;
01002 break;
01003 }
01004 break;
01005 case 6:
01006 switch (right) {
01007 case 0:
01008 result = 1;
01009 break;
01010 case 1:
01011 result = 1;
01012 break;
01013 case 2:
01014 result = 1;
01015 break;
01016 case 3:
01017 result = 1;
01018 break;
01019 case 4:
01020 result = 1;
01021 break;
01022 case 5:
01023 result = 1;
01024 break;
01025 case 6:
01026 result = 2;
01027 break;
01028 }
01029 break;
01030 }
01031 if (result == -1) throw new RuntimeException("Range04.geNoChoose(" + left + ", " + right + ") is undefined");
01032 return result;
01033 }
01034 public static byte geSet(int leftTokens, int rightTokens) {
01035 byte result = -1;
01036 for (int left = 0; (1 << left) <= leftTokens; left++) {
01037 if ((leftTokens & (1 << left)) == 0) continue;
01038 for (int right = 0; (1 << right) <= rightTokens; right++) {
01039 if ((rightTokens & (1 << right)) != 0) {
01040 if (result == -1) result = geNoChoose(left, right);
01041 else result = Abstraction.meetTest(result, geNoChoose(left, right));
01042 }
01043 }
01044 }
01045 return result;
01046 }
01047 public static String getBASLRepresentation() {
01048 return
01049 "abstraction Range04 extends integral \n"
01050 + " begin\n"
01051 + " TOKENS = {LT0, R0, R1, R2, R3, R4, GT4};\n"
01052 + " DEFAULT = R0;\n"
01053 + " ONE2ONE = {R0, R1, R2, R3, R4};\n"
01054 + " abstract (n)\n"
01055 + " begin\n"
01056 + " n < 0 -> LT0;\n"
01057 + " n == 0 -> R0;\n"
01058 + " n == 1 -> R1;\n"
01059 + " n == 2 -> R2;\n"
01060 + " n == 3 -> R3;\n"
01061 + " n == 4 -> R4;\n"
01062 + " n > 4 -> GT4;\n"
01063 + " end\n"
01064 + " operator + add \n"
01065 + " begin\n"
01066 + " (LT0, LT0) -> LT0;\n"
01067 + " (LT0, R0) -> LT0;\n"
01068 + " (LT0, R1) -> {LT0, R0};\n"
01069 + " (LT0, R2) -> {LT0, R0, R1};\n"
01070 + " (LT0, R3) -> {LT0, R0, R1, R2};\n"
01071 + " (LT0, R4) -> {LT0, R0, R1, R2, R3};\n"
01072 + " (LT0, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01073 + " (R0, LT0) -> LT0;\n"
01074 + " (R0, R0) -> R0;\n"
01075 + " (R0, R1) -> R1;\n"
01076 + " (R0, R2) -> R2;\n"
01077 + " (R0, R3) -> R3;\n"
01078 + " (R0, R4) -> R4;\n"
01079 + " (R0, GT4) -> GT4;\n"
01080 + " (R1, LT0) -> {LT0, R0};\n"
01081 + " (R1, R0) -> R1;\n"
01082 + " (R1, R1) -> R2;\n"
01083 + " (R1, R2) -> R3;\n"
01084 + " (R1, R3) -> R4;\n"
01085 + " (R1, R4) -> GT4;\n"
01086 + " (R1, GT4) -> GT4;\n"
01087 + " (R2, LT0) -> {LT0, R0, R1};\n"
01088 + " (R2, R0) -> R2;\n"
01089 + " (R2, R1) -> R3;\n"
01090 + " (R2, R2) -> R4;\n"
01091 + " (R2, R3) -> GT4;\n"
01092 + " (R2, R4) -> GT4;\n"
01093 + " (R2, GT4) -> GT4;\n"
01094 + " (R3, LT0) -> {LT0, R0, R1, R2};\n"
01095 + " (R3, R0) -> R3;\n"
01096 + " (R3, R1) -> R4;\n"
01097 + " (R3, R2) -> GT4;\n"
01098 + " (R3, R3) -> GT4;\n"
01099 + " (R3, R4) -> GT4;\n"
01100 + " (R3, GT4) -> GT4;\n"
01101 + " (R4, LT0) -> {LT0, R0, R1, R2, R3};\n"
01102 + " (R4, R0) -> R4;\n"
01103 + " (R4, R1) -> GT4;\n"
01104 + " (R4, R2) -> GT4;\n"
01105 + " (R4, R3) -> GT4;\n"
01106 + " (R4, R4) -> GT4;\n"
01107 + " (R4, GT4) -> GT4;\n"
01108 + " (GT4, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01109 + " (GT4, R0) -> GT4;\n"
01110 + " (GT4, R1) -> GT4;\n"
01111 + " (GT4, R2) -> GT4;\n"
01112 + " (GT4, R3) -> GT4;\n"
01113 + " (GT4, R4) -> GT4;\n"
01114 + " (GT4, GT4) -> GT4;\n"
01115 + " end\n"
01116 + " operator - sub \n"
01117 + " begin\n"
01118 + " (LT0, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01119 + " (LT0, R0) -> LT0;\n"
01120 + " (LT0, R1) -> LT0;\n"
01121 + " (LT0, R2) -> LT0;\n"
01122 + " (LT0, R3) -> LT0;\n"
01123 + " (LT0, R4) -> LT0;\n"
01124 + " (LT0, GT4) -> LT0;\n"
01125 + " (R0, LT0) -> {R1, R2, R3, R4, GT4};\n"
01126 + " (R0, R0) -> R0;\n"
01127 + " (R0, R1) -> LT0;\n"
01128 + " (R0, R2) -> LT0;\n"
01129 + " (R0, R3) -> LT0;\n"
01130 + " (R0, R4) -> LT0;\n"
01131 + " (R0, GT4) -> LT0;\n"
01132 + " (R1, LT0) -> {R2, R3, R4, GT4};\n"
01133 + " (R1, R0) -> R1;\n"
01134 + " (R1, R1) -> R0;\n"
01135 + " (R1, R2) -> LT0;\n"
01136 + " (R1, R3) -> LT0;\n"
01137 + " (R1, R4) -> LT0;\n"
01138 + " (R1, GT4) -> LT0;\n"
01139 + " (R2, LT0) -> {R3, R4, GT4};\n"
01140 + " (R2, R0) -> R2;\n"
01141 + " (R2, R1) -> R1;\n"
01142 + " (R2, R2) -> R0;\n"
01143 + " (R2, R3) -> LT0;\n"
01144 + " (R2, R4) -> LT0;\n"
01145 + " (R2, GT4) -> LT0;\n"
01146 + " (R3, LT0) -> {R4, GT4};\n"
01147 + " (R3, R0) -> R3;\n"
01148 + " (R3, R1) -> R2;\n"
01149 + " (R3, R2) -> R1;\n"
01150 + " (R3, R3) -> R0;\n"
01151 + " (R3, R4) -> LT0;\n"
01152 + " (R3, GT4) -> LT0;\n"
01153 + " (R4, LT0) -> GT4;\n"
01154 + " (R4, R0) -> R4;\n"
01155 + " (R4, R1) -> R3;\n"
01156 + " (R4, R2) -> R2;\n"
01157 + " (R4, R3) -> R1;\n"
01158 + " (R4, R4) -> R0;\n"
01159 + " (R4, GT4) -> LT0;\n"
01160 + " (GT4, LT0) -> GT4;\n"
01161 + " (GT4, R0) -> GT4;\n"
01162 + " (GT4, R1) -> {R4, GT4};\n"
01163 + " (GT4, R2) -> {R3, R4, GT4};\n"
01164 + " (GT4, R3) -> {R2, R3, R4, GT4};\n"
01165 + " (GT4, R4) -> {R1, R2, R3, R4, GT4};\n"
01166 + " (GT4, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01167 + " end\n"
01168 + " operator * mul \n"
01169 + " begin\n"
01170 + " (LT0, LT0) -> {R1, R2, R3, R4, GT4};\n"
01171 + " (LT0, R0) -> R0;\n"
01172 + " (LT0, R1) -> LT0;\n"
01173 + " (LT0, R2) -> LT0;\n"
01174 + " (LT0, R3) -> LT0;\n"
01175 + " (LT0, R4) -> LT0;\n"
01176 + " (LT0, GT4) -> {LT0, R1, R2, R3, R4, GT4};\n"
01177 + " (R0, LT0) -> R0;\n"
01178 + " (R0, R0) -> R0;\n"
01179 + " (R0, R1) -> R0;\n"
01180 + " (R0, R2) -> R0;\n"
01181 + " (R0, R3) -> R0;\n"
01182 + " (R0, R4) -> R0;\n"
01183 + " (R0, GT4) -> R0;\n"
01184 + " (R1, LT0) -> LT0;\n"
01185 + " (R1, R0) -> R0;\n"
01186 + " (R1, R1) -> R1;\n"
01187 + " (R1, R2) -> R2;\n"
01188 + " (R1, R3) -> R3;\n"
01189 + " (R1, R4) -> R4;\n"
01190 + " (R1, GT4) -> GT4;\n"
01191 + " (R2, LT0) -> LT0;\n"
01192 + " (R2, R0) -> R0;\n"
01193 + " (R2, R1) -> R2;\n"
01194 + " (R2, R2) -> R4;\n"
01195 + " (R2, R3) -> GT4;\n"
01196 + " (R2, R4) -> GT4;\n"
01197 + " (R2, GT4) -> GT4;\n"
01198 + " (R3, LT0) -> LT0;\n"
01199 + " (R3, R0) -> R0;\n"
01200 + " (R3, R1) -> R3;\n"
01201 + " (R3, R2) -> GT4;\n"
01202 + " (R3, R3) -> GT4;\n"
01203 + " (R3, R4) -> GT4;\n"
01204 + " (R3, GT4) -> GT4;\n"
01205 + " (R4, LT0) -> LT0;\n"
01206 + " (R4, R0) -> R0;\n"
01207 + " (R4, R1) -> R4;\n"
01208 + " (R4, R2) -> GT4;\n"
01209 + " (R4, R3) -> GT4;\n"
01210 + " (R4, R4) -> GT4;\n"
01211 + " (R4, GT4) -> GT4;\n"
01212 + " (GT4, LT0) -> {LT0, R1, R2, R3, R4, GT4};\n"
01213 + " (GT4, R0) -> R0;\n"
01214 + " (GT4, R1) -> GT4;\n"
01215 + " (GT4, R2) -> GT4;\n"
01216 + " (GT4, R3) -> GT4;\n"
01217 + " (GT4, R4) -> GT4;\n"
01218 + " (GT4, GT4) -> {R1, R2, R3, R4, GT4};\n"
01219 + " end\n"
01220 + " operator / div \n"
01221 + " begin\n"
01222 + " (LT0, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01223 + " (LT0, R0) -> T;\n"
01224 + " (LT0, R1) -> LT0;\n"
01225 + " (LT0, R2) -> LT0;\n"
01226 + " (LT0, R3) -> LT0;\n"
01227 + " (LT0, R4) -> LT0;\n"
01228 + " (LT0, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01229 + " (R0, LT0) -> R0;\n"
01230 + " (R0, R0) -> T;\n"
01231 + " (R0, R1) -> R0;\n"
01232 + " (R0, R2) -> R0;\n"
01233 + " (R0, R3) -> R0;\n"
01234 + " (R0, R4) -> R0;\n"
01235 + " (R0, GT4) -> R0;\n"
01236 + " (R1, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01237 + " (R1, R0) -> T;\n"
01238 + " (R1, R1) -> R1;\n"
01239 + " (R1, R2) -> R0;\n"
01240 + " (R1, R3) -> R0;\n"
01241 + " (R1, R4) -> R0;\n"
01242 + " (R1, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01243 + " (R2, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01244 + " (R2, R0) -> T;\n"
01245 + " (R2, R1) -> R2;\n"
01246 + " (R2, R2) -> R1;\n"
01247 + " (R2, R3) -> R0;\n"
01248 + " (R2, R4) -> R0;\n"
01249 + " (R2, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01250 + " (R3, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01251 + " (R3, R0) -> T;\n"
01252 + " (R3, R1) -> R3;\n"
01253 + " (R3, R2) -> R1;\n"
01254 + " (R3, R3) -> R1;\n"
01255 + " (R3, R4) -> R0;\n"
01256 + " (R3, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01257 + " (R4, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01258 + " (R4, R0) -> T;\n"
01259 + " (R4, R1) -> R4;\n"
01260 + " (R4, R2) -> R2;\n"
01261 + " (R4, R3) -> R1;\n"
01262 + " (R4, R4) -> R1;\n"
01263 + " (R4, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01264 + " (GT4, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01265 + " (GT4, R0) -> T;\n"
01266 + " (GT4, R1) -> GT4;\n"
01267 + " (GT4, R2) -> {R2, R3, R4, GT4};\n"
01268 + " (GT4, R3) -> {R1, R2, R3, R4, GT4};\n"
01269 + " (GT4, R4) -> {R1, R2, R3, R4, GT4};\n"
01270 + " (GT4, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01271 + " end\n"
01272 + " operator % rem \n"
01273 + " begin\n"
01274 + " (LT0, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01275 + " (LT0, R0) -> T;\n"
01276 + " (LT0, R1) -> R0;\n"
01277 + " (LT0, R2) -> {R0, R1};\n"
01278 + " (LT0, R3) -> {R0, R1, R2};\n"
01279 + " (LT0, R4) -> {R0, R1, R2, R3};\n"
01280 + " (LT0, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01281 + " (R0, LT0) -> R0;\n"
01282 + " (R0, R0) -> T;\n"
01283 + " (R0, R1) -> R0;\n"
01284 + " (R0, R2) -> R0;\n"
01285 + " (R0, R3) -> R0;\n"
01286 + " (R0, R4) -> R0;\n"
01287 + " (R0, GT4) -> R0;\n"
01288 + " (R1, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01289 + " (R1, R0) -> T;\n"
01290 + " (R1, R1) -> R0;\n"
01291 + " (R1, R2) -> R1;\n"
01292 + " (R1, R3) -> R1;\n"
01293 + " (R1, R4) -> R1;\n"
01294 + " (R1, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01295 + " (R2, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01296 + " (R2, R0) -> T;\n"
01297 + " (R2, R1) -> R0;\n"
01298 + " (R2, R2) -> R0;\n"
01299 + " (R2, R3) -> R2;\n"
01300 + " (R2, R4) -> R2;\n"
01301 + " (R2, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01302 + " (R3, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01303 + " (R3, R0) -> T;\n"
01304 + " (R3, R1) -> R0;\n"
01305 + " (R3, R2) -> R1;\n"
01306 + " (R3, R3) -> R0;\n"
01307 + " (R3, R4) -> R3;\n"
01308 + " (R3, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01309 + " (R4, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01310 + " (R4, R0) -> T;\n"
01311 + " (R4, R1) -> R0;\n"
01312 + " (R4, R2) -> R0;\n"
01313 + " (R4, R3) -> R1;\n"
01314 + " (R4, R4) -> R0;\n"
01315 + " (R4, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01316 + " (GT4, LT0) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01317 + " (GT4, R0) -> T;\n"
01318 + " (GT4, R1) -> R0;\n"
01319 + " (GT4, R2) -> {R0, R1};\n"
01320 + " (GT4, R3) -> {R0, R1, R2};\n"
01321 + " (GT4, R4) -> {R0, R1, R2, R3};\n"
01322 + " (GT4, GT4) -> {LT0, R0, R1, R2, R3, R4, GT4};\n"
01323 + " end\n"
01324 + " test == eq \n"
01325 + " begin\n"
01326 + " (LT0, LT0) -> {TRUE, FALSE};\n"
01327 + " (LT0, R0) -> FALSE;\n"
01328 + " (LT0, R1) -> FALSE;\n"
01329 + " (LT0, R2) -> FALSE;\n"
01330 + " (LT0, R3) -> FALSE;\n"
01331 + " (LT0, R4) -> FALSE;\n"
01332 + " (LT0, GT4) -> FALSE;\n"
01333 + " (R0, LT0) -> FALSE;\n"
01334 + " (R0, R0) -> TRUE;\n"
01335 + " (R0, R1) -> FALSE;\n"
01336 + " (R0, R2) -> FALSE;\n"
01337 + " (R0, R3) -> FALSE;\n"
01338 + " (R0, R4) -> FALSE;\n"
01339 + " (R0, GT4) -> FALSE;\n"
01340 + " (R1, LT0) -> FALSE;\n"
01341 + " (R1, R0) -> FALSE;\n"
01342 + " (R1, R1) -> TRUE;\n"
01343 + " (R1, R2) -> FALSE;\n"
01344 + " (R1, R3) -> FALSE;\n"
01345 + " (R1, R4) -> FALSE;\n"
01346 + " (R1, GT4) -> FALSE;\n"
01347 + " (R2, LT0) -> FALSE;\n"
01348 + " (R2, R0) -> FALSE;\n"
01349 + " (R2, R1) -> FALSE;\n"
01350 + " (R2, R2) -> TRUE;\n"
01351 + " (R2, R3) -> FALSE;\n"
01352 + " (R2, R4) -> FALSE;\n"
01353 + " (R2, GT4) -> FALSE;\n"
01354 + " (R3, LT0) -> FALSE;\n"
01355 + " (R3, R0) -> FALSE;\n"
01356 + " (R3, R1) -> FALSE;\n"
01357 + " (R3, R2) -> FALSE;\n"
01358 + " (R3, R3) -> TRUE;\n"
01359 + " (R3, R4) -> FALSE;\n"
01360 + " (R3, GT4) -> FALSE;\n"
01361 + " (R4, LT0) -> FALSE;\n"
01362 + " (R4, R0) -> FALSE;\n"
01363 + " (R4, R1) -> FALSE;\n"
01364 + " (R4, R2) -> FALSE;\n"
01365 + " (R4, R3) -> FALSE;\n"
01366 + " (R4, R4) -> TRUE;\n"
01367 + " (R4, GT4) -> FALSE;\n"
01368 + " (GT4, LT0) -> FALSE;\n"
01369 + " (GT4, R0) -> FALSE;\n"
01370 + " (GT4, R1) -> FALSE;\n"
01371 + " (GT4, R2) -> FALSE;\n"
01372 + " (GT4, R3) -> FALSE;\n"
01373 + " (GT4, R4) -> FALSE;\n"
01374 + " (GT4, GT4) -> {TRUE, FALSE};\n"
01375 + " end\n"
01376 + " test != neq \n"
01377 + " begin\n"
01378 + " (LT0, LT0) -> {TRUE, FALSE};\n"
01379 + " (LT0, R0) -> TRUE;\n"
01380 + " (LT0, R1) -> TRUE;\n"
01381 + " (LT0, R2) -> TRUE;\n"
01382 + " (LT0, R3) -> TRUE;\n"
01383 + " (LT0, R4) -> TRUE;\n"
01384 + " (LT0, GT4) -> TRUE;\n"
01385 + " (R0, LT0) -> TRUE;\n"
01386 + " (R0, R0) -> FALSE;\n"
01387 + " (R0, R1) -> TRUE;\n"
01388 + " (R0, R2) -> TRUE;\n"
01389 + " (R0, R3) -> TRUE;\n"
01390 + " (R0, R4) -> TRUE;\n"
01391 + " (R0, GT4) -> TRUE;\n"
01392 + " (R1, LT0) -> TRUE;\n"
01393 + " (R1, R0) -> TRUE;\n"
01394 + " (R1, R1) -> FALSE;\n"
01395 + " (R1, R2) -> TRUE;\n"
01396 + " (R1, R3) -> TRUE;\n"
01397 + " (R1, R4) -> TRUE;\n"
01398 + " (R1, GT4) -> TRUE;\n"
01399 + " (R2, LT0) -> TRUE;\n"
01400 + " (R2, R0) -> TRUE;\n"
01401 + " (R2, R1) -> TRUE;\n"
01402 + " (R2, R2) -> FALSE;\n"
01403 + " (R2, R3) -> TRUE;\n"
01404 + " (R2, R4) -> TRUE;\n"
01405 + " (R2, GT4) -> TRUE;\n"
01406 + " (R3, LT0) -> TRUE;\n"
01407 + " (R3, R0) -> TRUE;\n"
01408 + " (R3, R1) -> TRUE;\n"
01409 + " (R3, R2) -> TRUE;\n"
01410 + " (R3, R3) -> FALSE;\n"
01411 + " (R3, R4) -> TRUE;\n"
01412 + " (R3, GT4) -> TRUE;\n"
01413 + " (R4, LT0) -> TRUE;\n"
01414 + " (R4, R0) -> TRUE;\n"
01415 + " (R4, R1) -> TRUE;\n"
01416 + " (R4, R2) -> TRUE;\n"
01417 + " (R4, R3) -> TRUE;\n"
01418 + " (R4, R4) -> FALSE;\n"
01419 + " (R4, GT4) -> TRUE;\n"
01420 + " (GT4, LT0) -> TRUE;\n"
01421 + " (GT4, R0) -> TRUE;\n"
01422 + " (GT4, R1) -> TRUE;\n"
01423 + " (GT4, R2) -> TRUE;\n"
01424 + " (GT4, R3) -> TRUE;\n"
01425 + " (GT4, R4) -> TRUE;\n"
01426 + " (GT4, GT4) -> {TRUE, FALSE};\n"
01427 + " end\n"
01428 + " test < lt \n"
01429 + " begin\n"
01430 + " (LT0, LT0) -> {TRUE, FALSE};\n"
01431 + " (LT0, R0) -> TRUE;\n"
01432 + " (LT0, R1) -> TRUE;\n"
01433 + " (LT0, R2) -> TRUE;\n"
01434 + " (LT0, R3) -> TRUE;\n"
01435 + " (LT0, R4) -> TRUE;\n"
01436 + " (LT0, GT4) -> TRUE;\n"
01437 + " (R0, LT0) -> FALSE;\n"
01438 + " (R0, R0) -> FALSE;\n"
01439 + " (R0, R1) -> TRUE;\n"
01440 + " (R0, R2) -> TRUE;\n"
01441 + " (R0, R3) -> TRUE;\n"
01442 + " (R0, R4) -> TRUE;\n"
01443 + " (R0, GT4) -> TRUE;\n"
01444 + " (R1, LT0) -> FALSE;\n"
01445 + " (R1, R0) -> FALSE;\n"
01446 + " (R1, R1) -> FALSE;\n"
01447 + " (R1, R2) -> TRUE;\n"
01448 + " (R1, R3) -> TRUE;\n"
01449 + " (R1, R4) -> TRUE;\n"
01450 + " (R1, GT4) -> TRUE;\n"
01451 + " (R2, LT0) -> FALSE;\n"
01452 + " (R2, R0) -> FALSE;\n"
01453 + " (R2, R1) -> FALSE;\n"
01454 + " (R2, R2) -> FALSE;\n"
01455 + " (R2, R3) -> TRUE;\n"
01456 + " (R2, R4) -> TRUE;\n"
01457 + " (R2, GT4) -> TRUE;\n"
01458 + " (R3, LT0) -> FALSE;\n"
01459 + " (R3, R0) -> FALSE;\n"
01460 + " (R3, R1) -> FALSE;\n"
01461 + " (R3, R2) -> FALSE;\n"
01462 + " (R3, R3) -> FALSE;\n"
01463 + " (R3, R4) -> TRUE;\n"
01464 + " (R3, GT4) -> TRUE;\n"
01465 + " (R4, LT0) -> FALSE;\n"
01466 + " (R4, R0) -> FALSE;\n"
01467 + " (R4, R1) -> FALSE;\n"
01468 + " (R4, R2) -> FALSE;\n"
01469 + " (R4, R3) -> FALSE;\n"
01470 + " (R4, R4) -> FALSE;\n"
01471 + " (R4, GT4) -> TRUE;\n"
01472 + " (GT4, LT0) -> FALSE;\n"
01473 + " (GT4, R0) -> FALSE;\n"
01474 + " (GT4, R1) -> FALSE;\n"
01475 + " (GT4, R2) -> FALSE;\n"
01476 + " (GT4, R3) -> FALSE;\n"
01477 + " (GT4, R4) -> FALSE;\n"
01478 + " (GT4, GT4) -> {TRUE, FALSE};\n"
01479 + " end\n"
01480 + " test <= le \n"
01481 + " begin\n"
01482 + " (LT0, LT0) -> {TRUE, FALSE};\n"
01483 + " (LT0, R0) -> TRUE;\n"
01484 + " (LT0, R1) -> TRUE;\n"
01485 + " (LT0, R2) -> TRUE;\n"
01486 + " (LT0, R3) -> TRUE;\n"
01487 + " (LT0, R4) -> TRUE;\n"
01488 + " (LT0, GT4) -> TRUE;\n"
01489 + " (R0, LT0) -> FALSE;\n"
01490 + " (R0, R0) -> TRUE;\n"
01491 + " (R0, R1) -> TRUE;\n"
01492 + " (R0, R2) -> TRUE;\n"
01493 + " (R0, R3) -> TRUE;\n"
01494 + " (R0, R4) -> TRUE;\n"
01495 + " (R0, GT4) -> TRUE;\n"
01496 + " (R1, LT0) -> FALSE;\n"
01497 + " (R1, R0) -> FALSE;\n"
01498 + " (R1, R1) -> TRUE;\n"
01499 + " (R1, R2) -> TRUE;\n"
01500 + " (R1, R3) -> TRUE;\n"
01501 + " (R1, R4) -> TRUE;\n"
01502 + " (R1, GT4) -> TRUE;\n"
01503 + " (R2, LT0) -> FALSE;\n"
01504 + " (R2, R0) -> FALSE;\n"
01505 + " (R2, R1) -> FALSE;\n"
01506 + " (R2, R2) -> TRUE;\n"
01507 + " (R2, R3) -> TRUE;\n"
01508 + " (R2, R4) -> TRUE;\n"
01509 + " (R2, GT4) -> TRUE;\n"
01510 + " (R3, LT0) -> FALSE;\n"
01511 + " (R3, R0) -> FALSE;\n"
01512 + " (R3, R1) -> FALSE;\n"
01513 + " (R3, R2) -> FALSE;\n"
01514 + " (R3, R3) -> TRUE;\n"
01515 + " (R3, R4) -> TRUE;\n"
01516 + " (R3, GT4) -> TRUE;\n"
01517 + " (R4, LT0) -> FALSE;\n"
01518 + " (R4, R0) -> FALSE;\n"
01519 + " (R4, R1) -> FALSE;\n"
01520 + " (R4, R2) -> FALSE;\n"
01521 + " (R4, R3) -> FALSE;\n"
01522 + " (R4, R4) -> TRUE;\n"
01523 + " (R4, GT4) -> TRUE;\n"
01524 + " (GT4, LT0) -> FALSE;\n"
01525 + " (GT4, R0) -> FALSE;\n"
01526 + " (GT4, R1) -> FALSE;\n"
01527 + " (GT4, R2) -> FALSE;\n"
01528 + " (GT4, R3) -> FALSE;\n"
01529 + " (GT4, R4) -> FALSE;\n"
01530 + " (GT4, GT4) -> {TRUE, FALSE};\n"
01531 + " end\n"
01532 + " test > gt \n"
01533 + " begin\n"
01534 + " (LT0, LT0) -> {TRUE, FALSE};\n"
01535 + " (LT0, R0) -> FALSE;\n"
01536 + " (LT0, R1) -> FALSE;\n"
01537 + " (LT0, R2) -> FALSE;\n"
01538 + " (LT0, R3) -> FALSE;\n"
01539 + " (LT0, R4) -> FALSE;\n"
01540 + " (LT0, GT4) -> FALSE;\n"
01541 + " (R0, LT0) -> TRUE;\n"
01542 + " (R0, R0) -> FALSE;\n"
01543 + " (R0, R1) -> FALSE;\n"
01544 + " (R0, R2) -> FALSE;\n"
01545 + " (R0, R3) -> FALSE;\n"
01546 + " (R0, R4) -> FALSE;\n"
01547 + " (R0, GT4) -> FALSE;\n"
01548 + " (R1, LT0) -> TRUE;\n"
01549 + " (R1, R0) -> TRUE;\n"
01550 + " (R1, R1) -> FALSE;\n"
01551 + " (R1, R2) -> FALSE;\n"
01552 + " (R1, R3) -> FALSE;\n"
01553 + " (R1, R4) -> FALSE;\n"
01554 + " (R1, GT4) -> FALSE;\n"
01555 + " (R2, LT0) -> TRUE;\n"
01556 + " (R2, R0) -> TRUE;\n"
01557 + " (R2, R1) -> TRUE;\n"
01558 + " (R2, R2) -> FALSE;\n"
01559 + " (R2, R3) -> FALSE;\n"
01560 + " (R2, R4) -> FALSE;\n"
01561 + " (R2, GT4) -> FALSE;\n"
01562 + " (R3, LT0) -> TRUE;\n"
01563 + " (R3, R0) -> TRUE;\n"
01564 + " (R3, R1) -> TRUE;\n"
01565 + " (R3, R2) -> TRUE;\n"
01566 + " (R3, R3) -> FALSE;\n"
01567 + " (R3, R4) -> FALSE;\n"
01568 + " (R3, GT4) -> FALSE;\n"
01569 + " (R4, LT0) -> TRUE;\n"
01570 + " (R4, R0) -> TRUE;\n"
01571 + " (R4, R1) -> TRUE;\n"
01572 + " (R4, R2) -> TRUE;\n"
01573 + " (R4, R3) -> TRUE;\n"
01574 + " (R4, R4) -> FALSE;\n"
01575 + " (R4, GT4) -> FALSE;\n"
01576 + " (GT4, LT0) -> TRUE;\n"
01577 + " (GT4, R0) -> TRUE;\n"
01578 + " (GT4, R1) -> TRUE;\n"
01579 + " (GT4, R2) -> TRUE;\n"
01580 + " (GT4, R3) -> TRUE;\n"
01581 + " (GT4, R4) -> TRUE;\n"
01582 + " (GT4, GT4) -> {TRUE, FALSE};\n"
01583 + " end\n"
01584 + " test >= ge \n"
01585 + " begin\n"
01586 + " (LT0, LT0) -> {TRUE, FALSE};\n"
01587 + " (LT0, R0) -> FALSE;\n"
01588 + " (LT0, R1) -> FALSE;\n"
01589 + " (LT0, R2) -> FALSE;\n"
01590 + " (LT0, R3) -> FALSE;\n"
01591 + " (LT0, R4) -> FALSE;\n"
01592 + " (LT0, GT4) -> FALSE;\n"
01593 + " (R0, LT0) -> TRUE;\n"
01594 + " (R0, R0) -> TRUE;\n"
01595 + " (R0, R1) -> FALSE;\n"
01596 + " (R0, R2) -> FALSE;\n"
01597 + " (R0, R3) -> FALSE;\n"
01598 + " (R0, R4) -> FALSE;\n"
01599 + " (R0, GT4) -> FALSE;\n"
01600 + " (R1, LT0) -> TRUE;\n"
01601 + " (R1, R0) -> TRUE;\n"
01602 + " (R1, R1) -> TRUE;\n"
01603 + " (R1, R2) -> FALSE;\n"
01604 + " (R1, R3) -> FALSE;\n"
01605 + " (R1, R4) -> FALSE;\n"
01606 + " (R1, GT4) -> FALSE;\n"
01607 + " (R2, LT0) -> TRUE;\n"
01608 + " (R2, R0) -> TRUE;\n"
01609 + " (R2, R1) -> TRUE;\n"
01610 + " (R2, R2) -> TRUE;\n"
01611 + " (R2, R3) -> FALSE;\n"
01612 + " (R2, R4) -> FALSE;\n"
01613 + " (R2, GT4) -> FALSE;\n"
01614 + " (R3, LT0) -> TRUE;\n"
01615 + " (R3, R0) -> TRUE;\n"
01616 + " (R3, R1) -> TRUE;\n"
01617 + " (R3, R2) -> TRUE;\n"
01618 + " (R3, R3) -> TRUE;\n"
01619 + " (R3, R4) -> FALSE;\n"
01620 + " (R3, GT4) -> FALSE;\n"
01621 + " (R4, LT0) -> TRUE;\n"
01622 + " (R4, R0) -> TRUE;\n"
01623 + " (R4, R1) -> TRUE;\n"
01624 + " (R4, R2) -> TRUE;\n"
01625 + " (R4, R3) -> TRUE;\n"
01626 + " (R4, R4) -> TRUE;\n"
01627 + " (R4, GT4) -> FALSE;\n"
01628 + " (GT4, LT0) -> TRUE;\n"
01629 + " (GT4, R0) -> TRUE;\n"
01630 + " (GT4, R1) -> TRUE;\n"
01631 + " (GT4, R2) -> TRUE;\n"
01632 + " (GT4, R3) -> TRUE;\n"
01633 + " (GT4, R4) -> TRUE;\n"
01634 + " (GT4, GT4) -> {TRUE, FALSE};\n"
01635 + " end\n"
01636 + " end\n"
01637 ;
01638 }
01639 public static String getName() {
01640 return "Range04";
01641 }
01642 public static int getNumOfTokens() {
01643 return 7;
01644 }
01645 public static String getToken(int value) {
01646 switch(value) {
01647 case R0: return "Range04.R0";
01648 case LT0: return "Range04.LT0";
01649 case R1: return "Range04.R1";
01650 case R2: return "Range04.R2";
01651 case R3: return "Range04.R3";
01652 case R4: return "Range04.R4";
01653 case GT4: return "Range04.GT4";
01654 }
01655 return "Range04.???";
01656 }
01657 public static boolean gt(int left$, int right$) {
01658 if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
01659 if (left$ == LT0 && right$ == R0) return false;
01660 if (left$ == LT0 && right$ == R1) return false;
01661 if (left$ == LT0 && right$ == R2) return false;
01662 if (left$ == LT0 && right$ == R3) return false;
01663 if (left$ == LT0 && right$ == R4) return false;
01664 if (left$ == LT0 && right$ == GT4) return false;
01665 if (left$ == R0 && right$ == LT0) return true;
01666 if (left$ == R0 && right$ == R0) return false;
01667 if (left$ == R0 && right$ == R1) return false;
01668 if (left$ == R0 && right$ == R2) return false;
01669 if (left$ == R0 && right$ == R3) return false;
01670 if (left$ == R0 && right$ == R4) return false;
01671 if (left$ == R0 && right$ == GT4) return false;
01672 if (left$ == R1 && right$ == LT0) return true;
01673 if (left$ == R1 && right$ == R0) return true;
01674 if (left$ == R1 && right$ == R1) return false;
01675 if (left$ == R1 && right$ == R2) return false;
01676 if (left$ == R1 && right$ == R3) return false;
01677 if (left$ == R1 && right$ == R4) return false;
01678 if (left$ == R1 && right$ == GT4) return false;
01679 if (left$ == R2 && right$ == LT0) return true;
01680 if (left$ == R2 && right$ == R0) return true;
01681 if (left$ == R2 && right$ == R1) return true;
01682 if (left$ == R2 && right$ == R2) return false;
01683 if (left$ == R2 && right$ == R3) return false;
01684 if (left$ == R2 && right$ == R4) return false;
01685 if (left$ == R2 && right$ == GT4) return false;
01686 if (left$ == R3 && right$ == LT0) return true;
01687 if (left$ == R3 && right$ == R0) return true;
01688 if (left$ == R3 && right$ == R1) return true;
01689 if (left$ == R3 && right$ == R2) return true;
01690 if (left$ == R3 && right$ == R3) return false;
01691 if (left$ == R3 && right$ == R4) return false;
01692 if (left$ == R3 && right$ == GT4) return false;
01693 if (left$ == R4 && right$ == LT0) return true;
01694 if (left$ == R4 && right$ == R0) return true;
01695 if (left$ == R4 && right$ == R1) return true;
01696 if (left$ == R4 && right$ == R2) return true;
01697 if (left$ == R4 && right$ == R3) return true;
01698 if (left$ == R4 && right$ == R4) return false;
01699 if (left$ == R4 && right$ == GT4) return false;
01700 if (left$ == GT4 && right$ == LT0) return true;
01701 if (left$ == GT4 && right$ == R0) return true;
01702 if (left$ == GT4 && right$ == R1) return true;
01703 if (left$ == GT4 && right$ == R2) return true;
01704 if (left$ == GT4 && right$ == R3) return true;
01705 if (left$ == GT4 && right$ == R4) return true;
01706 if (left$ == GT4 && right$ == GT4) return Abstraction.choose();
01707 throw new RuntimeException("Range04.gt(" + left$ + ", " + right$ + ") is undefined");
01708 }
01709 private static byte gtNoChoose(int left, int right) {
01710 byte result = -1;
01711 switch (left) {
01712 case 0:
01713 switch (right) {
01714 case 0:
01715 result = 0;
01716 break;
01717 case 1:
01718 result = 1;
01719 break;
01720 case 2:
01721 result = 0;
01722 break;
01723 case 3:
01724 result = 0;
01725 break;
01726 case 4:
01727 result = 0;
01728 break;
01729 case 5:
01730 result = 0;
01731 break;
01732 case 6:
01733 result = 0;
01734 break;
01735 }
01736 break;
01737 case 1:
01738 switch (right) {
01739 case 0:
01740 result = 0;
01741 break;
01742 case 1:
01743 result = 2;
01744 break;
01745 case 2:
01746 result = 0;
01747 break;
01748 case 3:
01749 result = 0;
01750 break;
01751 case 4:
01752 result = 0;
01753 break;
01754 case 5:
01755 result = 0;
01756 break;
01757 case 6:
01758 result = 0;
01759 break;
01760 }
01761 break;
01762 case 2:
01763 switch (right) {
01764 case 0:
01765 result = 1;
01766 break;
01767 case 1:
01768 result = 1;
01769 break;
01770 case 2:
01771 result = 0;
01772 break;
01773 case 3:
01774 result = 0;
01775 break;
01776 case 4:
01777 result = 0;
01778 break;
01779 case 5:
01780 result = 0;
01781 break;
01782 case 6:
01783 result = 0;
01784 break;
01785 }
01786 break;
01787 case 3:
01788 switch (right) {
01789 case 0:
01790 result = 1;
01791 break;
01792 case 1:
01793 result = 1;
01794 break;
01795 case 2:
01796 result = 1;
01797 break;
01798 case 3:
01799 result = 0;
01800 break;
01801 case 4:
01802 result = 0;
01803 break;
01804 case 5:
01805 result = 0;
01806 break;
01807 case 6:
01808 result = 0;
01809 break;
01810 }
01811 break;
01812 case 4:
01813 switch (right) {
01814 case 0:
01815 result = 1;
01816 break;
01817 case 1:
01818 result = 1;
01819 break;
01820 case 2:
01821 result = 1;
01822 break;
01823 case 3:
01824 result = 1;
01825 break;
01826 case 4:
01827 result = 0;
01828 break;
01829 case 5:
01830 result = 0;
01831 break;
01832 case 6:
01833 result = 0;
01834 break;
01835 }
01836 break;
01837 case 5:
01838 switch (right) {
01839 case 0:
01840 result = 1;
01841 break;
01842 case 1:
01843 result = 1;
01844 break;
01845 case 2:
01846 result = 1;
01847 break;
01848 case 3:
01849 result = 1;
01850 break;
01851 case 4:
01852 result = 1;
01853 break;
01854 case 5:
01855 result = 0;
01856 break;
01857 case 6:
01858 result = 0;
01859 break;
01860 }
01861 break;
01862 case 6:
01863 switch (right) {
01864 case 0:
01865 result = 1;
01866 break;
01867 case 1:
01868 result = 1;
01869 break;
01870 case 2:
01871 result = 1;
01872 break;
01873 case 3:
01874 result = 1;
01875 break;
01876 case 4:
01877 result = 1;
01878 break;
01879 case 5:
01880 result = 1;
01881 break;
01882 case 6:
01883 result = 2;
01884 break;
01885 }
01886 break;
01887 }
01888 if (result == -1) throw new RuntimeException("Range04.gtNoChoose(" + left + ", " + right + ") is undefined");
01889 return result;
01890 }
01891 public static byte gtSet(int leftTokens, int rightTokens) {
01892 byte result = -1;
01893 for (int left = 0; (1 << left) <= leftTokens; left++) {
01894 if ((leftTokens & (1 << left)) == 0) continue;
01895 for (int right = 0; (1 << right) <= rightTokens; right++) {
01896 if ((rightTokens & (1 << right)) != 0) {
01897 if (result == -1) result = gtNoChoose(left, right);
01898 else result = Abstraction.meetTest(result, gtNoChoose(left, right));
01899 }
01900 }
01901 }
01902 return result;
01903 }
01904 public static boolean isOne2One(int value) {
01905 switch(value) {
01906 case R4: return true;
01907 case R3: return true;
01908 case R2: return true;
01909 case R1: return true;
01910 case R0: return true;
01911 }
01912 return false;
01913 }
01914 public static boolean le(int left$, int right$) {
01915 if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
01916 if (left$ == LT0 && right$ == R0) return true;
01917 if (left$ == LT0 && right$ == R1) return true;
01918 if (left$ == LT0 && right$ == R2) return true;
01919 if (left$ == LT0 && right$ == R3) return true;
01920 if (left$ == LT0 && right$ == R4) return true;
01921 if (left$ == LT0 && right$ == GT4) return true;
01922 if (left$ == R0 && right$ == LT0) return false;
01923 if (left$ == R0 && right$ == R0) return true;
01924 if (left$ == R0 && right$ == R1) return true;
01925 if (left$ == R0 && right$ == R2) return true;
01926 if (left$ == R0 && right$ == R3) return true;
01927 if (left$ == R0 && right$ == R4) return true;
01928 if (left$ == R0 && right$ == GT4) return true;
01929 if (left$ == R1 && right$ == LT0) return false;
01930 if (left$ == R1 && right$ == R0) return false;
01931 if (left$ == R1 && right$ == R1) return true;
01932 if (left$ == R1 && right$ == R2) return true;
01933 if (left$ == R1 && right$ == R3) return true;
01934 if (left$ == R1 && right$ == R4) return true;
01935 if (left$ == R1 && right$ == GT4) return true;
01936 if (left$ == R2 && right$ == LT0) return false;
01937 if (left$ == R2 && right$ == R0) return false;
01938 if (left$ == R2 && right$ == R1) return false;
01939 if (left$ == R2 && right$ == R2) return true;
01940 if (left$ == R2 && right$ == R3) return true;
01941 if (left$ == R2 && right$ == R4) return true;
01942 if (left$ == R2 && right$ == GT4) return true;
01943 if (left$ == R3 && right$ == LT0) return false;
01944 if (left$ == R3 && right$ == R0) return false;
01945 if (left$ == R3 && right$ == R1) return false;
01946 if (left$ == R3 && right$ == R2) return false;
01947 if (left$ == R3 && right$ == R3) return true;
01948 if (left$ == R3 && right$ == R4) return true;
01949 if (left$ == R3 && right$ == GT4) return true;
01950 if (left$ == R4 && right$ == LT0) return false;
01951 if (left$ == R4 && right$ == R0) return false;
01952 if (left$ == R4 && right$ == R1) return false;
01953 if (left$ == R4 && right$ == R2) return false;
01954 if (left$ == R4 && right$ == R3) return false;
01955 if (left$ == R4 && right$ == R4) return true;
01956 if (left$ == R4 && right$ == GT4) return true;
01957 if (left$ == GT4 && right$ == LT0) return false;
01958 if (left$ == GT4 && right$ == R0) return false;
01959 if (left$ == GT4 && right$ == R1) return false;
01960 if (left$ == GT4 && right$ == R2) return false;
01961 if (left$ == GT4 && right$ == R3) return false;
01962 if (left$ == GT4 && right$ == R4) return false;
01963 if (left$ == GT4 && right$ == GT4) return Abstraction.choose();
01964 throw new RuntimeException("Range04.le(" + left$ + ", " + right$ + ") is undefined");
01965 }
01966 private static byte leNoChoose(int left, int right) {
01967 byte result = -1;
01968 switch (left) {
01969 case 0:
01970 switch (right) {
01971 case 0:
01972 result = 1;
01973 break;
01974 case 1:
01975 result = 0;
01976 break;
01977 case 2:
01978 result = 1;
01979 break;
01980 case 3:
01981 result = 1;
01982 break;
01983 case 4:
01984 result = 1;
01985 break;
01986 case 5:
01987 result = 1;
01988 break;
01989 case 6:
01990 result = 1;
01991 break;
01992 }
01993 break;
01994 case 1:
01995 switch (right) {
01996 case 0:
01997 result = 1;
01998 break;
01999 case 1:
02000 result = 2;
02001 break;
02002 case 2:
02003 result = 1;
02004 break;
02005 case 3:
02006 result = 1;
02007 break;
02008 case 4:
02009 result = 1;
02010 break;
02011 case 5:
02012 result = 1;
02013 break;
02014 case 6:
02015 result = 1;
02016 break;
02017 }
02018 break;
02019 case 2:
02020 switch (right) {
02021 case 0:
02022 result = 0;
02023 break;
02024 case 1:
02025 result = 0;
02026 break;
02027 case 2:
02028 result = 1;
02029 break;
02030 case 3:
02031 result = 1;
02032 break;
02033 case 4:
02034 result = 1;
02035 break;
02036 case 5:
02037 result = 1;
02038 break;
02039 case 6:
02040 result = 1;
02041 break;
02042 }
02043 break;
02044 case 3:
02045 switch (right) {
02046 case 0:
02047 result = 0;
02048 break;
02049 case 1:
02050 result = 0;
02051 break;
02052 case 2:
02053 result = 0;
02054 break;
02055 case 3:
02056 result = 1;
02057 break;
02058 case 4:
02059 result = 1;
02060 break;
02061 case 5:
02062 result = 1;
02063 break;
02064 case 6:
02065 result = 1;
02066 break;
02067 }
02068 break;
02069 case 4:
02070 switch (right) {
02071 case 0:
02072 result = 0;
02073 break;
02074 case 1:
02075 result = 0;
02076 break;
02077 case 2:
02078 result = 0;
02079 break;
02080 case 3:
02081 result = 0;
02082 break;
02083 case 4:
02084 result = 1;
02085 break;
02086 case 5:
02087 result = 1;
02088 break;
02089 case 6:
02090 result = 1;
02091 break;
02092 }
02093 break;
02094 case 5:
02095 switch (right) {
02096 case 0:
02097 result = 0;
02098 break;
02099 case 1:
02100 result = 0;
02101 break;
02102 case 2:
02103 result = 0;
02104 break;
02105 case 3:
02106 result = 0;
02107 break;
02108 case 4:
02109 result = 0;
02110 break;
02111 case 5:
02112 result = 1;
02113 break;
02114 case 6:
02115 result = 1;
02116 break;
02117 }
02118 break;
02119 case 6:
02120 switch (right) {
02121 case 0:
02122 result = 0;
02123 break;
02124 case 1:
02125 result = 0;
02126 break;
02127 case 2:
02128 result = 0;
02129 break;
02130 case 3:
02131 result = 0;
02132 break;
02133 case 4:
02134 result = 0;
02135 break;
02136 case 5:
02137 result = 0;
02138 break;
02139 case 6:
02140 result = 2;
02141 break;
02142 }
02143 break;
02144 }
02145 if (result == -1) throw new RuntimeException("Range04.leNoChoose(" + left + ", " + right + ") is undefined");
02146 return result;
02147 }
02148 public static byte leSet(int leftTokens, int rightTokens) {
02149 byte result = -1;
02150 for (int left = 0; (1 << left) <= leftTokens; left++) {
02151 if ((leftTokens & (1 << left)) == 0) continue;
02152 for (int right = 0; (1 << right) <= rightTokens; right++) {
02153 if ((rightTokens & (1 << right)) != 0) {
02154 if (result == -1) result = leNoChoose(left, right);
02155 else result = Abstraction.meetTest(result, leNoChoose(left, right));
02156 }
02157 }
02158 }
02159 return result;
02160 }
02161 public static boolean lt(int left$, int right$) {
02162 if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
02163 if (left$ == LT0 && right$ == R0) return true;
02164 if (left$ == LT0 && right$ == R1) return true;
02165 if (left$ == LT0 && right$ == R2) return true;
02166 if (left$ == LT0 && right$ == R3) return true;
02167 if (left$ == LT0 && right$ == R4) return true;
02168 if (left$ == LT0 && right$ == GT4) return true;
02169 if (left$ == R0 && right$ == LT0) return false;
02170 if (left$ == R0 && right$ == R0) return false;
02171 if (left$ == R0 && right$ == R1) return true;
02172 if (left$ == R0 && right$ == R2) return true;
02173 if (left$ == R0 && right$ == R3) return true;
02174 if (left$ == R0 && right$ == R4) return true;
02175 if (left$ == R0 && right$ == GT4) return true;
02176 if (left$ == R1 && right$ == LT0) return false;
02177 if (left$ == R1 && right$ == R0) return false;
02178 if (left$ == R1 && right$ == R1) return false;
02179 if (left$ == R1 && right$ == R2) return true;
02180 if (left$ == R1 && right$ == R3) return true;
02181 if (left$ == R1 && right$ == R4) return true;
02182 if (left$ == R1 && right$ == GT4) return true;
02183 if (left$ == R2 && right$ == LT0) return false;
02184 if (left$ == R2 && right$ == R0) return false;
02185 if (left$ == R2 && right$ == R1) return false;
02186 if (left$ == R2 && right$ == R2) return false;
02187 if (left$ == R2 && right$ == R3) return true;
02188 if (left$ == R2 && right$ == R4) return true;
02189 if (left$ == R2 && right$ == GT4) return true;
02190 if (left$ == R3 && right$ == LT0) return false;
02191 if (left$ == R3 && right$ == R0) return false;
02192 if (left$ == R3 && right$ == R1) return false;
02193 if (left$ == R3 && right$ == R2) return false;
02194 if (left$ == R3 && right$ == R3) return false;
02195 if (left$ == R3 && right$ == R4) return true;
02196 if (left$ == R3 && right$ == GT4) return true;
02197 if (left$ == R4 && right$ == LT0) return false;
02198 if (left$ == R4 && right$ == R0) return false;
02199 if (left$ == R4 && right$ == R1) return false;
02200 if (left$ == R4 && right$ == R2) return false;
02201 if (left$ == R4 && right$ == R3) return false;
02202 if (left$ == R4 && right$ == R4) return false;
02203 if (left$ == R4 && right$ == GT4) return true;
02204 if (left$ == GT4 && right$ == LT0) return false;
02205 if (left$ == GT4 && right$ == R0) return false;
02206 if (left$ == GT4 && right$ == R1) return false;
02207 if (left$ == GT4 && right$ == R2) return false;
02208 if (left$ == GT4 && right$ == R3) return false;
02209 if (left$ == GT4 && right$ == R4) return false;
02210 if (left$ == GT4 && right$ == GT4) return Abstraction.choose();
02211 throw new RuntimeException("Range04.lt(" + left$ + ", " + right$ + ") is undefined");
02212 }
02213 private static byte ltNoChoose(int left, int right) {
02214 byte result = -1;
02215 switch (left) {
02216 case 0:
02217 switch (right) {
02218 case 0:
02219 result = 0;
02220 break;
02221 case 1:
02222 result = 0;
02223 break;
02224 case 2:
02225 result = 1;
02226 break;
02227 case 3:
02228 result = 1;
02229 break;
02230 case 4:
02231 result = 1;
02232 break;
02233 case 5:
02234 result = 1;
02235 break;
02236 case 6:
02237 result = 1;
02238 break;
02239 }
02240 break;
02241 case 1:
02242 switch (right) {
02243 case 0:
02244 result = 1;
02245 break;
02246 case 1:
02247 result = 2;
02248 break;
02249 case 2:
02250 result = 1;
02251 break;
02252 case 3:
02253 result = 1;
02254 break;
02255 case 4:
02256 result = 1;
02257 break;
02258 case 5:
02259 result = 1;
02260 break;
02261 case 6:
02262 result = 1;
02263 break;
02264 }
02265 break;
02266 case 2:
02267 switch (right) {
02268 case 0:
02269 result = 0;
02270 break;
02271 case 1:
02272 result = 0;
02273 break;
02274 case 2:
02275 result = 0;
02276 break;
02277 case 3:
02278 result = 1;
02279 break;
02280 case 4:
02281 result = 1;
02282 break;
02283 case 5:
02284 result = 1;
02285 break;
02286 case 6:
02287 result = 1;
02288 break;
02289 }
02290 break;
02291 case 3:
02292 switch (right) {
02293 case 0:
02294 result = 0;
02295 break;
02296 case 1:
02297 result = 0;
02298 break;
02299 case 2:
02300 result = 0;
02301 break;
02302 case 3:
02303 result = 0;
02304 break;
02305 case 4:
02306 result = 1;
02307 break;
02308 case 5:
02309 result = 1;
02310 break;
02311 case 6:
02312 result = 1;
02313 break;
02314 }
02315 break;
02316 case 4:
02317 switch (right) {
02318 case 0:
02319 result = 0;
02320 break;
02321 case 1:
02322 result = 0;
02323 break;
02324 case 2:
02325 result = 0;
02326 break;
02327 case 3:
02328 result = 0;
02329 break;
02330 case 4:
02331 result = 0;
02332 break;
02333 case 5:
02334 result = 1;
02335 break;
02336 case 6:
02337 result = 1;
02338 break;
02339 }
02340 break;
02341 case 5:
02342 switch (right) {
02343 case 0:
02344 result = 0;
02345 break;
02346 case 1:
02347 result = 0;
02348 break;
02349 case 2:
02350 result = 0;
02351 break;
02352 case 3:
02353 result = 0;
02354 break;
02355 case 4:
02356 result = 0;
02357 break;
02358 case 5:
02359 result = 0;
02360 break;
02361 case 6:
02362 result = 1;
02363 break;
02364 }
02365 break;
02366 case 6:
02367 switch (right) {
02368 case 0:
02369 result = 0;
02370 break;
02371 case 1:
02372 result = 0;
02373 break;
02374 case 2:
02375 result = 0;
02376 break;
02377 case 3:
02378 result = 0;
02379 break;
02380 case 4:
02381 result = 0;
02382 break;
02383 case 5:
02384 result = 0;
02385 break;
02386 case 6:
02387 result = 2;
02388 break;
02389 }
02390 break;
02391 }
02392 if (result == -1) throw new RuntimeException("Range04.ltNoChoose(" + left + ", " + right + ") is undefined");
02393 return result;
02394 }
02395 public static byte ltSet(int leftTokens, int rightTokens) {
02396 byte result = -1;
02397 for (int left = 0; (1 << left) <= leftTokens; left++) {
02398 if ((leftTokens & (1 << left)) == 0) continue;
02399 for (int right = 0; (1 << right) <= rightTokens; right++) {
02400 if ((rightTokens & (1 << right)) != 0) {
02401 if (result == -1) result = ltNoChoose(left, right);
02402 else result = Abstraction.meetTest(result, ltNoChoose(left, right));
02403 }
02404 }
02405 }
02406 return result;
02407 }
02408 public static int mul(int left$, int right$) {
02409 if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1));
02410 if (left$ == LT0 && right$ == R0) return R0;
02411 if (left$ == LT0 && right$ == R1) return LT0;
02412 if (left$ == LT0 && right$ == R2) return LT0;
02413 if (left$ == LT0 && right$ == R3) return LT0;
02414 if (left$ == LT0 && right$ == R4) return LT0;
02415 if (left$ == LT0 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << LT0));
02416 if (left$ == R0 && right$ == LT0) return R0;
02417 if (left$ == R0 && right$ == R0) return R0;
02418 if (left$ == R0 && right$ == R1) return R0;
02419 if (left$ == R0 && right$ == R2) return R0;
02420 if (left$ == R0 && right$ == R3) return R0;
02421 if (left$ == R0 && right$ == R4) return R0;
02422 if (left$ == R0 && right$ == GT4) return R0;
02423 if (left$ == R1 && right$ == LT0) return LT0;
02424 if (left$ == R1 && right$ == R0) return R0;
02425 if (left$ == R1 && right$ == R1) return R1;
02426 if (left$ == R1 && right$ == R2) return R2;
02427 if (left$ == R1 && right$ == R3) return R3;
02428 if (left$ == R1 && right$ == R4) return R4;
02429 if (left$ == R1 && right$ == GT4) return GT4;
02430 if (left$ == R2 && right$ == LT0) return LT0;
02431 if (left$ == R2 && right$ == R0) return R0;
02432 if (left$ == R2 && right$ == R1) return R2;
02433 if (left$ == R2 && right$ == R2) return R4;
02434 if (left$ == R2 && right$ == R3) return GT4;
02435 if (left$ == R2 && right$ == R4) return GT4;
02436 if (left$ == R2 && right$ == GT4) return GT4;
02437 if (left$ == R3 && right$ == LT0) return LT0;
02438 if (left$ == R3 && right$ == R0) return R0;
02439 if (left$ == R3 && right$ == R1) return R3;
02440 if (left$ == R3 && right$ == R2) return GT4;
02441 if (left$ == R3 && right$ == R3) return GT4;
02442 if (left$ == R3 && right$ == R4) return GT4;
02443 if (left$ == R3 && right$ == GT4) return GT4;
02444 if (left$ == R4 && right$ == LT0) return LT0;
02445 if (left$ == R4 && right$ == R0) return R0;
02446 if (left$ == R4 && right$ == R1) return R4;
02447 if (left$ == R4 && right$ == R2) return GT4;
02448 if (left$ == R4 && right$ == R3) return GT4;
02449 if (left$ == R4 && right$ == R4) return GT4;
02450 if (left$ == R4 && right$ == GT4) return GT4;
02451 if (left$ == GT4 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << LT0));
02452 if (left$ == GT4 && right$ == R0) return R0;
02453 if (left$ == GT4 && right$ == R1) return GT4;
02454 if (left$ == GT4 && right$ == R2) return GT4;
02455 if (left$ == GT4 && right$ == R3) return GT4;
02456 if (left$ == GT4 && right$ == R4) return GT4;
02457 if (left$ == GT4 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1));
02458 throw new RuntimeException("Range04.mul(" + left$ + ", " + right$ + ") is undefined");
02459 }
02460 private static int mulNoChoose(int left, int right) {
02461 int result = 0;
02462 switch (left) {
02463 case 0:
02464 switch (right) {
02465 case 0:
02466 result = 1;
02467 break;
02468 case 1:
02469 result = 1;
02470 break;
02471 case 2:
02472 result = 1;
02473 break;
02474 case 3:
02475 result = 1;
02476 break;
02477 case 4:
02478 result = 1;
02479 break;
02480 case 5:
02481 result = 1;
02482 break;
02483 case 6:
02484 result = 1;
02485 break;
02486 }
02487 break;
02488 case 1:
02489 switch (right) {
02490 case 0:
02491 result = 1;
02492 break;
02493 case 1:
02494 result = 124;
02495 break;
02496 case 2:
02497 result = 2;
02498 break;
02499 case 3:
02500 result = 2;
02501 break;
02502 case 4:
02503 result = 2;
02504 break;
02505 case 5:
02506 result = 2;
02507 break;
02508 case 6:
02509 result = 126;
02510 break;
02511 }
02512 break;
02513 case 2:
02514 switch (right) {
02515 case 0:
02516 result = 1;
02517 break;
02518 case 1:
02519 result = 2;
02520 break;
02521 case 2:
02522 result = 4;
02523 break;
02524 case 3:
02525 result = 8;
02526 break;
02527 case 4:
02528 result = 16;
02529 break;
02530 case 5:
02531 result = 32;
02532 break;
02533 case 6:
02534 result = 64;
02535 break;
02536 }
02537 break;
02538 case 3:
02539 switch (right) {
02540 case 0:
02541 result = 1;
02542 break;
02543 case 1:
02544 result = 2;
02545 break;
02546 case 2:
02547 result = 8;
02548 break;
02549 case 3:
02550 result = 32;
02551 break;
02552 case 4:
02553 result = 64;
02554 break;
02555 case 5:
02556 result = 64;
02557 break;
02558 case 6:
02559 result = 64;
02560 break;
02561 }
02562 break;
02563 case 4:
02564 switch (right) {
02565 case 0:
02566 result = 1;
02567 break;
02568 case 1:
02569 result = 2;
02570 break;
02571 case 2:
02572 result = 16;
02573 break;
02574 case 3:
02575 result = 64;
02576 break;
02577 case 4:
02578 result = 64;
02579 break;
02580 case 5:
02581 result = 64;
02582 break;
02583 case 6:
02584 result = 64;
02585 break;
02586 }
02587 break;
02588 case 5:
02589 switch (right) {
02590 case 0:
02591 result = 1;
02592 break;
02593 case 1:
02594 result = 2;
02595 break;
02596 case 2:
02597 result = 32;
02598 break;
02599 case 3:
02600 result = 64;
02601 break;
02602 case 4:
02603 result = 64;
02604 break;
02605 case 5:
02606 result = 64;
02607 break;
02608 case 6:
02609 result = 64;
02610 break;
02611 }
02612 break;
02613 case 6:
02614 switch (right) {
02615 case 0:
02616 result = 1;
02617 break;
02618 case 1:
02619 result = 126;
02620 break;
02621 case 2:
02622 result = 64;
02623 break;
02624 case 3:
02625 result = 64;
02626 break;
02627 case 4:
02628 result = 64;
02629 break;
02630 case 5:
02631 result = 64;
02632 break;
02633 case 6:
02634 result = 124;
02635 break;
02636 }
02637 break;
02638 }
02639 if (result == 0) throw new RuntimeException("Range04.mulNoChoose(" + left + ", " + right + ") is undefined");
02640 return result;
02641 }
02642 public static int mulSet(int leftTokens, int rightTokens) {
02643 int result = -1;
02644 for (int left = 0; (1 << left) <= leftTokens; left++) {
02645 if ((leftTokens & (1 << left)) == 0) continue;
02646 for (int right = 0; (1 << right) <= rightTokens; right++) {
02647 if ((rightTokens & (1 << right)) != 0) {
02648 if (result == -1) result = mulNoChoose(left, right);
02649 else result = Abstraction.meetArith(result, mulNoChoose(left, right));
02650 }
02651 }
02652 }
02653 return result;
02654 }
02655 public static boolean ne(int left$, int right$) {
02656 if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
02657 if (left$ == LT0 && right$ == R0) return true;
02658 if (left$ == LT0 && right$ == R1) return true;
02659 if (left$ == LT0 && right$ == R2) return true;
02660 if (left$ == LT0 && right$ == R3) return true;
02661 if (left$ == LT0 && right$ == R4) return true;
02662 if (left$ == LT0 && right$ == GT4) return true;
02663 if (left$ == R0 && right$ == LT0) return true;
02664 if (left$ == R0 && right$ == R0) return false;
02665 if (left$ == R0 && right$ == R1) return true;
02666 if (left$ == R0 && right$ == R2) return true;
02667 if (left$ == R0 && right$ == R3) return true;
02668 if (left$ == R0 && right$ == R4) return true;
02669 if (left$ == R0 && right$ == GT4) return true;
02670 if (left$ == R1 && right$ == LT0) return true;
02671 if (left$ == R1 && right$ == R0) return true;
02672 if (left$ == R1 && right$ == R1) return false;
02673 if (left$ == R1 && right$ == R2) return true;
02674 if (left$ == R1 && right$ == R3) return true;
02675 if (left$ == R1 && right$ == R4) return true;
02676 if (left$ == R1 && right$ == GT4) return true;
02677 if (left$ == R2 && right$ == LT0) return true;
02678 if (left$ == R2 && right$ == R0) return true;
02679 if (left$ == R2 && right$ == R1) return true;
02680 if (left$ == R2 && right$ == R2) return false;
02681 if (left$ == R2 && right$ == R3) return true;
02682 if (left$ == R2 && right$ == R4) return true;
02683 if (left$ == R2 && right$ == GT4) return true;
02684 if (left$ == R3 && right$ == LT0) return true;
02685 if (left$ == R3 && right$ == R0) return true;
02686 if (left$ == R3 && right$ == R1) return true;
02687 if (left$ == R3 && right$ == R2) return true;
02688 if (left$ == R3 && right$ == R3) return false;
02689 if (left$ == R3 && right$ == R4) return true;
02690 if (left$ == R3 && right$ == GT4) return true;
02691 if (left$ == R4 && right$ == LT0) return true;
02692 if (left$ == R4 && right$ == R0) return true;
02693 if (left$ == R4 && right$ == R1) return true;
02694 if (left$ == R4 && right$ == R2) return true;
02695 if (left$ == R4 && right$ == R3) return true;
02696 if (left$ == R4 && right$ == R4) return false;
02697 if (left$ == R4 && right$ == GT4) return true;
02698 if (left$ == GT4 && right$ == LT0) return true;
02699 if (left$ == GT4 && right$ == R0) return true;
02700 if (left$ == GT4 && right$ == R1) return true;
02701 if (left$ == GT4 && right$ == R2) return true;
02702 if (left$ == GT4 && right$ == R3) return true;
02703 if (left$ == GT4 && right$ == R4) return true;
02704 if (left$ == GT4 && right$ == GT4) return Abstraction.choose();
02705 throw new RuntimeException("Range04.ne(" + left$ + ", " + right$ + ") is undefined");
02706 }
02707 private static byte neNoChoose(int left, int right) {
02708 byte result = -1;
02709 switch (left) {
02710 case 0:
02711 switch (right) {
02712 case 0:
02713 result = 0;
02714 break;
02715 case 1:
02716 result = 1;
02717 break;
02718 case 2:
02719 result = 1;
02720 break;
02721 case 3:
02722 result = 1;
02723 break;
02724 case 4:
02725 result = 1;
02726 break;
02727 case 5:
02728 result = 1;
02729 break;
02730 case 6:
02731 result = 1;
02732 break;
02733 }
02734 break;
02735 case 1:
02736 switch (right) {
02737 case 0:
02738 result = 1;
02739 break;
02740 case 1:
02741 result = 2;
02742 break;
02743 case 2:
02744 result = 1;
02745 break;
02746 case 3:
02747 result = 1;
02748 break;
02749 case 4:
02750 result = 1;
02751 break;
02752 case 5:
02753 result = 1;
02754 break;
02755 case 6:
02756 result = 1;
02757 break;
02758 }
02759 break;
02760 case 2:
02761 switch (right) {
02762 case 0:
02763 result = 1;
02764 break;
02765 case 1:
02766 result = 1;
02767 break;
02768 case 2:
02769 result = 0;
02770 break;
02771 case 3:
02772 result = 1;
02773 break;
02774 case 4:
02775 result = 1;
02776 break;
02777 case 5:
02778 result = 1;
02779 break;
02780 case 6:
02781 result = 1;
02782 break;
02783 }
02784 break;
02785 case 3:
02786 switch (right) {
02787 case 0:
02788 result = 1;
02789 break;
02790 case 1:
02791 result = 1;
02792 break;
02793 case 2:
02794 result = 1;
02795 break;
02796 case 3:
02797 result = 0;
02798 break;
02799 case 4:
02800 result = 1;
02801 break;
02802 case 5:
02803 result = 1;
02804 break;
02805 case 6:
02806 result = 1;
02807 break;
02808 }
02809 break;
02810 case 4:
02811 switch (right) {
02812 case 0:
02813 result = 1;
02814 break;
02815 case 1:
02816 result = 1;
02817 break;
02818 case 2:
02819 result = 1;
02820 break;
02821 case 3:
02822 result = 1;
02823 break;
02824 case 4:
02825 result = 0;
02826 break;
02827 case 5:
02828 result = 1;
02829 break;
02830 case 6:
02831 result = 1;
02832 break;
02833 }
02834 break;
02835 case 5:
02836 switch (right) {
02837 case 0:
02838 result = 1;
02839 break;
02840 case 1:
02841 result = 1;
02842 break;
02843 case 2:
02844 result = 1;
02845 break;
02846 case 3:
02847 result = 1;
02848 break;
02849 case 4:
02850 result = 1;
02851 break;
02852 case 5:
02853 result = 0;
02854 break;
02855 case 6:
02856 result = 1;
02857 break;
02858 }
02859 break;
02860 case 6:
02861 switch (right) {
02862 case 0:
02863 result = 1;
02864 break;
02865 case 1:
02866 result = 1;
02867 break;
02868 case 2:
02869 result = 1;
02870 break;
02871 case 3:
02872 result = 1;
02873 break;
02874 case 4:
02875 result = 1;
02876 break;
02877 case 5:
02878 result = 1;
02879 break;
02880 case 6:
02881 result = 2;
02882 break;
02883 }
02884 break;
02885 }
02886 if (result == -1) throw new RuntimeException("Range04.neNoChoose(" + left + ", " + right + ") is undefined");
02887 return result;
02888 }
02889 public static byte neSet(int leftTokens, int rightTokens) {
02890 byte result = -1;
02891 for (int left = 0; (1 << left) <= leftTokens; left++) {
02892 if ((leftTokens & (1 << left)) == 0) continue;
02893 for (int right = 0; (1 << right) <= rightTokens; right++) {
02894 if ((rightTokens & (1 << right)) != 0) {
02895 if (result == -1) result = neNoChoose(left, right);
02896 else result = Abstraction.meetTest(result, neNoChoose(left, right));
02897 }
02898 }
02899 }
02900 return result;
02901 }
02902 public static int rem(int left$, int right$) {
02903 if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02904 if (left$ == LT0 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02905 if (left$ == LT0 && right$ == R1) return R0;
02906 if (left$ == LT0 && right$ == R2) return Abstraction.choose((1 << R1) | (1 << R0));
02907 if (left$ == LT0 && right$ == R3) return Abstraction.choose((1 << R2) | (1 << R1) | (1 << R0));
02908 if (left$ == LT0 && right$ == R4) return Abstraction.choose((1 << R3) | (1 << R2) | (1 << R1) | (1 << R0));
02909 if (left$ == LT0 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02910 if (left$ == R0 && right$ == LT0) return R0;
02911 if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02912 if (left$ == R0 && right$ == R1) return R0;
02913 if (left$ == R0 && right$ == R2) return R0;
02914 if (left$ == R0 && right$ == R3) return R0;
02915 if (left$ == R0 && right$ == R4) return R0;
02916 if (left$ == R0 && right$ == GT4) return R0;
02917 if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02918 if (left$ == R1 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02919 if (left$ == R1 && right$ == R1) return R0;
02920 if (left$ == R1 && right$ == R2) return R1;
02921 if (left$ == R1 && right$ == R3) return R1;
02922 if (left$ == R1 && right$ == R4) return R1;
02923 if (left$ == R1 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02924 if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02925 if (left$ == R2 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02926 if (left$ == R2 && right$ == R1) return R0;
02927 if (left$ == R2 && right$ == R2) return R0;
02928 if (left$ == R2 && right$ == R3) return R2;
02929 if (left$ == R2 && right$ == R4) return R2;
02930 if (left$ == R2 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02931 if (left$ == R3 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02932 if (left$ == R3 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02933 if (left$ == R3 && right$ == R1) return R0;
02934 if (left$ == R3 && right$ == R2) return R1;
02935 if (left$ == R3 && right$ == R3) return R0;
02936 if (left$ == R3 && right$ == R4) return R3;
02937 if (left$ == R3 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02938 if (left$ == R4 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02939 if (left$ == R4 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02940 if (left$ == R4 && right$ == R1) return R0;
02941 if (left$ == R4 && right$ == R2) return R0;
02942 if (left$ == R4 && right$ == R3) return R1;
02943 if (left$ == R4 && right$ == R4) return R0;
02944 if (left$ == R4 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02945 if (left$ == GT4 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02946 if (left$ == GT4 && right$ == R0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02947 if (left$ == GT4 && right$ == R1) return R0;
02948 if (left$ == GT4 && right$ == R2) return Abstraction.choose((1 << R1) | (1 << R0));
02949 if (left$ == GT4 && right$ == R3) return Abstraction.choose((1 << R2) | (1 << R1) | (1 << R0));
02950 if (left$ == GT4 && right$ == R4) return Abstraction.choose((1 << R3) | (1 << R2) | (1 << R1) | (1 << R0));
02951 if (left$ == GT4 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02952 throw new RuntimeException("Range04.rem(" + left$ + ", " + right$ + ") is undefined");
02953 }
02954 private static int remNoChoose(int left, int right) {
02955 int result = 0;
02956 switch (left) {
02957 case 0:
02958 switch (right) {
02959 case 0:
02960 result = 127;
02961 break;
02962 case 1:
02963 result = 1;
02964 break;
02965 case 2:
02966 result = 1;
02967 break;
02968 case 3:
02969 result = 1;
02970 break;
02971 case 4:
02972 result = 1;
02973 break;
02974 case 5:
02975 result = 1;
02976 break;
02977 case 6:
02978 result = 1;
02979 break;
02980 }
02981 break;
02982 case 1:
02983 switch (right) {
02984 case 0:
02985 result = 127;
02986 break;
02987 case 1:
02988 result = 127;
02989 break;
02990 case 2:
02991 result = 1;
02992 break;
02993 case 3:
02994 result = 5;
02995 break;
02996 case 4:
02997 result = 13;
02998 break;
02999 case 5:
03000 result = 29;
03001 break;
03002 case 6:
03003 result = 127;
03004 break;
03005 }
03006 break;
03007 case 2:
03008 switch (right) {
03009 case 0:
03010 result = 127;
03011 break;
03012 case 1:
03013 result = 127;
03014 break;
03015 case 2:
03016 result = 1;
03017 break;
03018 case 3:
03019 result = 4;
03020 break;
03021 case 4:
03022 result = 4;
03023 break;
03024 case 5:
03025 result = 4;
03026 break;
03027 case 6:
03028 result = 127;
03029 break;
03030 }
03031 break;
03032 case 3:
03033 switch (right) {
03034 case 0:
03035 result = 127;
03036 break;
03037 case 1:
03038 result = 127;
03039 break;
03040 case 2:
03041 result = 1;
03042 break;
03043 case 3:
03044 result = 1;
03045 break;
03046 case 4:
03047 result = 8;
03048 break;
03049 case 5:
03050 result = 8;
03051 break;
03052 case 6:
03053 result = 127;
03054 break;
03055 }
03056 break;
03057 case 4:
03058 switch (right) {
03059 case 0:
03060 result = 127;
03061 break;
03062 case 1:
03063 result = 127;
03064 break;
03065 case 2:
03066 result = 1;
03067 break;
03068 case 3:
03069 result = 4;
03070 break;
03071 case 4:
03072 result = 1;
03073 break;
03074 case 5:
03075 result = 16;
03076 break;
03077 case 6:
03078 result = 127;
03079 break;
03080 }
03081 break;
03082 case 5:
03083 switch (right) {
03084 case 0:
03085 result = 127;
03086 break;
03087 case 1:
03088 result = 127;
03089 break;
03090 case 2:
03091 result = 1;
03092 break;
03093 case 3:
03094 result = 1;
03095 break;
03096 case 4:
03097 result = 4;
03098 break;
03099 case 5:
03100 result = 1;
03101 break;
03102 case 6:
03103 result = 127;
03104 break;
03105 }
03106 break;
03107 case 6:
03108 switch (right) {
03109 case 0:
03110 result = 127;
03111 break;
03112 case 1:
03113 result = 127;
03114 break;
03115 case 2:
03116 result = 1;
03117 break;
03118 case 3:
03119 result = 5;
03120 break;
03121 case 4:
03122 result = 13;
03123 break;
03124 case 5:
03125 result = 29;
03126 break;
03127 case 6:
03128 result = 127;
03129 break;
03130 }
03131 break;
03132 }
03133 if (result == 0) throw new RuntimeException("Range04.remNoChoose(" + left + ", " + right + ") is undefined");
03134 return result;
03135 }
03136 public static int remSet(int leftTokens, int rightTokens) {
03137 int result = -1;
03138 for (int left = 0; (1 << left) <= leftTokens; left++) {
03139 if ((leftTokens & (1 << left)) == 0) continue;
03140 for (int right = 0; (1 << right) <= rightTokens; right++) {
03141 if ((rightTokens & (1 << right)) != 0) {
03142 if (result == -1) result = remNoChoose(left, right);
03143 else result = Abstraction.meetArith(result, remNoChoose(left, right));
03144 }
03145 }
03146 }
03147 return result;
03148 }
03149 public static int sub(int left$, int right$) {
03150 if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
03151 if (left$ == LT0 && right$ == R0) return LT0;
03152 if (left$ == LT0 && right$ == R1) return LT0;
03153 if (left$ == LT0 && right$ == R2) return LT0;
03154 if (left$ == LT0 && right$ == R3) return LT0;
03155 if (left$ == LT0 && right$ == R4) return LT0;
03156 if (left$ == LT0 && right$ == GT4) return LT0;
03157 if (left$ == R0 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1));
03158 if (left$ == R0 && right$ == R0) return R0;
03159 if (left$ == R0 && right$ == R1) return LT0;
03160 if (left$ == R0 && right$ == R2) return LT0;
03161 if (left$ == R0 && right$ == R3) return LT0;
03162 if (left$ == R0 && right$ == R4) return LT0;
03163 if (left$ == R0 && right$ == GT4) return LT0;
03164 if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2));
03165 if (left$ == R1 && right$ == R0) return R1;
03166 if (left$ == R1 && right$ == R1) return R0;
03167 if (left$ == R1 && right$ == R2) return LT0;
03168 if (left$ == R1 && right$ == R3) return LT0;
03169 if (left$ == R1 && right$ == R4) return LT0;
03170 if (left$ == R1 && right$ == GT4) return LT0;
03171 if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3));
03172 if (left$ == R2 && right$ == R0) return R2;
03173 if (left$ == R2 && right$ == R1) return R1;
03174 if (left$ == R2 && right$ == R2) return R0;
03175 if (left$ == R2 && right$ == R3) return LT0;
03176 if (left$ == R2 && right$ == R4) return LT0;
03177 if (left$ == R2 && right$ == GT4) return LT0;
03178 if (left$ == R3 && right$ == LT0) return Abstraction.choose((1 << GT4) | (1 << R4));
03179 if (left$ == R3 && right$ == R0) return R3;
03180 if (left$ == R3 && right$ == R1) return R2;
03181 if (left$ == R3 && right$ == R2) return R1;
03182 if (left$ == R3 && right$ == R3) return R0;
03183 if (left$ == R3 && right$ == R4) return LT0;
03184 if (left$ == R3 && right$ == GT4) return LT0;
03185 if (left$ == R4 && right$ == LT0) return GT4;
03186 if (left$ == R4 && right$ == R0) return R4;
03187 if (left$ == R4 && right$ == R1) return R3;
03188 if (left$ == R4 && right$ == R2) return R2;
03189 if (left$ == R4 && right$ == R3) return R1;
03190 if (left$ == R4 && right$ == R4) return R0;
03191 if (left$ == R4 && right$ == GT4) return LT0;
03192 if (left$ == GT4 && right$ == LT0) return GT4;
03193 if (left$ == GT4 && right$ == R0) return GT4;
03194 if (left$ == GT4 && right$ == R1) return Abstraction.choose((1 << GT4) | (1 << R4));
03195 if (left$ == GT4 && right$ == R2) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3));
03196 if (left$ == GT4 && right$ == R3) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2));
03197 if (left$ == GT4 && right$ == R4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1));
03198 if (left$ == GT4 && right$ == GT4) return Abstraction.choose((1 << GT4) | (1 << R4) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
03199 throw new RuntimeException("Range04.sub(" + left$ + ", " + right$ + ") is undefined");
03200 }
03201 private static int subNoChoose(int left, int right) {
03202 int result = 0;
03203 switch (left) {
03204 case 0:
03205 switch (right) {
03206 case 0:
03207 result = 1;
03208 break;
03209 case 1:
03210 result = 124;
03211 break;
03212 case 2:
03213 result = 2;
03214 break;
03215 case 3:
03216 result = 2;
03217 break;
03218 case 4:
03219 result = 2;
03220 break;
03221 case 5:
03222 result = 2;
03223 break;
03224 case 6:
03225 result = 2;
03226 break;
03227 }
03228 break;
03229 case 1:
03230 switch (right) {
03231 case 0:
03232 result = 2;
03233 break;
03234 case 1:
03235 result = 127;
03236 break;
03237 case 2:
03238 result = 2;
03239 break;
03240 case 3:
03241 result = 2;
03242 break;
03243 case 4:
03244 result = 2;
03245 break;
03246 case 5:
03247 result = 2;
03248 break;
03249 case 6:
03250 result = 2;
03251 break;
03252 }
03253 break;
03254 case 2:
03255 switch (right) {
03256 case 0:
03257 result = 4;
03258 break;
03259 case 1:
03260 result = 120;
03261 break;
03262 case 2:
03263 result = 1;
03264 break;
03265 case 3:
03266 result = 2;
03267 break;
03268 case 4:
03269 result = 2;
03270 break;
03271 case 5:
03272 result = 2;
03273 break;
03274 case 6:
03275 result = 2;
03276 break;
03277 }
03278 break;
03279 case 3:
03280 switch (right) {
03281 case 0:
03282 result = 8;
03283 break;
03284 case 1:
03285 result = 112;
03286 break;
03287 case 2:
03288 result = 4;
03289 break;
03290 case 3:
03291 result = 1;
03292 break;
03293 case 4:
03294 result = 2;
03295 break;
03296 case 5:
03297 result = 2;
03298 break;
03299 case 6:
03300 result = 2;
03301 break;
03302 }
03303 break;
03304 case 4:
03305 switch (right) {
03306 case 0:
03307 result = 16;
03308 break;
03309 case 1:
03310 result = 96;
03311 break;
03312 case 2:
03313 result = 8;
03314 break;
03315 case 3:
03316 result = 4;
03317 break;
03318 case 4:
03319 result = 1;
03320 break;
03321 case 5:
03322 result = 2;
03323 break;
03324 case 6:
03325 result = 2;
03326 break;
03327 }
03328 break;
03329 case 5:
03330 switch (right) {
03331 case 0:
03332 result = 32;
03333 break;
03334 case 1:
03335 result = 64;
03336 break;
03337 case 2:
03338 result = 16;
03339 break;
03340 case 3:
03341 result = 8;
03342 break;
03343 case 4:
03344 result = 4;
03345 break;
03346 case 5:
03347 result = 1;
03348 break;
03349 case 6:
03350 result = 2;
03351 break;
03352 }
03353 break;
03354 case 6:
03355 switch (right) {
03356 case 0:
03357 result = 64;
03358 break;
03359 case 1:
03360 result = 64;
03361 break;
03362 case 2:
03363 result = 96;
03364 break;
03365 case 3:
03366 result = 112;
03367 break;
03368 case 4:
03369 result = 120;
03370 break;
03371 case 5:
03372 result = 124;
03373 break;
03374 case 6:
03375 result = 127;
03376 break;
03377 }
03378 break;
03379 }
03380 if (result == 0) throw new RuntimeException("Range04.subNoChoose(" + left + ", " + right + ") is undefined");
03381 return result;
03382 }
03383 public static int subSet(int leftTokens, int rightTokens) {
03384 int result = -1;
03385 for (int left = 0; (1 << left) <= leftTokens; left++) {
03386 if ((leftTokens & (1 << left)) == 0) continue;
03387 for (int right = 0; (1 << right) <= rightTokens; right++) {
03388 if ((rightTokens & (1 << right)) != 0) {
03389 if (result == -1) result = subNoChoose(left, right);
03390 else result = Abstraction.meetArith(result, subNoChoose(left, right));
03391 }
03392 }
03393 }
03394 return result;
03395 }
03396 public String toString() {
03397 return getName();
03398 }
03399 public static Range04 v() {
03400 return v;
03401 }
03402 }
