Range02.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 Range02 extends IntegralAbstraction {
00039   private static final Range02 v = new Range02();
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 GT2 = 4;
00045   private Range02() {
00046   }  
00047   public static int abs(long n) {
00048     if (n < 0) return LT0;
00049     if (n == 0) return R0;
00050     if (n == 1) return R1;
00051     if (n == 2) return R2;
00052     if (n > 2) return GT2;
00053     throw new RuntimeException("Range02 cannot abstract value '" + n + "'");
00054   }  
00055   public static int add(int left$, int right$) {
00056     if (left$ == LT0 && right$ == LT0) return LT0;
00057     if (left$ == LT0 && right$ == R0) return LT0;
00058     if (left$ == LT0 && right$ == R1) return Abstraction.choose((1 << R0) | (1 << LT0));
00059     if (left$ == LT0 && right$ == R2) return Abstraction.choose((1 << R1) | (1 << R0) | (1 << LT0));
00060     if (left$ == LT0 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00061     if (left$ == R0 && right$ == LT0) return LT0;
00062     if (left$ == R0 && right$ == R0) return R0;
00063     if (left$ == R0 && right$ == R1) return R1;
00064     if (left$ == R0 && right$ == R2) return R2;
00065     if (left$ == R0 && right$ == GT2) return GT2;
00066     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << R0) | (1 << LT0));
00067     if (left$ == R1 && right$ == R0) return R1;
00068     if (left$ == R1 && right$ == R1) return R2;
00069     if (left$ == R1 && right$ == R2) return GT2;
00070     if (left$ == R1 && right$ == GT2) return GT2;
00071     if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << R1) | (1 << R0) | (1 << LT0));
00072     if (left$ == R2 && right$ == R0) return R2;
00073     if (left$ == R2 && right$ == R1) return GT2;
00074     if (left$ == R2 && right$ == R2) return GT2;
00075     if (left$ == R2 && right$ == GT2) return GT2;
00076     if (left$ == GT2 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00077     if (left$ == GT2 && right$ == R0) return GT2;
00078     if (left$ == GT2 && right$ == R1) return GT2;
00079     if (left$ == GT2 && right$ == R2) return GT2;
00080     if (left$ == GT2 && right$ == GT2) return GT2;
00081     throw new RuntimeException("Range02.add(" + left$ + ", " + right$ + ") is undefined");
00082   }  
00083   private static int addNoChoose(int left, int right) {
00084     int result = 0;
00085     switch (left) {
00086       case 0:
00087         switch (right) {
00088           case 0:
00089             result = 1;
00090             break;
00091           case 1:
00092             result = 2;
00093             break;
00094           case 2:
00095             result = 4;
00096             break;
00097           case 3:
00098             result = 8;
00099             break;
00100           case 4:
00101             result = 16;
00102             break;
00103         }
00104         break;
00105       case 1:
00106         switch (right) {
00107           case 0:
00108             result = 2;
00109             break;
00110           case 1:
00111             result = 2;
00112             break;
00113           case 2:
00114             result = 3;
00115             break;
00116           case 3:
00117             result = 7;
00118             break;
00119           case 4:
00120             result = 31;
00121             break;
00122         }
00123         break;
00124       case 2:
00125         switch (right) {
00126           case 0:
00127             result = 4;
00128             break;
00129           case 1:
00130             result = 3;
00131             break;
00132           case 2:
00133             result = 8;
00134             break;
00135           case 3:
00136             result = 16;
00137             break;
00138           case 4:
00139             result = 16;
00140             break;
00141         }
00142         break;
00143       case 3:
00144         switch (right) {
00145           case 0:
00146             result = 8;
00147             break;
00148           case 1:
00149             result = 7;
00150             break;
00151           case 2:
00152             result = 16;
00153             break;
00154           case 3:
00155             result = 16;
00156             break;
00157           case 4:
00158             result = 16;
00159             break;
00160         }
00161         break;
00162       case 4:
00163         switch (right) {
00164           case 0:
00165             result = 16;
00166             break;
00167           case 1:
00168             result = 31;
00169             break;
00170           case 2:
00171             result = 16;
00172             break;
00173           case 3:
00174             result = 16;
00175             break;
00176           case 4:
00177             result = 16;
00178             break;
00179         }
00180         break;
00181     }
00182     if (result == 0) throw new RuntimeException("Range02.addNoChoose(" + left + ", " + right + ") is undefined");
00183     return result;
00184   }  
00185   public static int addSet(int leftTokens, int rightTokens) {
00186     int result = -1;
00187     for (int left = 0; (1 << left) <= leftTokens; left++) {
00188       if ((leftTokens & (1 << left)) == 0) continue;
00189       for (int right = 0; (1 << right) <= rightTokens; right++) {
00190         if ((rightTokens & (1 << right)) != 0) {
00191           if (result == -1) result = addNoChoose(left, right);
00192           else result = Abstraction.meetArith(result, addNoChoose(left, right));
00193         }
00194       }
00195     }
00196     return result;
00197   }  
00198   public static int div(int left$, int right$) {
00199     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00200     if (left$ == LT0 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00201     if (left$ == LT0 && right$ == R1) return LT0;
00202     if (left$ == LT0 && right$ == R2) return LT0;
00203     if (left$ == LT0 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00204     if (left$ == R0 && right$ == LT0) return R0;
00205     if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00206     if (left$ == R0 && right$ == R1) return R0;
00207     if (left$ == R0 && right$ == R2) return R0;
00208     if (left$ == R0 && right$ == GT2) return R0;
00209     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00210     if (left$ == R1 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00211     if (left$ == R1 && right$ == R1) return R1;
00212     if (left$ == R1 && right$ == R2) return R0;
00213     if (left$ == R1 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00214     if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00215     if (left$ == R2 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00216     if (left$ == R2 && right$ == R1) return R2;
00217     if (left$ == R2 && right$ == R2) return R1;
00218     if (left$ == R2 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00219     if (left$ == GT2 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00220     if (left$ == GT2 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00221     if (left$ == GT2 && right$ == R1) return GT2;
00222     if (left$ == GT2 && right$ == R2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1));
00223     if (left$ == GT2 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
00224     throw new RuntimeException("Range02.div(" + left$ + ", " + right$ + ") is undefined");
00225   }  
00226   private static int divNoChoose(int left, int right) {
00227     int result = 0;
00228     switch (left) {
00229       case 0:
00230         switch (right) {
00231           case 0:
00232             result = 31;
00233             break;
00234           case 1:
00235             result = 1;
00236             break;
00237           case 2:
00238             result = 1;
00239             break;
00240           case 3:
00241             result = 1;
00242             break;
00243           case 4:
00244             result = 1;
00245             break;
00246         }
00247         break;
00248       case 1:
00249         switch (right) {
00250           case 0:
00251             result = 31;
00252             break;
00253           case 1:
00254             result = 31;
00255             break;
00256           case 2:
00257             result = 2;
00258             break;
00259           case 3:
00260             result = 2;
00261             break;
00262           case 4:
00263             result = 31;
00264             break;
00265         }
00266         break;
00267       case 2:
00268         switch (right) {
00269           case 0:
00270             result = 31;
00271             break;
00272           case 1:
00273             result = 31;
00274             break;
00275           case 2:
00276             result = 4;
00277             break;
00278           case 3:
00279             result = 1;
00280             break;
00281           case 4:
00282             result = 31;
00283             break;
00284         }
00285         break;
00286       case 3:
00287         switch (right) {
00288           case 0:
00289             result = 31;
00290             break;
00291           case 1:
00292             result = 31;
00293             break;
00294           case 2:
00295             result = 8;
00296             break;
00297           case 3:
00298             result = 4;
00299             break;
00300           case 4:
00301             result = 31;
00302             break;
00303         }
00304         break;
00305       case 4:
00306         switch (right) {
00307           case 0:
00308             result = 31;
00309             break;
00310           case 1:
00311             result = 31;
00312             break;
00313           case 2:
00314             result = 16;
00315             break;
00316           case 3:
00317             result = 28;
00318             break;
00319           case 4:
00320             result = 31;
00321             break;
00322         }
00323         break;
00324     }
00325     if (result == 0) throw new RuntimeException("Range02.divNoChoose(" + left + ", " + right + ") is undefined");
00326     return result;
00327   }  
00328   public static int divSet(int leftTokens, int rightTokens) {
00329     int result = -1;
00330     for (int left = 0; (1 << left) <= leftTokens; left++) {
00331       if ((leftTokens & (1 << left)) == 0) continue;
00332       for (int right = 0; (1 << right) <= rightTokens; right++) {
00333         if ((rightTokens & (1 << right)) != 0) {
00334           if (result == -1) result = divNoChoose(left, right);
00335           else result = Abstraction.meetArith(result, divNoChoose(left, right));
00336         }
00337       }
00338     }
00339     return result;
00340   }  
00341   public static boolean eq(int left$, int right$) {
00342     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00343     if (left$ == LT0 && right$ == R0) return false;
00344     if (left$ == LT0 && right$ == R1) return false;
00345     if (left$ == LT0 && right$ == R2) return false;
00346     if (left$ == LT0 && right$ == GT2) return false;
00347     if (left$ == R0 && right$ == LT0) return false;
00348     if (left$ == R0 && right$ == R0) return true;
00349     if (left$ == R0 && right$ == R1) return false;
00350     if (left$ == R0 && right$ == R2) return false;
00351     if (left$ == R0 && right$ == GT2) return false;
00352     if (left$ == R1 && right$ == LT0) return false;
00353     if (left$ == R1 && right$ == R0) return false;
00354     if (left$ == R1 && right$ == R1) return true;
00355     if (left$ == R1 && right$ == R2) return false;
00356     if (left$ == R1 && right$ == GT2) return false;
00357     if (left$ == R2 && right$ == LT0) return false;
00358     if (left$ == R2 && right$ == R0) return false;
00359     if (left$ == R2 && right$ == R1) return false;
00360     if (left$ == R2 && right$ == R2) return true;
00361     if (left$ == R2 && right$ == GT2) return false;
00362     if (left$ == GT2 && right$ == LT0) return false;
00363     if (left$ == GT2 && right$ == R0) return false;
00364     if (left$ == GT2 && right$ == R1) return false;
00365     if (left$ == GT2 && right$ == R2) return false;
00366     if (left$ == GT2 && right$ == GT2) return Abstraction.choose();
00367     throw new RuntimeException("Range02.eq(" + left$ + ", " + right$ + ") is undefined");
00368   }  
00369   private static byte eqNoChoose(int left, int right) {
00370     byte result = -1;
00371     switch (left) {
00372       case 0:
00373         switch (right) {
00374           case 0:
00375             result = 1;
00376             break;
00377           case 1:
00378             result = 0;
00379             break;
00380           case 2:
00381             result = 0;
00382             break;
00383           case 3:
00384             result = 0;
00385             break;
00386           case 4:
00387             result = 0;
00388             break;
00389         }
00390         break;
00391       case 1:
00392         switch (right) {
00393           case 0:
00394             result = 0;
00395             break;
00396           case 1:
00397             result = 2;
00398             break;
00399           case 2:
00400             result = 0;
00401             break;
00402           case 3:
00403             result = 0;
00404             break;
00405           case 4:
00406             result = 0;
00407             break;
00408         }
00409         break;
00410       case 2:
00411         switch (right) {
00412           case 0:
00413             result = 0;
00414             break;
00415           case 1:
00416             result = 0;
00417             break;
00418           case 2:
00419             result = 1;
00420             break;
00421           case 3:
00422             result = 0;
00423             break;
00424           case 4:
00425             result = 0;
00426             break;
00427         }
00428         break;
00429       case 3:
00430         switch (right) {
00431           case 0:
00432             result = 0;
00433             break;
00434           case 1:
00435             result = 0;
00436             break;
00437           case 2:
00438             result = 0;
00439             break;
00440           case 3:
00441             result = 1;
00442             break;
00443           case 4:
00444             result = 0;
00445             break;
00446         }
00447         break;
00448       case 4:
00449         switch (right) {
00450           case 0:
00451             result = 0;
00452             break;
00453           case 1:
00454             result = 0;
00455             break;
00456           case 2:
00457             result = 0;
00458             break;
00459           case 3:
00460             result = 0;
00461             break;
00462           case 4:
00463             result = 2;
00464             break;
00465         }
00466         break;
00467     }
00468     if (result == -1) throw new RuntimeException("Range02.eqNoChoose(" + left + ", " + right + ") is undefined");
00469     return result;
00470   }  
00471   public static byte eqSet(int leftTokens, int rightTokens) {
00472     byte result = -1;
00473     for (int left = 0; (1 << left) <= leftTokens; left++) {
00474       if ((leftTokens & (1 << left)) == 0) continue;
00475       for (int right = 0; (1 << right) <= rightTokens; right++) {
00476         if ((rightTokens & (1 << right)) != 0) {
00477           if (result == -1) result = eqNoChoose(left, right);
00478           else result = Abstraction.meetTest(result, eqNoChoose(left, right));
00479         }
00480       }
00481     }
00482     return result;
00483   }  
00484   public static boolean ge(int left$, int right$) {
00485     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00486     if (left$ == LT0 && right$ == R0) return false;
00487     if (left$ == LT0 && right$ == R1) return false;
00488     if (left$ == LT0 && right$ == R2) return false;
00489     if (left$ == LT0 && right$ == GT2) return false;
00490     if (left$ == R0 && right$ == LT0) return true;
00491     if (left$ == R0 && right$ == R0) return true;
00492     if (left$ == R0 && right$ == R1) return false;
00493     if (left$ == R0 && right$ == R2) return false;
00494     if (left$ == R0 && right$ == GT2) return false;
00495     if (left$ == R1 && right$ == LT0) return true;
00496     if (left$ == R1 && right$ == R0) return true;
00497     if (left$ == R1 && right$ == R1) return true;
00498     if (left$ == R1 && right$ == R2) return false;
00499     if (left$ == R1 && right$ == GT2) return false;
00500     if (left$ == R2 && right$ == LT0) return true;
00501     if (left$ == R2 && right$ == R0) return true;
00502     if (left$ == R2 && right$ == R1) return true;
00503     if (left$ == R2 && right$ == R2) return true;
00504     if (left$ == R2 && right$ == GT2) return false;
00505     if (left$ == GT2 && right$ == LT0) return true;
00506     if (left$ == GT2 && right$ == R0) return true;
00507     if (left$ == GT2 && right$ == R1) return true;
00508     if (left$ == GT2 && right$ == R2) return true;
00509     if (left$ == GT2 && right$ == GT2) return Abstraction.choose();
00510     throw new RuntimeException("Range02.ge(" + left$ + ", " + right$ + ") is undefined");
00511   }  
00512   private static byte geNoChoose(int left, int right) {
00513     byte result = -1;
00514     switch (left) {
00515       case 0:
00516         switch (right) {
00517           case 0:
00518             result = 1;
00519             break;
00520           case 1:
00521             result = 1;
00522             break;
00523           case 2:
00524             result = 0;
00525             break;
00526           case 3:
00527             result = 0;
00528             break;
00529           case 4:
00530             result = 0;
00531             break;
00532         }
00533         break;
00534       case 1:
00535         switch (right) {
00536           case 0:
00537             result = 0;
00538             break;
00539           case 1:
00540             result = 2;
00541             break;
00542           case 2:
00543             result = 0;
00544             break;
00545           case 3:
00546             result = 0;
00547             break;
00548           case 4:
00549             result = 0;
00550             break;
00551         }
00552         break;
00553       case 2:
00554         switch (right) {
00555           case 0:
00556             result = 1;
00557             break;
00558           case 1:
00559             result = 1;
00560             break;
00561           case 2:
00562             result = 1;
00563             break;
00564           case 3:
00565             result = 0;
00566             break;
00567           case 4:
00568             result = 0;
00569             break;
00570         }
00571         break;
00572       case 3:
00573         switch (right) {
00574           case 0:
00575             result = 1;
00576             break;
00577           case 1:
00578             result = 1;
00579             break;
00580           case 2:
00581             result = 1;
00582             break;
00583           case 3:
00584             result = 1;
00585             break;
00586           case 4:
00587             result = 0;
00588             break;
00589         }
00590         break;
00591       case 4:
00592         switch (right) {
00593           case 0:
00594             result = 1;
00595             break;
00596           case 1:
00597             result = 1;
00598             break;
00599           case 2:
00600             result = 1;
00601             break;
00602           case 3:
00603             result = 1;
00604             break;
00605           case 4:
00606             result = 2;
00607             break;
00608         }
00609         break;
00610     }
00611     if (result == -1) throw new RuntimeException("Range02.geNoChoose(" + left + ", " + right + ") is undefined");
00612     return result;
00613   }  
00614   public static byte geSet(int leftTokens, int rightTokens) {
00615     byte result = -1;
00616     for (int left = 0; (1 << left) <= leftTokens; left++) {
00617       if ((leftTokens & (1 << left)) == 0) continue;
00618       for (int right = 0; (1 << right) <= rightTokens; right++) {
00619         if ((rightTokens & (1 << right)) != 0) {
00620           if (result == -1) result = geNoChoose(left, right);
00621           else result = Abstraction.meetTest(result, geNoChoose(left, right));
00622         }
00623       }
00624     }
00625     return result;
00626   }  
00627   public static String getBASLRepresentation() {
00628     return
00629       "abstraction Range02 extends integral \n"
00630       + "  begin\n"
00631       + "    TOKENS = {LT0, R0, R1, R2, GT2};\n"
00632       + "    DEFAULT = R0;\n"
00633       + "    ONE2ONE = {R0, R1, R2};\n"
00634       + "    abstract (n)\n"
00635       + "      begin\n"
00636       + "        n < 0 -> LT0;\n"
00637       + "        n == 0 -> R0;\n"
00638       + "        n == 1 -> R1;\n"
00639       + "        n == 2 -> R2;\n"
00640       + "        n > 2 -> GT2;\n"
00641       + "      end\n"
00642       + "    operator + add \n"
00643       + "      begin\n"
00644       + "        (LT0, LT0) -> LT0;\n"
00645       + "        (LT0, R0) -> LT0;\n"
00646       + "        (LT0, R1) -> {LT0, R0};\n"
00647       + "        (LT0, R2) -> {LT0, R0, R1};\n"
00648       + "        (LT0, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00649       + "        (R0, LT0) -> LT0;\n"
00650       + "        (R0, R0) -> R0;\n"
00651       + "        (R0, R1) -> R1;\n"
00652       + "        (R0, R2) -> R2;\n"
00653       + "        (R0, GT2) -> GT2;\n"
00654       + "        (R1, LT0) -> {LT0, R0};\n"
00655       + "        (R1, R0) -> R1;\n"
00656       + "        (R1, R1) -> R2;\n"
00657       + "        (R1, R2) -> GT2;\n"
00658       + "        (R1, GT2) -> GT2;\n"
00659       + "        (R2, LT0) -> {LT0, R0, R1};\n"
00660       + "        (R2, R0) -> R2;\n"
00661       + "        (R2, R1) -> GT2;\n"
00662       + "        (R2, R2) -> GT2;\n"
00663       + "        (R2, GT2) -> GT2;\n"
00664       + "        (GT2, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00665       + "        (GT2, R0) -> GT2;\n"
00666       + "        (GT2, R1) -> GT2;\n"
00667       + "        (GT2, R2) -> GT2;\n"
00668       + "        (GT2, GT2) -> GT2;\n"
00669       + "      end\n"
00670       + "    operator - sub \n"
00671       + "      begin\n"
00672       + "        (LT0, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00673       + "        (LT0, R0) -> LT0;\n"
00674       + "        (LT0, R1) -> LT0;\n"
00675       + "        (LT0, R2) -> LT0;\n"
00676       + "        (LT0, GT2) -> LT0;\n"
00677       + "        (R0, LT0) -> {R1, R2, GT2};\n"
00678       + "        (R0, R0) -> R0;\n"
00679       + "        (R0, R1) -> LT0;\n"
00680       + "        (R0, R2) -> LT0;\n"
00681       + "        (R0, GT2) -> LT0;\n"
00682       + "        (R1, LT0) -> {R2, GT2};\n"
00683       + "        (R1, R0) -> R1;\n"
00684       + "        (R1, R1) -> R0;\n"
00685       + "        (R1, R2) -> LT0;\n"
00686       + "        (R1, GT2) -> LT0;\n"
00687       + "        (R2, LT0) -> GT2;\n"
00688       + "        (R2, R0) -> R2;\n"
00689       + "        (R2, R1) -> R1;\n"
00690       + "        (R2, R2) -> R0;\n"
00691       + "        (R2, GT2) -> LT0;\n"
00692       + "        (GT2, LT0) -> GT2;\n"
00693       + "        (GT2, R0) -> GT2;\n"
00694       + "        (GT2, R1) -> {R2, GT2};\n"
00695       + "        (GT2, R2) -> {R1, R2, GT2};\n"
00696       + "        (GT2, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00697       + "      end\n"
00698       + "    operator * mul \n"
00699       + "      begin\n"
00700       + "        (LT0, LT0) -> {R1, R2, GT2};\n"
00701       + "        (LT0, R0) -> R0;\n"
00702       + "        (LT0, R1) -> LT0;\n"
00703       + "        (LT0, R2) -> LT0;\n"
00704       + "        (LT0, GT2) -> {LT0, R1, R2, GT2};\n"
00705       + "        (R0, LT0) -> R0;\n"
00706       + "        (R0, R0) -> R0;\n"
00707       + "        (R0, R1) -> R0;\n"
00708       + "        (R0, R2) -> R0;\n"
00709       + "        (R0, GT2) -> R0;\n"
00710       + "        (R1, LT0) -> LT0;\n"
00711       + "        (R1, R0) -> R0;\n"
00712       + "        (R1, R1) -> R1;\n"
00713       + "        (R1, R2) -> R2;\n"
00714       + "        (R1, GT2) -> GT2;\n"
00715       + "        (R2, LT0) -> LT0;\n"
00716       + "        (R2, R0) -> R0;\n"
00717       + "        (R2, R1) -> R2;\n"
00718       + "        (R2, R2) -> GT2;\n"
00719       + "        (R2, GT2) -> GT2;\n"
00720       + "        (GT2, LT0) -> {LT0, R1, R2, GT2};\n"
00721       + "        (GT2, R0) -> R0;\n"
00722       + "        (GT2, R1) -> GT2;\n"
00723       + "        (GT2, R2) -> GT2;\n"
00724       + "        (GT2, GT2) -> {R1, R2, GT2};\n"
00725       + "      end\n"
00726       + "    operator / div \n"
00727       + "      begin\n"
00728       + "        (LT0, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00729       + "        (LT0, R0) -> T;\n"
00730       + "        (LT0, R1) -> LT0;\n"
00731       + "        (LT0, R2) -> LT0;\n"
00732       + "        (LT0, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00733       + "        (R0, LT0) -> R0;\n"
00734       + "        (R0, R0) -> T;\n"
00735       + "        (R0, R1) -> R0;\n"
00736       + "        (R0, R2) -> R0;\n"
00737       + "        (R0, GT2) -> R0;\n"
00738       + "        (R1, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00739       + "        (R1, R0) -> T;\n"
00740       + "        (R1, R1) -> R1;\n"
00741       + "        (R1, R2) -> R0;\n"
00742       + "        (R1, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00743       + "        (R2, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00744       + "        (R2, R0) -> T;\n"
00745       + "        (R2, R1) -> R2;\n"
00746       + "        (R2, R2) -> R1;\n"
00747       + "        (R2, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00748       + "        (GT2, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00749       + "        (GT2, R0) -> T;\n"
00750       + "        (GT2, R1) -> GT2;\n"
00751       + "        (GT2, R2) -> {R1, R2, GT2};\n"
00752       + "        (GT2, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00753       + "      end\n"
00754       + "    operator % rem \n"
00755       + "      begin\n"
00756       + "        (LT0, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00757       + "        (LT0, R0) -> T;\n"
00758       + "        (LT0, R1) -> R0;\n"
00759       + "        (LT0, R2) -> {R0, R1};\n"
00760       + "        (LT0, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00761       + "        (R0, LT0) -> R0;\n"
00762       + "        (R0, R0) -> T;\n"
00763       + "        (R0, R1) -> R0;\n"
00764       + "        (R0, R2) -> R0;\n"
00765       + "        (R0, GT2) -> R0;\n"
00766       + "        (R1, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00767       + "        (R1, R0) -> T;\n"
00768       + "        (R1, R1) -> R0;\n"
00769       + "        (R1, R2) -> R1;\n"
00770       + "        (R1, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00771       + "        (R2, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00772       + "        (R2, R0) -> T;\n"
00773       + "        (R2, R1) -> R0;\n"
00774       + "        (R2, R2) -> R0;\n"
00775       + "        (R2, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00776       + "        (GT2, LT0) -> {LT0, R0, R1, R2, GT2};\n"
00777       + "        (GT2, R0) -> T;\n"
00778       + "        (GT2, R1) -> R0;\n"
00779       + "        (GT2, R2) -> {R0, R1};\n"
00780       + "        (GT2, GT2) -> {LT0, R0, R1, R2, GT2};\n"
00781       + "      end\n"
00782       + "    test == eq \n"
00783       + "      begin\n"
00784       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00785       + "        (LT0, R0) -> FALSE;\n"
00786       + "        (LT0, R1) -> FALSE;\n"
00787       + "        (LT0, R2) -> FALSE;\n"
00788       + "        (LT0, GT2) -> FALSE;\n"
00789       + "        (R0, LT0) -> FALSE;\n"
00790       + "        (R0, R0) -> TRUE;\n"
00791       + "        (R0, R1) -> FALSE;\n"
00792       + "        (R0, R2) -> FALSE;\n"
00793       + "        (R0, GT2) -> FALSE;\n"
00794       + "        (R1, LT0) -> FALSE;\n"
00795       + "        (R1, R0) -> FALSE;\n"
00796       + "        (R1, R1) -> TRUE;\n"
00797       + "        (R1, R2) -> FALSE;\n"
00798       + "        (R1, GT2) -> FALSE;\n"
00799       + "        (R2, LT0) -> FALSE;\n"
00800       + "        (R2, R0) -> FALSE;\n"
00801       + "        (R2, R1) -> FALSE;\n"
00802       + "        (R2, R2) -> TRUE;\n"
00803       + "        (R2, GT2) -> FALSE;\n"
00804       + "        (GT2, LT0) -> FALSE;\n"
00805       + "        (GT2, R0) -> FALSE;\n"
00806       + "        (GT2, R1) -> FALSE;\n"
00807       + "        (GT2, R2) -> FALSE;\n"
00808       + "        (GT2, GT2) -> {TRUE, FALSE};\n"
00809       + "      end\n"
00810       + "    test != neq \n"
00811       + "      begin\n"
00812       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00813       + "        (LT0, R0) -> TRUE;\n"
00814       + "        (LT0, R1) -> TRUE;\n"
00815       + "        (LT0, R2) -> TRUE;\n"
00816       + "        (LT0, GT2) -> TRUE;\n"
00817       + "        (R0, LT0) -> TRUE;\n"
00818       + "        (R0, R0) -> FALSE;\n"
00819       + "        (R0, R1) -> TRUE;\n"
00820       + "        (R0, R2) -> TRUE;\n"
00821       + "        (R0, GT2) -> TRUE;\n"
00822       + "        (R1, LT0) -> TRUE;\n"
00823       + "        (R1, R0) -> TRUE;\n"
00824       + "        (R1, R1) -> FALSE;\n"
00825       + "        (R1, R2) -> TRUE;\n"
00826       + "        (R1, GT2) -> TRUE;\n"
00827       + "        (R2, LT0) -> TRUE;\n"
00828       + "        (R2, R0) -> TRUE;\n"
00829       + "        (R2, R1) -> TRUE;\n"
00830       + "        (R2, R2) -> FALSE;\n"
00831       + "        (R2, GT2) -> TRUE;\n"
00832       + "        (GT2, LT0) -> TRUE;\n"
00833       + "        (GT2, R0) -> TRUE;\n"
00834       + "        (GT2, R1) -> TRUE;\n"
00835       + "        (GT2, R2) -> TRUE;\n"
00836       + "        (GT2, GT2) -> {TRUE, FALSE};\n"
00837       + "      end\n"
00838       + "    test < lt \n"
00839       + "      begin\n"
00840       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00841       + "        (LT0, R0) -> TRUE;\n"
00842       + "        (LT0, R1) -> TRUE;\n"
00843       + "        (LT0, R2) -> TRUE;\n"
00844       + "        (LT0, GT2) -> TRUE;\n"
00845       + "        (R0, LT0) -> FALSE;\n"
00846       + "        (R0, R0) -> FALSE;\n"
00847       + "        (R0, R1) -> TRUE;\n"
00848       + "        (R0, R2) -> TRUE;\n"
00849       + "        (R0, GT2) -> TRUE;\n"
00850       + "        (R1, LT0) -> FALSE;\n"
00851       + "        (R1, R0) -> FALSE;\n"
00852       + "        (R1, R1) -> FALSE;\n"
00853       + "        (R1, R2) -> TRUE;\n"
00854       + "        (R1, GT2) -> TRUE;\n"
00855       + "        (R2, LT0) -> FALSE;\n"
00856       + "        (R2, R0) -> FALSE;\n"
00857       + "        (R2, R1) -> FALSE;\n"
00858       + "        (R2, R2) -> FALSE;\n"
00859       + "        (R2, GT2) -> TRUE;\n"
00860       + "        (GT2, LT0) -> FALSE;\n"
00861       + "        (GT2, R0) -> FALSE;\n"
00862       + "        (GT2, R1) -> FALSE;\n"
00863       + "        (GT2, R2) -> FALSE;\n"
00864       + "        (GT2, GT2) -> {TRUE, FALSE};\n"
00865       + "      end\n"
00866       + "    test <= le \n"
00867       + "      begin\n"
00868       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00869       + "        (LT0, R0) -> TRUE;\n"
00870       + "        (LT0, R1) -> TRUE;\n"
00871       + "        (LT0, R2) -> TRUE;\n"
00872       + "        (LT0, GT2) -> TRUE;\n"
00873       + "        (R0, LT0) -> FALSE;\n"
00874       + "        (R0, R0) -> TRUE;\n"
00875       + "        (R0, R1) -> TRUE;\n"
00876       + "        (R0, R2) -> TRUE;\n"
00877       + "        (R0, GT2) -> TRUE;\n"
00878       + "        (R1, LT0) -> FALSE;\n"
00879       + "        (R1, R0) -> FALSE;\n"
00880       + "        (R1, R1) -> TRUE;\n"
00881       + "        (R1, R2) -> TRUE;\n"
00882       + "        (R1, GT2) -> TRUE;\n"
00883       + "        (R2, LT0) -> FALSE;\n"
00884       + "        (R2, R0) -> FALSE;\n"
00885       + "        (R2, R1) -> FALSE;\n"
00886       + "        (R2, R2) -> TRUE;\n"
00887       + "        (R2, GT2) -> TRUE;\n"
00888       + "        (GT2, LT0) -> FALSE;\n"
00889       + "        (GT2, R0) -> FALSE;\n"
00890       + "        (GT2, R1) -> FALSE;\n"
00891       + "        (GT2, R2) -> FALSE;\n"
00892       + "        (GT2, GT2) -> {TRUE, FALSE};\n"
00893       + "      end\n"
00894       + "    test > gt \n"
00895       + "      begin\n"
00896       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00897       + "        (LT0, R0) -> FALSE;\n"
00898       + "        (LT0, R1) -> FALSE;\n"
00899       + "        (LT0, R2) -> FALSE;\n"
00900       + "        (LT0, GT2) -> FALSE;\n"
00901       + "        (R0, LT0) -> TRUE;\n"
00902       + "        (R0, R0) -> FALSE;\n"
00903       + "        (R0, R1) -> FALSE;\n"
00904       + "        (R0, R2) -> FALSE;\n"
00905       + "        (R0, GT2) -> FALSE;\n"
00906       + "        (R1, LT0) -> TRUE;\n"
00907       + "        (R1, R0) -> TRUE;\n"
00908       + "        (R1, R1) -> FALSE;\n"
00909       + "        (R1, R2) -> FALSE;\n"
00910       + "        (R1, GT2) -> FALSE;\n"
00911       + "        (R2, LT0) -> TRUE;\n"
00912       + "        (R2, R0) -> TRUE;\n"
00913       + "        (R2, R1) -> TRUE;\n"
00914       + "        (R2, R2) -> FALSE;\n"
00915       + "        (R2, GT2) -> FALSE;\n"
00916       + "        (GT2, LT0) -> TRUE;\n"
00917       + "        (GT2, R0) -> TRUE;\n"
00918       + "        (GT2, R1) -> TRUE;\n"
00919       + "        (GT2, R2) -> TRUE;\n"
00920       + "        (GT2, GT2) -> {TRUE, FALSE};\n"
00921       + "      end\n"
00922       + "    test >= ge \n"
00923       + "      begin\n"
00924       + "        (LT0, LT0) -> {TRUE, FALSE};\n"
00925       + "        (LT0, R0) -> FALSE;\n"
00926       + "        (LT0, R1) -> FALSE;\n"
00927       + "        (LT0, R2) -> FALSE;\n"
00928       + "        (LT0, GT2) -> FALSE;\n"
00929       + "        (R0, LT0) -> TRUE;\n"
00930       + "        (R0, R0) -> TRUE;\n"
00931       + "        (R0, R1) -> FALSE;\n"
00932       + "        (R0, R2) -> FALSE;\n"
00933       + "        (R0, GT2) -> FALSE;\n"
00934       + "        (R1, LT0) -> TRUE;\n"
00935       + "        (R1, R0) -> TRUE;\n"
00936       + "        (R1, R1) -> TRUE;\n"
00937       + "        (R1, R2) -> FALSE;\n"
00938       + "        (R1, GT2) -> FALSE;\n"
00939       + "        (R2, LT0) -> TRUE;\n"
00940       + "        (R2, R0) -> TRUE;\n"
00941       + "        (R2, R1) -> TRUE;\n"
00942       + "        (R2, R2) -> TRUE;\n"
00943       + "        (R2, GT2) -> FALSE;\n"
00944       + "        (GT2, LT0) -> TRUE;\n"
00945       + "        (GT2, R0) -> TRUE;\n"
00946       + "        (GT2, R1) -> TRUE;\n"
00947       + "        (GT2, R2) -> TRUE;\n"
00948       + "        (GT2, GT2) -> {TRUE, FALSE};\n"
00949       + "      end\n"
00950       + "  end\n"
00951     ;
00952   }  
00953   public static String getName() {
00954     return "Range02";
00955   }  
00956   public static int getNumOfTokens() {
00957     return 5;
00958   }  
00959   public static String getToken(int value) {
00960     switch(value) {
00961       case R0: return "Range02.R0";
00962       case LT0: return "Range02.LT0";
00963       case R1: return "Range02.R1";
00964       case R2: return "Range02.R2";
00965       case GT2: return "Range02.GT2";
00966     }
00967     return "Range02.???";
00968   }  
00969   public static boolean gt(int left$, int right$) {
00970     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
00971     if (left$ == LT0 && right$ == R0) return false;
00972     if (left$ == LT0 && right$ == R1) return false;
00973     if (left$ == LT0 && right$ == R2) return false;
00974     if (left$ == LT0 && right$ == GT2) return false;
00975     if (left$ == R0 && right$ == LT0) return true;
00976     if (left$ == R0 && right$ == R0) return false;
00977     if (left$ == R0 && right$ == R1) return false;
00978     if (left$ == R0 && right$ == R2) return false;
00979     if (left$ == R0 && right$ == GT2) return false;
00980     if (left$ == R1 && right$ == LT0) return true;
00981     if (left$ == R1 && right$ == R0) return true;
00982     if (left$ == R1 && right$ == R1) return false;
00983     if (left$ == R1 && right$ == R2) return false;
00984     if (left$ == R1 && right$ == GT2) return false;
00985     if (left$ == R2 && right$ == LT0) return true;
00986     if (left$ == R2 && right$ == R0) return true;
00987     if (left$ == R2 && right$ == R1) return true;
00988     if (left$ == R2 && right$ == R2) return false;
00989     if (left$ == R2 && right$ == GT2) return false;
00990     if (left$ == GT2 && right$ == LT0) return true;
00991     if (left$ == GT2 && right$ == R0) return true;
00992     if (left$ == GT2 && right$ == R1) return true;
00993     if (left$ == GT2 && right$ == R2) return true;
00994     if (left$ == GT2 && right$ == GT2) return Abstraction.choose();
00995     throw new RuntimeException("Range02.gt(" + left$ + ", " + right$ + ") is undefined");
00996   }  
00997   private static byte gtNoChoose(int left, int right) {
00998     byte result = -1;
00999     switch (left) {
01000       case 0:
01001         switch (right) {
01002           case 0:
01003             result = 0;
01004             break;
01005           case 1:
01006             result = 1;
01007             break;
01008           case 2:
01009             result = 0;
01010             break;
01011           case 3:
01012             result = 0;
01013             break;
01014           case 4:
01015             result = 0;
01016             break;
01017         }
01018         break;
01019       case 1:
01020         switch (right) {
01021           case 0:
01022             result = 0;
01023             break;
01024           case 1:
01025             result = 2;
01026             break;
01027           case 2:
01028             result = 0;
01029             break;
01030           case 3:
01031             result = 0;
01032             break;
01033           case 4:
01034             result = 0;
01035             break;
01036         }
01037         break;
01038       case 2:
01039         switch (right) {
01040           case 0:
01041             result = 1;
01042             break;
01043           case 1:
01044             result = 1;
01045             break;
01046           case 2:
01047             result = 0;
01048             break;
01049           case 3:
01050             result = 0;
01051             break;
01052           case 4:
01053             result = 0;
01054             break;
01055         }
01056         break;
01057       case 3:
01058         switch (right) {
01059           case 0:
01060             result = 1;
01061             break;
01062           case 1:
01063             result = 1;
01064             break;
01065           case 2:
01066             result = 1;
01067             break;
01068           case 3:
01069             result = 0;
01070             break;
01071           case 4:
01072             result = 0;
01073             break;
01074         }
01075         break;
01076       case 4:
01077         switch (right) {
01078           case 0:
01079             result = 1;
01080             break;
01081           case 1:
01082             result = 1;
01083             break;
01084           case 2:
01085             result = 1;
01086             break;
01087           case 3:
01088             result = 1;
01089             break;
01090           case 4:
01091             result = 2;
01092             break;
01093         }
01094         break;
01095     }
01096     if (result == -1) throw new RuntimeException("Range02.gtNoChoose(" + left + ", " + right + ") is undefined");
01097     return result;
01098   }  
01099   public static byte gtSet(int leftTokens, int rightTokens) {
01100     byte result = -1;
01101     for (int left = 0; (1 << left) <= leftTokens; left++) {
01102       if ((leftTokens & (1 << left)) == 0) continue;
01103       for (int right = 0; (1 << right) <= rightTokens; right++) {
01104         if ((rightTokens & (1 << right)) != 0) {
01105           if (result == -1) result = gtNoChoose(left, right);
01106           else result = Abstraction.meetTest(result, gtNoChoose(left, right));
01107         }
01108       }
01109     }
01110     return result;
01111   }  
01112   public static boolean isOne2One(int value) {
01113     switch(value) {
01114       case R2: return true;
01115       case R1: return true;
01116       case R0: return true;
01117     }
01118     return false;
01119   }  
01120   public static boolean le(int left$, int right$) {
01121     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
01122     if (left$ == LT0 && right$ == R0) return true;
01123     if (left$ == LT0 && right$ == R1) return true;
01124     if (left$ == LT0 && right$ == R2) return true;
01125     if (left$ == LT0 && right$ == GT2) return true;
01126     if (left$ == R0 && right$ == LT0) return false;
01127     if (left$ == R0 && right$ == R0) return true;
01128     if (left$ == R0 && right$ == R1) return true;
01129     if (left$ == R0 && right$ == R2) return true;
01130     if (left$ == R0 && right$ == GT2) return true;
01131     if (left$ == R1 && right$ == LT0) return false;
01132     if (left$ == R1 && right$ == R0) return false;
01133     if (left$ == R1 && right$ == R1) return true;
01134     if (left$ == R1 && right$ == R2) return true;
01135     if (left$ == R1 && right$ == GT2) return true;
01136     if (left$ == R2 && right$ == LT0) return false;
01137     if (left$ == R2 && right$ == R0) return false;
01138     if (left$ == R2 && right$ == R1) return false;
01139     if (left$ == R2 && right$ == R2) return true;
01140     if (left$ == R2 && right$ == GT2) return true;
01141     if (left$ == GT2 && right$ == LT0) return false;
01142     if (left$ == GT2 && right$ == R0) return false;
01143     if (left$ == GT2 && right$ == R1) return false;
01144     if (left$ == GT2 && right$ == R2) return false;
01145     if (left$ == GT2 && right$ == GT2) return Abstraction.choose();
01146     throw new RuntimeException("Range02.le(" + left$ + ", " + right$ + ") is undefined");
01147   }  
01148   private static byte leNoChoose(int left, int right) {
01149     byte result = -1;
01150     switch (left) {
01151       case 0:
01152         switch (right) {
01153           case 0:
01154             result = 1;
01155             break;
01156           case 1:
01157             result = 0;
01158             break;
01159           case 2:
01160             result = 1;
01161             break;
01162           case 3:
01163             result = 1;
01164             break;
01165           case 4:
01166             result = 1;
01167             break;
01168         }
01169         break;
01170       case 1:
01171         switch (right) {
01172           case 0:
01173             result = 1;
01174             break;
01175           case 1:
01176             result = 2;
01177             break;
01178           case 2:
01179             result = 1;
01180             break;
01181           case 3:
01182             result = 1;
01183             break;
01184           case 4:
01185             result = 1;
01186             break;
01187         }
01188         break;
01189       case 2:
01190         switch (right) {
01191           case 0:
01192             result = 0;
01193             break;
01194           case 1:
01195             result = 0;
01196             break;
01197           case 2:
01198             result = 1;
01199             break;
01200           case 3:
01201             result = 1;
01202             break;
01203           case 4:
01204             result = 1;
01205             break;
01206         }
01207         break;
01208       case 3:
01209         switch (right) {
01210           case 0:
01211             result = 0;
01212             break;
01213           case 1:
01214             result = 0;
01215             break;
01216           case 2:
01217             result = 0;
01218             break;
01219           case 3:
01220             result = 1;
01221             break;
01222           case 4:
01223             result = 1;
01224             break;
01225         }
01226         break;
01227       case 4:
01228         switch (right) {
01229           case 0:
01230             result = 0;
01231             break;
01232           case 1:
01233             result = 0;
01234             break;
01235           case 2:
01236             result = 0;
01237             break;
01238           case 3:
01239             result = 0;
01240             break;
01241           case 4:
01242             result = 2;
01243             break;
01244         }
01245         break;
01246     }
01247     if (result == -1) throw new RuntimeException("Range02.leNoChoose(" + left + ", " + right + ") is undefined");
01248     return result;
01249   }  
01250   public static byte leSet(int leftTokens, int rightTokens) {
01251     byte result = -1;
01252     for (int left = 0; (1 << left) <= leftTokens; left++) {
01253       if ((leftTokens & (1 << left)) == 0) continue;
01254       for (int right = 0; (1 << right) <= rightTokens; right++) {
01255         if ((rightTokens & (1 << right)) != 0) {
01256           if (result == -1) result = leNoChoose(left, right);
01257           else result = Abstraction.meetTest(result, leNoChoose(left, right));
01258         }
01259       }
01260     }
01261     return result;
01262   }  
01263   public static boolean lt(int left$, int right$) {
01264     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
01265     if (left$ == LT0 && right$ == R0) return true;
01266     if (left$ == LT0 && right$ == R1) return true;
01267     if (left$ == LT0 && right$ == R2) return true;
01268     if (left$ == LT0 && right$ == GT2) return true;
01269     if (left$ == R0 && right$ == LT0) return false;
01270     if (left$ == R0 && right$ == R0) return false;
01271     if (left$ == R0 && right$ == R1) return true;
01272     if (left$ == R0 && right$ == R2) return true;
01273     if (left$ == R0 && right$ == GT2) return true;
01274     if (left$ == R1 && right$ == LT0) return false;
01275     if (left$ == R1 && right$ == R0) return false;
01276     if (left$ == R1 && right$ == R1) return false;
01277     if (left$ == R1 && right$ == R2) return true;
01278     if (left$ == R1 && right$ == GT2) return true;
01279     if (left$ == R2 && right$ == LT0) return false;
01280     if (left$ == R2 && right$ == R0) return false;
01281     if (left$ == R2 && right$ == R1) return false;
01282     if (left$ == R2 && right$ == R2) return false;
01283     if (left$ == R2 && right$ == GT2) return true;
01284     if (left$ == GT2 && right$ == LT0) return false;
01285     if (left$ == GT2 && right$ == R0) return false;
01286     if (left$ == GT2 && right$ == R1) return false;
01287     if (left$ == GT2 && right$ == R2) return false;
01288     if (left$ == GT2 && right$ == GT2) return Abstraction.choose();
01289     throw new RuntimeException("Range02.lt(" + left$ + ", " + right$ + ") is undefined");
01290   }  
01291   private static byte ltNoChoose(int left, int right) {
01292     byte result = -1;
01293     switch (left) {
01294       case 0:
01295         switch (right) {
01296           case 0:
01297             result = 0;
01298             break;
01299           case 1:
01300             result = 0;
01301             break;
01302           case 2:
01303             result = 1;
01304             break;
01305           case 3:
01306             result = 1;
01307             break;
01308           case 4:
01309             result = 1;
01310             break;
01311         }
01312         break;
01313       case 1:
01314         switch (right) {
01315           case 0:
01316             result = 1;
01317             break;
01318           case 1:
01319             result = 2;
01320             break;
01321           case 2:
01322             result = 1;
01323             break;
01324           case 3:
01325             result = 1;
01326             break;
01327           case 4:
01328             result = 1;
01329             break;
01330         }
01331         break;
01332       case 2:
01333         switch (right) {
01334           case 0:
01335             result = 0;
01336             break;
01337           case 1:
01338             result = 0;
01339             break;
01340           case 2:
01341             result = 0;
01342             break;
01343           case 3:
01344             result = 1;
01345             break;
01346           case 4:
01347             result = 1;
01348             break;
01349         }
01350         break;
01351       case 3:
01352         switch (right) {
01353           case 0:
01354             result = 0;
01355             break;
01356           case 1:
01357             result = 0;
01358             break;
01359           case 2:
01360             result = 0;
01361             break;
01362           case 3:
01363             result = 0;
01364             break;
01365           case 4:
01366             result = 1;
01367             break;
01368         }
01369         break;
01370       case 4:
01371         switch (right) {
01372           case 0:
01373             result = 0;
01374             break;
01375           case 1:
01376             result = 0;
01377             break;
01378           case 2:
01379             result = 0;
01380             break;
01381           case 3:
01382             result = 0;
01383             break;
01384           case 4:
01385             result = 2;
01386             break;
01387         }
01388         break;
01389     }
01390     if (result == -1) throw new RuntimeException("Range02.ltNoChoose(" + left + ", " + right + ") is undefined");
01391     return result;
01392   }  
01393   public static byte ltSet(int leftTokens, int rightTokens) {
01394     byte result = -1;
01395     for (int left = 0; (1 << left) <= leftTokens; left++) {
01396       if ((leftTokens & (1 << left)) == 0) continue;
01397       for (int right = 0; (1 << right) <= rightTokens; right++) {
01398         if ((rightTokens & (1 << right)) != 0) {
01399           if (result == -1) result = ltNoChoose(left, right);
01400           else result = Abstraction.meetTest(result, ltNoChoose(left, right));
01401         }
01402       }
01403     }
01404     return result;
01405   }  
01406   public static int mul(int left$, int right$) {
01407     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1));
01408     if (left$ == LT0 && right$ == R0) return R0;
01409     if (left$ == LT0 && right$ == R1) return LT0;
01410     if (left$ == LT0 && right$ == R2) return LT0;
01411     if (left$ == LT0 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << LT0));
01412     if (left$ == R0 && right$ == LT0) return R0;
01413     if (left$ == R0 && right$ == R0) return R0;
01414     if (left$ == R0 && right$ == R1) return R0;
01415     if (left$ == R0 && right$ == R2) return R0;
01416     if (left$ == R0 && right$ == GT2) return R0;
01417     if (left$ == R1 && right$ == LT0) return LT0;
01418     if (left$ == R1 && right$ == R0) return R0;
01419     if (left$ == R1 && right$ == R1) return R1;
01420     if (left$ == R1 && right$ == R2) return R2;
01421     if (left$ == R1 && right$ == GT2) return GT2;
01422     if (left$ == R2 && right$ == LT0) return LT0;
01423     if (left$ == R2 && right$ == R0) return R0;
01424     if (left$ == R2 && right$ == R1) return R2;
01425     if (left$ == R2 && right$ == R2) return GT2;
01426     if (left$ == R2 && right$ == GT2) return GT2;
01427     if (left$ == GT2 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << LT0));
01428     if (left$ == GT2 && right$ == R0) return R0;
01429     if (left$ == GT2 && right$ == R1) return GT2;
01430     if (left$ == GT2 && right$ == R2) return GT2;
01431     if (left$ == GT2 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1));
01432     throw new RuntimeException("Range02.mul(" + left$ + ", " + right$ + ") is undefined");
01433   }  
01434   private static int mulNoChoose(int left, int right) {
01435     int result = 0;
01436     switch (left) {
01437       case 0:
01438         switch (right) {
01439           case 0:
01440             result = 1;
01441             break;
01442           case 1:
01443             result = 1;
01444             break;
01445           case 2:
01446             result = 1;
01447             break;
01448           case 3:
01449             result = 1;
01450             break;
01451           case 4:
01452             result = 1;
01453             break;
01454         }
01455         break;
01456       case 1:
01457         switch (right) {
01458           case 0:
01459             result = 1;
01460             break;
01461           case 1:
01462             result = 28;
01463             break;
01464           case 2:
01465             result = 2;
01466             break;
01467           case 3:
01468             result = 2;
01469             break;
01470           case 4:
01471             result = 30;
01472             break;
01473         }
01474         break;
01475       case 2:
01476         switch (right) {
01477           case 0:
01478             result = 1;
01479             break;
01480           case 1:
01481             result = 2;
01482             break;
01483           case 2:
01484             result = 4;
01485             break;
01486           case 3:
01487             result = 8;
01488             break;
01489           case 4:
01490             result = 16;
01491             break;
01492         }
01493         break;
01494       case 3:
01495         switch (right) {
01496           case 0:
01497             result = 1;
01498             break;
01499           case 1:
01500             result = 2;
01501             break;
01502           case 2:
01503             result = 8;
01504             break;
01505           case 3:
01506             result = 16;
01507             break;
01508           case 4:
01509             result = 16;
01510             break;
01511         }
01512         break;
01513       case 4:
01514         switch (right) {
01515           case 0:
01516             result = 1;
01517             break;
01518           case 1:
01519             result = 30;
01520             break;
01521           case 2:
01522             result = 16;
01523             break;
01524           case 3:
01525             result = 16;
01526             break;
01527           case 4:
01528             result = 28;
01529             break;
01530         }
01531         break;
01532     }
01533     if (result == 0) throw new RuntimeException("Range02.mulNoChoose(" + left + ", " + right + ") is undefined");
01534     return result;
01535   }  
01536   public static int mulSet(int leftTokens, int rightTokens) {
01537     int result = -1;
01538     for (int left = 0; (1 << left) <= leftTokens; left++) {
01539       if ((leftTokens & (1 << left)) == 0) continue;
01540       for (int right = 0; (1 << right) <= rightTokens; right++) {
01541         if ((rightTokens & (1 << right)) != 0) {
01542           if (result == -1) result = mulNoChoose(left, right);
01543           else result = Abstraction.meetArith(result, mulNoChoose(left, right));
01544         }
01545       }
01546     }
01547     return result;
01548   }  
01549   public static boolean ne(int left$, int right$) {
01550     if (left$ == LT0 && right$ == LT0) return Abstraction.choose();
01551     if (left$ == LT0 && right$ == R0) return true;
01552     if (left$ == LT0 && right$ == R1) return true;
01553     if (left$ == LT0 && right$ == R2) return true;
01554     if (left$ == LT0 && right$ == GT2) return true;
01555     if (left$ == R0 && right$ == LT0) return true;
01556     if (left$ == R0 && right$ == R0) return false;
01557     if (left$ == R0 && right$ == R1) return true;
01558     if (left$ == R0 && right$ == R2) return true;
01559     if (left$ == R0 && right$ == GT2) return true;
01560     if (left$ == R1 && right$ == LT0) return true;
01561     if (left$ == R1 && right$ == R0) return true;
01562     if (left$ == R1 && right$ == R1) return false;
01563     if (left$ == R1 && right$ == R2) return true;
01564     if (left$ == R1 && right$ == GT2) return true;
01565     if (left$ == R2 && right$ == LT0) return true;
01566     if (left$ == R2 && right$ == R0) return true;
01567     if (left$ == R2 && right$ == R1) return true;
01568     if (left$ == R2 && right$ == R2) return false;
01569     if (left$ == R2 && right$ == GT2) return true;
01570     if (left$ == GT2 && right$ == LT0) return true;
01571     if (left$ == GT2 && right$ == R0) return true;
01572     if (left$ == GT2 && right$ == R1) return true;
01573     if (left$ == GT2 && right$ == R2) return true;
01574     if (left$ == GT2 && right$ == GT2) return Abstraction.choose();
01575     throw new RuntimeException("Range02.ne(" + left$ + ", " + right$ + ") is undefined");
01576   }  
01577   private static byte neNoChoose(int left, int right) {
01578     byte result = -1;
01579     switch (left) {
01580       case 0:
01581         switch (right) {
01582           case 0:
01583             result = 0;
01584             break;
01585           case 1:
01586             result = 1;
01587             break;
01588           case 2:
01589             result = 1;
01590             break;
01591           case 3:
01592             result = 1;
01593             break;
01594           case 4:
01595             result = 1;
01596             break;
01597         }
01598         break;
01599       case 1:
01600         switch (right) {
01601           case 0:
01602             result = 1;
01603             break;
01604           case 1:
01605             result = 2;
01606             break;
01607           case 2:
01608             result = 1;
01609             break;
01610           case 3:
01611             result = 1;
01612             break;
01613           case 4:
01614             result = 1;
01615             break;
01616         }
01617         break;
01618       case 2:
01619         switch (right) {
01620           case 0:
01621             result = 1;
01622             break;
01623           case 1:
01624             result = 1;
01625             break;
01626           case 2:
01627             result = 0;
01628             break;
01629           case 3:
01630             result = 1;
01631             break;
01632           case 4:
01633             result = 1;
01634             break;
01635         }
01636         break;
01637       case 3:
01638         switch (right) {
01639           case 0:
01640             result = 1;
01641             break;
01642           case 1:
01643             result = 1;
01644             break;
01645           case 2:
01646             result = 1;
01647             break;
01648           case 3:
01649             result = 0;
01650             break;
01651           case 4:
01652             result = 1;
01653             break;
01654         }
01655         break;
01656       case 4:
01657         switch (right) {
01658           case 0:
01659             result = 1;
01660             break;
01661           case 1:
01662             result = 1;
01663             break;
01664           case 2:
01665             result = 1;
01666             break;
01667           case 3:
01668             result = 1;
01669             break;
01670           case 4:
01671             result = 2;
01672             break;
01673         }
01674         break;
01675     }
01676     if (result == -1) throw new RuntimeException("Range02.neNoChoose(" + left + ", " + right + ") is undefined");
01677     return result;
01678   }  
01679   public static byte neSet(int leftTokens, int rightTokens) {
01680     byte result = -1;
01681     for (int left = 0; (1 << left) <= leftTokens; left++) {
01682       if ((leftTokens & (1 << left)) == 0) continue;
01683       for (int right = 0; (1 << right) <= rightTokens; right++) {
01684         if ((rightTokens & (1 << right)) != 0) {
01685           if (result == -1) result = neNoChoose(left, right);
01686           else result = Abstraction.meetTest(result, neNoChoose(left, right));
01687         }
01688       }
01689     }
01690     return result;
01691   }  
01692   public static int rem(int left$, int right$) {
01693     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01694     if (left$ == LT0 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01695     if (left$ == LT0 && right$ == R1) return R0;
01696     if (left$ == LT0 && right$ == R2) return Abstraction.choose((1 << R1) | (1 << R0));
01697     if (left$ == LT0 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01698     if (left$ == R0 && right$ == LT0) return R0;
01699     if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01700     if (left$ == R0 && right$ == R1) return R0;
01701     if (left$ == R0 && right$ == R2) return R0;
01702     if (left$ == R0 && right$ == GT2) return R0;
01703     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01704     if (left$ == R1 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01705     if (left$ == R1 && right$ == R1) return R0;
01706     if (left$ == R1 && right$ == R2) return R1;
01707     if (left$ == R1 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01708     if (left$ == R2 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01709     if (left$ == R2 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01710     if (left$ == R2 && right$ == R1) return R0;
01711     if (left$ == R2 && right$ == R2) return R0;
01712     if (left$ == R2 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01713     if (left$ == GT2 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01714     if (left$ == GT2 && right$ == R0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01715     if (left$ == GT2 && right$ == R1) return R0;
01716     if (left$ == GT2 && right$ == R2) return Abstraction.choose((1 << R1) | (1 << R0));
01717     if (left$ == GT2 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01718     throw new RuntimeException("Range02.rem(" + left$ + ", " + right$ + ") is undefined");
01719   }  
01720   private static int remNoChoose(int left, int right) {
01721     int result = 0;
01722     switch (left) {
01723       case 0:
01724         switch (right) {
01725           case 0:
01726             result = 31;
01727             break;
01728           case 1:
01729             result = 1;
01730             break;
01731           case 2:
01732             result = 1;
01733             break;
01734           case 3:
01735             result = 1;
01736             break;
01737           case 4:
01738             result = 1;
01739             break;
01740         }
01741         break;
01742       case 1:
01743         switch (right) {
01744           case 0:
01745             result = 31;
01746             break;
01747           case 1:
01748             result = 31;
01749             break;
01750           case 2:
01751             result = 1;
01752             break;
01753           case 3:
01754             result = 5;
01755             break;
01756           case 4:
01757             result = 31;
01758             break;
01759         }
01760         break;
01761       case 2:
01762         switch (right) {
01763           case 0:
01764             result = 31;
01765             break;
01766           case 1:
01767             result = 31;
01768             break;
01769           case 2:
01770             result = 1;
01771             break;
01772           case 3:
01773             result = 4;
01774             break;
01775           case 4:
01776             result = 31;
01777             break;
01778         }
01779         break;
01780       case 3:
01781         switch (right) {
01782           case 0:
01783             result = 31;
01784             break;
01785           case 1:
01786             result = 31;
01787             break;
01788           case 2:
01789             result = 1;
01790             break;
01791           case 3:
01792             result = 1;
01793             break;
01794           case 4:
01795             result = 31;
01796             break;
01797         }
01798         break;
01799       case 4:
01800         switch (right) {
01801           case 0:
01802             result = 31;
01803             break;
01804           case 1:
01805             result = 31;
01806             break;
01807           case 2:
01808             result = 1;
01809             break;
01810           case 3:
01811             result = 5;
01812             break;
01813           case 4:
01814             result = 31;
01815             break;
01816         }
01817         break;
01818     }
01819     if (result == 0) throw new RuntimeException("Range02.remNoChoose(" + left + ", " + right + ") is undefined");
01820     return result;
01821   }  
01822   public static int remSet(int leftTokens, int rightTokens) {
01823     int result = -1;
01824     for (int left = 0; (1 << left) <= leftTokens; left++) {
01825       if ((leftTokens & (1 << left)) == 0) continue;
01826       for (int right = 0; (1 << right) <= rightTokens; right++) {
01827         if ((rightTokens & (1 << right)) != 0) {
01828           if (result == -1) result = remNoChoose(left, right);
01829           else result = Abstraction.meetArith(result, remNoChoose(left, right));
01830         }
01831       }
01832     }
01833     return result;
01834   }  
01835   public static int sub(int left$, int right$) {
01836     if (left$ == LT0 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01837     if (left$ == LT0 && right$ == R0) return LT0;
01838     if (left$ == LT0 && right$ == R1) return LT0;
01839     if (left$ == LT0 && right$ == R2) return LT0;
01840     if (left$ == LT0 && right$ == GT2) return LT0;
01841     if (left$ == R0 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1));
01842     if (left$ == R0 && right$ == R0) return R0;
01843     if (left$ == R0 && right$ == R1) return LT0;
01844     if (left$ == R0 && right$ == R2) return LT0;
01845     if (left$ == R0 && right$ == GT2) return LT0;
01846     if (left$ == R1 && right$ == LT0) return Abstraction.choose((1 << GT2) | (1 << R2));
01847     if (left$ == R1 && right$ == R0) return R1;
01848     if (left$ == R1 && right$ == R1) return R0;
01849     if (left$ == R1 && right$ == R2) return LT0;
01850     if (left$ == R1 && right$ == GT2) return LT0;
01851     if (left$ == R2 && right$ == LT0) return GT2;
01852     if (left$ == R2 && right$ == R0) return R2;
01853     if (left$ == R2 && right$ == R1) return R1;
01854     if (left$ == R2 && right$ == R2) return R0;
01855     if (left$ == R2 && right$ == GT2) return LT0;
01856     if (left$ == GT2 && right$ == LT0) return GT2;
01857     if (left$ == GT2 && right$ == R0) return GT2;
01858     if (left$ == GT2 && right$ == R1) return Abstraction.choose((1 << GT2) | (1 << R2));
01859     if (left$ == GT2 && right$ == R2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1));
01860     if (left$ == GT2 && right$ == GT2) return Abstraction.choose((1 << GT2) | (1 << R2) | (1 << R1) | (1 << R0) | (1 << LT0));
01861     throw new RuntimeException("Range02.sub(" + left$ + ", " + right$ + ") is undefined");
01862   }  
01863   private static int subNoChoose(int left, int right) {
01864     int result = 0;
01865     switch (left) {
01866       case 0:
01867         switch (right) {
01868           case 0:
01869             result = 1;
01870             break;
01871           case 1:
01872             result = 28;
01873             break;
01874           case 2:
01875             result = 2;
01876             break;
01877           case 3:
01878             result = 2;
01879             break;
01880           case 4:
01881             result = 2;
01882             break;
01883         }
01884         break;
01885       case 1:
01886         switch (right) {
01887           case 0:
01888             result = 2;
01889             break;
01890           case 1:
01891             result = 31;
01892             break;
01893           case 2:
01894             result = 2;
01895             break;
01896           case 3:
01897             result = 2;
01898             break;
01899           case 4:
01900             result = 2;
01901             break;
01902         }
01903         break;
01904       case 2:
01905         switch (right) {
01906           case 0:
01907             result = 4;
01908             break;
01909           case 1:
01910             result = 24;
01911             break;
01912           case 2:
01913             result = 1;
01914             break;
01915           case 3:
01916             result = 2;
01917             break;
01918           case 4:
01919             result = 2;
01920             break;
01921         }
01922         break;
01923       case 3:
01924         switch (right) {
01925           case 0:
01926             result = 8;
01927             break;
01928           case 1:
01929             result = 16;
01930             break;
01931           case 2:
01932             result = 4;
01933             break;
01934           case 3:
01935             result = 1;
01936             break;
01937           case 4:
01938             result = 2;
01939             break;
01940         }
01941         break;
01942       case 4:
01943         switch (right) {
01944           case 0:
01945             result = 16;
01946             break;
01947           case 1:
01948             result = 16;
01949             break;
01950           case 2:
01951             result = 24;
01952             break;
01953           case 3:
01954             result = 28;
01955             break;
01956           case 4:
01957             result = 31;
01958             break;
01959         }
01960         break;
01961     }
01962     if (result == 0) throw new RuntimeException("Range02.subNoChoose(" + left + ", " + right + ") is undefined");
01963     return result;
01964   }  
01965   public static int subSet(int leftTokens, int rightTokens) {
01966     int result = -1;
01967     for (int left = 0; (1 << left) <= leftTokens; left++) {
01968       if ((leftTokens & (1 << left)) == 0) continue;
01969       for (int right = 0; (1 << right) <= rightTokens; right++) {
01970         if ((rightTokens & (1 << right)) != 0) {
01971           if (result == -1) result = subNoChoose(left, right);
01972           else result = Abstraction.meetArith(result, subNoChoose(left, right));
01973         }
01974       }
01975     }
01976     return result;
01977   }  
01978   public String toString() {
01979     return getName();
01980   }  
01981   public static Range02 v() {
01982     return v;
01983   }  
01984 }