Set0.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 Set0 extends IntegralAbstraction {
00039   private static final Set0 v = new Set0();
00040   public static final int R0 = 0;
00041   public static final int REST = 1;
00042   private Set0() {
00043   }  
00044   public static int abs(long n) {
00045     if (n == 0) return R0;
00046     if (n != 0) return REST;
00047     throw new RuntimeException("Set0 cannot abstract value '" + n + "'");
00048   }  
00049   public static int add(int left$, int right$) {
00050     if (left$ == R0 && right$ == R0) return R0;
00051     if (left$ == R0 && right$ == REST) return REST;
00052     if (left$ == REST && right$ == R0) return REST;
00053     if (left$ == REST && right$ == REST) return Abstraction.choose((1 << R0) | (1 << REST));
00054     throw new RuntimeException("Set0.add(" + left$ + ", " + right$ + ") is undefined");
00055   }  
00056   private static int addNoChoose(int left, int right) {
00057     int result = 0;
00058     switch (left) {
00059       case 0:
00060         switch (right) {
00061           case 0:
00062             result = 1;
00063             break;
00064           case 1:
00065             result = 2;
00066             break;
00067         }
00068         break;
00069       case 1:
00070         switch (right) {
00071           case 0:
00072             result = 2;
00073             break;
00074           case 1:
00075             result = 3;
00076             break;
00077         }
00078         break;
00079     }
00080     if (result == 0) throw new RuntimeException("Set0.addNoChoose(" + left + ", " + right + ") is undefined");
00081     return result;
00082   }  
00083   public static int addSet(int leftTokens, int rightTokens) {
00084     int result = -1;
00085     for (int left = 0; (1 << left) <= leftTokens; left++) {
00086       if ((leftTokens & (1 << left)) == 0) continue;
00087       for (int right = 0; (1 << right) <= rightTokens; right++) {
00088         if ((rightTokens & (1 << right)) != 0) {
00089           if (result == -1) result = addNoChoose(left, right);
00090           else result = Abstraction.meetArith(result, addNoChoose(left, right));
00091         }
00092       }
00093     }
00094     return result;
00095   }  
00096   public static int div(int left$, int right$) {
00097     if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << R0) | (1 << REST));
00098     if (left$ == R0 && right$ == REST) return R0;
00099     if (left$ == REST && right$ == R0) return Abstraction.choose((1 << R0) | (1 << REST));
00100     if (left$ == REST && right$ == REST) return Abstraction.choose((1 << R0) | (1 << REST));
00101     throw new RuntimeException("Set0.div(" + left$ + ", " + right$ + ") is undefined");
00102   }  
00103   private static int divNoChoose(int left, int right) {
00104     int result = 0;
00105     switch (left) {
00106       case 0:
00107         switch (right) {
00108           case 0:
00109             result = 3;
00110             break;
00111           case 1:
00112             result = 1;
00113             break;
00114         }
00115         break;
00116       case 1:
00117         switch (right) {
00118           case 0:
00119             result = 3;
00120             break;
00121           case 1:
00122             result = 3;
00123             break;
00124         }
00125         break;
00126     }
00127     if (result == 0) throw new RuntimeException("Set0.divNoChoose(" + left + ", " + right + ") is undefined");
00128     return result;
00129   }  
00130   public static int divSet(int leftTokens, int rightTokens) {
00131     int result = -1;
00132     for (int left = 0; (1 << left) <= leftTokens; left++) {
00133       if ((leftTokens & (1 << left)) == 0) continue;
00134       for (int right = 0; (1 << right) <= rightTokens; right++) {
00135         if ((rightTokens & (1 << right)) != 0) {
00136           if (result == -1) result = divNoChoose(left, right);
00137           else result = Abstraction.meetArith(result, divNoChoose(left, right));
00138         }
00139       }
00140     }
00141     return result;
00142   }  
00143   public static boolean eq(int left$, int right$) {
00144     if (left$ == R0 && right$ == R0) return true;
00145     if (left$ == R0 && right$ == REST) return false;
00146     if (left$ == REST && right$ == R0) return false;
00147     if (left$ == REST && right$ == REST) return Abstraction.choose();
00148     throw new RuntimeException("Set0.eq(" + left$ + ", " + right$ + ") is undefined");
00149   }  
00150   private static byte eqNoChoose(int left, int right) {
00151     byte result = -1;
00152     switch (left) {
00153       case 0:
00154         switch (right) {
00155           case 0:
00156             result = 1;
00157             break;
00158           case 1:
00159             result = 0;
00160             break;
00161         }
00162         break;
00163       case 1:
00164         switch (right) {
00165           case 0:
00166             result = 0;
00167             break;
00168           case 1:
00169             result = 2;
00170             break;
00171         }
00172         break;
00173     }
00174     if (result == -1) throw new RuntimeException("Set0.eqNoChoose(" + left + ", " + right + ") is undefined");
00175     return result;
00176   }  
00177   public static byte eqSet(int leftTokens, int rightTokens) {
00178     byte result = -1;
00179     for (int left = 0; (1 << left) <= leftTokens; left++) {
00180       if ((leftTokens & (1 << left)) == 0) continue;
00181       for (int right = 0; (1 << right) <= rightTokens; right++) {
00182         if ((rightTokens & (1 << right)) != 0) {
00183           if (result == -1) result = eqNoChoose(left, right);
00184           else result = Abstraction.meetTest(result, eqNoChoose(left, right));
00185         }
00186       }
00187     }
00188     return result;
00189   }  
00190   public static boolean ge(int left$, int right$) {
00191     if (left$ == R0 && right$ == R0) return true;
00192     if (left$ == R0 && right$ == REST) return Abstraction.choose();
00193     if (left$ == REST && right$ == R0) return Abstraction.choose();
00194     if (left$ == REST && right$ == REST) return Abstraction.choose();
00195     throw new RuntimeException("Set0.ge(" + left$ + ", " + right$ + ") is undefined");
00196   }  
00197   private static byte geNoChoose(int left, int right) {
00198     byte result = -1;
00199     switch (left) {
00200       case 0:
00201         switch (right) {
00202           case 0:
00203             result = 1;
00204             break;
00205           case 1:
00206             result = 2;
00207             break;
00208         }
00209         break;
00210       case 1:
00211         switch (right) {
00212           case 0:
00213             result = 2;
00214             break;
00215           case 1:
00216             result = 2;
00217             break;
00218         }
00219         break;
00220     }
00221     if (result == -1) throw new RuntimeException("Set0.geNoChoose(" + left + ", " + right + ") is undefined");
00222     return result;
00223   }  
00224   public static byte geSet(int leftTokens, int rightTokens) {
00225     byte result = -1;
00226     for (int left = 0; (1 << left) <= leftTokens; left++) {
00227       if ((leftTokens & (1 << left)) == 0) continue;
00228       for (int right = 0; (1 << right) <= rightTokens; right++) {
00229         if ((rightTokens & (1 << right)) != 0) {
00230           if (result == -1) result = geNoChoose(left, right);
00231           else result = Abstraction.meetTest(result, geNoChoose(left, right));
00232         }
00233       }
00234     }
00235     return result;
00236   }  
00237   public static String getBASLRepresentation() {
00238     return
00239       "abstraction Set0 extends integral \n"
00240       + "  begin\n"
00241       + "    TOKENS = {R0, REST};\n"
00242       + "    DEFAULT = R0;\n"
00243       + "    ONE2ONE = {R0};\n"
00244       + "    abstract (n)\n"
00245       + "      begin\n"
00246       + "        n == 0 -> R0;\n"
00247       + "        n != 0 -> REST;\n"
00248       + "      end\n"
00249       + "    operator + add \n"
00250       + "      begin\n"
00251       + "        (R0, R0) -> R0;\n"
00252       + "        (R0, REST) -> REST;\n"
00253       + "        (REST, R0) -> REST;\n"
00254       + "        (REST, REST) -> {R0, REST};\n"
00255       + "      end\n"
00256       + "    operator - sub \n"
00257       + "      begin\n"
00258       + "        (R0, R0) -> R0;\n"
00259       + "        (R0, REST) -> REST;\n"
00260       + "        (REST, R0) -> REST;\n"
00261       + "        (REST, REST) -> {R0, REST};\n"
00262       + "      end\n"
00263       + "    operator * mul \n"
00264       + "      begin\n"
00265       + "        (R0, R0) -> R0;\n"
00266       + "        (R0, REST) -> R0;\n"
00267       + "        (REST, R0) -> R0;\n"
00268       + "        (REST, REST) -> REST;\n"
00269       + "      end\n"
00270       + "    operator / div \n"
00271       + "      begin\n"
00272       + "        (R0, R0) -> T;\n"
00273       + "        (R0, REST) -> R0;\n"
00274       + "        (REST, R0) -> T;\n"
00275       + "        (REST, REST) -> {R0, REST};\n"
00276       + "      end\n"
00277       + "    operator % rem \n"
00278       + "      begin\n"
00279       + "        (R0, R0) -> T;\n"
00280       + "        (R0, REST) -> R0;\n"
00281       + "        (REST, R0) -> T;\n"
00282       + "        (REST, REST) -> {R0, REST};\n"
00283       + "      end\n"
00284       + "    test == eq \n"
00285       + "      begin\n"
00286       + "        (R0, R0) -> TRUE;\n"
00287       + "        (R0, REST) -> FALSE;\n"
00288       + "        (REST, R0) -> FALSE;\n"
00289       + "        (REST, REST) -> {TRUE, FALSE};\n"
00290       + "      end\n"
00291       + "    test != neq \n"
00292       + "      begin\n"
00293       + "        (R0, R0) -> FALSE;\n"
00294       + "        (R0, REST) -> TRUE;\n"
00295       + "        (REST, R0) -> TRUE;\n"
00296       + "        (REST, REST) -> {TRUE, FALSE};\n"
00297       + "      end\n"
00298       + "    test < lt \n"
00299       + "      begin\n"
00300       + "        (R0, R0) -> FALSE;\n"
00301       + "        (R0, REST) -> {TRUE, FALSE};\n"
00302       + "        (REST, R0) -> {TRUE, FALSE};\n"
00303       + "        (REST, REST) -> {TRUE, FALSE};\n"
00304       + "      end\n"
00305       + "    test <= le \n"
00306       + "      begin\n"
00307       + "        (R0, R0) -> TRUE;\n"
00308       + "        (R0, REST) -> {TRUE, FALSE};\n"
00309       + "        (REST, R0) -> {TRUE, FALSE};\n"
00310       + "        (REST, REST) -> {TRUE, FALSE};\n"
00311       + "      end\n"
00312       + "    test > gt \n"
00313       + "      begin\n"
00314       + "        (R0, R0) -> FALSE;\n"
00315       + "        (R0, REST) -> {TRUE, FALSE};\n"
00316       + "        (REST, R0) -> {TRUE, FALSE};\n"
00317       + "        (REST, REST) -> {TRUE, FALSE};\n"
00318       + "      end\n"
00319       + "    test >= ge \n"
00320       + "      begin\n"
00321       + "        (R0, R0) -> TRUE;\n"
00322       + "        (R0, REST) -> {TRUE, FALSE};\n"
00323       + "        (REST, R0) -> {TRUE, FALSE};\n"
00324       + "        (REST, REST) -> {TRUE, FALSE};\n"
00325       + "      end\n"
00326       + "  end\n"
00327     ;
00328   }  
00329   public static String getName() {
00330     return "Set0";
00331   }  
00332   public static int getNumOfTokens() {
00333     return 2;
00334   }  
00335   public static String getToken(int value) {
00336     switch(value) {
00337       case R0: return "Set0.R0";
00338       case REST: return "Set0.REST";
00339     }
00340     return "Set0.???";
00341   }  
00342   public static boolean gt(int left$, int right$) {
00343     if (left$ == R0 && right$ == R0) return false;
00344     if (left$ == R0 && right$ == REST) return Abstraction.choose();
00345     if (left$ == REST && right$ == R0) return Abstraction.choose();
00346     if (left$ == REST && right$ == REST) return Abstraction.choose();
00347     throw new RuntimeException("Set0.gt(" + left$ + ", " + right$ + ") is undefined");
00348   }  
00349   private static byte gtNoChoose(int left, int right) {
00350     byte result = -1;
00351     switch (left) {
00352       case 0:
00353         switch (right) {
00354           case 0:
00355             result = 0;
00356             break;
00357           case 1:
00358             result = 2;
00359             break;
00360         }
00361         break;
00362       case 1:
00363         switch (right) {
00364           case 0:
00365             result = 2;
00366             break;
00367           case 1:
00368             result = 2;
00369             break;
00370         }
00371         break;
00372     }
00373     if (result == -1) throw new RuntimeException("Set0.gtNoChoose(" + left + ", " + right + ") is undefined");
00374     return result;
00375   }  
00376   public static byte gtSet(int leftTokens, int rightTokens) {
00377     byte result = -1;
00378     for (int left = 0; (1 << left) <= leftTokens; left++) {
00379       if ((leftTokens & (1 << left)) == 0) continue;
00380       for (int right = 0; (1 << right) <= rightTokens; right++) {
00381         if ((rightTokens & (1 << right)) != 0) {
00382           if (result == -1) result = gtNoChoose(left, right);
00383           else result = Abstraction.meetTest(result, gtNoChoose(left, right));
00384         }
00385       }
00386     }
00387     return result;
00388   }  
00389   public static boolean isOne2One(int value) {
00390     switch(value) {
00391       case R0: return true;
00392     }
00393     return false;
00394   }  
00395   public static boolean le(int left$, int right$) {
00396     if (left$ == R0 && right$ == R0) return true;
00397     if (left$ == R0 && right$ == REST) return Abstraction.choose();
00398     if (left$ == REST && right$ == R0) return Abstraction.choose();
00399     if (left$ == REST && right$ == REST) return Abstraction.choose();
00400     throw new RuntimeException("Set0.le(" + left$ + ", " + right$ + ") is undefined");
00401   }  
00402   private static byte leNoChoose(int left, int right) {
00403     byte result = -1;
00404     switch (left) {
00405       case 0:
00406         switch (right) {
00407           case 0:
00408             result = 1;
00409             break;
00410           case 1:
00411             result = 2;
00412             break;
00413         }
00414         break;
00415       case 1:
00416         switch (right) {
00417           case 0:
00418             result = 2;
00419             break;
00420           case 1:
00421             result = 2;
00422             break;
00423         }
00424         break;
00425     }
00426     if (result == -1) throw new RuntimeException("Set0.leNoChoose(" + left + ", " + right + ") is undefined");
00427     return result;
00428   }  
00429   public static byte leSet(int leftTokens, int rightTokens) {
00430     byte result = -1;
00431     for (int left = 0; (1 << left) <= leftTokens; left++) {
00432       if ((leftTokens & (1 << left)) == 0) continue;
00433       for (int right = 0; (1 << right) <= rightTokens; right++) {
00434         if ((rightTokens & (1 << right)) != 0) {
00435           if (result == -1) result = leNoChoose(left, right);
00436           else result = Abstraction.meetTest(result, leNoChoose(left, right));
00437         }
00438       }
00439     }
00440     return result;
00441   }  
00442   public static boolean lt(int left$, int right$) {
00443     if (left$ == R0 && right$ == R0) return false;
00444     if (left$ == R0 && right$ == REST) return Abstraction.choose();
00445     if (left$ == REST && right$ == R0) return Abstraction.choose();
00446     if (left$ == REST && right$ == REST) return Abstraction.choose();
00447     throw new RuntimeException("Set0.lt(" + left$ + ", " + right$ + ") is undefined");
00448   }  
00449   private static byte ltNoChoose(int left, int right) {
00450     byte result = -1;
00451     switch (left) {
00452       case 0:
00453         switch (right) {
00454           case 0:
00455             result = 0;
00456             break;
00457           case 1:
00458             result = 2;
00459             break;
00460         }
00461         break;
00462       case 1:
00463         switch (right) {
00464           case 0:
00465             result = 2;
00466             break;
00467           case 1:
00468             result = 2;
00469             break;
00470         }
00471         break;
00472     }
00473     if (result == -1) throw new RuntimeException("Set0.ltNoChoose(" + left + ", " + right + ") is undefined");
00474     return result;
00475   }  
00476   public static byte ltSet(int leftTokens, int rightTokens) {
00477     byte result = -1;
00478     for (int left = 0; (1 << left) <= leftTokens; left++) {
00479       if ((leftTokens & (1 << left)) == 0) continue;
00480       for (int right = 0; (1 << right) <= rightTokens; right++) {
00481         if ((rightTokens & (1 << right)) != 0) {
00482           if (result == -1) result = ltNoChoose(left, right);
00483           else result = Abstraction.meetTest(result, ltNoChoose(left, right));
00484         }
00485       }
00486     }
00487     return result;
00488   }  
00489   public static int mul(int left$, int right$) {
00490     if (left$ == R0 && right$ == R0) return R0;
00491     if (left$ == R0 && right$ == REST) return R0;
00492     if (left$ == REST && right$ == R0) return R0;
00493     if (left$ == REST && right$ == REST) return REST;
00494     throw new RuntimeException("Set0.mul(" + left$ + ", " + right$ + ") is undefined");
00495   }  
00496   private static int mulNoChoose(int left, int right) {
00497     int result = 0;
00498     switch (left) {
00499       case 0:
00500         switch (right) {
00501           case 0:
00502             result = 1;
00503             break;
00504           case 1:
00505             result = 1;
00506             break;
00507         }
00508         break;
00509       case 1:
00510         switch (right) {
00511           case 0:
00512             result = 1;
00513             break;
00514           case 1:
00515             result = 2;
00516             break;
00517         }
00518         break;
00519     }
00520     if (result == 0) throw new RuntimeException("Set0.mulNoChoose(" + left + ", " + right + ") is undefined");
00521     return result;
00522   }  
00523   public static int mulSet(int leftTokens, int rightTokens) {
00524     int result = -1;
00525     for (int left = 0; (1 << left) <= leftTokens; left++) {
00526       if ((leftTokens & (1 << left)) == 0) continue;
00527       for (int right = 0; (1 << right) <= rightTokens; right++) {
00528         if ((rightTokens & (1 << right)) != 0) {
00529           if (result == -1) result = mulNoChoose(left, right);
00530           else result = Abstraction.meetArith(result, mulNoChoose(left, right));
00531         }
00532       }
00533     }
00534     return result;
00535   }  
00536   public static boolean ne(int left$, int right$) {
00537     if (left$ == R0 && right$ == R0) return false;
00538     if (left$ == R0 && right$ == REST) return true;
00539     if (left$ == REST && right$ == R0) return true;
00540     if (left$ == REST && right$ == REST) return Abstraction.choose();
00541     throw new RuntimeException("Set0.ne(" + left$ + ", " + right$ + ") is undefined");
00542   }  
00543   private static byte neNoChoose(int left, int right) {
00544     byte result = -1;
00545     switch (left) {
00546       case 0:
00547         switch (right) {
00548           case 0:
00549             result = 0;
00550             break;
00551           case 1:
00552             result = 1;
00553             break;
00554         }
00555         break;
00556       case 1:
00557         switch (right) {
00558           case 0:
00559             result = 1;
00560             break;
00561           case 1:
00562             result = 2;
00563             break;
00564         }
00565         break;
00566     }
00567     if (result == -1) throw new RuntimeException("Set0.neNoChoose(" + left + ", " + right + ") is undefined");
00568     return result;
00569   }  
00570   public static byte neSet(int leftTokens, int rightTokens) {
00571     byte result = -1;
00572     for (int left = 0; (1 << left) <= leftTokens; left++) {
00573       if ((leftTokens & (1 << left)) == 0) continue;
00574       for (int right = 0; (1 << right) <= rightTokens; right++) {
00575         if ((rightTokens & (1 << right)) != 0) {
00576           if (result == -1) result = neNoChoose(left, right);
00577           else result = Abstraction.meetTest(result, neNoChoose(left, right));
00578         }
00579       }
00580     }
00581     return result;
00582   }  
00583   public static int rem(int left$, int right$) {
00584     if (left$ == R0 && right$ == R0) return Abstraction.choose((1 << R0) | (1 << REST));
00585     if (left$ == R0 && right$ == REST) return R0;
00586     if (left$ == REST && right$ == R0) return Abstraction.choose((1 << R0) | (1 << REST));
00587     if (left$ == REST && right$ == REST) return Abstraction.choose((1 << R0) | (1 << REST));
00588     throw new RuntimeException("Set0.rem(" + left$ + ", " + right$ + ") is undefined");
00589   }  
00590   private static int remNoChoose(int left, int right) {
00591     int result = 0;
00592     switch (left) {
00593       case 0:
00594         switch (right) {
00595           case 0:
00596             result = 3;
00597             break;
00598           case 1:
00599             result = 1;
00600             break;
00601         }
00602         break;
00603       case 1:
00604         switch (right) {
00605           case 0:
00606             result = 3;
00607             break;
00608           case 1:
00609             result = 3;
00610             break;
00611         }
00612         break;
00613     }
00614     if (result == 0) throw new RuntimeException("Set0.remNoChoose(" + left + ", " + right + ") is undefined");
00615     return result;
00616   }  
00617   public static int remSet(int leftTokens, int rightTokens) {
00618     int result = -1;
00619     for (int left = 0; (1 << left) <= leftTokens; left++) {
00620       if ((leftTokens & (1 << left)) == 0) continue;
00621       for (int right = 0; (1 << right) <= rightTokens; right++) {
00622         if ((rightTokens & (1 << right)) != 0) {
00623           if (result == -1) result = remNoChoose(left, right);
00624           else result = Abstraction.meetArith(result, remNoChoose(left, right));
00625         }
00626       }
00627     }
00628     return result;
00629   }  
00630   public static int sub(int left$, int right$) {
00631     if (left$ == R0 && right$ == R0) return R0;
00632     if (left$ == R0 && right$ == REST) return REST;
00633     if (left$ == REST && right$ == R0) return REST;
00634     if (left$ == REST && right$ == REST) return Abstraction.choose((1 << R0) | (1 << REST));
00635     throw new RuntimeException("Set0.sub(" + left$ + ", " + right$ + ") is undefined");
00636   }  
00637   private static int subNoChoose(int left, int right) {
00638     int result = 0;
00639     switch (left) {
00640       case 0:
00641         switch (right) {
00642           case 0:
00643             result = 1;
00644             break;
00645           case 1:
00646             result = 2;
00647             break;
00648         }
00649         break;
00650       case 1:
00651         switch (right) {
00652           case 0:
00653             result = 2;
00654             break;
00655           case 1:
00656             result = 3;
00657             break;
00658         }
00659         break;
00660     }
00661     if (result == 0) throw new RuntimeException("Set0.subNoChoose(" + left + ", " + right + ") is undefined");
00662     return result;
00663   }  
00664   public static int subSet(int leftTokens, int rightTokens) {
00665     int result = -1;
00666     for (int left = 0; (1 << left) <= leftTokens; left++) {
00667       if ((leftTokens & (1 << left)) == 0) continue;
00668       for (int right = 0; (1 << right) <= rightTokens; right++) {
00669         if ((rightTokens & (1 << right)) != 0) {
00670           if (result == -1) result = subNoChoose(left, right);
00671           else result = Abstraction.meetArith(result, subNoChoose(left, right));
00672         }
00673       }
00674     }
00675     return result;
00676   }  
00677   public String toString() {
00678     return getName();
00679   }  
00680   public static Set0 v() {
00681     return v;
00682   }  
00683 }