SpecificationAbstractor.java Source File

00001 package edu.ksu.cis.bandera.abstraction;
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 import edu.ksu.cis.bandera.abstraction.typeinference.*;
00037 import edu.ksu.cis.bandera.specification.nnf.*;
00038 import java.util.*;
00039 import ca.mcgill.sable.soot.*;
00040 import ca.mcgill.sable.soot.jimple.*;
00041 import ca.mcgill.sable.soot.grimp.*;
00042 public class SpecificationAbstractor {
00043     private Hashtable parameterTable;
00044     private String ltlFormula;
00045 /**
00046  * 
00047  * @param typeTable edu.ksu.cis.bandera.abstraction.typeinference.TypeTable
00048  * @param ltlFormula java.lang.String
00049  * @param parameterTable java.util.Hashtable
00050  */
00051 public void abstractLTL(CoercionManager cm, TypeTable typeTable, String ltlForm, Hashtable parameterTable) {
00052     ltlFormula = ltlForm;
00053     this.parameterTable = parameterTable;
00054     if (typeTable.size() == 0) return;
00055 
00056     ltlFormula = NNFTransformer.transformLTL(ltlFormula);
00057     for (Enumeration e = parameterTable.keys(); e.hasMoreElements();) {
00058         String p = (String) e.nextElement();
00059         if ("a".equals(p)) continue;
00060         Value pExp = (Value) parameterTable.get(p);
00061         String nP = "!" + p;
00062         String notP = "not_" + p;
00063         if (ltlFormula.indexOf(nP) >= 0) {
00064             parameterTable.put(notP, PredicateAbstractor.abs(cm, typeTable, PredicateTransformer.negate(pExp)));
00065             int idx;
00066             while((idx = ltlFormula.indexOf("!" + p)) >= 0) {
00067                 ltlFormula = ltlFormula.substring(0, idx) + notP + ltlFormula.substring(idx + nP.length());
00068             }       
00069         }
00070         parameterTable.put(p, PredicateAbstractor.abs(cm, typeTable, PredicateTransformer.pushComplement(pExp)));
00071     }
00072 }
00073 /**
00074  * 
00075  * @return java.lang.String
00076  */
00077 public java.lang.String getLtlFormula() {
00078     return ltlFormula;
00079 }
00080 /**
00081  * 
00082  * @return java.util.Hashtable
00083  */
00084 public java.util.Hashtable getParameterTable() {
00085     return parameterTable;
00086 }
00087 }