001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: // This file is part of KeY - Integrated Deductive Software Design
009: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof.init;
019:
020: import java.io.IOException;
021:
022: import de.uka.ilkd.key.proof.decproc.JavaDecisionProcedureTranslationFactory;
023: import de.uka.ilkd.key.rule.*;
024:
025: /** This class represents a standardized implementation of <tt>AbstractExecDecproc</tt>.
026: * <p>
027: * It checks the availability of a decision procedure by invoking it with one or zero command
028: * line arguments. Thereby a normal termination of execution is presumed, which, in most cases,
029: * can be reached by the use of a single command line argument.
030: * <p>
031: * All decicion procedures that can be treated in this way should be handled by this class
032: * <p>
033: * To modify the actual availability check, a hook for subclassing is provided by the
034: * <tt>isCurrentDecprocAvailable</tt> method
035: * @see #isCurrentDecprocAvailable(String, String)
036: * <p>
037: *
038: * @author akuwertz
039: * @version 1.0, 09/10/2006
040: */
041:
042: public class ConcreteExecDecproc extends AbstractExecDecproc {
043:
044: /* Attributes */
045:
046: /** <tt>Array</tt> containing the needed information for each decision procedure.
047: * That is the name of executable, the argument to be handed over and the rule to create,
048: * if the decision procedure is available */
049: private static final Object[][] decisionProcedures = {
050: /* If this class is extended by further decision procedures, this array also has to
051: be extended properly */
052: {
053: "Simplify",
054: "-help",
055: new SimplifyIntegerRule(
056: new JavaDecisionProcedureTranslationFactory()) },
057: {
058: "ics",
059: "-help",
060: new ICSIntegerRule(
061: new JavaDecisionProcedureTranslationFactory()) },
062: {
063: "cvcl",
064: "-help",
065: new CVCLiteIntegerRule(
066: new JavaDecisionProcedureTranslationFactory()) },
067: {
068: "cvc3",
069: "-help",
070: new CVC3IntegerRule(
071: new JavaDecisionProcedureTranslationFactory()) },
072: {
073: "yices",
074: "--help",
075: new YicesIntegerRule(
076: new JavaDecisionProcedureTranslationFactory()) }, };
077:
078: /** The command for the configured decision procedure to execute */
079: protected final String cmd;
080: /** The argument to be passed on execution */
081: protected final String arg;
082: /** The <tt>AbstractIntegerRule</tt> to be added to the <tt>ListOfBuiltInRule</tt>, if the
083: * configured decision procedure is available */
084: protected final AbstractIntegerRule rule;
085:
086: /** String constants representing error messages */
087: private static final String noDecprocForIndex = "No decision procedure exists for the given index!";
088: private static final String internalError = "An internal error occured: Expected an object of type String in decisionProcedure"
089: + " array at index ";
090: private static final String internalErrorRule = "An internal error occured: Expected an object of type Rule in decisionProcedure"
091: + " array at index ";
092:
093: /* Constructors */
094:
095: /** Explicit constructor. Creates a new <tt>ConcreteExecDecproc</tt> configured with one the
096: * internally stored decision procedures, choosen by the given integer index
097: * <tt>concreteDecproc</tt>
098: *
099: * @param concreteDecproc the integer index specifying the decision procedure this
100: * <tt>ConcreteExecDecproc</tt> should be configured with
101: */
102: public ConcreteExecDecproc(int concreteDecproc) {
103: if (concreteDecproc < 0
104: || concreteDecproc >= decisionProcedures.length)
105: throw new IllegalArgumentException(noDecprocForIndex);
106: Object helper = decisionProcedures[concreteDecproc][0];
107: if (helper instanceof String)
108: cmd = (String) helper;
109: else
110: throw new RuntimeException(internalError + concreteDecproc);
111: helper = decisionProcedures[concreteDecproc][1];
112: if (helper instanceof String)
113: arg = (String) helper;
114: else
115: throw new RuntimeException(internalError + concreteDecproc);
116: helper = decisionProcedures[concreteDecproc][2];
117: if (helper instanceof AbstractIntegerRule)
118: rule = (AbstractIntegerRule) helper;
119: else
120: throw new RuntimeException(internalErrorRule
121: + concreteDecproc);
122: }
123:
124: /* Public and private methods */
125:
126: /* (non-Javadoc)
127: * @see de.uka.ilkd.key.proof.init.AbstractExecDecproc#isAvailable()
128: */
129: public boolean isAvailable() {
130: return isCurrentDecprocAvailable(cmd, arg);
131: }
132:
133: /* (non-Javadoc)
134: * @see de.uka.ilkd.key.proof.init.AbstractExecDecproc#getRule()
135: */
136: public AbstractIntegerRule getRule() {
137: return rule;
138: }
139:
140: /** Returns the command for the configured decision procedure
141: * @return the command <tt>String </tt>for the configured decision procedure
142: */
143: public String getCmd() {
144: return cmd;
145: }
146:
147: /** Returns the number of elements in the decision procedure array
148: * @return the number of elements in the decision procedure array
149: */
150: public static int getDecprocNumber() {
151: return decisionProcedures.length;
152: }
153:
154: /** Checks if the given <tt>decisionProcedure</tt> is available by executing it with
155: * the given <tt>argument</tt>.<br>
156: * If the decision procedure does not terminate normally before a given timeout, it will
157: * be regarded as not available.
158: * <p>
159: * This method is protected so that subclasses can use it as a hook for doing a
160: * modified availability check
161: *
162: * @param decisionProcedure the String with the name of the executable
163: * @param argument a String to be handed over as an argument (in order to ensure
164: * normal termination of the procedure, e.g. Simplify would wait
165: * for input and not terminate)
166: * @return <tt>true</tt> if the decision procedure was found and could be executed properly
167: */
168: protected boolean isCurrentDecprocAvailable(
169: final String decisionProcedure, final String argument) {
170: boolean available = false;
171: Process process = null;
172: try {
173: process = Runtime.getRuntime().exec(
174: new String[] { decisionProcedure, argument });
175:
176: long start = System.currentTimeMillis();
177:
178: while (System.currentTimeMillis() - start < TIMEOUT) {
179: try {
180: available = process.exitValue() == 0;
181: } catch (IllegalThreadStateException itse) {
182: // process has not terminated yet
183: available = false;
184: continue;
185: }
186: break;
187: }
188: } catch (IOException e) {
189: available = false;
190: }
191:
192: return available;
193: }
194:
195: }
|