Skip to content
Snippets Groups Projects
Commit 99737118 authored by birkhoff's avatar birkhoff
Browse files

Merge branch 'develop' of https://github.com/bendisposto/prob into develop

parents 93ee2eda ef6421d6
No related branches found
No related tags found
No related merge requests found
......@@ -13,11 +13,10 @@ import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import org.apache.commons.lang.StringUtils;
import org.eclipse.core.runtime.Assert;
import org.eventb.core.IAxiom;
import org.eventb.core.IContextRoot;
import org.eventb.core.IExtendsContext;
import org.eventb.core.ILabeledElement;
import org.eventb.core.IPOSequent;
import org.eventb.core.IPOSource;
import org.eventb.core.IPSRoot;
......@@ -54,8 +53,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.eventb.translator.internal.DischargedProof;
import de.prob.logging.Logger;
import de.prob.eventb.translator.internal.ProofObligation;
import de.prob.eventb.translator.internal.SequentSource;
public final class ContextTranslator extends AbstractComponentTranslator {
......@@ -63,7 +62,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private final ISCContext context;
private final AEventBContextParseUnit model = new AEventBContextParseUnit();
private final Map<String, ISCContext> depContext = new HashMap<String, ISCContext>();
private final List<DischargedProof> proofs = new ArrayList<DischargedProof>();
private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
private final List<ClassifiedPragma> proofspragmas = new ArrayList<ClassifiedPragma>();
private final FormulaFactory ff;
private ITypeEnvironment te;
......@@ -136,10 +135,10 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
private void collectProofInfo(ISCContextRoot context_root)
private void collectProofInfo(ISCContextRoot origin)
throws RodinDBException {
IPSRoot proofStatus = context_root.getPSRoot();
IPSRoot proofStatus = origin.getPSRoot();
IPSStatus[] statuses = proofStatus.getStatuses();
List<String> bugs = new LinkedList<String>();
......@@ -147,34 +146,31 @@ public final class ContextTranslator extends AbstractComponentTranslator {
for (IPSStatus status : statuses) {
final int confidence = status.getConfidence();
boolean broken = status.isBroken();
if (!broken && confidence == IConfidence.DISCHARGED_MAX) {
boolean discharged = !broken
&& confidence == IConfidence.DISCHARGED_MAX;
IPOSequent sequent = status.getPOSequent();
IPOSource[] sources = sequent.getSources();
String name = sequent.getDescription();
ArrayList<SequentSource> s = new ArrayList<SequentSource>(sources.length);
for (IPOSource source : sources) {
IRodinElement srcElement = source.getSource();
if (!srcElement.exists()) {
if (!srcElement.exists()
|| !(srcElement instanceof ILabeledElement)) {
bugs.add(status.getElementName());
break;
}
if (srcElement instanceof IAxiom) {
IAxiom tmp = (IAxiom) srcElement;
if (((IContextRoot) tmp.getParent())
.equals(context_root.getContextRoot())) {
proofs.add(new DischargedProof(context_root, tmp,
null));
}
}
}
}
}
ILabeledElement le = (ILabeledElement) srcElement;
if (!bugs.isEmpty()) {
String message = "Translation incomplete due to a Bug in Rodin. This does not affect correctness of the Animation/Model Checking but can decrease its performance. Skipped discharged information about: "
+ StringUtils.join(bugs, ",");
Logger.notifyUser(message);
s.add(new SequentSource(srcElement.getElementType(), le.getLabel()));
}
proofs.add(new ProofObligation(origin, s, name, discharged));
}
}
......@@ -330,7 +326,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
return list;
}
public List<DischargedProof> getProofs() {
public List<ProofObligation> getProofs() {
return proofs;
}
......
......@@ -11,13 +11,11 @@ import java.util.Collection;
import java.util.Map;
import org.eclipse.core.runtime.Assert;
import org.eventb.core.IEvent;
import org.eventb.core.IEventBProject;
import org.eventb.core.IEventBRoot;
import org.eventb.core.ISCInternalContext;
import org.eventb.core.ISCMachineRoot;
import org.rodinp.core.IInternalElement;
import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
......@@ -27,16 +25,13 @@ import de.prob.core.translator.ITranslator;
import de.prob.core.translator.TranslationFailedException;
import de.prob.eventb.translator.AbstractComponentTranslator;
import de.prob.eventb.translator.ContextTranslator;
import de.prob.eventb.translator.Theories;
import de.prob.prolog.output.IPrologTermOutput;
public abstract class EventBTranslator implements ITranslator {
protected final IEventBProject project;
private final String name;
protected EventBTranslator(final IEventBRoot root) {
this.project = root.getEventBProject();
this.name = root.getComponentName();
}
// another constructor to cater for ISCInternalContext (which is not a root
......@@ -44,7 +39,6 @@ public abstract class EventBTranslator implements ITranslator {
protected EventBTranslator(final ISCInternalContext ctx) {
Assert.isTrue(ctx.getRoot() instanceof ISCMachineRoot);
this.project = ((ISCMachineRoot) ctx.getRoot()).getEventBProject();
this.name = ctx.getComponentName();
}
private LabelPositionPrinter createPrinter(
......@@ -89,7 +83,7 @@ public abstract class EventBTranslator implements ITranslator {
Collection<ContextTranslator> contextTranslators,
final IPrologTermOutput pout) throws TranslationFailedException {
ArrayList<DischargedProof> list = new ArrayList<DischargedProof>();
ArrayList<ProofObligation> list = new ArrayList<ProofObligation>();
for (ContextTranslator contextTranslator : contextTranslators) {
list.addAll(contextTranslator.getProofs());
......@@ -98,20 +92,19 @@ public abstract class EventBTranslator implements ITranslator {
list.addAll(modelTranslator.getProofs());
}
for (DischargedProof proof : list) {
pout.openTerm("discharged");
pout.printAtom(proof.machine.getRodinFile().getBareName());
try {
IEvent event = proof.event;
final String elementName = proof.predicate;
if (event != null)
pout.printAtom(event.getLabel());
pout.printAtom(elementName);
} catch (RodinDBException e) {
final String details = "Translation error while getting information about discharged proof obligations";
throw new TranslationFailedException(name, details);
for (ProofObligation proof : list) {
pout.openTerm("po");
pout.printAtom(proof.origin.getRodinFile().getBareName());
pout.printAtom(proof.kind);
pout.openList();
for (SequentSource source : proof.sources) {
pout.openTerm(source.type);
pout.printAtom(source.label);
pout.closeTerm();
}
pout.closeList();
pout.printAtom(Boolean.toString(proof.discharged));
pout.closeTerm();
}
......@@ -142,6 +135,9 @@ public abstract class EventBTranslator implements ITranslator {
printModels(refinementChainTranslators, pout, prolog);
printContexts(contextTranslators, pout, prolog);
pout.openList();
pout.openTerm("exporter_version");
pout.printNumber(2);
pout.closeTerm();
printProofInformation(refinementChainTranslators, contextTranslators,
pout);
// FIXME THEORY-PLUGIN re-enable when the theory plugin was released
......
......@@ -15,8 +15,7 @@ import java.util.List;
import org.apache.commons.lang.StringUtils;
import org.eventb.core.IConvergenceElement.Convergence;
import org.eventb.core.IEvent;
import org.eventb.core.IInvariant;
import org.eventb.core.ILabeledElement;
import org.eventb.core.IMachineRoot;
import org.eventb.core.IPOSequent;
import org.eventb.core.IPOSource;
......@@ -40,6 +39,7 @@ import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.IConfidence;
import org.rodinp.core.IElementType;
import org.rodinp.core.IRodinElement;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.RodinDBException;
......@@ -80,7 +80,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
private final FormulaFactory ff;
private final ITypeEnvironment te;
private final IMachineRoot origin;
private final List<DischargedProof> proofs = new ArrayList<DischargedProof>();
private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
// private final List<String> depContext = new ArrayList<String>();
// Confined in the thread calling the factory method
......@@ -113,7 +113,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
return modelTranslator;
}
public List<DischargedProof> getProofs() {
public List<ProofObligation> getProofs() {
return Collections.unmodifiableList(proofs);
}
......@@ -176,41 +176,33 @@ public class ModelTranslator extends AbstractComponentTranslator {
for (IPSStatus status : statuses) {
final int confidence = status.getConfidence();
boolean broken = status.isBroken();
if (!broken && confidence == IConfidence.DISCHARGED_MAX) {
boolean discharged = !broken
&& confidence == IConfidence.DISCHARGED_MAX;
IPOSequent sequent = status.getPOSequent();
IPOSource[] sources = sequent.getSources();
IEvent evt = null;
IInvariant inv = null;
String name = sequent.getDescription();
ArrayList<SequentSource> s = new ArrayList<SequentSource>(
sources.length);
for (IPOSource source : sources) {
IRodinElement srcElement = source.getSource();
if (!srcElement.exists()) {
if (!srcElement.exists()
|| !(srcElement instanceof ILabeledElement)) {
bugs.add(status.getElementName());
break;
}
if (srcElement instanceof IEvent) {
IEvent tmp = (IEvent) srcElement;
if (((IMachineRoot) tmp.getParent()).equals(origin)) {
evt = tmp;
}
}
if (srcElement instanceof IInvariant) {
IInvariant tmp = (IInvariant) srcElement;
if (((IMachineRoot) tmp.getParent()).equals(origin)) {
inv = tmp;
}
}
}
if (evt != null && inv != null) {
proofs.add(new DischargedProof(origin, inv, evt));
}
if (evt == null && inv != null && inv.isTheorem()) {
proofs.add(new DischargedProof(origin, inv, evt));
}
ILabeledElement le = (ILabeledElement) srcElement;
IElementType<? extends IRodinElement> type = srcElement
.getElementType();
s.add(new SequentSource(type, le.getLabel()));
}
proofs.add(new ProofObligation(origin, s, name, discharged));
}
if (!bugs.isEmpty()) {
......
package de.prob.eventb.translator.internal;
import java.util.ArrayList;
import org.eventb.core.IEventBRoot;
public class ProofObligation {
public final IEventBRoot origin;
public final ArrayList<SequentSource> sources;
public final String kind;
public final boolean discharged;
public ProofObligation(IEventBRoot origin, ArrayList<SequentSource> s,
String name, boolean discharged) {
this.origin = origin;
this.sources = s;
this.kind = name;
this.discharged = discharged;
}
}
package de.prob.eventb.translator.internal;
import org.rodinp.core.IElementType;
import org.rodinp.core.IRodinElement;
public class SequentSource {
public final String type;
public final String label;
public SequentSource(IElementType<? extends IRodinElement> type,
String label) {
this.type = type.toString().replaceAll("org.eventb.core.", "");
this.label = label;
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment