Range01.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 Range01 extends IntegralAbstraction {
00039   private static final Range01 v = new Range01();
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 GT1 = 3;
00044   private Range01() {
00045   }  
00046   public static int abs(long n) {
00047     if (n < 0) return LT0;
00048     if (n == 0) return R0;
00049     if (n == 1) return R1;
00050     if (n > 1) return GT1;
00051     throw new RuntimeException("Range01 cannot abstract value '" + n + "'");
00052   }  
00053   public static int add(int left$, int right$) {
00054     if (left$ == LT0 && right$ == LT0) return LT0;
00055     if (left$ == LT0 && right$ == R0) return LT0;
00056     if (left$ == LT0 && right$ == R1) return Abstraction.choose((1 << R0) | (1 << LT0));
00057     if (left$ == LT0 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00058     if (left$ == R0 && right$ == LT0) return LT0;
00059     if (left$ == R0 && right$ == R0) return R0;
00060     if (left$ == R0 && right$ == R1) return R1;
00061     if (left$ == R0 && right$ == GT1) return GT1;
00062     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << R0) | (1 << LT0));
00063     if (left$ == R1 && right$ == R0) return R1;
00064     if (left$ == R1 && right$ == R1) return GT1;
00065     if (left$ == R1 && right$ == GT1) return GT1;
00066     if (left$ == GT1 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00067     if (left$ == GT1 && right$ == R0) return GT1;
00068     if (left$ == GT1 && right$ == R1) return GT1;
00069     if (left$ == GT1 && right$ == GT1) return GT1;
00070     throw new RuntimeException("Range01.add(" + left$ + ", " + right$ + ") is undefined");
00071   }  
00072   private static int addNoChoose(int left, int right) {
00073     int result = 0;
00074     switch (left) {
00075       case 0:
00076         switch (right) {
00077           case 0:
00078             result = 1;
00079             break;
00080           case 1:
00081             result = 2;
00082             break;
00083           case 2:
00084             result = 4;
00085             break;
00086           case 3:
00087             result = 8;
00088             break;
00089         }
00090         break;
00091       case 1:
00092         switch (right) {
00093           case 0:
00094             result = 2;
00095             break;
00096           case 1:
00097             result = 2;
00098             break;
00099           case 2:
00100             result = 3;
00101             break;
00102           case 3:
00103             result = 15;
00104             break;
00105         }
00106         break;
00107       case 2:
00108         switch (right) {
00109           case 0:
00110             result = 4;
00111             break;
00112           case 1:
00113             result = 3;
00114             break;
00115           case 2:
00116             result = 8;
00117             break;
00118           case 3:
00119             result = 8;
00120             break;
00121         }
00122         break;
00123       case 3:
00124         switch (right) {
00125           case 0:
00126             result = 8;
00127             break;
00128           case 1:
00129             result = 15;
00130             break;
00131           case 2:
00132             result = 8;
00133             break;
00134           case 3:
00135             result = 8;
00136             break;
00137         }
00138         break;
00139     }
00140     if (result == 0) throw new RuntimeException("Range01.addNoChoose(" + left + ", " + right + ") is undefined");
00141     return result;
00142   }  
00143   public static int addSet(int leftTokens, int rightTokens) {
00144     int result = -1;
00145     for (int left = 0; (1 << left) <= leftTokens; left++) {
00146       if ((leftTokens & (1 << left)) == 0) continue;
00147       for (int right = 0; (1 << right) <= rightTokens; right++) {
00148         if ((rightTokens & (1 << right)) != 0) {
00149           if (result == -1) result = addNoChoose(left, right);
00150           else result = Abstraction.meetArith(result, addNoChoose(left, right));
00151         }
00152       }
00153     }
00154     return result;
00155   }  
00156   public static int div(int left$, int right$) {
00157     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00158     if (left$ == LT0 && right$ == R0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00159     if (left$ == LT0 && right$ == R1) return LT0;
00160     if (left$ == LT0 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00161     if (left$ == R0 && right$ == LT0) return R0;
00162     if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00163     if (left$ == R0 && right$ == R1) return R0;
00164     if (left$ == R0 && right$ == GT1) return R0;
00165     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00166     if (left$ == R1 && right$ == R0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00167     if (left$ == R1 && right$ == R1) return R1;
00168     if (left$ == R1 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00169     if (left$ == GT1 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00170     if (left$ == GT1 && right$ == R0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00171     if (left$ == GT1 && right$ == R1) return GT1;
00172     if (left$ == GT1 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
00173     throw new RuntimeException("Range01.div(" + left$ + ", " + right$ + ") is undefined");
00174   }  
00175   private static int divNoChoose(int left, int right) {
00176     int result = 0;
00177     switch (left) {
00178       case 0:
00179         switch (right) {
00180           case 0:
00181             result = 15;
00182             break;
00183           case 1:
00184             result = 1;
00185             break;
00186           case 2:
00187             result = 1;
00188             break;
00189           case 3:
00190             result = 1;
00191             break;
00192         }
00193         break;
00194       case 1:
00195         switch (right) {
00196           case 0:
00197             result = 15;
00198             break;
00199           case 1:
00200             result = 15;
00201             break;
00202           case 2:
00203             result = 2;
00204             break;
00205           case 3:
00206             result = 15;
00207             break;
00208         }
00209         break;
00210       case 2:
00211         switch (right) {
00212           case 0:
00213             result = 15;
00214             break;
00215           case 1:
00216             result = 15;
00217             break;
00218           case 2:
00219             result = 4;
00220             break;
00221           case 3:
00222             result = 15;
00223             break;
00224         }
00225         break;
00226       case 3:
00227         switch (right) {
00228           case 0:
00229             result = 15;
00230             break;
00231           case 1:
00232             result = 15;
00233             break;
00234           case 2:
00235             result = 8;
00236             break;
00237           case 3:
00238             result = 15;
00239             break;
00240         }
00241         break;
00242     }
00243     if (result == 0) throw new RuntimeException("Range01.divNoChoose(" + left + ", " + right + ") is undefined");
00244     return result;
00245   }  
00246   public static int divSet(int leftTokens, int rightTokens) {
00247     int result = -1;
00248     for (int left = 0; (1 << left) <= leftTokens; left++) {
00249       if ((leftTokens & (1 << left)) == 0) continue;
00250       for (int right = 0; (1 << right) <= rightTokens; right++) {
00251         if ((rightTokens & (1 << right)) != 0) {
00252           if (result == -1) result = divNoChoose(left, right);
00253           else result = Abstraction.meetArith(result, divNoChoose(left, right));
00254         }
00255       }
00256     }
00257     return result;
00258   }  
00259   public static boolean eq(int left$, int right$) {
00260     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00261     if (left$ == LT0 && right$ == R0) return false;
00262     if (left$ == LT0 && right$ == R1) return false;
00263     if (left$ == LT0 && right$ == GT1) return false;
00264     if (left$ == R0 && right$ == LT0) return false;
00265     if (left$ == R0 && right$ == R0) return true;
00266     if (left$ == R0 && right$ == R1) return false;
00267     if (left$ == R0 && right$ == GT1) return false;
00268     if (left$ == R1 && right$ == LT0) return false;
00269     if (left$ == R1 && right$ == R0) return false;
00270     if (left$ == R1 && right$ == R1) return true;
00271     if (left$ == R1 && right$ == GT1) return false;
00272     if (left$ == GT1 && right$ == LT0) return false;
00273     if (left$ == GT1 && right$ == R0) return false;
00274     if (left$ == GT1 && right$ == R1) return false;
00275     if (left$ == GT1 && right$ == GT1) return Abstraction.choose();
00276     throw new RuntimeException("Range01.eq(" + left$ + ", " + right$ + ") is undefined");
00277   }  
00278   private static byte eqNoChoose(int left, int right) {
00279     byte result = -1;
00280     switch (left) {
00281       case 0:
00282         switch (right) {
00283           case 0:
00284             result = 1;
00285             break;
00286           case 1:
00287             result = 0;
00288             break;
00289           case 2:
00290             result = 0;
00291             break;
00292           case 3:
00293             result = 0;
00294             break;
00295         }
00296         break;
00297       case 1:
00298         switch (right) {
00299           case 0:
00300             result = 0;
00301             break;
00302           case 1:
00303             result = 2;
00304             break;
00305           case 2:
00306             result = 0;
00307             break;
00308           case 3:
00309             result = 0;
00310             break;
00311         }
00312         break;
00313       case 2:
00314         switch (right) {
00315           case 0:
00316             result = 0;
00317             break;
00318           case 1:
00319             result = 0;
00320             break;
00321           case 2:
00322             result = 1;
00323             break;
00324           case 3:
00325             result = 0;
00326             break;
00327         }
00328         break;
00329       case 3:
00330         switch (right) {
00331           case 0:
00332             result = 0;
00333             break;
00334           case 1:
00335             result = 0;
00336             break;
00337           case 2:
00338             result = 0;
00339             break;
00340           case 3:
00341             result = 2;
00342             break;
00343         }
00344         break;
00345     }
00346     if (result == -1) throw new RuntimeException("Range01.eqNoChoose(" + left + ", " + right + ") is undefined");
00347     return result;
00348   }  
00349   public static byte eqSet(int leftTokens, int rightTokens) {
00350     byte result = -1;
00351     for (int left = 0; (1 << left) <= leftTokens; left++) {
00352       if ((leftTokens & (1 << left)) == 0) continue;
00353       for (int right = 0; (1 << right) <= rightTokens; right++) {
00354         if ((rightTokens & (1 << right)) != 0) {
00355           if (result == -1) result = eqNoChoose(left, right);
00356           else result = Abstraction.meetTest(result, eqNoChoose(left, right));
00357         }
00358       }
00359     }
00360     return result;
00361   }  
00362   public static boolean ge(int left$, int right$) {
00363     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00364     if (left$ == LT0 && right$ == R0) return false;
00365     if (left$ == LT0 && right$ == R1) return false;
00366     if (left$ == LT0 && right$ == GT1) return false;
00367     if (left$ == R0 && right$ == LT0) return true;
00368     if (left$ == R0 && right$ == R0) return true;
00369     if (left$ == R0 && right$ == R1) return false;
00370     if (left$ == R0 && right$ == GT1) return false;
00371     if (left$ == R1 && right$ == LT0) return true;
00372     if (left$ == R1 && right$ == R0) return true;
00373     if (left$ == R1 && right$ == R1) return true;
00374     if (left$ == R1 && right$ == GT1) return false;
00375     if (left$ == GT1 && right$ == LT0) return true;
00376     if (left$ == GT1 && right$ == R0) return true;
00377     if (left$ == GT1 && right$ == R1) return true;
00378     if (left$ == GT1 && right$ == GT1) return Abstraction.choose();
00379     throw new RuntimeException("Range01.ge(" + left$ + ", " + right$ + ") is undefined");
00380   }  
00381   private static byte geNoChoose(int left, int right) {
00382     byte result = -1;
00383     switch (left) {
00384       case 0:
00385         switch (right) {
00386           case 0:
00387             result = 1;
00388             break;
00389           case 1:
00390             result = 1;
00391             break;
00392           case 2:
00393             result = 0;
00394             break;
00395           case 3:
00396             result = 0;
00397             break;
00398         }
00399         break;
00400       case 1:
00401         switch (right) {
00402           case 0:
00403             result = 0;
00404             break;
00405           case 1:
00406             result = 2;
00407             break;
00408           case 2:
00409             result = 0;
00410             break;
00411           case 3:
00412             result = 0;
00413             break;
00414         }
00415         break;
00416       case 2:
00417         switch (right) {
00418           case 0:
00419             result = 1;
00420             break;
00421           case 1:
00422             result = 1;
00423             break;
00424           case 2:
00425             result = 1;
00426             break;
00427           case 3:
00428             result = 0;
00429             break;
00430         }
00431         break;
00432       case 3:
00433         switch (right) {
00434           case 0:
00435             result = 1;
00436             break;
00437           case 1:
00438             result = 1;
00439             break;
00440           case 2:
00441             result = 1;
00442             break;
00443           case 3:
00444             result = 2;
00445             break;
00446         }
00447         break;
00448     }
00449     if (result == -1) throw new RuntimeException("Range01.geNoChoose(" + left + ", " + right + ") is undefined");
00450     return result;
00451   }  
00452   public static byte geSet(int leftTokens, int rightTokens) {
00453     byte result = -1;
00454     for (int left = 0; (1 << left) <= leftTokens; left++) {
00455       if ((leftTokens & (1 << left)) == 0) continue;
00456       for (int right = 0; (1 << right) <= rightTokens; right++) {
00457         if ((rightTokens & (1 << right)) != 0) {
00458           if (result == -1) result = geNoChoose(left, right);
00459           else result = Abstraction.meetTest(result, geNoChoose(left, right));
00460         }
00461       }
00462     }
00463     return result;
00464   }  
00465   public static String getBASLRepresentation() {
00466     return
00467       "abstraction Range01 extends integral \n"
00468       + "  begin\n"
00469       + "    TOKENS = {LT0, R0, R1, GT1};\n"
00470       + "    DEFAULT = R0;\n"
00471       + "    ONE2ONE = {R0, R1};\n"
00472       + "    abstract (n)\n"
00473       + "      begin\n"
00474       + "        n < 0 -> LT0;\n"
00475       + "        n == 0 -> R0;\n"
00476       + "        n == 1 -> R1;\n"
00477       + "        n > 1 -> GT1;\n"
00478       + "      end\n"
00479       + "    operator + add \n"
00480       + "      begin\n"
00481       + "        (LT0, LT0) -> LT0;\n"
00482       + "        (LT0, R0) -> LT0;\n"
00483       + "        (LT0, R1) -> {LT0, R0};\n"
00484       + "        (LT0, GT1) -> {LT0, R0, R1, GT1};\n"
00485       + "        (R0, LT0) -> LT0;\n"
00486       + "        (R0, R0) -> R0;\n"
00487       + "        (R0, R1) -> R1;\n"
00488       + "        (R0, GT1) -> GT1;\n"
00489       + "        (R1, LT0) -> {LT0, R0};\n"
00490       + "        (R1, R0) -> R1;\n"
00491       + "        (R1, R1) -> GT1;\n"
00492       + "        (R1, GT1) -> GT1;\n"
00493       + "        (GT1, LT0) -> {LT0, R0, R1, GT1};\n"
00494       + "        (GT1, R0) -> GT1;\n"
00495       + "        (GT1, R1) -> GT1;\n"
00496       + "        (GT1, GT1) -> GT1;\n"
00497       + "      end\n"
00498       + "    operator - sub \n"
00499       + "      begin\n"
00500       + "        (LT0, LT0) -> {LT0, R0, R1, GT1};\n"
00501       + "        (LT0, R0) -> LT0;\n"
00502       + "        (LT0, R1) -> LT0;\n"
00503       + "        (LT0, GT1) -> LT0;\n"
00504       + "        (R0, LT0) -> {R1, GT1};\n"
00505       + "        (R0, R0) -> R0;\n"
00506       + "        (R0, R1) -> LT0;\n"
00507       + "        (R0, GT1) -> LT0;\n"
00508       + "        (R1, LT0) -> GT1;\n"
00509       + "        (R1, R0) -> R1;\n"
00510       + "        (R1, R1) -> R0;\n"
00511       + "        (R1, GT1) -> LT0;\n"
00512       + "        (GT1, LT0) -> GT1;\n"
00513       + "        (GT1, R0) -> GT1;\n"
00514       + "        (GT1, R1) -> {R1, GT1};\n"
00515       + "        (GT1, GT1) -> {LT0, R0, R1, GT1};\n"
00516       + "      end\n"
00517       + "    operator * mul \n"
00518       + "      begin\n"
00519       + "        (LT0, LT0) -> {R1, GT1};\n"
00520       + "        (LT0, R0) -> R0;\n"
00521       + "        (LT0, R1) -> LT0;\n"
00522       + "        (LT0, GT1) -> {LT0, R1, GT1};\n"
00523       + "        (R0, LT0) -> R0;\n"
00524       + "        (R0, R0) -> R0;\n"
00525       + "        (R0, R1) -> R0;\n"
00526       + "        (R0, GT1) -> R0;\n"
00527       + "        (R1, LT0) -> LT0;\n"
00528       + "        (R1, R0) -> R0;\n"
00529       + "        (R1, R1) -> R1;\n"
00530       + "        (R1, GT1) -> GT1;\n"
00531       + "        (GT1, LT0) -> {LT0, R1, GT1};\n"
00532       + "        (GT1, R0) -> R0;\n"
00533       + "        (GT1, R1) -> GT1;\n"
00534       + "        (GT1, GT1) -> {R1, GT1};\n"
00535       + "      end\n"
00536       + "    operator / div \n"
00537       + "      begin\n"
00538       + "        (LT0, LT0) -> {LT0, R0, R1, GT1};\n"
00539       + "        (LT0, R0) -> T;\n"
00540       + "        (LT0, R1) -> LT0;\n"
00541       + "        (LT0, GT1) -> {LT0, R0, R1, GT1};\n"
00542       + "        (R0, LT0) -> R0;\n"
00543       + "        (R0, R0) -> T;\n"
00544       + "        (R0, R1) -> R0;\n"
00545       + "        (R0, GT1) -> R0;\n"
00546       + "        (R1, LT0) -> {LT0, R0, R1, GT1};\n"
00547       + "        (R1, R0) -> T;\n"
00548       + "        (R1, R1) -> R1;\n"
00549       + "        (R1, GT1) -> {LT0, R0, R1, GT1};\n"
00550       + "        (GT1, LT0) -> {LT0, R0, R1, GT1};\n"
00551       + "        (GT1, R0) -> T;\n"
00552       + "        (GT1, R1) -> GT1;\n"
00553       + "        (GT1, GT1) -> {LT0, R0, R1, GT1};\n"
00554       + "      end\n"
00555       + "    operator % rem \n"
00556       + "      begin\n"
00557       + "        (LT0, LT0) -> {LT0, R0, R1, GT1};\n"
00558       + "        (LT0, R0) -> T;\n"
00559       + "        (LT0, R1) -> R0;\n"
00560       + "        (LT0, GT1) -> {LT0, R0, R1, GT1};\n"
00561       + "        (R0, LT0) -> R0;\n"
00562       + "        (R0, R0) -> T;\n"
00563       + "        (R0, R1) -> R0;\n"
00564       + "        (R0, GT1) -> R0;\n"
00565       + "        (R1, LT0) -> {LT0, R0, R1, GT1};\n"
00566       + "        (R1, R0) -> T;\n"
00567       + "        (R1, R1) -> R0;\n"
00568       + "        (R1, GT1) -> {LT0, R0, R1, GT1};\n"
00569       + "        (GT1, LT0) -> {LT0, R0, R1, GT1};\n"
00570       + "        (GT1, R0) -> T;\n"
00571       + "        (GT1, R1) -> R0;\n"
00572       + "        (GT1, GT1) -> {LT0, R0, R1, GT1};\n"
00573       + "      end\n"
00574       + "    test == eq \n"
00575       + "      begin\n"
00576       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00577       + "        (LT0, R0) -> FALSE;\n"
00578       + "        (LT0, R1) -> FALSE;\n"
00579       + "        (LT0, GT1) -> FALSE;\n"
00580       + "        (R0, LT0) -> FALSE;\n"
00581       + "        (R0, R0) -> TRUE;\n"
00582       + "        (R0, R1) -> FALSE;\n"
00583       + "        (R0, GT1) -> FALSE;\n"
00584       + "        (R1, LT0) -> FALSE;\n"
00585       + "        (R1, R0) -> FALSE;\n"
00586       + "        (R1, R1) -> TRUE;\n"
00587       + "        (R1, GT1) -> FALSE;\n"
00588       + "        (GT1, LT0) -> FALSE;\n"
00589       + "        (GT1, R0) -> FALSE;\n"
00590       + "        (GT1, R1) -> FALSE;\n"
00591       + "        (GT1, GT1) -> {TRUE, FALSE};\n"
00592       + "      end\n"
00593       + "    test != neq \n"
00594       + "      begin\n"
00595       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00596       + "        (LT0, R0) -> TRUE;\n"
00597       + "        (LT0, R1) -> TRUE;\n"
00598       + "        (LT0, GT1) -> TRUE;\n"
00599       + "        (R0, LT0) -> TRUE;\n"
00600       + "        (R0, R0) -> FALSE;\n"
00601       + "        (R0, R1) -> TRUE;\n"
00602       + "        (R0, GT1) -> TRUE;\n"
00603       + "        (R1, LT0) -> TRUE;\n"
00604       + "        (R1, R0) -> TRUE;\n"
00605       + "        (R1, R1) -> FALSE;\n"
00606       + "        (R1, GT1) -> TRUE;\n"
00607       + "        (GT1, LT0) -> TRUE;\n"
00608       + "        (GT1, R0) -> TRUE;\n"
00609       + "        (GT1, R1) -> TRUE;\n"
00610       + "        (GT1, GT1) -> {TRUE, FALSE};\n"
00611       + "      end\n"
00612       + "    test < lt \n"
00613       + "      begin\n"
00614       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00615       + "        (LT0, R0) -> TRUE;\n"
00616       + "        (LT0, R1) -> TRUE;\n"
00617       + "        (LT0, GT1) -> TRUE;\n"
00618       + "        (R0, LT0) -> FALSE;\n"
00619       + "        (R0, R0) -> FALSE;\n"
00620       + "        (R0, R1) -> TRUE;\n"
00621       + "        (R0, GT1) -> TRUE;\n"
00622       + "        (R1, LT0) -> FALSE;\n"
00623       + "        (R1, R0) -> FALSE;\n"
00624       + "        (R1, R1) -> FALSE;\n"
00625       + "        (R1, GT1) -> TRUE;\n"
00626       + "        (GT1, LT0) -> FALSE;\n"
00627       + "        (GT1, R0) -> FALSE;\n"
00628       + "        (GT1, R1) -> FALSE;\n"
00629       + "        (GT1, GT1) -> {TRUE, FALSE};\n"
00630       + "      end\n"
00631       + "    test <= le \n"
00632       + "      begin\n"
00633       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00634       + "        (LT0, R0) -> TRUE;\n"
00635       + "        (LT0, R1) -> TRUE;\n"
00636       + "        (LT0, GT1) -> TRUE;\n"
00637       + "        (R0, LT0) -> FALSE;\n"
00638       + "        (R0, R0) -> TRUE;\n"
00639       + "        (R0, R1) -> TRUE;\n"
00640       + "        (R0, GT1) -> TRUE;\n"
00641       + "        (R1, LT0) -> FALSE;\n"
00642       + "        (R1, R0) -> FALSE;\n"
00643       + "        (R1, R1) -> TRUE;\n"
00644       + "        (R1, GT1) -> TRUE;\n"
00645       + "        (GT1, LT0) -> FALSE;\n"
00646       + "        (GT1, R0) -> FALSE;\n"
00647       + "        (GT1, R1) -> FALSE;\n"
00648       + "        (GT1, GT1) -> {TRUE, FALSE};\n"
00649       + "      end\n"
00650       + "    test > gt \n"
00651       + "      begin\n"
00652       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00653       + "        (LT0, R0) -> FALSE;\n"
00654       + "        (LT0, R1) -> FALSE;\n"
00655       + "        (LT0, GT1) -> FALSE;\n"
00656       + "        (R0, LT0) -> TRUE;\n"
00657       + "        (R0, R0) -> FALSE;\n"
00658       + "        (R0, R1) -> FALSE;\n"
00659       + "        (R0, GT1) -> FALSE;\n"
00660       + "        (R1, LT0) -> TRUE;\n"
00661       + "        (R1, R0) -> TRUE;\n"
00662       + "        (R1, R1) -> FALSE;\n"
00663       + "        (R1, GT1) -> FALSE;\n"
00664       + "        (GT1, LT0) -> TRUE;\n"
00665       + "        (GT1, R0) -> TRUE;\n"
00666       + "        (GT1, R1) -> TRUE;\n"
00667       + "        (GT1, GT1) -> {TRUE, FALSE};\n"
00668       + "      end\n"
00669       + "    test >= ge \n"
00670       + "      begin\n"
00671       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00672       + "        (LT0, R0) -> FALSE;\n"
00673       + "        (LT0, R1) -> FALSE;\n"
00674       + "        (LT0, GT1) -> FALSE;\n"
00675       + "        (R0, LT0) -> TRUE;\n"
00676       + "        (R0, R0) -> TRUE;\n"
00677       + "        (R0, R1) -> FALSE;\n"
00678       + "        (R0, GT1) -> FALSE;\n"
00679       + "        (R1, LT0) -> TRUE;\n"
00680       + "        (R1, R0) -> TRUE;\n"
00681       + "        (R1, R1) -> TRUE;\n"
00682       + "        (R1, GT1) -> FALSE;\n"
00683       + "        (GT1, LT0) -> TRUE;\n"
00684       + "        (GT1, R0) -> TRUE;\n"
00685       + "        (GT1, R1) -> TRUE;\n"
00686       + "        (GT1, GT1) -> {TRUE, FALSE};\n"
00687       + "      end\n"
00688       + "  end\n"
00689     ;
00690   }  
00691   public static String getName() {
00692     return "Range01";
00693   }  
00694   public static int getNumOfTokens() {
00695     return 4;
00696   }  
00697   public static String getToken(int value) {
00698     switch(value) {
00699       case R0: return "Range01.R0";
00700       case LT0: return "Range01.LT0";
00701       case R1: return "Range01.R1";
00702       case GT1: return "Range01.GT1";
00703     }
00704     return "Range01.???";
00705   }  
00706   public static boolean gt(int left$, int right$) {
00707     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00708     if (left$ == LT0 && right$ == R0) return false;
00709     if (left$ == LT0 && right$ == R1) return false;
00710     if (left$ == LT0 && right$ == GT1) return false;
00711     if (left$ == R0 && right$ == LT0) return true;
00712     if (left$ == R0 && right$ == R0) return false;
00713     if (left$ == R0 && right$ == R1) return false;
00714     if (left$ == R0 && right$ == GT1) return false;
00715     if (left$ == R1 && right$ == LT0) return true;
00716     if (left$ == R1 && right$ == R0) return true;
00717     if (left$ == R1 && right$ == R1) return false;
00718     if (left$ == R1 && right$ == GT1) return false;
00719     if (left$ == GT1 && right$ == LT0) return true;
00720     if (left$ == GT1 && right$ == R0) return true;
00721     if (left$ == GT1 && right$ == R1) return true;
00722     if (left$ == GT1 && right$ == GT1) return Abstraction.choose();
00723     throw new RuntimeException("Range01.gt(" + left$ + ", " + right$ + ") is undefined");
00724   }  
00725   private static byte gtNoChoose(int left, int right) {
00726     byte result = -1;
00727     switch (left) {
00728       case 0:
00729         switch (right) {
00730           case 0:
00731             result = 0;
00732             break;
00733           case 1:
00734             result = 1;
00735             break;
00736           case 2:
00737             result = 0;
00738             break;
00739           case 3:
00740             result = 0;
00741             break;
00742         }
00743         break;
00744       case 1:
00745         switch (right) {
00746           case 0:
00747             result = 0;
00748             break;
00749           case 1:
00750             result = 2;
00751             break;
00752           case 2:
00753             result = 0;
00754             break;
00755           case 3:
00756             result = 0;
00757             break;
00758         }
00759         break;
00760       case 2:
00761         switch (right) {
00762           case 0:
00763             result = 1;
00764             break;
00765           case 1:
00766             result = 1;
00767             break;
00768           case 2:
00769             result = 0;
00770             break;
00771           case 3:
00772             result = 0;
00773             break;
00774         }
00775         break;
00776       case 3:
00777         switch (right) {
00778           case 0:
00779             result = 1;
00780             break;
00781           case 1:
00782             result = 1;
00783             break;
00784           case 2:
00785             result = 1;
00786             break;
00787           case 3:
00788             result = 2;
00789             break;
00790         }
00791         break;
00792     }
00793     if (result == -1) throw new RuntimeException("Range01.gtNoChoose(" + left + ", " + right + ") is undefined");
00794     return result;
00795   }  
00796   public static byte gtSet(int leftTokens, int rightTokens) {
00797     byte result = -1;
00798     for (int left = 0; (1 << left) <= leftTokens; left++) {
00799       if ((leftTokens & (1 << left)) == 0) continue;
00800       for (int right = 0; (1 << right) <= rightTokens; right++) {
00801         if ((rightTokens & (1 << right)) != 0) {
00802           if (result == -1) result = gtNoChoose(left, right);
00803           else result = Abstraction.meetTest(result, gtNoChoose(left, right));
00804         }
00805       }
00806     }
00807     return result;
00808   }  
00809   public static boolean isOne2One(int value) {
00810     switch(value) {
00811       case R1: return true;
00812       case R0: return true;
00813     }
00814     return false;
00815   }  
00816   public static boolean le(int left$, int right$) {
00817     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00818     if (left$ == LT0 && right$ == R0) return true;
00819     if (left$ == LT0 && right$ == R1) return true;
00820     if (left$ == LT0 && right$ == GT1) return true;
00821     if (left$ == R0 && right$ == LT0) return false;
00822     if (left$ == R0 && right$ == R0) return true;
00823     if (left$ == R0 && right$ == R1) return true;
00824     if (left$ == R0 && right$ == GT1) return true;
00825     if (left$ == R1 && right$ == LT0) return false;
00826     if (left$ == R1 && right$ == R0) return false;
00827     if (left$ == R1 && right$ == R1) return true;
00828     if (left$ == R1 && right$ == GT1) return true;
00829     if (left$ == GT1 && right$ == LT0) return false;
00830     if (left$ == GT1 && right$ == R0) return false;
00831     if (left$ == GT1 && right$ == R1) return false;
00832     if (left$ == GT1 && right$ == GT1) return Abstraction.choose();
00833     throw new RuntimeException("Range01.le(" + left$ + ", " + right$ + ") is undefined");
00834   }  
00835   private static byte leNoChoose(int left, int right) {
00836     byte result = -1;
00837     switch (left) {
00838       case 0:
00839         switch (right) {
00840           case 0:
00841             result = 1;
00842             break;
00843           case 1:
00844             result = 0;
00845             break;
00846           case 2:
00847             result = 1;
00848             break;
00849           case 3:
00850             result = 1;
00851             break;
00852         }
00853         break;
00854       case 1:
00855         switch (right) {
00856           case 0:
00857             result = 1;
00858             break;
00859           case 1:
00860             result = 2;
00861             break;
00862           case 2:
00863             result = 1;
00864             break;
00865           case 3:
00866             result = 1;
00867             break;
00868         }
00869         break;
00870       case 2:
00871         switch (right) {
00872           case 0:
00873             result = 0;
00874             break;
00875           case 1:
00876             result = 0;
00877             break;
00878           case 2:
00879             result = 1;
00880             break;
00881           case 3:
00882             result = 1;
00883             break;
00884         }
00885         break;
00886       case 3:
00887         switch (right) {
00888           case 0:
00889             result = 0;
00890             break;
00891           case 1:
00892             result = 0;
00893             break;
00894           case 2:
00895             result = 0;
00896             break;
00897           case 3:
00898             result = 2;
00899             break;
00900         }
00901         break;
00902     }
00903     if (result == -1) throw new RuntimeException("Range01.leNoChoose(" + left + ", " + right + ") is undefined");
00904     return result;
00905   }  
00906   public static byte leSet(int leftTokens, int rightTokens) {
00907     byte result = -1;
00908     for (int left = 0; (1 << left) <= leftTokens; left++) {
00909       if ((leftTokens & (1 << left)) == 0) continue;
00910       for (int right = 0; (1 << right) <= rightTokens; right++) {
00911         if ((rightTokens & (1 << right)) != 0) {
00912           if (result == -1) result = leNoChoose(left, right);
00913           else result = Abstraction.meetTest(result, leNoChoose(left, right));
00914         }
00915       }
00916     }
00917     return result;
00918   }  
00919   public static boolean lt(int left$, int right$) {
00920     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00921     if (left$ == LT0 && right$ == R0) return true;
00922     if (left$ == LT0 && right$ == R1) return true;
00923     if (left$ == LT0 && right$ == GT1) return true;
00924     if (left$ == R0 && right$ == LT0) return false;
00925     if (left$ == R0 && right$ == R0) return false;
00926     if (left$ == R0 && right$ == R1) return true;
00927     if (left$ == R0 && right$ == GT1) return true;
00928     if (left$ == R1 && right$ == LT0) return false;
00929     if (left$ == R1 && right$ == R0) return false;
00930     if (left$ == R1 && right$ == R1) return false;
00931     if (left$ == R1 && right$ == GT1) return true;
00932     if (left$ == GT1 && right$ == LT0) return false;
00933     if (left$ == GT1 && right$ == R0) return false;
00934     if (left$ == GT1 && right$ == R1) return false;
00935     if (left$ == GT1 && right$ == GT1) return Abstraction.choose();
00936     throw new RuntimeException("Range01.lt(" + left$ + ", " + right$ + ") is undefined");
00937   }  
00938   private static byte ltNoChoose(int left, int right) {
00939     byte result = -1;
00940     switch (left) {
00941       case 0:
00942         switch (right) {
00943           case 0:
00944             result = 0;
00945             break;
00946           case 1:
00947             result = 0;
00948             break;
00949           case 2:
00950             result = 1;
00951             break;
00952           case 3:
00953             result = 1;
00954             break;
00955         }
00956         break;
00957       case 1:
00958         switch (right) {
00959           case 0:
00960             result = 1;
00961             break;
00962           case 1:
00963             result = 2;
00964             break;
00965           case 2:
00966             result = 1;
00967             break;
00968           case 3:
00969             result = 1;
00970             break;
00971         }
00972         break;
00973       case 2:
00974         switch (right) {
00975           case 0:
00976             result = 0;
00977             break;
00978           case 1:
00979             result = 0;
00980             break;
00981           case 2:
00982             result = 0;
00983             break;
00984           case 3:
00985             result = 1;
00986             break;
00987         }
00988         break;
00989       case 3:
00990         switch (right) {
00991           case 0:
00992             result = 0;
00993             break;
00994           case 1:
00995             result = 0;
00996             break;
00997           case 2:
00998             result = 0;
00999             break;
01000           case 3:
01001             result = 2;
01002             break;
01003         }
01004         break;
01005     }
01006     if (result == -1) throw new RuntimeException("Range01.ltNoChoose(" + left + ", " + right + ") is undefined");
01007     return result;
01008   }  
01009   public static byte ltSet(int leftTokens, int rightTokens) {
01010     byte result = -1;
01011     for (int left = 0; (1 << left) <= leftTokens; left++) {
01012       if ((leftTokens & (1 << left)) == 0) continue;
01013       for (int right = 0; (1 << right) <= rightTokens; right++) {
01014         if ((rightTokens & (1 << right)) != 0) {
01015           if (result == -1) result = ltNoChoose(left, right);
01016           else result = Abstraction.meetTest(result, ltNoChoose(left, right));
01017         }
01018       }
01019     }
01020     return result;
01021   }  
01022   public static int mul(int left$, int right$) {
01023     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1));
01024     if (left$ == LT0 && right$ == R0) return R0;
01025     if (left$ == LT0 && right$ == R1) return LT0;
01026     if (left$ == LT0 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << LT0));
01027     if (left$ == R0 && right$ == LT0) return R0;
01028     if (left$ == R0 && right$ == R0) return R0;
01029     if (left$ == R0 && right$ == R1) return R0;
01030     if (left$ == R0 && right$ == GT1) return R0;
01031     if (left$ == R1 && right$ == LT0) return LT0;
01032     if (left$ == R1 && right$ == R0) return R0;
01033     if (left$ == R1 && right$ == R1) return R1;
01034     if (left$ == R1 && right$ == GT1) return GT1;
01035     if (left$ == GT1 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << LT0));
01036     if (left$ == GT1 && right$ == R0) return R0;
01037     if (left$ == GT1 && right$ == R1) return GT1;
01038     if (left$ == GT1 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1));
01039     throw new RuntimeException("Range01.mul(" + left$ + ", " + right$ + ") is undefined");
01040   }  
01041   private static int mulNoChoose(int left, int right) {
01042     int result = 0;
01043     switch (left) {
01044       case 0:
01045         switch (right) {
01046           case 0:
01047             result = 1;
01048             break;
01049           case 1:
01050             result = 1;
01051             break;
01052           case 2:
01053             result = 1;
01054             break;
01055           case 3:
01056             result = 1;
01057             break;
01058         }
01059         break;
01060       case 1:
01061         switch (right) {
01062           case 0:
01063             result = 1;
01064             break;
01065           case 1:
01066             result = 12;
01067             break;
01068           case 2:
01069             result = 2;
01070             break;
01071           case 3:
01072             result = 14;
01073             break;
01074         }
01075         break;
01076       case 2:
01077         switch (right) {
01078           case 0:
01079             result = 1;
01080             break;
01081           case 1:
01082             result = 2;
01083             break;
01084           case 2:
01085             result = 4;
01086             break;
01087           case 3:
01088             result = 8;
01089             break;
01090         }
01091         break;
01092       case 3:
01093         switch (right) {
01094           case 0:
01095             result = 1;
01096             break;
01097           case 1:
01098             result = 14;
01099             break;
01100           case 2:
01101             result = 8;
01102             break;
01103           case 3:
01104             result = 12;
01105             break;
01106         }
01107         break;
01108     }
01109     if (result == 0) throw new RuntimeException("Range01.mulNoChoose(" + left + ", " + right + ") is undefined");
01110     return result;
01111   }  
01112   public static int mulSet(int leftTokens, int rightTokens) {
01113     int result = -1;
01114     for (int left = 0; (1 << left) <= leftTokens; left++) {
01115       if ((leftTokens & (1 << left)) == 0) continue;
01116       for (int right = 0; (1 << right) <= rightTokens; right++) {
01117         if ((rightTokens & (1 << right)) != 0) {
01118           if (result == -1) result = mulNoChoose(left, right);
01119           else result = Abstraction.meetArith(result, mulNoChoose(left, right));
01120         }
01121       }
01122     }
01123     return result;
01124   }  
01125   public static boolean ne(int left$, int right$) {
01126     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
01127     if (left$ == LT0 && right$ == R0) return true;
01128     if (left$ == LT0 && right$ == R1) return true;
01129     if (left$ == LT0 && right$ == GT1) return true;
01130     if (left$ == R0 && right$ == LT0) return true;
01131     if (left$ == R0 && right$ == R0) return false;
01132     if (left$ == R0 && right$ == R1) return true;
01133     if (left$ == R0 && right$ == GT1) return true;
01134     if (left$ == R1 && right$ == LT0) return true;
01135     if (left$ == R1 && right$ == R0) return true;
01136     if (left$ == R1 && right$ == R1) return false;
01137     if (left$ == R1 && right$ == GT1) return true;
01138     if (left$ == GT1 && right$ == LT0) return true;
01139     if (left$ == GT1 && right$ == R0) return true;
01140     if (left$ == GT1 && right$ == R1) return true;
01141     if (left$ == GT1 && right$ == GT1) return Abstraction.choose();
01142     throw new RuntimeException("Range01.ne(" + left$ + ", " + right$ + ") is undefined");
01143   }  
01144   private static byte neNoChoose(int left, int right) {
01145     byte result = -1;
01146     switch (left) {
01147       case 0:
01148         switch (right) {
01149           case 0:
01150             result = 0;
01151             break;
01152           case 1:
01153             result = 1;
01154             break;
01155           case 2:
01156             result = 1;
01157             break;
01158           case 3:
01159             result = 1;
01160             break;
01161         }
01162         break;
01163       case 1:
01164         switch (right) {
01165           case 0:
01166             result = 1;
01167             break;
01168           case 1:
01169             result = 2;
01170             break;
01171           case 2:
01172             result = 1;
01173             break;
01174           case 3:
01175             result = 1;
01176             break;
01177         }
01178         break;
01179       case 2:
01180         switch (right) {
01181           case 0:
01182             result = 1;
01183             break;
01184           case 1:
01185             result = 1;
01186             break;
01187           case 2:
01188             result = 0;
01189             break;
01190           case 3:
01191             result = 1;
01192             break;
01193         }
01194         break;
01195       case 3:
01196         switch (right) {
01197           case 0:
01198             result = 1;
01199             break;
01200           case 1:
01201             result = 1;
01202             break;
01203           case 2:
01204             result = 1;
01205             break;
01206           case 3:
01207             result = 2;
01208             break;
01209         }
01210         break;
01211     }
01212     if (result == -1) throw new RuntimeException("Range01.neNoChoose(" + left + ", " + right + ") is undefined");
01213     return result;
01214   }  
01215   public static byte neSet(int leftTokens, int rightTokens) {
01216     byte result = -1;
01217     for (int left = 0; (1 << left) <= leftTokens; left++) {
01218       if ((leftTokens & (1 << left)) == 0) continue;
01219       for (int right = 0; (1 << right) <= rightTokens; right++) {
01220         if ((rightTokens & (1 << right)) != 0) {
01221           if (result == -1) result = neNoChoose(left, right);
01222           else result = Abstraction.meetTest(result, neNoChoose(left, right));
01223         }
01224       }
01225     }
01226     return result;
01227   }  
01228   public static int rem(int left$, int right$) {
01229     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01230     if (left$ == LT0 && right$ == R0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01231     if (left$ == LT0 && right$ == R1) return R0;
01232     if (left$ == LT0 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01233     if (left$ == R0 && right$ == LT0) return R0;
01234     if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01235     if (left$ == R0 && right$ == R1) return R0;
01236     if (left$ == R0 && right$ == GT1) return R0;
01237     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01238     if (left$ == R1 && right$ == R0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01239     if (left$ == R1 && right$ == R1) return R0;
01240     if (left$ == R1 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01241     if (left$ == GT1 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01242     if (left$ == GT1 && right$ == R0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01243     if (left$ == GT1 && right$ == R1) return R0;
01244     if (left$ == GT1 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01245     throw new RuntimeException("Range01.rem(" + left$ + ", " + right$ + ") is undefined");
01246   }  
01247   private static int remNoChoose(int left, int right) {
01248     int result = 0;
01249     switch (left) {
01250       case 0:
01251         switch (right) {
01252           case 0:
01253             result = 15;
01254             break;
01255           case 1:
01256             result = 1;
01257             break;
01258           case 2:
01259             result = 1;
01260             break;
01261           case 3:
01262             result = 1;
01263             break;
01264         }
01265         break;
01266       case 1:
01267         switch (right) {
01268           case 0:
01269             result = 15;
01270             break;
01271           case 1:
01272             result = 15;
01273             break;
01274           case 2:
01275             result = 1;
01276             break;
01277           case 3:
01278             result = 15;
01279             break;
01280         }
01281         break;
01282       case 2:
01283         switch (right) {
01284           case 0:
01285             result = 15;
01286             break;
01287           case 1:
01288             result = 15;
01289             break;
01290           case 2:
01291             result = 1;
01292             break;
01293           case 3:
01294             result = 15;
01295             break;
01296         }
01297         break;
01298       case 3:
01299         switch (right) {
01300           case 0:
01301             result = 15;
01302             break;
01303           case 1:
01304             result = 15;
01305             break;
01306           case 2:
01307             result = 1;
01308             break;
01309           case 3:
01310             result = 15;
01311             break;
01312         }
01313         break;
01314     }
01315     if (result == 0) throw new RuntimeException("Range01.remNoChoose(" + left + ", " + right + ") is undefined");
01316     return result;
01317   }  
01318   public static int remSet(int leftTokens, int rightTokens) {
01319     int result = -1;
01320     for (int left = 0; (1 << left) <= leftTokens; left++) {
01321       if ((leftTokens & (1 << left)) == 0) continue;
01322       for (int right = 0; (1 << right) <= rightTokens; right++) {
01323         if ((rightTokens & (1 << right)) != 0) {
01324           if (result == -1) result = remNoChoose(left, right);
01325           else result = Abstraction.meetArith(result, remNoChoose(left, right));
01326         }
01327       }
01328     }
01329     return result;
01330   }  
01331   public static int sub(int left$, int right$) {
01332     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01333     if (left$ == LT0 && right$ == R0) return LT0;
01334     if (left$ == LT0 && right$ == R1) return LT0;
01335     if (left$ == LT0 && right$ == GT1) return LT0;
01336     if (left$ == R0 && right$ == LT0) return Abstraction.choose((1 << GT1) | (1 << R1));
01337     if (left$ == R0 && right$ == R0) return R0;
01338     if (left$ == R0 && right$ == R1) return LT0;
01339     if (left$ == R0 && right$ == GT1) return LT0;
01340     if (left$ == R1 && right$ == LT0) return GT1;
01341     if (left$ == R1 && right$ == R0) return R1;
01342     if (left$ == R1 && right$ == R1) return R0;
01343     if (left$ == R1 && right$ == GT1) return LT0;
01344     if (left$ == GT1 && right$ == LT0) return GT1;
01345     if (left$ == GT1 && right$ == R0) return GT1;
01346     if (left$ == GT1 && right$ == R1) return Abstraction.choose((1 << GT1) | (1 << R1));
01347     if (left$ == GT1 && right$ == GT1) return Abstraction.choose((1 << GT1) | (1 << R1) | (1 << R0) | (1 << LT0));
01348     throw new RuntimeException("Range01.sub(" + left$ + ", " + right$ + ") is undefined");
01349   }  
01350   private static int subNoChoose(int left, int right) {
01351     int result = 0;
01352     switch (left) {
01353       case 0:
01354         switch (right) {
01355           case 0:
01356             result = 1;
01357             break;
01358           case 1:
01359             result = 12;
01360             break;
01361           case 2:
01362             result = 2;
01363             break;
01364           case 3:
01365             result = 2;
01366             break;
01367         }
01368         break;
01369       case 1:
01370         switch (right) {
01371           case 0:
01372             result = 2;
01373             break;
01374           case 1:
01375             result = 15;
01376             break;
01377           case 2:
01378             result = 2;
01379             break;
01380           case 3:
01381             result = 2;
01382             break;
01383         }
01384         break;
01385       case 2:
01386         switch (right) {
01387           case 0:
01388             result = 4;
01389             break;
01390           case 1:
01391             result = 8;
01392             break;
01393           case 2:
01394             result = 1;
01395             break;
01396           case 3:
01397             result = 2;
01398             break;
01399         }
01400         break;
01401       case 3:
01402         switch (right) {
01403           case 0:
01404             result = 8;
01405             break;
01406           case 1:
01407             result = 8;
01408             break;
01409           case 2:
01410             result = 12;
01411             break;
01412           case 3:
01413             result = 15;
01414             break;
01415         }
01416         break;
01417     }
01418     if (result == 0) throw new RuntimeException("Range01.subNoChoose(" + left + ", " + right + ") is undefined");
01419     return result;
01420   }  
01421   public static int subSet(int leftTokens, int rightTokens) {
01422     int result = -1;
01423     for (int left = 0; (1 << left) <= leftTokens; left++) {
01424       if ((leftTokens & (1 << left)) == 0) continue;
01425       for (int right = 0; (1 << right) <= rightTokens; right++) {
01426         if ((rightTokens & (1 << right)) != 0) {
01427           if (result == -1) result = subNoChoose(left, right);
01428           else result = Abstraction.meetArith(result, subNoChoose(left, right));
01429         }
01430       }
01431     }
01432     return result;
01433   }  
01434   public String toString() {
01435     return getName();
01436   }  
01437   public static Range01 v() {
01438     return v;
01439   }  
01440 }