Range03.java Source File

00001 package edu.ksu.cis.bandera.abstraction.lib.integral;
00002 
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004  * Bandera, a Java(TM) analysis and transformation toolkit           *
00005  * Copyright (C) 1998-2001 SAnToS Laboratories (santos@cis.ksu.edu)  *
00006 
00007  * All rights reserved.                                              *
00008  *                                                                   *
00009  * This work was done as a project in the SAnToS Laboratory,         *
00010  * Department of Computing and Information Sciences, Kansas State    *
00011  * University, USA (http://www.cis.ksu.edu/santos).                  *
00012  * It is understood that any modification not identified as such is  *
00013  * not covered by the preceding statement.                           *
00014  *                                                                   *
00015  * This work is free software; you can redistribute it and/or        *
00016  * modify it under the terms of the GNU Library General Public       *
00017  * License as published by the Free Software Foundation; either      *
00018  * version 2 of the License, or (at your option) any later version.  *
00019  *                                                                   *
00020  * This work is distributed in the hope that it will be useful,      *
00021  * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
00022  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
00023  * Library General Public License for more details.                  *
00024  *                                                                   *
00025  * You should have received a copy of the GNU Library General Public *
00026  * License along with this toolkit; if not, write to the             *
00027  * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
00028  * Boston, MA  02111-1307, USA.                                      *
00029  *                                                                   *
00030  * Java is a trademark of Sun Microsystems, Inc.                     *
00031  *                                                                   *
00032  * To submit a bug report, send a comment, or get the latest news on *
00033  * this project and other SAnToS projects, please visit the web-site *
00034  *                http://www.cis.ksu.edu/santos                      *
00035  * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
00036 // This file was generated by Bandera (http://www.cis.ksu.edu/santos/bandera).
00037 import edu.ksu.cis.bandera.abstraction.*;
00038 public class Range03 extends IntegralAbstraction {
00039   private static final Range03 v = new Range03();
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 GT3 = 5;
00046   private Range03() {
00047   }  
00048   public static int abs(long n) {
00049     if (n < 0) return LT0;
00050     if (n == 0) return R0;
00051     if (n == 1) return R1;
00052     if (n == 2) return R2;
00053     if (n == 3) return R3;
00054     if (n > 3) return GT3;
00055     throw new RuntimeException("Range03 cannot abstract value '" + n + "'");
00056   }  
00057   public static int add(int left$, int right$) {
00058     if (left$ == LT0 && right$ == LT0) return LT0;
00059     if (left$ == LT0 && right$ == R0) return LT0;
00060     if (left$ == LT0 && right$ == R1) return Abstraction.choose((1 << R0) | (1 << LT0));
00061     if (left$ == LT0 && right$ == R2) return Abstraction.choose((1 << R1) | (1 << R0) | (1 << LT0));
00062     if (left$ == LT0 && right$ == R3) return Abstraction.choose((1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00063     if (left$ == LT0 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00064     if (left$ == R0 && right$ == LT0) return LT0;
00065     if (left$ == R0 && right$ == R0) return R0;
00066     if (left$ == R0 && right$ == R1) return R1;
00067     if (left$ == R0 && right$ == R2) return R2;
00068     if (left$ == R0 && right$ == R3) return R3;
00069     if (left$ == R0 && right$ == GT3) return GT3;
00070     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << R0) | (1 << LT0));
00071     if (left$ == R1 && right$ == R0) return R1;
00072     if (left$ == R1 && right$ == R1) return R2;
00073     if (left$ == R1 && right$ == R2) return R3;
00074     if (left$ == R1 && right$ == R3) return GT3;
00075     if (left$ == R1 && right$ == GT3) return GT3;
00076     if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << R1) | (1 << R0) | (1 << LT0));
00077     if (left$ == R2 && right$ == R0) return R2;
00078     if (left$ == R2 && right$ == R1) return R3;
00079     if (left$ == R2 && right$ == R2) return GT3;
00080     if (left$ == R2 && right$ == R3) return GT3;
00081     if (left$ == R2 && right$ == GT3) return GT3;
00082     if (left$ == R3 && right$ == LT0) return Abstraction.choose((1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00083     if (left$ == R3 && right$ == R0) return R3;
00084     if (left$ == R3 && right$ == R1) return GT3;
00085     if (left$ == R3 && right$ == R2) return GT3;
00086     if (left$ == R3 && right$ == R3) return GT3;
00087     if (left$ == R3 && right$ == GT3) return GT3;
00088     if (left$ == GT3 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00089     if (left$ == GT3 && right$ == R0) return GT3;
00090     if (left$ == GT3 && right$ == R1) return GT3;
00091     if (left$ == GT3 && right$ == R2) return GT3;
00092     if (left$ == GT3 && right$ == R3) return GT3;
00093     if (left$ == GT3 && right$ == GT3) return GT3;
00094     throw new RuntimeException("Range03.add(" + left$ + ", " + right$ + ") is undefined");
00095   }  
00096   private static int addNoChoose(int left, int right) {
00097     int result = 0;
00098     switch (left) {
00099       case 0:
00100         switch (right) {
00101           case 0:
00102             result = 1;
00103             break;
00104           case 1:
00105             result = 2;
00106             break;
00107           case 2:
00108             result = 4;
00109             break;
00110           case 3:
00111             result = 8;
00112             break;
00113           case 4:
00114             result = 16;
00115             break;
00116           case 5:
00117             result = 32;
00118             break;
00119         }
00120         break;
00121       case 1:
00122         switch (right) {
00123           case 0:
00124             result = 2;
00125             break;
00126           case 1:
00127             result = 2;
00128             break;
00129           case 2:
00130             result = 3;
00131             break;
00132           case 3:
00133             result = 7;
00134             break;
00135           case 4:
00136             result = 15;
00137             break;
00138           case 5:
00139             result = 63;
00140             break;
00141         }
00142         break;
00143       case 2:
00144         switch (right) {
00145           case 0:
00146             result = 4;
00147             break;
00148           case 1:
00149             result = 3;
00150             break;
00151           case 2:
00152             result = 8;
00153             break;
00154           case 3:
00155             result = 16;
00156             break;
00157           case 4:
00158             result = 32;
00159             break;
00160           case 5:
00161             result = 32;
00162             break;
00163         }
00164         break;
00165       case 3:
00166         switch (right) {
00167           case 0:
00168             result = 8;
00169             break;
00170           case 1:
00171             result = 7;
00172             break;
00173           case 2:
00174             result = 16;
00175             break;
00176           case 3:
00177             result = 32;
00178             break;
00179           case 4:
00180             result = 32;
00181             break;
00182           case 5:
00183             result = 32;
00184             break;
00185         }
00186         break;
00187       case 4:
00188         switch (right) {
00189           case 0:
00190             result = 16;
00191             break;
00192           case 1:
00193             result = 15;
00194             break;
00195           case 2:
00196             result = 32;
00197             break;
00198           case 3:
00199             result = 32;
00200             break;
00201           case 4:
00202             result = 32;
00203             break;
00204           case 5:
00205             result = 32;
00206             break;
00207         }
00208         break;
00209       case 5:
00210         switch (right) {
00211           case 0:
00212             result = 32;
00213             break;
00214           case 1:
00215             result = 63;
00216             break;
00217           case 2:
00218             result = 32;
00219             break;
00220           case 3:
00221             result = 32;
00222             break;
00223           case 4:
00224             result = 32;
00225             break;
00226           case 5:
00227             result = 32;
00228             break;
00229         }
00230         break;
00231     }
00232     if (result == 0) throw new RuntimeException("Range03.addNoChoose(" + left + ", " + right + ") is undefined");
00233     return result;
00234   }  
00235   public static int addSet(int leftTokens, int rightTokens) {
00236     int result = -1;
00237     for (int left = 0; (1 << left) <= leftTokens; left++) {
00238       if ((leftTokens & (1 << left)) == 0) continue;
00239       for (int right = 0; (1 << right) <= rightTokens; right++) {
00240         if ((rightTokens & (1 << right)) != 0) {
00241           if (result == -1) result = addNoChoose(left, right);
00242           else result = Abstraction.meetArith(result, addNoChoose(left, right));
00243         }
00244       }
00245     }
00246     return result;
00247   }  
00248   public static int div(int left$, int right$) {
00249     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00250     if (left$ == LT0 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00251     if (left$ == LT0 && right$ == R1) return LT0;
00252     if (left$ == LT0 && right$ == R2) return LT0;
00253     if (left$ == LT0 && right$ == R3) return LT0;
00254     if (left$ == LT0 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00255     if (left$ == R0 && right$ == LT0) return R0;
00256     if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00257     if (left$ == R0 && right$ == R1) return R0;
00258     if (left$ == R0 && right$ == R2) return R0;
00259     if (left$ == R0 && right$ == R3) return R0;
00260     if (left$ == R0 && right$ == GT3) return R0;
00261     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00262     if (left$ == R1 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00263     if (left$ == R1 && right$ == R1) return R1;
00264     if (left$ == R1 && right$ == R2) return R0;
00265     if (left$ == R1 && right$ == R3) return R0;
00266     if (left$ == R1 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00267     if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00268     if (left$ == R2 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00269     if (left$ == R2 && right$ == R1) return R2;
00270     if (left$ == R2 && right$ == R2) return R1;
00271     if (left$ == R2 && right$ == R3) return R0;
00272     if (left$ == R2 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00273     if (left$ == R3 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00274     if (left$ == R3 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00275     if (left$ == R3 && right$ == R1) return R3;
00276     if (left$ == R3 && right$ == R2) return R1;
00277     if (left$ == R3 && right$ == R3) return R1;
00278     if (left$ == R3 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00279     if (left$ == GT3 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00280     if (left$ == GT3 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00281     if (left$ == GT3 && right$ == R1) return GT3;
00282     if (left$ == GT3 && right$ == R2) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2));
00283     if (left$ == GT3 && right$ == R3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1));
00284     if (left$ == GT3 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00285     throw new RuntimeException("Range03.div(" + left$ + ", " + right$ + ") is undefined");
00286   }  
00287   private static int divNoChoose(int left, int right) {
00288     int result = 0;
00289     switch (left) {
00290       case 0:
00291         switch (right) {
00292           case 0:
00293             result = 63;
00294             break;
00295           case 1:
00296             result = 1;
00297             break;
00298           case 2:
00299             result = 1;
00300             break;
00301           case 3:
00302             result = 1;
00303             break;
00304           case 4:
00305             result = 1;
00306             break;
00307           case 5:
00308             result = 1;
00309             break;
00310         }
00311         break;
00312       case 1:
00313         switch (right) {
00314           case 0:
00315             result = 63;
00316             break;
00317           case 1:
00318             result = 63;
00319             break;
00320           case 2:
00321             result = 2;
00322             break;
00323           case 3:
00324             result = 2;
00325             break;
00326           case 4:
00327             result = 2;
00328             break;
00329           case 5:
00330             result = 63;
00331             break;
00332         }
00333         break;
00334       case 2:
00335         switch (right) {
00336           case 0:
00337             result = 63;
00338             break;
00339           case 1:
00340             result = 63;
00341             break;
00342           case 2:
00343             result = 4;
00344             break;
00345           case 3:
00346             result = 1;
00347             break;
00348           case 4:
00349             result = 1;
00350             break;
00351           case 5:
00352             result = 63;
00353             break;
00354         }
00355         break;
00356       case 3:
00357         switch (right) {
00358           case 0:
00359             result = 63;
00360             break;
00361           case 1:
00362             result = 63;
00363             break;
00364           case 2:
00365             result = 8;
00366             break;
00367           case 3:
00368             result = 4;
00369             break;
00370           case 4:
00371             result = 1;
00372             break;
00373           case 5:
00374             result = 63;
00375             break;
00376         }
00377         break;
00378       case 4:
00379         switch (right) {
00380           case 0:
00381             result = 63;
00382             break;
00383           case 1:
00384             result = 63;
00385             break;
00386           case 2:
00387             result = 16;
00388             break;
00389           case 3:
00390             result = 4;
00391             break;
00392           case 4:
00393             result = 4;
00394             break;
00395           case 5:
00396             result = 63;
00397             break;
00398         }
00399         break;
00400       case 5:
00401         switch (right) {
00402           case 0:
00403             result = 63;
00404             break;
00405           case 1:
00406             result = 63;
00407             break;
00408           case 2:
00409             result = 32;
00410             break;
00411           case 3:
00412             result = 56;
00413             break;
00414           case 4:
00415             result = 60;
00416             break;
00417           case 5:
00418             result = 63;
00419             break;
00420         }
00421         break;
00422     }
00423     if (result == 0) throw new RuntimeException("Range03.divNoChoose(" + left + ", " + right + ") is undefined");
00424     return result;
00425   }  
00426   public static int divSet(int leftTokens, int rightTokens) {
00427     int result = -1;
00428     for (int left = 0; (1 << left) <= leftTokens; left++) {
00429       if ((leftTokens & (1 << left)) == 0) continue;
00430       for (int right = 0; (1 << right) <= rightTokens; right++) {
00431         if ((rightTokens & (1 << right)) != 0) {
00432           if (result == -1) result = divNoChoose(left, right);
00433           else result = Abstraction.meetArith(result, divNoChoose(left, right));
00434         }
00435       }
00436     }
00437     return result;
00438   }  
00439   public static boolean eq(int left$, int right$) {
00440     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00441     if (left$ == LT0 && right$ == R0) return false;
00442     if (left$ == LT0 && right$ == R1) return false;
00443     if (left$ == LT0 && right$ == R2) return false;
00444     if (left$ == LT0 && right$ == R3) return false;
00445     if (left$ == LT0 && right$ == GT3) return false;
00446     if (left$ == R0 && right$ == LT0) return false;
00447     if (left$ == R0 && right$ == R0) return true;
00448     if (left$ == R0 && right$ == R1) return false;
00449     if (left$ == R0 && right$ == R2) return false;
00450     if (left$ == R0 && right$ == R3) return false;
00451     if (left$ == R0 && right$ == GT3) return false;
00452     if (left$ == R1 && right$ == LT0) return false;
00453     if (left$ == R1 && right$ == R0) return false;
00454     if (left$ == R1 && right$ == R1) return true;
00455     if (left$ == R1 && right$ == R2) return false;
00456     if (left$ == R1 && right$ == R3) return false;
00457     if (left$ == R1 && right$ == GT3) return false;
00458     if (left$ == R2 && right$ == LT0) return false;
00459     if (left$ == R2 && right$ == R0) return false;
00460     if (left$ == R2 && right$ == R1) return false;
00461     if (left$ == R2 && right$ == R2) return true;
00462     if (left$ == R2 && right$ == R3) return false;
00463     if (left$ == R2 && right$ == GT3) return false;
00464     if (left$ == R3 && right$ == LT0) return false;
00465     if (left$ == R3 && right$ == R0) return false;
00466     if (left$ == R3 && right$ == R1) return false;
00467     if (left$ == R3 && right$ == R2) return false;
00468     if (left$ == R3 && right$ == R3) return true;
00469     if (left$ == R3 && right$ == GT3) return false;
00470     if (left$ == GT3 && right$ == LT0) return false;
00471     if (left$ == GT3 && right$ == R0) return false;
00472     if (left$ == GT3 && right$ == R1) return false;
00473     if (left$ == GT3 && right$ == R2) return false;
00474     if (left$ == GT3 && right$ == R3) return false;
00475     if (left$ == GT3 && right$ == GT3) return Abstraction.choose();
00476     throw new RuntimeException("Range03.eq(" + left$ + ", " + right$ + ") is undefined");
00477   }  
00478   private static byte eqNoChoose(int left, int right) {
00479     byte result = -1;
00480     switch (left) {
00481       case 0:
00482         switch (right) {
00483           case 0:
00484             result = 1;
00485             break;
00486           case 1:
00487             result = 0;
00488             break;
00489           case 2:
00490             result = 0;
00491             break;
00492           case 3:
00493             result = 0;
00494             break;
00495           case 4:
00496             result = 0;
00497             break;
00498           case 5:
00499             result = 0;
00500             break;
00501         }
00502         break;
00503       case 1:
00504         switch (right) {
00505           case 0:
00506             result = 0;
00507             break;
00508           case 1:
00509             result = 2;
00510             break;
00511           case 2:
00512             result = 0;
00513             break;
00514           case 3:
00515             result = 0;
00516             break;
00517           case 4:
00518             result = 0;
00519             break;
00520           case 5:
00521             result = 0;
00522             break;
00523         }
00524         break;
00525       case 2:
00526         switch (right) {
00527           case 0:
00528             result = 0;
00529             break;
00530           case 1:
00531             result = 0;
00532             break;
00533           case 2:
00534             result = 1;
00535             break;
00536           case 3:
00537             result = 0;
00538             break;
00539           case 4:
00540             result = 0;
00541             break;
00542           case 5:
00543             result = 0;
00544             break;
00545         }
00546         break;
00547       case 3:
00548         switch (right) {
00549           case 0:
00550             result = 0;
00551             break;
00552           case 1:
00553             result = 0;
00554             break;
00555           case 2:
00556             result = 0;
00557             break;
00558           case 3:
00559             result = 1;
00560             break;
00561           case 4:
00562             result = 0;
00563             break;
00564           case 5:
00565             result = 0;
00566             break;
00567         }
00568         break;
00569       case 4:
00570         switch (right) {
00571           case 0:
00572             result = 0;
00573             break;
00574           case 1:
00575             result = 0;
00576             break;
00577           case 2:
00578             result = 0;
00579             break;
00580           case 3:
00581             result = 0;
00582             break;
00583           case 4:
00584             result = 1;
00585             break;
00586           case 5:
00587             result = 0;
00588             break;
00589         }
00590         break;
00591       case 5:
00592         switch (right) {
00593           case 0:
00594             result = 0;
00595             break;
00596           case 1:
00597             result = 0;
00598             break;
00599           case 2:
00600             result = 0;
00601             break;
00602           case 3:
00603             result = 0;
00604             break;
00605           case 4:
00606             result = 0;
00607             break;
00608           case 5:
00609             result = 2;
00610             break;
00611         }
00612         break;
00613     }
00614     if (result == -1) throw new RuntimeException("Range03.eqNoChoose(" + left + ", " + right + ") is undefined");
00615     return result;
00616   }  
00617   public static byte eqSet(int leftTokens, int rightTokens) {
00618     byte result = -1;
00619     for (int left = 0; (1 << left) <= leftTokens; left++) {
00620       if ((leftTokens & (1 << left)) == 0) continue;
00621       for (int right = 0; (1 << right) <= rightTokens; right++) {
00622         if ((rightTokens & (1 << right)) != 0) {
00623           if (result == -1) result = eqNoChoose(left, right);
00624           else result = Abstraction.meetTest(result, eqNoChoose(left, right));
00625         }
00626       }
00627     }
00628     return result;
00629   }  
00630   public static boolean ge(int left$, int right$) {
00631     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00632     if (left$ == LT0 && right$ == R0) return false;
00633     if (left$ == LT0 && right$ == R1) return false;
00634     if (left$ == LT0 && right$ == R2) return false;
00635     if (left$ == LT0 && right$ == R3) return false;
00636     if (left$ == LT0 && right$ == GT3) return false;
00637     if (left$ == R0 && right$ == LT0) return true;
00638     if (left$ == R0 && right$ == R0) return true;
00639     if (left$ == R0 && right$ == R1) return false;
00640     if (left$ == R0 && right$ == R2) return false;
00641     if (left$ == R0 && right$ == R3) return false;
00642     if (left$ == R0 && right$ == GT3) return false;
00643     if (left$ == R1 && right$ == LT0) return true;
00644     if (left$ == R1 && right$ == R0) return true;
00645     if (left$ == R1 && right$ == R1) return true;
00646     if (left$ == R1 && right$ == R2) return false;
00647     if (left$ == R1 && right$ == R3) return false;
00648     if (left$ == R1 && right$ == GT3) return false;
00649     if (left$ == R2 && right$ == LT0) return true;
00650     if (left$ == R2 && right$ == R0) return true;
00651     if (left$ == R2 && right$ == R1) return true;
00652     if (left$ == R2 && right$ == R2) return true;
00653     if (left$ == R2 && right$ == R3) return false;
00654     if (left$ == R2 && right$ == GT3) return false;
00655     if (left$ == R3 && right$ == LT0) return true;
00656     if (left$ == R3 && right$ == R0) return true;
00657     if (left$ == R3 && right$ == R1) return true;
00658     if (left$ == R3 && right$ == R2) return true;
00659     if (left$ == R3 && right$ == R3) return true;
00660     if (left$ == R3 && right$ == GT3) return false;
00661     if (left$ == GT3 && right$ == LT0) return true;
00662     if (left$ == GT3 && right$ == R0) return true;
00663     if (left$ == GT3 && right$ == R1) return true;
00664     if (left$ == GT3 && right$ == R2) return true;
00665     if (left$ == GT3 && right$ == R3) return true;
00666     if (left$ == GT3 && right$ == GT3) return Abstraction.choose();
00667     throw new RuntimeException("Range03.ge(" + left$ + ", " + right$ + ") is undefined");
00668   }  
00669   private static byte geNoChoose(int left, int right) {
00670     byte result = -1;
00671     switch (left) {
00672       case 0:
00673         switch (right) {
00674           case 0:
00675             result = 1;
00676             break;
00677           case 1:
00678             result = 1;
00679             break;
00680           case 2:
00681             result = 0;
00682             break;
00683           case 3:
00684             result = 0;
00685             break;
00686           case 4:
00687             result = 0;
00688             break;
00689           case 5:
00690             result = 0;
00691             break;
00692         }
00693         break;
00694       case 1:
00695         switch (right) {
00696           case 0:
00697             result = 0;
00698             break;
00699           case 1:
00700             result = 2;
00701             break;
00702           case 2:
00703             result = 0;
00704             break;
00705           case 3:
00706             result = 0;
00707             break;
00708           case 4:
00709             result = 0;
00710             break;
00711           case 5:
00712             result = 0;
00713             break;
00714         }
00715         break;
00716       case 2:
00717         switch (right) {
00718           case 0:
00719             result = 1;
00720             break;
00721           case 1:
00722             result = 1;
00723             break;
00724           case 2:
00725             result = 1;
00726             break;
00727           case 3:
00728             result = 0;
00729             break;
00730           case 4:
00731             result = 0;
00732             break;
00733           case 5:
00734             result = 0;
00735             break;
00736         }
00737         break;
00738       case 3:
00739         switch (right) {
00740           case 0:
00741             result = 1;
00742             break;
00743           case 1:
00744             result = 1;
00745             break;
00746           case 2:
00747             result = 1;
00748             break;
00749           case 3:
00750             result = 1;
00751             break;
00752           case 4:
00753             result = 0;
00754             break;
00755           case 5:
00756             result = 0;
00757             break;
00758         }
00759         break;
00760       case 4:
00761         switch (right) {
00762           case 0:
00763             result = 1;
00764             break;
00765           case 1:
00766             result = 1;
00767             break;
00768           case 2:
00769             result = 1;
00770             break;
00771           case 3:
00772             result = 1;
00773             break;
00774           case 4:
00775             result = 1;
00776             break;
00777           case 5:
00778             result = 0;
00779             break;
00780         }
00781         break;
00782       case 5:
00783         switch (right) {
00784           case 0:
00785             result = 1;
00786             break;
00787           case 1:
00788             result = 1;
00789             break;
00790           case 2:
00791             result = 1;
00792             break;
00793           case 3:
00794             result = 1;
00795             break;
00796           case 4:
00797             result = 1;
00798             break;
00799           case 5:
00800             result = 2;
00801             break;
00802         }
00803         break;
00804     }
00805     if (result == -1) throw new RuntimeException("Range03.geNoChoose(" + left + ", " + right + ") is undefined");
00806     return result;
00807   }  
00808   public static byte geSet(int leftTokens, int rightTokens) {
00809     byte result = -1;
00810     for (int left = 0; (1 << left) <= leftTokens; left++) {
00811       if ((leftTokens & (1 << left)) == 0) continue;
00812       for (int right = 0; (1 << right) <= rightTokens; right++) {
00813         if ((rightTokens & (1 << right)) != 0) {
00814           if (result == -1) result = geNoChoose(left, right);
00815           else result = Abstraction.meetTest(result, geNoChoose(left, right));
00816         }
00817       }
00818     }
00819     return result;
00820   }  
00821   public static String getBASLRepresentation() {
00822     return
00823       "abstraction Range03 extends integral \n"
00824       + "  begin\n"
00825       + "    TOKENS = {LT0, R0, R1, R2, R3, GT3};\n"
00826       + "    DEFAULT = R0;\n"
00827       + "    ONE2ONE = {R0, R1, R2, R3};\n"
00828       + "    abstract (n)\n"
00829       + "      begin\n"
00830       + "        n < 0 -> LT0;\n"
00831       + "        n == 0 -> R0;\n"
00832       + "        n == 1 -> R1;\n"
00833       + "        n == 2 -> R2;\n"
00834       + "        n == 3 -> R3;\n"
00835       + "        n > 3 -> GT3;\n"
00836       + "      end\n"
00837       + "    operator + add \n"
00838       + "      begin\n"
00839       + "        (LT0, LT0) -> LT0;\n"
00840       + "        (LT0, R0) -> LT0;\n"
00841       + "        (LT0, R1) -> {LT0, R0};\n"
00842       + "        (LT0, R2) -> {LT0, R0, R1};\n"
00843       + "        (LT0, R3) -> {LT0, R0, R1, R2};\n"
00844       + "        (LT0, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
00845       + "        (R0, LT0) -> LT0;\n"
00846       + "        (R0, R0) -> R0;\n"
00847       + "        (R0, R1) -> R1;\n"
00848       + "        (R0, R2) -> R2;\n"
00849       + "        (R0, R3) -> R3;\n"
00850       + "        (R0, GT3) -> GT3;\n"
00851       + "        (R1, LT0) -> {LT0, R0};\n"
00852       + "        (R1, R0) -> R1;\n"
00853       + "        (R1, R1) -> R2;\n"
00854       + "        (R1, R2) -> R3;\n"
00855       + "        (R1, R3) -> GT3;\n"
00856       + "        (R1, GT3) -> GT3;\n"
00857       + "        (R2, LT0) -> {LT0, R0, R1};\n"
00858       + "        (R2, R0) -> R2;\n"
00859       + "        (R2, R1) -> R3;\n"
00860       + "        (R2, R2) -> GT3;\n"
00861       + "        (R2, R3) -> GT3;\n"
00862       + "        (R2, GT3) -> GT3;\n"
00863       + "        (R3, LT0) -> {LT0, R0, R1, R2};\n"
00864       + "        (R3, R0) -> R3;\n"
00865       + "        (R3, R1) -> GT3;\n"
00866       + "        (R3, R2) -> GT3;\n"
00867       + "        (R3, R3) -> GT3;\n"
00868       + "        (R3, GT3) -> GT3;\n"
00869       + "        (GT3, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
00870       + "        (GT3, R0) -> GT3;\n"
00871       + "        (GT3, R1) -> GT3;\n"
00872       + "        (GT3, R2) -> GT3;\n"
00873       + "        (GT3, R3) -> GT3;\n"
00874       + "        (GT3, GT3) -> GT3;\n"
00875       + "      end\n"
00876       + "    operator - sub \n"
00877       + "      begin\n"
00878       + "        (LT0, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
00879       + "        (LT0, R0) -> LT0;\n"
00880       + "        (LT0, R1) -> LT0;\n"
00881       + "        (LT0, R2) -> LT0;\n"
00882       + "        (LT0, R3) -> LT0;\n"
00883       + "        (LT0, GT3) -> LT0;\n"
00884       + "        (R0, LT0) -> {R1, R2, R3, GT3};\n"
00885       + "        (R0, R0) -> R0;\n"
00886       + "        (R0, R1) -> LT0;\n"
00887       + "        (R0, R2) -> LT0;\n"
00888       + "        (R0, R3) -> LT0;\n"
00889       + "        (R0, GT3) -> LT0;\n"
00890       + "        (R1, LT0) -> {R2, R3, GT3};\n"
00891       + "        (R1, R0) -> R1;\n"
00892       + "        (R1, R1) -> R0;\n"
00893       + "        (R1, R2) -> LT0;\n"
00894       + "        (R1, R3) -> LT0;\n"
00895       + "        (R1, GT3) -> LT0;\n"
00896       + "        (R2, LT0) -> {R3, GT3};\n"
00897       + "        (R2, R0) -> R2;\n"
00898       + "        (R2, R1) -> R1;\n"
00899       + "        (R2, R2) -> R0;\n"
00900       + "        (R2, R3) -> LT0;\n"
00901       + "        (R2, GT3) -> LT0;\n"
00902       + "        (R3, LT0) -> GT3;\n"
00903       + "        (R3, R0) -> R3;\n"
00904       + "        (R3, R1) -> R2;\n"
00905       + "        (R3, R2) -> R1;\n"
00906       + "        (R3, R3) -> R0;\n"
00907       + "        (R3, GT3) -> LT0;\n"
00908       + "        (GT3, LT0) -> GT3;\n"
00909       + "        (GT3, R0) -> GT3;\n"
00910       + "        (GT3, R1) -> {R3, GT3};\n"
00911       + "        (GT3, R2) -> {R2, R3, GT3};\n"
00912       + "        (GT3, R3) -> {R1, R2, R3, GT3};\n"
00913       + "        (GT3, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
00914       + "      end\n"
00915       + "    operator * mul \n"
00916       + "      begin\n"
00917       + "        (LT0, LT0) -> {R1, R2, R3, GT3};\n"
00918       + "        (LT0, R0) -> R0;\n"
00919       + "        (LT0, R1) -> LT0;\n"
00920       + "        (LT0, R2) -> LT0;\n"
00921       + "        (LT0, R3) -> LT0;\n"
00922       + "        (LT0, GT3) -> {LT0, R1, R2, R3, GT3};\n"
00923       + "        (R0, LT0) -> R0;\n"
00924       + "        (R0, R0) -> R0;\n"
00925       + "        (R0, R1) -> R0;\n"
00926       + "        (R0, R2) -> R0;\n"
00927       + "        (R0, R3) -> R0;\n"
00928       + "        (R0, GT3) -> R0;\n"
00929       + "        (R1, LT0) -> LT0;\n"
00930       + "        (R1, R0) -> R0;\n"
00931       + "        (R1, R1) -> R1;\n"
00932       + "        (R1, R2) -> R2;\n"
00933       + "        (R1, R3) -> R3;\n"
00934       + "        (R1, GT3) -> GT3;\n"
00935       + "        (R2, LT0) -> LT0;\n"
00936       + "        (R2, R0) -> R0;\n"
00937       + "        (R2, R1) -> R2;\n"
00938       + "        (R2, R2) -> GT3;\n"
00939       + "        (R2, R3) -> GT3;\n"
00940       + "        (R2, GT3) -> GT3;\n"
00941       + "        (R3, LT0) -> LT0;\n"
00942       + "        (R3, R0) -> R0;\n"
00943       + "        (R3, R1) -> R3;\n"
00944       + "        (R3, R2) -> GT3;\n"
00945       + "        (R3, R3) -> GT3;\n"
00946       + "        (R3, GT3) -> GT3;\n"
00947       + "        (GT3, LT0) -> {LT0, R1, R2, R3, GT3};\n"
00948       + "        (GT3, R0) -> R0;\n"
00949       + "        (GT3, R1) -> GT3;\n"
00950       + "        (GT3, R2) -> GT3;\n"
00951       + "        (GT3, R3) -> GT3;\n"
00952       + "        (GT3, GT3) -> {R1, R2, R3, GT3};\n"
00953       + "      end\n"
00954       + "    operator / div \n"
00955       + "      begin\n"
00956       + "        (LT0, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
00957       + "        (LT0, R0) -> T;\n"
00958       + "        (LT0, R1) -> LT0;\n"
00959       + "        (LT0, R2) -> LT0;\n"
00960       + "        (LT0, R3) -> LT0;\n"
00961       + "        (LT0, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
00962       + "        (R0, LT0) -> R0;\n"
00963       + "        (R0, R0) -> T;\n"
00964       + "        (R0, R1) -> R0;\n"
00965       + "        (R0, R2) -> R0;\n"
00966       + "        (R0, R3) -> R0;\n"
00967       + "        (R0, GT3) -> R0;\n"
00968       + "        (R1, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
00969       + "        (R1, R0) -> T;\n"
00970       + "        (R1, R1) -> R1;\n"
00971       + "        (R1, R2) -> R0;\n"
00972       + "        (R1, R3) -> R0;\n"
00973       + "        (R1, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
00974       + "        (R2, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
00975       + "        (R2, R0) -> T;\n"
00976       + "        (R2, R1) -> R2;\n"
00977       + "        (R2, R2) -> R1;\n"
00978       + "        (R2, R3) -> R0;\n"
00979       + "        (R2, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
00980       + "        (R3, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
00981       + "        (R3, R0) -> T;\n"
00982       + "        (R3, R1) -> R3;\n"
00983       + "        (R3, R2) -> R1;\n"
00984       + "        (R3, R3) -> R1;\n"
00985       + "        (R3, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
00986       + "        (GT3, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
00987       + "        (GT3, R0) -> T;\n"
00988       + "        (GT3, R1) -> GT3;\n"
00989       + "        (GT3, R2) -> {R2, R3, GT3};\n"
00990       + "        (GT3, R3) -> {R1, R2, R3, GT3};\n"
00991       + "        (GT3, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
00992       + "      end\n"
00993       + "    operator % rem \n"
00994       + "      begin\n"
00995       + "        (LT0, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
00996       + "        (LT0, R0) -> T;\n"
00997       + "        (LT0, R1) -> R0;\n"
00998       + "        (LT0, R2) -> {R0, R1};\n"
00999       + "        (LT0, R3) -> {R0, R1, R2};\n"
01000       + "        (LT0, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
01001       + "        (R0, LT0) -> R0;\n"
01002       + "        (R0, R0) -> T;\n"
01003       + "        (R0, R1) -> R0;\n"
01004       + "        (R0, R2) -> R0;\n"
01005       + "        (R0, R3) -> R0;\n"
01006       + "        (R0, GT3) -> R0;\n"
01007       + "        (R1, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
01008       + "        (R1, R0) -> T;\n"
01009       + "        (R1, R1) -> R0;\n"
01010       + "        (R1, R2) -> R1;\n"
01011       + "        (R1, R3) -> R1;\n"
01012       + "        (R1, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
01013       + "        (R2, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
01014       + "        (R2, R0) -> T;\n"
01015       + "        (R2, R1) -> R0;\n"
01016       + "        (R2, R2) -> R0;\n"
01017       + "        (R2, R3) -> R2;\n"
01018       + "        (R2, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
01019       + "        (R3, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
01020       + "        (R3, R0) -> T;\n"
01021       + "        (R3, R1) -> R0;\n"
01022       + "        (R3, R2) -> R1;\n"
01023       + "        (R3, R3) -> R0;\n"
01024       + "        (R3, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
01025       + "        (GT3, LT0) -> {LT0, R0, R1, R2, R3, GT3};\n"
01026       + "        (GT3, R0) -> T;\n"
01027       + "        (GT3, R1) -> R0;\n"
01028       + "        (GT3, R2) -> {R0, R1};\n"
01029       + "        (GT3, R3) -> {R0, R1, R2};\n"
01030       + "        (GT3, GT3) -> {LT0, R0, R1, R2, R3, GT3};\n"
01031       + "      end\n"
01032       + "    test == eq \n"
01033       + "      begin\n"
01034       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
01035       + "        (LT0, R0) -> FALSE;\n"
01036       + "        (LT0, R1) -> FALSE;\n"
01037       + "        (LT0, R2) -> FALSE;\n"
01038       + "        (LT0, R3) -> FALSE;\n"
01039       + "        (LT0, GT3) -> FALSE;\n"
01040       + "        (R0, LT0) -> FALSE;\n"
01041       + "        (R0, R0) -> TRUE;\n"
01042       + "        (R0, R1) -> FALSE;\n"
01043       + "        (R0, R2) -> FALSE;\n"
01044       + "        (R0, R3) -> FALSE;\n"
01045       + "        (R0, GT3) -> FALSE;\n"
01046       + "        (R1, LT0) -> FALSE;\n"
01047       + "        (R1, R0) -> FALSE;\n"
01048       + "        (R1, R1) -> TRUE;\n"
01049       + "        (R1, R2) -> FALSE;\n"
01050       + "        (R1, R3) -> FALSE;\n"
01051       + "        (R1, GT3) -> FALSE;\n"
01052       + "        (R2, LT0) -> FALSE;\n"
01053       + "        (R2, R0) -> FALSE;\n"
01054       + "        (R2, R1) -> FALSE;\n"
01055       + "        (R2, R2) -> TRUE;\n"
01056       + "        (R2, R3) -> FALSE;\n"
01057       + "        (R2, GT3) -> FALSE;\n"
01058       + "        (R3, LT0) -> FALSE;\n"
01059       + "        (R3, R0) -> FALSE;\n"
01060       + "        (R3, R1) -> FALSE;\n"
01061       + "        (R3, R2) -> FALSE;\n"
01062       + "        (R3, R3) -> TRUE;\n"
01063       + "        (R3, GT3) -> FALSE;\n"
01064       + "        (GT3, LT0) -> FALSE;\n"
01065       + "        (GT3, R0) -> FALSE;\n"
01066       + "        (GT3, R1) -> FALSE;\n"
01067       + "        (GT3, R2) -> FALSE;\n"
01068       + "        (GT3, R3) -> FALSE;\n"
01069       + "        (GT3, GT3) -> {TRUE, FALSE};\n"
01070       + "      end\n"
01071       + "    test != neq \n"
01072       + "      begin\n"
01073       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
01074       + "        (LT0, R0) -> TRUE;\n"
01075       + "        (LT0, R1) -> TRUE;\n"
01076       + "        (LT0, R2) -> TRUE;\n"
01077       + "        (LT0, R3) -> TRUE;\n"
01078       + "        (LT0, GT3) -> TRUE;\n"
01079       + "        (R0, LT0) -> TRUE;\n"
01080       + "        (R0, R0) -> FALSE;\n"
01081       + "        (R0, R1) -> TRUE;\n"
01082       + "        (R0, R2) -> TRUE;\n"
01083       + "        (R0, R3) -> TRUE;\n"
01084       + "        (R0, GT3) -> TRUE;\n"
01085       + "        (R1, LT0) -> TRUE;\n"
01086       + "        (R1, R0) -> TRUE;\n"
01087       + "        (R1, R1) -> FALSE;\n"
01088       + "        (R1, R2) -> TRUE;\n"
01089       + "        (R1, R3) -> TRUE;\n"
01090       + "        (R1, GT3) -> TRUE;\n"
01091       + "        (R2, LT0) -> TRUE;\n"
01092       + "        (R2, R0) -> TRUE;\n"
01093       + "        (R2, R1) -> TRUE;\n"
01094       + "        (R2, R2) -> FALSE;\n"
01095       + "        (R2, R3) -> TRUE;\n"
01096       + "        (R2, GT3) -> TRUE;\n"
01097       + "        (R3, LT0) -> TRUE;\n"
01098       + "        (R3, R0) -> TRUE;\n"
01099       + "        (R3, R1) -> TRUE;\n"
01100       + "        (R3, R2) -> TRUE;\n"
01101       + "        (R3, R3) -> FALSE;\n"
01102       + "        (R3, GT3) -> TRUE;\n"
01103       + "        (GT3, LT0) -> TRUE;\n"
01104       + "        (GT3, R0) -> TRUE;\n"
01105       + "        (GT3, R1) -> TRUE;\n"
01106       + "        (GT3, R2) -> TRUE;\n"
01107       + "        (GT3, R3) -> TRUE;\n"
01108       + "        (GT3, GT3) -> {TRUE, FALSE};\n"
01109       + "      end\n"
01110       + "    test < lt \n"
01111       + "      begin\n"
01112       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
01113       + "        (LT0, R0) -> TRUE;\n"
01114       + "        (LT0, R1) -> TRUE;\n"
01115       + "        (LT0, R2) -> TRUE;\n"
01116       + "        (LT0, R3) -> TRUE;\n"
01117       + "        (LT0, GT3) -> TRUE;\n"
01118       + "        (R0, LT0) -> FALSE;\n"
01119       + "        (R0, R0) -> FALSE;\n"
01120       + "        (R0, R1) -> TRUE;\n"
01121       + "        (R0, R2) -> TRUE;\n"
01122       + "        (R0, R3) -> TRUE;\n"
01123       + "        (R0, GT3) -> TRUE;\n"
01124       + "        (R1, LT0) -> FALSE;\n"
01125       + "        (R1, R0) -> FALSE;\n"
01126       + "        (R1, R1) -> FALSE;\n"
01127       + "        (R1, R2) -> TRUE;\n"
01128       + "        (R1, R3) -> TRUE;\n"
01129       + "        (R1, GT3) -> TRUE;\n"
01130       + "        (R2, LT0) -> FALSE;\n"
01131       + "        (R2, R0) -> FALSE;\n"
01132       + "        (R2, R1) -> FALSE;\n"
01133       + "        (R2, R2) -> FALSE;\n"
01134       + "        (R2, R3) -> TRUE;\n"
01135       + "        (R2, GT3) -> TRUE;\n"
01136       + "        (R3, LT0) -> FALSE;\n"
01137       + "        (R3, R0) -> FALSE;\n"
01138       + "        (R3, R1) -> FALSE;\n"
01139       + "        (R3, R2) -> FALSE;\n"
01140       + "        (R3, R3) -> FALSE;\n"
01141       + "        (R3, GT3) -> TRUE;\n"
01142       + "        (GT3, LT0) -> FALSE;\n"
01143       + "        (GT3, R0) -> FALSE;\n"
01144       + "        (GT3, R1) -> FALSE;\n"
01145       + "        (GT3, R2) -> FALSE;\n"
01146       + "        (GT3, R3) -> FALSE;\n"
01147       + "        (GT3, GT3) -> {TRUE, FALSE};\n"
01148       + "      end\n"
01149       + "    test <= le \n"
01150       + "      begin\n"
01151       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
01152       + "        (LT0, R0) -> TRUE;\n"
01153       + "        (LT0, R1) -> TRUE;\n"
01154       + "        (LT0, R2) -> TRUE;\n"
01155       + "        (LT0, R3) -> TRUE;\n"
01156       + "        (LT0, GT3) -> TRUE;\n"
01157       + "        (R0, LT0) -> FALSE;\n"
01158       + "        (R0, R0) -> TRUE;\n"
01159       + "        (R0, R1) -> TRUE;\n"
01160       + "        (R0, R2) -> TRUE;\n"
01161       + "        (R0, R3) -> TRUE;\n"
01162       + "        (R0, GT3) -> TRUE;\n"
01163       + "        (R1, LT0) -> FALSE;\n"
01164       + "        (R1, R0) -> FALSE;\n"
01165       + "        (R1, R1) -> TRUE;\n"
01166       + "        (R1, R2) -> TRUE;\n"
01167       + "        (R1, R3) -> TRUE;\n"
01168       + "        (R1, GT3) -> TRUE;\n"
01169       + "        (R2, LT0) -> FALSE;\n"
01170       + "        (R2, R0) -> FALSE;\n"
01171       + "        (R2, R1) -> FALSE;\n"
01172       + "        (R2, R2) -> TRUE;\n"
01173       + "        (R2, R3) -> TRUE;\n"
01174       + "        (R2, GT3) -> TRUE;\n"
01175       + "        (R3, LT0) -> FALSE;\n"
01176       + "        (R3, R0) -> FALSE;\n"
01177       + "        (R3, R1) -> FALSE;\n"
01178       + "        (R3, R2) -> FALSE;\n"
01179       + "        (R3, R3) -> TRUE;\n"
01180       + "        (R3, GT3) -> TRUE;\n"
01181       + "        (GT3, LT0) -> FALSE;\n"
01182       + "        (GT3, R0) -> FALSE;\n"
01183       + "        (GT3, R1) -> FALSE;\n"
01184       + "        (GT3, R2) -> FALSE;\n"
01185       + "        (GT3, R3) -> FALSE;\n"
01186       + "        (GT3, GT3) -> {TRUE, FALSE};\n"
01187       + "      end\n"
01188       + "    test > gt \n"
01189       + "      begin\n"
01190       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
01191       + "        (LT0, R0) -> FALSE;\n"
01192       + "        (LT0, R1) -> FALSE;\n"
01193       + "        (LT0, R2) -> FALSE;\n"
01194       + "        (LT0, R3) -> FALSE;\n"
01195       + "        (LT0, GT3) -> FALSE;\n"
01196       + "        (R0, LT0) -> TRUE;\n"
01197       + "        (R0, R0) -> FALSE;\n"
01198       + "        (R0, R1) -> FALSE;\n"
01199       + "        (R0, R2) -> FALSE;\n"
01200       + "        (R0, R3) -> FALSE;\n"
01201       + "        (R0, GT3) -> FALSE;\n"
01202       + "        (R1, LT0) -> TRUE;\n"
01203       + "        (R1, R0) -> TRUE;\n"
01204       + "        (R1, R1) -> FALSE;\n"
01205       + "        (R1, R2) -> FALSE;\n"
01206       + "        (R1, R3) -> FALSE;\n"
01207       + "        (R1, GT3) -> FALSE;\n"
01208       + "        (R2, LT0) -> TRUE;\n"
01209       + "        (R2, R0) -> TRUE;\n"
01210       + "        (R2, R1) -> TRUE;\n"
01211       + "        (R2, R2) -> FALSE;\n"
01212       + "        (R2, R3) -> FALSE;\n"
01213       + "        (R2, GT3) -> FALSE;\n"
01214       + "        (R3, LT0) -> TRUE;\n"
01215       + "        (R3, R0) -> TRUE;\n"
01216       + "        (R3, R1) -> TRUE;\n"
01217       + "        (R3, R2) -> TRUE;\n"
01218       + "        (R3, R3) -> FALSE;\n"
01219       + "        (R3, GT3) -> FALSE;\n"
01220       + "        (GT3, LT0) -> TRUE;\n"
01221       + "        (GT3, R0) -> TRUE;\n"
01222       + "        (GT3, R1) -> TRUE;\n"
01223       + "        (GT3, R2) -> TRUE;\n"
01224       + "        (GT3, R3) -> TRUE;\n"
01225       + "        (GT3, GT3) -> {TRUE, FALSE};\n"
01226       + "      end\n"
01227       + "    test >= ge \n"
01228       + "      begin\n"
01229       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
01230       + "        (LT0, R0) -> FALSE;\n"
01231       + "        (LT0, R1) -> FALSE;\n"
01232       + "        (LT0, R2) -> FALSE;\n"
01233       + "        (LT0, R3) -> FALSE;\n"
01234       + "        (LT0, GT3) -> FALSE;\n"
01235       + "        (R0, LT0) -> TRUE;\n"
01236       + "        (R0, R0) -> TRUE;\n"
01237       + "        (R0, R1) -> FALSE;\n"
01238       + "        (R0, R2) -> FALSE;\n"
01239       + "        (R0, R3) -> FALSE;\n"
01240       + "        (R0, GT3) -> FALSE;\n"
01241       + "        (R1, LT0) -> TRUE;\n"
01242       + "        (R1, R0) -> TRUE;\n"
01243       + "        (R1, R1) -> TRUE;\n"
01244       + "        (R1, R2) -> FALSE;\n"
01245       + "        (R1, R3) -> FALSE;\n"
01246       + "        (R1, GT3) -> FALSE;\n"
01247       + "        (R2, LT0) -> TRUE;\n"
01248       + "        (R2, R0) -> TRUE;\n"
01249       + "        (R2, R1) -> TRUE;\n"
01250       + "        (R2, R2) -> TRUE;\n"
01251       + "        (R2, R3) -> FALSE;\n"
01252       + "        (R2, GT3) -> FALSE;\n"
01253       + "        (R3, LT0) -> TRUE;\n"
01254       + "        (R3, R0) -> TRUE;\n"
01255       + "        (R3, R1) -> TRUE;\n"
01256       + "        (R3, R2) -> TRUE;\n"
01257       + "        (R3, R3) -> TRUE;\n"
01258       + "        (R3, GT3) -> FALSE;\n"
01259       + "        (GT3, LT0) -> TRUE;\n"
01260       + "        (GT3, R0) -> TRUE;\n"
01261       + "        (GT3, R1) -> TRUE;\n"
01262       + "        (GT3, R2) -> TRUE;\n"
01263       + "        (GT3, R3) -> TRUE;\n"
01264       + "        (GT3, GT3) -> {TRUE, FALSE};\n"
01265       + "      end\n"
01266       + "  end\n"
01267     ;
01268   }  
01269   public static String getName() {
01270     return "Range03";
01271   }  
01272   public static int getNumOfTokens() {
01273     return 6;
01274   }  
01275   public static String getToken(int value) {
01276     switch(value) {
01277       case R0: return "Range03.R0";
01278       case LT0: return "Range03.LT0";
01279       case R1: return "Range03.R1";
01280       case R2: return "Range03.R2";
01281       case R3: return "Range03.R3";
01282       case GT3: return "Range03.GT3";
01283     }
01284     return "Range03.???";
01285   }  
01286   public static boolean gt(int left$, int right$) {
01287     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
01288     if (left$ == LT0 && right$ == R0) return false;
01289     if (left$ == LT0 && right$ == R1) return false;
01290     if (left$ == LT0 && right$ == R2) return false;
01291     if (left$ == LT0 && right$ == R3) return false;
01292     if (left$ == LT0 && right$ == GT3) return false;
01293     if (left$ == R0 && right$ == LT0) return true;
01294     if (left$ == R0 && right$ == R0) return false;
01295     if (left$ == R0 && right$ == R1) return false;
01296     if (left$ == R0 && right$ == R2) return false;
01297     if (left$ == R0 && right$ == R3) return false;
01298     if (left$ == R0 && right$ == GT3) return false;
01299     if (left$ == R1 && right$ == LT0) return true;
01300     if (left$ == R1 && right$ == R0) return true;
01301     if (left$ == R1 && right$ == R1) return false;
01302     if (left$ == R1 && right$ == R2) return false;
01303     if (left$ == R1 && right$ == R3) return false;
01304     if (left$ == R1 && right$ == GT3) return false;
01305     if (left$ == R2 && right$ == LT0) return true;
01306     if (left$ == R2 && right$ == R0) return true;
01307     if (left$ == R2 && right$ == R1) return true;
01308     if (left$ == R2 && right$ == R2) return false;
01309     if (left$ == R2 && right$ == R3) return false;
01310     if (left$ == R2 && right$ == GT3) return false;
01311     if (left$ == R3 && right$ == LT0) return true;
01312     if (left$ == R3 && right$ == R0) return true;
01313     if (left$ == R3 && right$ == R1) return true;
01314     if (left$ == R3 && right$ == R2) return true;
01315     if (left$ == R3 && right$ == R3) return false;
01316     if (left$ == R3 && right$ == GT3) return false;
01317     if (left$ == GT3 && right$ == LT0) return true;
01318     if (left$ == GT3 && right$ == R0) return true;
01319     if (left$ == GT3 && right$ == R1) return true;
01320     if (left$ == GT3 && right$ == R2) return true;
01321     if (left$ == GT3 && right$ == R3) return true;
01322     if (left$ == GT3 && right$ == GT3) return Abstraction.choose();
01323     throw new RuntimeException("Range03.gt(" + left$ + ", " + right$ + ") is undefined");
01324   }  
01325   private static byte gtNoChoose(int left, int right) {
01326     byte result = -1;
01327     switch (left) {
01328       case 0:
01329         switch (right) {
01330           case 0:
01331             result = 0;
01332             break;
01333           case 1:
01334             result = 1;
01335             break;
01336           case 2:
01337             result = 0;
01338             break;
01339           case 3:
01340             result = 0;
01341             break;
01342           case 4:
01343             result = 0;
01344             break;
01345           case 5:
01346             result = 0;
01347             break;
01348         }
01349         break;
01350       case 1:
01351         switch (right) {
01352           case 0:
01353             result = 0;
01354             break;
01355           case 1:
01356             result = 2;
01357             break;
01358           case 2:
01359             result = 0;
01360             break;
01361           case 3:
01362             result = 0;
01363             break;
01364           case 4:
01365             result = 0;
01366             break;
01367           case 5:
01368             result = 0;
01369             break;
01370         }
01371         break;
01372       case 2:
01373         switch (right) {
01374           case 0:
01375             result = 1;
01376             break;
01377           case 1:
01378             result = 1;
01379             break;
01380           case 2:
01381             result = 0;
01382             break;
01383           case 3:
01384             result = 0;
01385             break;
01386           case 4:
01387             result = 0;
01388             break;
01389           case 5:
01390             result = 0;
01391             break;
01392         }
01393         break;
01394       case 3:
01395         switch (right) {
01396           case 0:
01397             result = 1;
01398             break;
01399           case 1:
01400             result = 1;
01401             break;
01402           case 2:
01403             result = 1;
01404             break;
01405           case 3:
01406             result = 0;
01407             break;
01408           case 4:
01409             result = 0;
01410             break;
01411           case 5:
01412             result = 0;
01413             break;
01414         }
01415         break;
01416       case 4:
01417         switch (right) {
01418           case 0:
01419             result = 1;
01420             break;
01421           case 1:
01422             result = 1;
01423             break;
01424           case 2:
01425             result = 1;
01426             break;
01427           case 3:
01428             result = 1;
01429             break;
01430           case 4:
01431             result = 0;
01432             break;
01433           case 5:
01434             result = 0;
01435             break;
01436         }
01437         break;
01438       case 5:
01439         switch (right) {
01440           case 0:
01441             result = 1;
01442             break;
01443           case 1:
01444             result = 1;
01445             break;
01446           case 2:
01447             result = 1;
01448             break;
01449           case 3:
01450             result = 1;
01451             break;
01452           case 4:
01453             result = 1;
01454             break;
01455           case 5:
01456             result = 2;
01457             break;
01458         }
01459         break;
01460     }
01461     if (result == -1) throw new RuntimeException("Range03.gtNoChoose(" + left + ", " + right + ") is undefined");
01462     return result;
01463   }  
01464   public static byte gtSet(int leftTokens, int rightTokens) {
01465     byte result = -1;
01466     for (int left = 0; (1 << left) <= leftTokens; left++) {
01467       if ((leftTokens & (1 << left)) == 0) continue;
01468       for (int right = 0; (1 << right) <= rightTokens; right++) {
01469         if ((rightTokens & (1 << right)) != 0) {
01470           if (result == -1) result = gtNoChoose(left, right);
01471           else result = Abstraction.meetTest(result, gtNoChoose(left, right));
01472         }
01473       }
01474     }
01475     return result;
01476   }  
01477   public static boolean isOne2One(int value) {
01478     switch(value) {
01479       case R3: return true;
01480       case R2: return true;
01481       case R1: return true;
01482       case R0: return true;
01483     }
01484     return false;
01485   }  
01486   public static boolean le(int left$, int right$) {
01487     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
01488     if (left$ == LT0 && right$ == R0) return true;
01489     if (left$ == LT0 && right$ == R1) return true;
01490     if (left$ == LT0 && right$ == R2) return true;
01491     if (left$ == LT0 && right$ == R3) return true;
01492     if (left$ == LT0 && right$ == GT3) return true;
01493     if (left$ == R0 && right$ == LT0) return false;
01494     if (left$ == R0 && right$ == R0) return true;
01495     if (left$ == R0 && right$ == R1) return true;
01496     if (left$ == R0 && right$ == R2) return true;
01497     if (left$ == R0 && right$ == R3) return true;
01498     if (left$ == R0 && right$ == GT3) return true;
01499     if (left$ == R1 && right$ == LT0) return false;
01500     if (left$ == R1 && right$ == R0) return false;
01501     if (left$ == R1 && right$ == R1) return true;
01502     if (left$ == R1 && right$ == R2) return true;
01503     if (left$ == R1 && right$ == R3) return true;
01504     if (left$ == R1 && right$ == GT3) return true;
01505     if (left$ == R2 && right$ == LT0) return false;
01506     if (left$ == R2 && right$ == R0) return false;
01507     if (left$ == R2 && right$ == R1) return false;
01508     if (left$ == R2 && right$ == R2) return true;
01509     if (left$ == R2 && right$ == R3) return true;
01510     if (left$ == R2 && right$ == GT3) return true;
01511     if (left$ == R3 && right$ == LT0) return false;
01512     if (left$ == R3 && right$ == R0) return false;
01513     if (left$ == R3 && right$ == R1) return false;
01514     if (left$ == R3 && right$ == R2) return false;
01515     if (left$ == R3 && right$ == R3) return true;
01516     if (left$ == R3 && right$ == GT3) return true;
01517     if (left$ == GT3 && right$ == LT0) return false;
01518     if (left$ == GT3 && right$ == R0) return false;
01519     if (left$ == GT3 && right$ == R1) return false;
01520     if (left$ == GT3 && right$ == R2) return false;
01521     if (left$ == GT3 && right$ == R3) return false;
01522     if (left$ == GT3 && right$ == GT3) return Abstraction.choose();
01523     throw new RuntimeException("Range03.le(" + left$ + ", " + right$ + ") is undefined");
01524   }  
01525   private static byte leNoChoose(int left, int right) {
01526     byte result = -1;
01527     switch (left) {
01528       case 0:
01529         switch (right) {
01530           case 0:
01531             result = 1;
01532             break;
01533           case 1:
01534             result = 0;
01535             break;
01536           case 2:
01537             result = 1;
01538             break;
01539           case 3:
01540             result = 1;
01541             break;
01542           case 4:
01543             result = 1;
01544             break;
01545           case 5:
01546             result = 1;
01547             break;
01548         }
01549         break;
01550       case 1:
01551         switch (right) {
01552           case 0:
01553             result = 1;
01554             break;
01555           case 1:
01556             result = 2;
01557             break;
01558           case 2:
01559             result = 1;
01560             break;
01561           case 3:
01562             result = 1;
01563             break;
01564           case 4:
01565             result = 1;
01566             break;
01567           case 5:
01568             result = 1;
01569             break;
01570         }
01571         break;
01572       case 2:
01573         switch (right) {
01574           case 0:
01575             result = 0;
01576             break;
01577           case 1:
01578             result = 0;
01579             break;
01580           case 2:
01581             result = 1;
01582             break;
01583           case 3:
01584             result = 1;
01585             break;
01586           case 4:
01587             result = 1;
01588             break;
01589           case 5:
01590             result = 1;
01591             break;
01592         }
01593         break;
01594       case 3:
01595         switch (right) {
01596           case 0:
01597             result = 0;
01598             break;
01599           case 1:
01600             result = 0;
01601             break;
01602           case 2:
01603             result = 0;
01604             break;
01605           case 3:
01606             result = 1;
01607             break;
01608           case 4:
01609             result = 1;
01610             break;
01611           case 5:
01612             result = 1;
01613             break;
01614         }
01615         break;
01616       case 4:
01617         switch (right) {
01618           case 0:
01619             result = 0;
01620             break;
01621           case 1:
01622             result = 0;
01623             break;
01624           case 2:
01625             result = 0;
01626             break;
01627           case 3:
01628             result = 0;
01629             break;
01630           case 4:
01631             result = 1;
01632             break;
01633           case 5:
01634             result = 1;
01635             break;
01636         }
01637         break;
01638       case 5:
01639         switch (right) {
01640           case 0:
01641             result = 0;
01642             break;
01643           case 1:
01644             result = 0;
01645             break;
01646           case 2:
01647             result = 0;
01648             break;
01649           case 3:
01650             result = 0;
01651             break;
01652           case 4:
01653             result = 0;
01654             break;
01655           case 5:
01656             result = 2;
01657             break;
01658         }
01659         break;
01660     }
01661     if (result == -1) throw new RuntimeException("Range03.leNoChoose(" + left + ", " + right + ") is undefined");
01662     return result;
01663   }  
01664   public static byte leSet(int leftTokens, int rightTokens) {
01665     byte result = -1;
01666     for (int left = 0; (1 << left) <= leftTokens; left++) {
01667       if ((leftTokens & (1 << left)) == 0) continue;
01668       for (int right = 0; (1 << right) <= rightTokens; right++) {
01669         if ((rightTokens & (1 << right)) != 0) {
01670           if (result == -1) result = leNoChoose(left, right);
01671           else result = Abstraction.meetTest(result, leNoChoose(left, right));
01672         }
01673       }
01674     }
01675     return result;
01676   }  
01677   public static boolean lt(int left$, int right$) {
01678     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
01679     if (left$ == LT0 && right$ == R0) return true;
01680     if (left$ == LT0 && right$ == R1) return true;
01681     if (left$ == LT0 && right$ == R2) return true;
01682     if (left$ == LT0 && right$ == R3) return true;
01683     if (left$ == LT0 && right$ == GT3) return true;
01684     if (left$ == R0 && right$ == LT0) return false;
01685     if (left$ == R0 && right$ == R0) return false;
01686     if (left$ == R0 && right$ == R1) return true;
01687     if (left$ == R0 && right$ == R2) return true;
01688     if (left$ == R0 && right$ == R3) return true;
01689     if (left$ == R0 && right$ == GT3) return true;
01690     if (left$ == R1 && right$ == LT0) return false;
01691     if (left$ == R1 && right$ == R0) return false;
01692     if (left$ == R1 && right$ == R1) return false;
01693     if (left$ == R1 && right$ == R2) return true;
01694     if (left$ == R1 && right$ == R3) return true;
01695     if (left$ == R1 && right$ == GT3) return true;
01696     if (left$ == R2 && right$ == LT0) return false;
01697     if (left$ == R2 && right$ == R0) return false;
01698     if (left$ == R2 && right$ == R1) return false;
01699     if (left$ == R2 && right$ == R2) return false;
01700     if (left$ == R2 && right$ == R3) return true;
01701     if (left$ == R2 && right$ == GT3) return true;
01702     if (left$ == R3 && right$ == LT0) return false;
01703     if (left$ == R3 && right$ == R0) return false;
01704     if (left$ == R3 && right$ == R1) return false;
01705     if (left$ == R3 && right$ == R2) return false;
01706     if (left$ == R3 && right$ == R3) return false;
01707     if (left$ == R3 && right$ == GT3) return true;
01708     if (left$ == GT3 && right$ == LT0) return false;
01709     if (left$ == GT3 && right$ == R0) return false;
01710     if (left$ == GT3 && right$ == R1) return false;
01711     if (left$ == GT3 && right$ == R2) return false;
01712     if (left$ == GT3 && right$ == R3) return false;
01713     if (left$ == GT3 && right$ == GT3) return Abstraction.choose();
01714     throw new RuntimeException("Range03.lt(" + left$ + ", " + right$ + ") is undefined");
01715   }  
01716   private static byte ltNoChoose(int left, int right) {
01717     byte result = -1;
01718     switch (left) {
01719       case 0:
01720         switch (right) {
01721           case 0:
01722             result = 0;
01723             break;
01724           case 1:
01725             result = 0;
01726             break;
01727           case 2:
01728             result = 1;
01729             break;
01730           case 3:
01731             result = 1;
01732             break;
01733           case 4:
01734             result = 1;
01735             break;
01736           case 5:
01737             result = 1;
01738             break;
01739         }
01740         break;
01741       case 1:
01742         switch (right) {
01743           case 0:
01744             result = 1;
01745             break;
01746           case 1:
01747             result = 2;
01748             break;
01749           case 2:
01750             result = 1;
01751             break;
01752           case 3:
01753             result = 1;
01754             break;
01755           case 4:
01756             result = 1;
01757             break;
01758           case 5:
01759             result = 1;
01760             break;
01761         }
01762         break;
01763       case 2:
01764         switch (right) {
01765           case 0:
01766             result = 0;
01767             break;
01768           case 1:
01769             result = 0;
01770             break;
01771           case 2:
01772             result = 0;
01773             break;
01774           case 3:
01775             result = 1;
01776             break;
01777           case 4:
01778             result = 1;
01779             break;
01780           case 5:
01781             result = 1;
01782             break;
01783         }
01784         break;
01785       case 3:
01786         switch (right) {
01787           case 0:
01788             result = 0;
01789             break;
01790           case 1:
01791             result = 0;
01792             break;
01793           case 2:
01794             result = 0;
01795             break;
01796           case 3:
01797             result = 0;
01798             break;
01799           case 4:
01800             result = 1;
01801             break;
01802           case 5:
01803             result = 1;
01804             break;
01805         }
01806         break;
01807       case 4:
01808         switch (right) {
01809           case 0:
01810             result = 0;
01811             break;
01812           case 1:
01813             result = 0;
01814             break;
01815           case 2:
01816             result = 0;
01817             break;
01818           case 3:
01819             result = 0;
01820             break;
01821           case 4:
01822             result = 0;
01823             break;
01824           case 5:
01825             result = 1;
01826             break;
01827         }
01828         break;
01829       case 5:
01830         switch (right) {
01831           case 0:
01832             result = 0;
01833             break;
01834           case 1:
01835             result = 0;
01836             break;
01837           case 2:
01838             result = 0;
01839             break;
01840           case 3:
01841             result = 0;
01842             break;
01843           case 4:
01844             result = 0;
01845             break;
01846           case 5:
01847             result = 2;
01848             break;
01849         }
01850         break;
01851     }
01852     if (result == -1) throw new RuntimeException("Range03.ltNoChoose(" + left + ", " + right + ") is undefined");
01853     return result;
01854   }  
01855   public static byte ltSet(int leftTokens, int rightTokens) {
01856     byte result = -1;
01857     for (int left = 0; (1 << left) <= leftTokens; left++) {
01858       if ((leftTokens & (1 << left)) == 0) continue;
01859       for (int right = 0; (1 << right) <= rightTokens; right++) {
01860         if ((rightTokens & (1 << right)) != 0) {
01861           if (result == -1) result = ltNoChoose(left, right);
01862           else result = Abstraction.meetTest(result, ltNoChoose(left, right));
01863         }
01864       }
01865     }
01866     return result;
01867   }  
01868   public static int mul(int left$, int right$) {
01869     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1));
01870     if (left$ == LT0 && right$ == R0) return R0;
01871     if (left$ == LT0 && right$ == R1) return LT0;
01872     if (left$ == LT0 && right$ == R2) return LT0;
01873     if (left$ == LT0 && right$ == R3) return LT0;
01874     if (left$ == LT0 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << LT0));
01875     if (left$ == R0 && right$ == LT0) return R0;
01876     if (left$ == R0 && right$ == R0) return R0;
01877     if (left$ == R0 && right$ == R1) return R0;
01878     if (left$ == R0 && right$ == R2) return R0;
01879     if (left$ == R0 && right$ == R3) return R0;
01880     if (left$ == R0 && right$ == GT3) return R0;
01881     if (left$ == R1 && right$ == LT0) return LT0;
01882     if (left$ == R1 && right$ == R0) return R0;
01883     if (left$ == R1 && right$ == R1) return R1;
01884     if (left$ == R1 && right$ == R2) return R2;
01885     if (left$ == R1 && right$ == R3) return R3;
01886     if (left$ == R1 && right$ == GT3) return GT3;
01887     if (left$ == R2 && right$ == LT0) return LT0;
01888     if (left$ == R2 && right$ == R0) return R0;
01889     if (left$ == R2 && right$ == R1) return R2;
01890     if (left$ == R2 && right$ == R2) return GT3;
01891     if (left$ == R2 && right$ == R3) return GT3;
01892     if (left$ == R2 && right$ == GT3) return GT3;
01893     if (left$ == R3 && right$ == LT0) return LT0;
01894     if (left$ == R3 && right$ == R0) return R0;
01895     if (left$ == R3 && right$ == R1) return R3;
01896     if (left$ == R3 && right$ == R2) return GT3;
01897     if (left$ == R3 && right$ == R3) return GT3;
01898     if (left$ == R3 && right$ == GT3) return GT3;
01899     if (left$ == GT3 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << LT0));
01900     if (left$ == GT3 && right$ == R0) return R0;
01901     if (left$ == GT3 && right$ == R1) return GT3;
01902     if (left$ == GT3 && right$ == R2) return GT3;
01903     if (left$ == GT3 && right$ == R3) return GT3;
01904     if (left$ == GT3 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1));
01905     throw new RuntimeException("Range03.mul(" + left$ + ", " + right$ + ") is undefined");
01906   }  
01907   private static int mulNoChoose(int left, int right) {
01908     int result = 0;
01909     switch (left) {
01910       case 0:
01911         switch (right) {
01912           case 0:
01913             result = 1;
01914             break;
01915           case 1:
01916             result = 1;
01917             break;
01918           case 2:
01919             result = 1;
01920             break;
01921           case 3:
01922             result = 1;
01923             break;
01924           case 4:
01925             result = 1;
01926             break;
01927           case 5:
01928             result = 1;
01929             break;
01930         }
01931         break;
01932       case 1:
01933         switch (right) {
01934           case 0:
01935             result = 1;
01936             break;
01937           case 1:
01938             result = 60;
01939             break;
01940           case 2:
01941             result = 2;
01942             break;
01943           case 3:
01944             result = 2;
01945             break;
01946           case 4:
01947             result = 2;
01948             break;
01949           case 5:
01950             result = 62;
01951             break;
01952         }
01953         break;
01954       case 2:
01955         switch (right) {
01956           case 0:
01957             result = 1;
01958             break;
01959           case 1:
01960             result = 2;
01961             break;
01962           case 2:
01963             result = 4;
01964             break;
01965           case 3:
01966             result = 8;
01967             break;
01968           case 4:
01969             result = 16;
01970             break;
01971           case 5:
01972             result = 32;
01973             break;
01974         }
01975         break;
01976       case 3:
01977         switch (right) {
01978           case 0:
01979             result = 1;
01980             break;
01981           case 1:
01982             result = 2;
01983             break;
01984           case 2:
01985             result = 8;
01986             break;
01987           case 3:
01988             result = 32;
01989             break;
01990           case 4:
01991             result = 32;
01992             break;
01993           case 5:
01994             result = 32;
01995             break;
01996         }
01997         break;
01998       case 4:
01999         switch (right) {
02000           case 0:
02001             result = 1;
02002             break;
02003           case 1:
02004             result = 2;
02005             break;
02006           case 2:
02007             result = 16;
02008             break;
02009           case 3:
02010             result = 32;
02011             break;
02012           case 4:
02013             result = 32;
02014             break;
02015           case 5:
02016             result = 32;
02017             break;
02018         }
02019         break;
02020       case 5:
02021         switch (right) {
02022           case 0:
02023             result = 1;
02024             break;
02025           case 1:
02026             result = 62;
02027             break;
02028           case 2:
02029             result = 32;
02030             break;
02031           case 3:
02032             result = 32;
02033             break;
02034           case 4:
02035             result = 32;
02036             break;
02037           case 5:
02038             result = 60;
02039             break;
02040         }
02041         break;
02042     }
02043     if (result == 0) throw new RuntimeException("Range03.mulNoChoose(" + left + ", " + right + ") is undefined");
02044     return result;
02045   }  
02046   public static int mulSet(int leftTokens, int rightTokens) {
02047     int result = -1;
02048     for (int left = 0; (1 << left) <= leftTokens; left++) {
02049       if ((leftTokens & (1 << left)) == 0) continue;
02050       for (int right = 0; (1 << right) <= rightTokens; right++) {
02051         if ((rightTokens & (1 << right)) != 0) {
02052           if (result == -1) result = mulNoChoose(left, right);
02053           else result = Abstraction.meetArith(result, mulNoChoose(left, right));
02054         }
02055       }
02056     }
02057     return result;
02058   }  
02059   public static boolean ne(int left$, int right$) {
02060     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
02061     if (left$ == LT0 && right$ == R0) return true;
02062     if (left$ == LT0 && right$ == R1) return true;
02063     if (left$ == LT0 && right$ == R2) return true;
02064     if (left$ == LT0 && right$ == R3) return true;
02065     if (left$ == LT0 && right$ == GT3) return true;
02066     if (left$ == R0 && right$ == LT0) return true;
02067     if (left$ == R0 && right$ == R0) return false;
02068     if (left$ == R0 && right$ == R1) return true;
02069     if (left$ == R0 && right$ == R2) return true;
02070     if (left$ == R0 && right$ == R3) return true;
02071     if (left$ == R0 && right$ == GT3) return true;
02072     if (left$ == R1 && right$ == LT0) return true;
02073     if (left$ == R1 && right$ == R0) return true;
02074     if (left$ == R1 && right$ == R1) return false;
02075     if (left$ == R1 && right$ == R2) return true;
02076     if (left$ == R1 && right$ == R3) return true;
02077     if (left$ == R1 && right$ == GT3) return true;
02078     if (left$ == R2 && right$ == LT0) return true;
02079     if (left$ == R2 && right$ == R0) return true;
02080     if (left$ == R2 && right$ == R1) return true;
02081     if (left$ == R2 && right$ == R2) return false;
02082     if (left$ == R2 && right$ == R3) return true;
02083     if (left$ == R2 && right$ == GT3) return true;
02084     if (left$ == R3 && right$ == LT0) return true;
02085     if (left$ == R3 && right$ == R0) return true;
02086     if (left$ == R3 && right$ == R1) return true;
02087     if (left$ == R3 && right$ == R2) return true;
02088     if (left$ == R3 && right$ == R3) return false;
02089     if (left$ == R3 && right$ == GT3) return true;
02090     if (left$ == GT3 && right$ == LT0) return true;
02091     if (left$ == GT3 && right$ == R0) return true;
02092     if (left$ == GT3 && right$ == R1) return true;
02093     if (left$ == GT3 && right$ == R2) return true;
02094     if (left$ == GT3 && right$ == R3) return true;
02095     if (left$ == GT3 && right$ == GT3) return Abstraction.choose();
02096     throw new RuntimeException("Range03.ne(" + left$ + ", " + right$ + ") is undefined");
02097   }  
02098   private static byte neNoChoose(int left, int right) {
02099     byte result = -1;
02100     switch (left) {
02101       case 0:
02102         switch (right) {
02103           case 0:
02104             result = 0;
02105             break;
02106           case 1:
02107             result = 1;
02108             break;
02109           case 2:
02110             result = 1;
02111             break;
02112           case 3:
02113             result = 1;
02114             break;
02115           case 4:
02116             result = 1;
02117             break;
02118           case 5:
02119             result = 1;
02120             break;
02121         }
02122         break;
02123       case 1:
02124         switch (right) {
02125           case 0:
02126             result = 1;
02127             break;
02128           case 1:
02129             result = 2;
02130             break;
02131           case 2:
02132             result = 1;
02133             break;
02134           case 3:
02135             result = 1;
02136             break;
02137           case 4:
02138             result = 1;
02139             break;
02140           case 5:
02141             result = 1;
02142             break;
02143         }
02144         break;
02145       case 2:
02146         switch (right) {
02147           case 0:
02148             result = 1;
02149             break;
02150           case 1:
02151             result = 1;
02152             break;
02153           case 2:
02154             result = 0;
02155             break;
02156           case 3:
02157             result = 1;
02158             break;
02159           case 4:
02160             result = 1;
02161             break;
02162           case 5:
02163             result = 1;
02164             break;
02165         }
02166         break;
02167       case 3:
02168         switch (right) {
02169           case 0:
02170             result = 1;
02171             break;
02172           case 1:
02173             result = 1;
02174             break;
02175           case 2:
02176             result = 1;
02177             break;
02178           case 3:
02179             result = 0;
02180             break;
02181           case 4:
02182             result = 1;
02183             break;
02184           case 5:
02185             result = 1;
02186             break;
02187         }
02188         break;
02189       case 4:
02190         switch (right) {
02191           case 0:
02192             result = 1;
02193             break;
02194           case 1:
02195             result = 1;
02196             break;
02197           case 2:
02198             result = 1;
02199             break;
02200           case 3:
02201             result = 1;
02202             break;
02203           case 4:
02204             result = 0;
02205             break;
02206           case 5:
02207             result = 1;
02208             break;
02209         }
02210         break;
02211       case 5:
02212         switch (right) {
02213           case 0:
02214             result = 1;
02215             break;
02216           case 1:
02217             result = 1;
02218             break;
02219           case 2:
02220             result = 1;
02221             break;
02222           case 3:
02223             result = 1;
02224             break;
02225           case 4:
02226             result = 1;
02227             break;
02228           case 5:
02229             result = 2;
02230             break;
02231         }
02232         break;
02233     }
02234     if (result == -1) throw new RuntimeException("Range03.neNoChoose(" + left + ", " + right + ") is undefined");
02235     return result;
02236   }  
02237   public static byte neSet(int leftTokens, int rightTokens) {
02238     byte result = -1;
02239     for (int left = 0; (1 << left) <= leftTokens; left++) {
02240       if ((leftTokens & (1 << left)) == 0) continue;
02241       for (int right = 0; (1 << right) <= rightTokens; right++) {
02242         if ((rightTokens & (1 << right)) != 0) {
02243           if (result == -1) result = neNoChoose(left, right);
02244           else result = Abstraction.meetTest(result, neNoChoose(left, right));
02245         }
02246       }
02247     }
02248     return result;
02249   }  
02250   public static int rem(int left$, int right$) {
02251     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02252     if (left$ == LT0 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02253     if (left$ == LT0 && right$ == R1) return R0;
02254     if (left$ == LT0 && right$ == R2) return Abstraction.choose((1 << R1) | (1 << R0));
02255     if (left$ == LT0 && right$ == R3) return Abstraction.choose((1 << R2) | (1 << R1) | (1 << R0));
02256     if (left$ == LT0 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02257     if (left$ == R0 && right$ == LT0) return R0;
02258     if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02259     if (left$ == R0 && right$ == R1) return R0;
02260     if (left$ == R0 && right$ == R2) return R0;
02261     if (left$ == R0 && right$ == R3) return R0;
02262     if (left$ == R0 && right$ == GT3) return R0;
02263     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02264     if (left$ == R1 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02265     if (left$ == R1 && right$ == R1) return R0;
02266     if (left$ == R1 && right$ == R2) return R1;
02267     if (left$ == R1 && right$ == R3) return R1;
02268     if (left$ == R1 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02269     if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02270     if (left$ == R2 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02271     if (left$ == R2 && right$ == R1) return R0;
02272     if (left$ == R2 && right$ == R2) return R0;
02273     if (left$ == R2 && right$ == R3) return R2;
02274     if (left$ == R2 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02275     if (left$ == R3 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02276     if (left$ == R3 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02277     if (left$ == R3 && right$ == R1) return R0;
02278     if (left$ == R3 && right$ == R2) return R1;
02279     if (left$ == R3 && right$ == R3) return R0;
02280     if (left$ == R3 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02281     if (left$ == GT3 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02282     if (left$ == GT3 && right$ == R0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02283     if (left$ == GT3 && right$ == R1) return R0;
02284     if (left$ == GT3 && right$ == R2) return Abstraction.choose((1 << R1) | (1 << R0));
02285     if (left$ == GT3 && right$ == R3) return Abstraction.choose((1 << R2) | (1 << R1) | (1 << R0));
02286     if (left$ == GT3 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02287     throw new RuntimeException("Range03.rem(" + left$ + ", " + right$ + ") is undefined");
02288   }  
02289   private static int remNoChoose(int left, int right) {
02290     int result = 0;
02291     switch (left) {
02292       case 0:
02293         switch (right) {
02294           case 0:
02295             result = 63;
02296             break;
02297           case 1:
02298             result = 1;
02299             break;
02300           case 2:
02301             result = 1;
02302             break;
02303           case 3:
02304             result = 1;
02305             break;
02306           case 4:
02307             result = 1;
02308             break;
02309           case 5:
02310             result = 1;
02311             break;
02312         }
02313         break;
02314       case 1:
02315         switch (right) {
02316           case 0:
02317             result = 63;
02318             break;
02319           case 1:
02320             result = 63;
02321             break;
02322           case 2:
02323             result = 1;
02324             break;
02325           case 3:
02326             result = 5;
02327             break;
02328           case 4:
02329             result = 13;
02330             break;
02331           case 5:
02332             result = 63;
02333             break;
02334         }
02335         break;
02336       case 2:
02337         switch (right) {
02338           case 0:
02339             result = 63;
02340             break;
02341           case 1:
02342             result = 63;
02343             break;
02344           case 2:
02345             result = 1;
02346             break;
02347           case 3:
02348             result = 4;
02349             break;
02350           case 4:
02351             result = 4;
02352             break;
02353           case 5:
02354             result = 63;
02355             break;
02356         }
02357         break;
02358       case 3:
02359         switch (right) {
02360           case 0:
02361             result = 63;
02362             break;
02363           case 1:
02364             result = 63;
02365             break;
02366           case 2:
02367             result = 1;
02368             break;
02369           case 3:
02370             result = 1;
02371             break;
02372           case 4:
02373             result = 8;
02374             break;
02375           case 5:
02376             result = 63;
02377             break;
02378         }
02379         break;
02380       case 4:
02381         switch (right) {
02382           case 0:
02383             result = 63;
02384             break;
02385           case 1:
02386             result = 63;
02387             break;
02388           case 2:
02389             result = 1;
02390             break;
02391           case 3:
02392             result = 4;
02393             break;
02394           case 4:
02395             result = 1;
02396             break;
02397           case 5:
02398             result = 63;
02399             break;
02400         }
02401         break;
02402       case 5:
02403         switch (right) {
02404           case 0:
02405             result = 63;
02406             break;
02407           case 1:
02408             result = 63;
02409             break;
02410           case 2:
02411             result = 1;
02412             break;
02413           case 3:
02414             result = 5;
02415             break;
02416           case 4:
02417             result = 13;
02418             break;
02419           case 5:
02420             result = 63;
02421             break;
02422         }
02423         break;
02424     }
02425     if (result == 0) throw new RuntimeException("Range03.remNoChoose(" + left + ", " + right + ") is undefined");
02426     return result;
02427   }  
02428   public static int remSet(int leftTokens, int rightTokens) {
02429     int result = -1;
02430     for (int left = 0; (1 << left) <= leftTokens; left++) {
02431       if ((leftTokens & (1 << left)) == 0) continue;
02432       for (int right = 0; (1 << right) <= rightTokens; right++) {
02433         if ((rightTokens & (1 << right)) != 0) {
02434           if (result == -1) result = remNoChoose(left, right);
02435           else result = Abstraction.meetArith(result, remNoChoose(left, right));
02436         }
02437       }
02438     }
02439     return result;
02440   }  
02441   public static int sub(int left$, int right$) {
02442     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02443     if (left$ == LT0 && right$ == R0) return LT0;
02444     if (left$ == LT0 && right$ == R1) return LT0;
02445     if (left$ == LT0 && right$ == R2) return LT0;
02446     if (left$ == LT0 && right$ == R3) return LT0;
02447     if (left$ == LT0 && right$ == GT3) return LT0;
02448     if (left$ == R0 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1));
02449     if (left$ == R0 && right$ == R0) return R0;
02450     if (left$ == R0 && right$ == R1) return LT0;
02451     if (left$ == R0 && right$ == R2) return LT0;
02452     if (left$ == R0 && right$ == R3) return LT0;
02453     if (left$ == R0 && right$ == GT3) return LT0;
02454     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2));
02455     if (left$ == R1 && right$ == R0) return R1;
02456     if (left$ == R1 && right$ == R1) return R0;
02457     if (left$ == R1 && right$ == R2) return LT0;
02458     if (left$ == R1 && right$ == R3) return LT0;
02459     if (left$ == R1 && right$ == GT3) return LT0;
02460     if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << GT3) | (1 << R3));
02461     if (left$ == R2 && right$ == R0) return R2;
02462     if (left$ == R2 && right$ == R1) return R1;
02463     if (left$ == R2 && right$ == R2) return R0;
02464     if (left$ == R2 && right$ == R3) return LT0;
02465     if (left$ == R2 && right$ == GT3) return LT0;
02466     if (left$ == R3 && right$ == LT0) return GT3;
02467     if (left$ == R3 && right$ == R0) return R3;
02468     if (left$ == R3 && right$ == R1) return R2;
02469     if (left$ == R3 && right$ == R2) return R1;
02470     if (left$ == R3 && right$ == R3) return R0;
02471     if (left$ == R3 && right$ == GT3) return LT0;
02472     if (left$ == GT3 && right$ == LT0) return GT3;
02473     if (left$ == GT3 && right$ == R0) return GT3;
02474     if (left$ == GT3 && right$ == R1) return Abstraction.choose((1 << GT3) | (1 << R3));
02475     if (left$ == GT3 && right$ == R2) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2));
02476     if (left$ == GT3 && right$ == R3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1));
02477     if (left$ == GT3 && right$ == GT3) return Abstraction.choose((1 << GT3) | (1 << R3) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
02478     throw new RuntimeException("Range03.sub(" + left$ + ", " + right$ + ") is undefined");
02479   }  
02480   private static int subNoChoose(int left, int right) {
02481     int result = 0;
02482     switch (left) {
02483       case 0:
02484         switch (right) {
02485           case 0:
02486             result = 1;
02487             break;
02488           case 1:
02489             result = 60;
02490             break;
02491           case 2:
02492             result = 2;
02493             break;
02494           case 3:
02495             result = 2;
02496             break;
02497           case 4:
02498             result = 2;
02499             break;
02500           case 5:
02501             result = 2;
02502             break;
02503         }
02504         break;
02505       case 1:
02506         switch (right) {
02507           case 0:
02508             result = 2;
02509             break;
02510           case 1:
02511             result = 63;
02512             break;
02513           case 2:
02514             result = 2;
02515             break;
02516           case 3:
02517             result = 2;
02518             break;
02519           case 4:
02520             result = 2;
02521             break;
02522           case 5:
02523             result = 2;
02524             break;
02525         }
02526         break;
02527       case 2:
02528         switch (right) {
02529           case 0:
02530             result = 4;
02531             break;
02532           case 1:
02533             result = 56;
02534             break;
02535           case 2:
02536             result = 1;
02537             break;
02538           case 3:
02539             result = 2;
02540             break;
02541           case 4:
02542             result = 2;
02543             break;
02544           case 5:
02545             result = 2;
02546             break;
02547         }
02548         break;
02549       case 3:
02550         switch (right) {
02551           case 0:
02552             result = 8;
02553             break;
02554           case 1:
02555             result = 48;
02556             break;
02557           case 2:
02558             result = 4;
02559             break;
02560           case 3:
02561             result = 1;
02562             break;
02563           case 4:
02564             result = 2;
02565             break;
02566           case 5:
02567             result = 2;
02568             break;
02569         }
02570         break;
02571       case 4:
02572         switch (right) {
02573           case 0:
02574             result = 16;
02575             break;
02576           case 1:
02577             result = 32;
02578             break;
02579           case 2:
02580             result = 8;
02581             break;
02582           case 3:
02583             result = 4;
02584             break;
02585           case 4:
02586             result = 1;
02587             break;
02588           case 5:
02589             result = 2;
02590             break;
02591         }
02592         break;
02593       case 5:
02594         switch (right) {
02595           case 0:
02596             result = 32;
02597             break;
02598           case 1:
02599             result = 32;
02600             break;
02601           case 2:
02602             result = 48;
02603             break;
02604           case 3:
02605             result = 56;
02606             break;
02607           case 4:
02608             result = 60;
02609             break;
02610           case 5:
02611             result = 63;
02612             break;
02613         }
02614         break;
02615     }
02616     if (result == 0) throw new RuntimeException("Range03.subNoChoose(" + left + ", " + right + ") is undefined");
02617     return result;
02618   }  
02619   public static int subSet(int leftTokens, int rightTokens) {
02620     int result = -1;
02621     for (int left = 0; (1 << left) <= leftTokens; left++) {
02622       if ((leftTokens & (1 << left)) == 0) continue;
02623       for (int right = 0; (1 << right) <= rightTokens; right++) {
02624         if ((rightTokens & (1 << right)) != 0) {
02625           if (result == -1) result = subNoChoose(left, right);
02626           else result = Abstraction.meetArith(result, subNoChoose(left, right));
02627         }
02628       }
02629     }
02630     return result;
02631   }  
02632   public String toString() {
02633     return getName();
02634   }  
02635   public static Range03 v() {
02636     return v;
02637   }  
02638 }