Commit 27fe06e4 authored by Lukas Ladenberger's avatar Lukas Ladenberger
Browse files

Merge branch 'develop' into feature/multiview

parents 6d4120fb 531082b7
package de.prob.core.domainobjects.ltl.unittests;
package de.prob.core.domainobjects.ltl.tests;
import java.util.ArrayList;
import java.util.Collection;
......
package de.prob.core.domainobjects.ltl.unittests;
package de.prob.core.domainobjects.ltl.tests;
import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.core.domainobjects.ltl.CounterExample;
......
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xmlpull-1.1.3.1.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xpp3_min-1.1.4c.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.3.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-lang-2.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jgrapht-0.8.3.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jsr305-1.3.9.jar"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry kind="src" path="test"/>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/4"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-lang-2.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jgrapht-0.8.3.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jsr305-1.3.9.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xmlpull-1.1.3.1.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xpp3_min-1.1.4c.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.3.jar"/>
<classpathentry kind="output" path="bin"/>
</classpath>
/**
* (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
* Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
* (http://www.eclipse.org/org/documents/epl-v10.html)
* */
package de.prob.core.command;
import de.prob.core.Animator;
import de.prob.exceptions.ProBException;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.term.PrologTerm;
public class ActivateUnitPluginCommand implements IComposableCommand {
private static final ActivateCmd ACTIVATE_CMD = new ActivateCmd();
private final GetPrologRandomSeed getRandomSeed;
private final ComposedCommand cmd;
public ActivateUnitPluginCommand() {
this.getRandomSeed = new GetPrologRandomSeed();
this.cmd = new ComposedCommand(getRandomSeed, ACTIVATE_CMD);
}
public static void activateUnitPlugin(final Animator animator)
throws ProBException {
animator.execute(new ActivateUnitPluginCommand());
}
public void processResult(
final ISimplifiedROMap<String, PrologTerm> bindings)
throws CommandException {
cmd.processResult(bindings);
final Animator animator = Animator.getAnimator();
animator.setRandomSeed(getRandomSeed.getSeed());
}
public void writeCommand(final IPrologTermOutput pto)
throws CommandException {
cmd.writeCommand(pto);
}
private final static class ActivateCmd implements IComposableCommand {
public void processResult(
final ISimplifiedROMap<String, PrologTerm> bindings)
throws CommandException {
}
public void writeCommand(final IPrologTermOutput pto) {
pto.openTerm("activate_plugin");
pto.printAtom("units");
pto.closeTerm();
}
}
}
/**
* (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
* Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
* (http://www.eclipse.org/org/documents/epl-v10.html)
* */
package de.prob.core.command;
import de.prob.parser.BindingGenerator;
import de.prob.parser.ISimplifiedROMap;
import de.prob.parser.ResultParserException;
import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
public final class GetPluginResultCommand implements IComposableCommand {
private final String resultID;
private ListPrologTerm result;
public GetPluginResultCommand(final String resultID) {
this.resultID = resultID;
}
public ListPrologTerm getResult() {
return result;
}
public void processResult(
final ISimplifiedROMap<String, PrologTerm> bindings)
throws CommandException {
try {
result = BindingGenerator.getList(bindings, "Bindings");
} catch (ResultParserException e) {
CommandException commandException = new CommandException(
e.getLocalizedMessage(), e);
commandException.notifyUserOnce();
throw commandException;
}
}
public void writeCommand(final IPrologTermOutput pto) {
pto.openTerm("get_plugin_output").printAtomOrNumber(resultID)
.printVariable("Bindings").closeTerm();
}
}
......@@ -19,17 +19,15 @@ import org.rodinp.core.RodinDBException;
import de.prob.core.Animator;
import de.prob.core.LanguageDependendAnimationPart;
import de.prob.core.command.internal.InternalLoadCommand;
import de.prob.core.domainobjects.MachineDescription;
import de.prob.core.domainobjects.Operation;
import de.prob.core.domainobjects.ProBPreference;
import de.prob.core.domainobjects.State;
import de.prob.core.langdep.EventBAnimatorPart;
import de.prob.core.translator.TranslationFailedException;
import de.prob.eventb.translator.TranslatorFactory;
import de.prob.exceptions.ProBException;
import de.prob.logging.Logger;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.output.StructuredPrologOutput;
import de.prob.prolog.term.PrologTerm;
......@@ -162,32 +160,4 @@ public final class LoadEventBModelCommand {
animator.announceReset();
}
}
private static class InternalLoadCommand implements IComposableCommand {
private final IEventBRoot model;
public InternalLoadCommand(final IEventBRoot model) {
this.model = model;
}
@Override
public void writeCommand(final IPrologTermOutput pto)
throws CommandException {
try {
TranslatorFactory.translate(model, pto);
} catch (TranslationFailedException e) {
throw new CommandException(
"Translation from Event-B to ProB's internal representation failed",
e);
}
}
@Override
public void processResult(
final ISimplifiedROMap<String, PrologTerm> bindings)
throws CommandException {
// there are no results to process
}
}
}
package de.prob.core.command.internal;
import org.eventb.core.IEventBRoot;
import de.prob.core.command.CommandException;
import de.prob.core.command.IComposableCommand;
import de.prob.core.translator.TranslationFailedException;
import de.prob.eventb.translator.TranslatorFactory;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.term.PrologTerm;
public final class InternalLoadCommand implements IComposableCommand {
private final IEventBRoot model;
public InternalLoadCommand(final IEventBRoot model) {
this.model = model;
}
@Override
public void writeCommand(final IPrologTermOutput pto)
throws CommandException {
try {
TranslatorFactory.translate(model, pto);
} catch (TranslationFailedException e) {
throw new CommandException(
"Translation from Event-B to ProB's internal representation failed",
e);
}
}
@Override
public void processResult(
final ISimplifiedROMap<String, PrologTerm> bindings)
throws CommandException {
// there are no results to process
}
}
\ No newline at end of file
/**
* (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
* Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
* (http://www.eclipse.org/org/documents/epl-v10.html)
* */
package de.prob.core.translator.pragmas;
import de.prob.prolog.output.IPrologTermOutput;
public interface IPragma {
void output(IPrologTermOutput pout);
}
/**
* (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
* Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
* (http://www.eclipse.org/org/documents/epl-v10.html)
* */
package de.prob.core.translator.pragmas;
import de.prob.prolog.output.IPrologTermOutput;
public class UnitPragma implements IPragma {
private String definedIn;
private String attachedTo;
private String content;
public UnitPragma(String definedIn, String attachedTo, String content) {
this.definedIn = definedIn;
this.attachedTo = attachedTo;
this.content = content;
}
@Override
public void output(IPrologTermOutput pout) {
pout.openTerm("pragma");
pout.printAtom("unit");
pout.printAtom(definedIn);
pout.printAtom(attachedTo);
pout.openList();
pout.printAtom(content);
pout.closeList();
pout.closeTerm();
}
}
......@@ -15,6 +15,7 @@ import java.util.Map;
import org.eclipse.core.runtime.Assert;
import org.eventb.core.IContextRoot;
import org.eventb.core.IEventBRoot;
import org.eventb.core.IExtendsContext;
import org.eventb.core.ILabeledElement;
import org.eventb.core.IPOSequent;
......@@ -28,13 +29,15 @@ import org.eventb.core.ISCContext;
import org.eventb.core.ISCContextRoot;
import org.eventb.core.ISCExtendsContext;
import org.eventb.core.ISCInternalContext;
import org.eventb.core.ISCMachineRoot;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.seqprover.IConfidence;
import org.rodinp.core.IAttributeType;
import org.rodinp.core.IInternalElement;
import org.rodinp.core.IRodinElement;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.IRodinProject;
import org.rodinp.core.RodinCore;
import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.analysis.pragma.internal.ClassifiedPragma;
......@@ -53,6 +56,8 @@ import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.hhu.stups.sablecc.patch.SourcePosition;
import de.prob.core.translator.TranslationFailedException;
import de.prob.core.translator.pragmas.IPragma;
import de.prob.core.translator.pragmas.UnitPragma;
import de.prob.eventb.translator.internal.EProofStatus;
import de.prob.eventb.translator.internal.ProofObligation;
import de.prob.eventb.translator.internal.SequentSource;
......@@ -65,18 +70,72 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private final Map<String, ISCContext> depContext = new HashMap<String, ISCContext>();
private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
private final List<ClassifiedPragma> proofspragmas = new ArrayList<ClassifiedPragma>();
private final List<IPragma> pragmas = new ArrayList<IPragma>();
public static ContextTranslator create(final ISCContext context)
private final IEventBRoot root;
private final FormulaFactory ff;
private final ITypeEnvironment te;
public static ContextTranslator create(final ISCContextRoot context)
throws TranslationFailedException {
ContextTranslator contextTranslator = new ContextTranslator(context);
try {
contextTranslator.translate();
assertConsistentModel(context);
final FormulaFactory ff = context.getFormulaFactory();
final ITypeEnvironment te = context.getTypeEnvironment(ff);
final ContextTranslator translator = new ContextTranslator(context,
ff, te, context);
translator.translate();
return translator;
} catch (RodinDBException e) {
final String message = "A Rodin exception occured during translation process. Possible cause: building aborted or still in progress. Please wait until building has finished before starting ProB. If this does not help, perform a clean and start ProB after building has finished. Original Exception: ";
throw new TranslationFailedException(context.getComponentName(),
message + e.getLocalizedMessage());
throw createTranslationFailedException(context, e);
}
}
public static ContextTranslator create(final ISCInternalContext context,
final FormulaFactory ff, final ITypeEnvironment te)
throws TranslationFailedException {
final IEventBRoot root = getRootContext(context);
final ContextTranslator translator = new ContextTranslator(context, ff,
te, root);
try {
assertConsistentModel(context.getRoot());
translator.translate();
} catch (RodinDBException e) {
throw createTranslationFailedException(context, e);
}
return translator;
}
private static IEventBRoot getRootContext(ISCInternalContext context) {
try {
String elementName = context.getElementName();
IRodinProject rodinProject = context.getRodinProject();
IRodinFile rodinFile = rodinProject.getRodinFile(elementName
+ ".bcc");
if (rodinFile.exists()) {
final IInternalElement element = rodinFile.getRoot();
if (element instanceof IEventBRoot) {
return (IEventBRoot) element;
}
}
} catch (Exception e) {
// We do not guarantee to include proof infos. If something goes
// wrong, we ignore the Proof info.
}
return contextTranslator;
return null;
}
private static TranslationFailedException createTranslationFailedException(
final ISCContext context, RodinDBException e)
throws TranslationFailedException {
final String message = "A Rodin exception occured during translation process. Possible cause: building aborted or still in progress. Please wait until building has finished before starting ProB. If this does not help, perform a clean and start ProB after building has finished. Original Exception: ";
return new TranslationFailedException(context.getComponentName(),
message + e.getLocalizedMessage());
}
private static boolean assertConsistentModel(IInternalElement machine_root)
throws RodinDBException {
return Assert.isTrue(machine_root.getRodinFile().isConsistent());
}
/**
......@@ -86,46 +145,56 @@ public final class ContextTranslator extends AbstractComponentTranslator {
* contains errors)
*
* @param context
* The context to translate
* @param ff
* The FormulaFactory needed to extract the predicates
* @param te
* The TypeEnvironment needed to extract the predicates
* @param root
* the root to access the proofs
* @throws TranslationFailedException
* @throws RodinDBException
*/
private ContextTranslator(final ISCContext context)
throws TranslationFailedException {
private ContextTranslator(final ISCContext context,
final FormulaFactory ff, final ITypeEnvironment te,
final IEventBRoot root) throws TranslationFailedException {
this.context = context;
this.ff = ff;
this.te = te;
this.root = root;
}
private void translate() throws RodinDBException {
if (context instanceof ISCContextRoot) {
ISCContextRoot context_root = (ISCContextRoot) context;
Assert.isTrue(context_root.getRodinFile().isConsistent());
} else if (context instanceof ISCInternalContext) {
ISCInternalContext context_internal = (ISCInternalContext) context;
try {
String elementName = context_internal.getElementName();
IRodinProject rodinProject = context_internal.getRodinProject();
IRodinFile rodinFile = rodinProject.getRodinFile(elementName
+ ".bcc");
if (rodinFile.exists()) {
ISCContextRoot root = (ISCContextRoot) rodinFile.getRoot();
collectProofInfo(root);
translateContext();
collectProofInfo();
collectPragmas();
}
private void collectPragmas() throws RodinDBException {
// unit pragma, attached to constants
final IAttributeType.String UNITATTRIBUTE = RodinCore
.getStringAttrType("de.prob.units.unitPragmaAttribute");
final ISCConstant[] constants = context.getSCConstants();
for (final ISCConstant constant : constants) {
if (constant.hasAttribute(UNITATTRIBUTE)) {
String content = constant.getAttributeValue(UNITATTRIBUTE);
if (!content.isEmpty()) {
pragmas.add(new UnitPragma(getResource(), constant
.getIdentifierString(), content));
}
} catch (Exception e) {
// We do not guarantee to include proof infos. If something goes
// wrong, we ignore the Proof info.
}
ISCMachineRoot machine_root = (ISCMachineRoot) context_internal
.getRoot();
Assert.isTrue(machine_root.getRodinFile().isConsistent());
}
translateContext();
}
private void collectProofInfo() throws RodinDBException {
if (root != null) {
collectProofInfo(root);
}
}
private void collectProofInfo(ISCContextRoot origin)
throws RodinDBException {
private void collectProofInfo(IEventBRoot origin) throws RodinDBException {
IPSRoot proofStatus = origin.getPSRoot();
IPSStatus[] statuses = proofStatus.getStatuses();
......@@ -305,20 +374,17 @@ public final class ContextTranslator extends AbstractComponentTranslator {
final List<PPredicate> list = new ArrayList<PPredicate>(
predicates.length);
for (final ISCAxiom element : predicates) {
if (element.isTheorem() != theorems) {
continue;
if (element.isTheorem() == theorems) {
final PredicateVisitor visitor = new PredicateVisitor(
new LinkedList<String>());
element.getPredicate(ff, te).accept(visitor);
final PPredicate predicate = visitor.getPredicate();
list.add(predicate);
labelMapping.put(predicate, element);
proofspragmas.add(new ClassifiedPragma("discharged", predicate,
Arrays.asList(new String[0]), Arrays
.asList(new String[0]), NO_POS, NO_POS));
}
final PredicateVisitor visitor = new PredicateVisitor(
new LinkedList<String>());
final FormulaFactory ff = FormulaFactory.getDefault();
final ITypeEnvironment te = ff.makeTypeEnvironment();
element.getPredicate(ff, te).accept(visitor);
final PPredicate predicate = visitor.getPredicate();
list.add(predicate);
labelMapping.put(predicate, element);
proofspragmas.add(new ClassifiedPragma("discharged", predicate,
Arrays.asList(new String[0]), Arrays.asList(new String[0]),
NO_POS, NO_POS));
}
return list;
}
......@@ -327,6 +393,10 @@ public final class ContextTranslator extends AbstractComponentTranslator {
return proofs;
}
public List<IPragma> getPragmas() {
return pragmas;
}
public List<ClassifiedPragma> getProofspragmas() {
return proofspragmas;
}
......
......@@ -51,13 +51,15 @@ public final class EventBContextTranslator extends EventBTranslator {
private void constructTranslation(final IPrologTermOutput pto)
throws TranslationFailedException {
List<ContextTranslator> translators = new ArrayList<ContextTranslator>();
// translators.add(ContextTranslator.create(context));
List<ContextTranslator> contextTranslators = new ArrayList<ContextTranslator>();
// translators.add(ContextTranslator.create(context));
if (context instanceof ISCContextRoot) {
ISCContextRoot root = (ISCContextRoot) context;
collectContexts(translators, new ArrayList<String>(), root);
collectContexts(contextTranslators, new ArrayList<String>(), root);
}
printProlog(new ArrayList<ModelTranslator>(), translators, pto);
printProlog(new ArrayList<ModelTranslator>(), contextTranslators, pto);
}
private void collectContexts(final List<ContextTranslator> translatorMap,
......
......@@ -11,6 +11,8 @@ import java.util.List;
import org.eventb.core.ISCInternalContext;
import org.eventb.core.ISCMachineRoot;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.RodinDBException;
......@@ -102,12 +104,14 @@ public final class EventBMachineTranslator extends EventBTranslator {
throws TranslationFailedException {
final List<ContextTranslator> translators = new ArrayList<ContextTranslator>();
final List<String> processed = new ArrayList<String>();
for (ISCMachineRoot m : models) {
ISCInternalContext[] seenContexts;
for (final ISCMachineRoot m : models) {
try {