Commit 6db74eec authored by Daniel Ratiu's avatar Daniel Ratiu
Browse files

Issue #306: added documentation of packages.

parent 334484e3
......@@ -10,8 +10,10 @@ Bundle-RequiredExecutionEnvironment: JavaSE-1.6
Bundle-ActivationPolicy: lazy
Bundle-Activator: org.fortiss.af3.tools.ToolsActivator
Require-Bundle: org.fortiss.af3.project,
org.fortiss.af3.expression;bundle-version="1.0.0"
org.fortiss.af3.expression;bundle-version="1.0.0",
org.fortiss.af3.analyses;bundle-version="1.0.0"
Export-Package: org.fortiss.af3.tools,
org.fortiss.af3.tools.base,
org.fortiss.af3.tools.yices.model,
org.fortiss.af3.tools.yices.model.commands,
org.fortiss.af3.tools.yices.model.run,
......
......@@ -15,7 +15,7 @@ $Id: codetemplates.xml 1 2011-01-01 00:00:01Z hoelzl $
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.tools.yices.run;
package org.fortiss.af3.tools.base;
import java.util.concurrent.Future;
import java.util.concurrent.TimeUnit;
......
<!--
$Id: package.html 894 2011-07-07 07:36:03Z ratiu $
@version $Rev: 894 $
@ConQAT.Rating GREEN Hash: 9B508364648BA6EBEFA9C5CC2B173408
-->
<body>
This package contains base classes for the integration of external tools.
</body>
<!--
$Id: package.html 894 2011-07-07 07:36:03Z ratiu $
@version $Rev: 894 $
@ConQAT.Rating GREEN Hash: 9B508364648BA6EBEFA9C5CC2B173408
-->
<body>
Main plugin package for the AF3 tools.
</body>
<!--
$Id: package.html 894 2011-07-07 07:36:03Z ratiu $
@version $Rev: 894 $
@ConQAT.Rating GREEN Hash: 9B508364648BA6EBEFA9C5CC2B173408
-->
<body>
This package contains utility classes for manipulating and accessing the model of the Yices tool.
</body>
/*--------------------------------------------------------------------------+
$Id: YicesFile.java 1270 2011-08-29 08:55:46Z ratiu $
| |
| Copyright 2011 ForTISS GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.tools.yices.run;
/**
* Syntactic representation of the "assert" command.
*
* @author ratiu
* @author $Author: ratiu $
* @version $Rev: 1270 $
* @ConQAT.Rating GREEN Hash: 53A60236CE73FED796AAE4B9C90EC5EA
*/
@SuppressWarnings("serial")
public class UnknownLanguageFragmentException extends Exception {
public UnknownLanguageFragmentException(String msg) {
super(msg);
}
}
/*--------------------------------------------------------------------------+
$Id: IntType.java 1270 2011-08-29 08:55:46Z ratiu $
| |
| Copyright 2011 ForTISS GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.tools.yices.run;
import java.util.HashMap;
import java.util.Map;
/**
* Class for running Yices.
*
* @author ratiu
* @author $Author: ratiu $
* @version $Rev: 1270 $
* @ConQAT.Rating GREEN Hash: 745E401305D55EB353F3D826CF14DEA0
*/
class YicesResul {
/** Map variable names to their values. */
private Map<String, String> varName2Value = new HashMap<String, String>();
/** Flag whether result is satisfiable. */
private boolean satisfiable;
/** Constructor. */
public YicesResul(boolean satisfiable) {
this.satisfiable = satisfiable;
}
/** Returns true is the result is satisfiable. */
public boolean isSatisfiable() {
return satisfiable;
}
/** Adds variable name and value. */
public void addVarNameVarValue(String variableName, String variableValue) {
varName2Value.put(variableName, variableValue);
}
/** Returns variables and their values. */
public Map<String, String> getVarsAndVals() {
return varName2Value;
}
/** Returns the size of this evidence. */
public int getEvidenceSize() {
return varName2Value.size();
}
/** Returns the value of the variable. */
public String getValue(String variableName) {
return varName2Value.get(variableName);
}
}
......@@ -32,7 +32,9 @@ import java.util.concurrent.TimeUnit;
import java.util.concurrent.TimeoutException;
import org.eclipse.core.runtime.IPath;
import org.fortiss.af3.analyses.base.UnknownLanguageFragmentException;
import org.fortiss.af3.tools.ToolsActivator;
import org.fortiss.af3.tools.base.LazyResult;
import org.fortiss.af3.tools.yices.model.YicesFile;
import org.fortiss.af3.tools.yices.model.run.YicesResult;
import org.fortiss.af3.tools.yices.textgen.YicesTextGenerator;
......
<!--
$Id: package.html 894 2011-07-07 07:36:03Z ratiu $
@version $Rev: 894 $
@ConQAT.Rating GREEN Hash: 9B508364648BA6EBEFA9C5CC2B173408
-->
<body>
This package contains classes for running the Yices tool and collecting the result.
</body>
/*--------------------------------------------------------------------------+
$Id: YicesFile.java 1270 2011-08-29 08:55:46Z ratiu $
| |
| Copyright 2011 ForTISS GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.tools.yices.textgen;
import org.fortiss.af3.expression.language.evaluation.NoVal;
import org.fortiss.af3.expression.model.terms.BoolConst;
import org.fortiss.af3.expression.model.terms.DefinedConst;
import org.fortiss.af3.expression.model.terms.EOperator;
import org.fortiss.af3.expression.model.terms.FunctionCall;
import org.fortiss.af3.expression.model.terms.IntConst;
import org.fortiss.af3.expression.model.terms.PredefinedFunction;
import org.fortiss.af3.expression.model.terms.Var;
import org.fortiss.af3.expression.model.terms.impl.DefinedConstStaticImpl;
import org.fortiss.af3.expression.utils.ExpressionModelElementFactory;
import org.fortiss.af3.project.model.typesystem.IFunction;
import org.fortiss.af3.project.model.typesystem.ITerm;
import org.fortiss.af3.tools.yices.run.UnknownLanguageFragmentException;
/**
* Syntactic representation of the "assert" command.
*
* @author ratiu
* @author $Author: ratiu $
* @version $Rev: 1270 $
* @ConQAT.Rating GREEN Hash: 97A527905EF61FD94E4CB1C9CEEA91B6
*/
public class YicesTextGenerationUtils {
/** NoVal constant. */
private static final DefinedConst NoVal_Const = ExpressionModelElementFactory.createNoVal();
/** Converts an expression to string. */
public static String convertExpressionToString(ITerm term) throws UnknownLanguageFragmentException {
if (term instanceof BoolConst) {
return Boolean.toString(((BoolConst)term).isValue());
} else if (term instanceof IntConst) {
return Integer.toString(((IntConst)term).getValue());
} else if (term.equals(NoVal_Const)) {
return NoVal.NOVAL_STRING;
} else if (term instanceof FunctionCall) {
FunctionCall call = (FunctionCall)term;
IFunction func = call.getFunction();
if (func instanceof PredefinedFunction) {
StringBuffer sb = new StringBuffer("(");
EOperator op = ((PredefinedFunction) func).getOperator();
sb.append(getYicesString(op)).append(" ");
for(ITerm arg : call.getArguments()) {
sb.append(convertExpressionToString(arg)).append(" ");
}
sb.deleteCharAt(sb.length() - 1);
sb.append(")");
return sb.toString();
}
} else if (term instanceof Var) {
return ((Var)term).getIdentifier();
}
throw new UnknownLanguageFragmentException(term.toString());
}
/** Yices string representation of an EOperator */
private static String getYicesString(EOperator op) throws UnknownLanguageFragmentException {
switch (op) {
case ADD:
return "+";
case SUBTRACT:
return "-";
case MULTIPLY:
return "*";
case DIVIDE:
return "/";
case MODULO:
return "mod";
case AND:
return "and";
case OR:
return "or";
case NOT:
return "not";
case EQUAL:
return "=";
case NOT_EQUAL:
return "/=";
case GREATER_THAN:
return ">";
case GREATER_EQUAL:
return ">=";
case LOWER_THAN:
return "<";
case LOWER_EQUAL:
return "<=";
default:
break;
}
throw new UnknownLanguageFragmentException("Cannot transform operator to Yices: " + op);
}
}
......@@ -20,6 +20,18 @@ package org.fortiss.af3.tools.yices.textgen;
import java.io.IOException;
import java.io.Writer;
import org.fortiss.af3.analyses.base.UnknownLanguageFragmentException;
import org.fortiss.af3.expression.language.evaluation.NoVal;
import org.fortiss.af3.expression.model.terms.BoolConst;
import org.fortiss.af3.expression.model.terms.DefinedConst;
import org.fortiss.af3.expression.model.terms.EOperator;
import org.fortiss.af3.expression.model.terms.FunctionCall;
import org.fortiss.af3.expression.model.terms.IntConst;
import org.fortiss.af3.expression.model.terms.PredefinedFunction;
import org.fortiss.af3.expression.model.terms.Var;
import org.fortiss.af3.expression.utils.ExpressionModelElementFactory;
import org.fortiss.af3.project.model.typesystem.IFunction;
import org.fortiss.af3.project.model.typesystem.ITerm;
import org.fortiss.af3.tools.yices.model.ConstantDeclaration;
import org.fortiss.af3.tools.yices.model.YicesFile;
import org.fortiss.af3.tools.yices.model.YicesFileContent;
......@@ -33,10 +45,9 @@ import org.fortiss.af3.tools.yices.model.types.DefinedType;
import org.fortiss.af3.tools.yices.model.types.IntType;
import org.fortiss.af3.tools.yices.model.types.ScalarType;
import org.fortiss.af3.tools.yices.model.types.YicesTypeBase;
import org.fortiss.af3.tools.yices.run.UnknownLanguageFragmentException;
/**
* Generates Yices interpretable text from a Yices logical file. demo
* Generates Yices interpretable text from a Yices logical file.
*
* @author ratiu
* @author $Author: hoelzl $
......@@ -45,6 +56,10 @@ import org.fortiss.af3.tools.yices.run.UnknownLanguageFragmentException;
*/
public class YicesTextGenerator {
/** NoVal constant. */
private final DefinedConst NoVal_Const = ExpressionModelElementFactory
.createNoVal();
/** Text generator for Yices logical files. */
public void generateText(Writer w, YicesFile logical) throws IOException,
UnknownLanguageFragmentException {
......@@ -116,8 +131,7 @@ public class YicesTextGenerator {
private void generateText(Writer w, Assert assertCommand)
throws IOException, UnknownLanguageFragmentException {
w.append("(assert ");
w.append(YicesTextGenerationUtils
.convertExpressionToString(assertCommand.getExpression()));
w.append(convertExpressionToString(assertCommand.getExpression()));
w.append(")\n");
}
......@@ -125,9 +139,7 @@ public class YicesTextGenerator {
private void generateText(Writer w, ExtendedAssert extendedAssert)
throws IOException, UnknownLanguageFragmentException {
w.append("(assert+ "
+ YicesTextGenerationUtils
.convertExpressionToString(extendedAssert
.getExpression()));
+ convertExpressionToString(extendedAssert.getExpression()));
w.append(" " + extendedAssert.getWeight());
w.append(")\n");
}
......@@ -141,8 +153,75 @@ public class YicesTextGenerator {
generateText(w, defineSubtype.getType());
}
w.append(") ");
w.append(YicesTextGenerationUtils
.convertExpressionToString(defineSubtype.getExpression()));
w.append(convertExpressionToString(defineSubtype.getExpression()));
w.append(")\n");
}
/** Converts an expression to string. */
public String convertExpressionToString(ITerm term)
throws UnknownLanguageFragmentException {
if (term instanceof BoolConst) {
return Boolean.toString(((BoolConst) term).isValue());
} else if (term instanceof IntConst) {
return Integer.toString(((IntConst) term).getValue());
} else if (term.equals(NoVal_Const)) {
return NoVal.NOVAL_STRING;
} else if (term instanceof FunctionCall) {
FunctionCall call = (FunctionCall) term;
IFunction func = call.getFunction();
if (func instanceof PredefinedFunction) {
StringBuffer sb = new StringBuffer("(");
EOperator op = ((PredefinedFunction) func).getOperator();
sb.append(getYicesString(op)).append(" ");
for (ITerm arg : call.getArguments()) {
sb.append(convertExpressionToString(arg)).append(" ");
}
sb.deleteCharAt(sb.length() - 1);
sb.append(")");
return sb.toString();
}
} else if (term instanceof Var) {
return ((Var) term).getIdentifier();
}
throw new UnknownLanguageFragmentException(term.toString());
}
/** Yices string representation of an EOperator */
private String getYicesString(EOperator op)
throws UnknownLanguageFragmentException {
switch (op) {
case ADD:
return "+";
case SUBTRACT:
return "-";
case MULTIPLY:
return "*";
case DIVIDE:
return "/";
case MODULO:
return "mod";
case AND:
return "and";
case OR:
return "or";
case NOT:
return "not";
case EQUAL:
return "=";
case NOT_EQUAL:
return "/=";
case GREATER_THAN:
return ">";
case GREATER_EQUAL:
return ">=";
case LOWER_THAN:
return "<";
case LOWER_EQUAL:
return "<=";
default:
break;
}
throw new UnknownLanguageFragmentException(
"Cannot transform operator to Yices: " + op);
}
}
<!--
$Id: package.html 894 2011-07-07 07:36:03Z ratiu $
@version $Rev: 894 $
@ConQAT.Rating GREEN Hash: 9B508364648BA6EBEFA9C5CC2B173408
-->
<body>
This package contains classes for generating the Yices text files.
</body>
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment