diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java index de2a5fdf7d875359e1da65c0e666f12128875251..844b47802434d5b3ceecb2a3bd717a99979e81d6 100644 --- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java +++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java @@ -13,6 +13,7 @@ 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.eclipse.core.runtime.CoreException; import org.eventb.core.IContextRoot; @@ -62,6 +63,7 @@ import de.prob.core.translator.TranslationFailedException; import de.prob.eventb.translator.internal.EProofStatus; import de.prob.eventb.translator.internal.ProofObligation; import de.prob.eventb.translator.internal.SequentSource; +import de.prob.logging.Logger; public final class ContextTranslator extends AbstractComponentTranslator { @@ -181,47 +183,57 @@ public final class ContextTranslator extends AbstractComponentTranslator { } private void collectProofInfo(IEventBRoot origin) throws RodinDBException { - - IPSRoot proofStatus = origin.getPSRoot(); - IPSStatus[] statuses = proofStatus.getStatuses(); - List<String> bugs = new LinkedList<String>(); - for (IPSStatus status : statuses) { - final int confidence = status.getConfidence(); - boolean broken = status.isBroken(); + try { + IPSRoot proofStatus = origin.getPSRoot(); + IPSStatus[] statuses = proofStatus.getStatuses(); - EProofStatus pstatus = EProofStatus.UNPROVEN; + for (IPSStatus status : statuses) { + final int confidence = status.getConfidence(); + boolean broken = status.isBroken(); - if (!broken && confidence == IConfidence.REVIEWED_MAX) - pstatus = EProofStatus.REVIEWED; - if (!broken && confidence == IConfidence.DISCHARGED_MAX) - pstatus = EProofStatus.PROVEN; + EProofStatus pstatus = EProofStatus.UNPROVEN; - IPOSequent sequent = status.getPOSequent(); - IPOSource[] sources = sequent.getSources(); + if (!broken && confidence == IConfidence.REVIEWED_MAX) + pstatus = EProofStatus.REVIEWED; + if (!broken && confidence == IConfidence.DISCHARGED_MAX) + pstatus = EProofStatus.PROVEN; - String name = sequent.getDescription(); + IPOSequent sequent = status.getPOSequent(); + IPOSource[] sources = sequent.getSources(); - ArrayList<SequentSource> s = new ArrayList<SequentSource>( - sources.length); - for (IPOSource source : sources) { + String name = sequent.getDescription(); - IRodinElement srcElement = source.getSource(); - if (!srcElement.exists() - || !(srcElement instanceof ILabeledElement)) { - bugs.add(status.getElementName()); - break; - } + ArrayList<SequentSource> s = new ArrayList<SequentSource>( + sources.length); + for (IPOSource source : sources) { + + IRodinElement srcElement = source.getSource(); + if (!srcElement.exists() + || !(srcElement instanceof ILabeledElement)) { + bugs.add(status.getElementName()); + break; + } - ILabeledElement le = (ILabeledElement) srcElement; + ILabeledElement le = (ILabeledElement) srcElement; - s.add(new SequentSource(srcElement.getElementType(), le - .getLabel())); + s.add(new SequentSource(srcElement.getElementType(), le + .getLabel())); + } + addProof(new ProofObligation(origin, s, name, pstatus)); } - addProof(new ProofObligation(origin, s, name, pstatus)); + } catch (RodinDBException e) { + bugs.add(e.getLocalizedMessage()); } + + 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); + } + } diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java index 917f73416a5dced8df76b6342f9ea26368ffa358..2d49189534ac8c5078961f00de3eeb0f0f15c80a 100644 --- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java +++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java @@ -171,55 +171,57 @@ public class ModelTranslator extends AbstractComponentTranslator { addUnitPragmas(machine.getSCVariables()); } - private void collectProofInfo() throws RodinDBException { - - IPSRoot proofStatus = machine.getPSRoot(); - IPSStatus[] statuses = proofStatus.getStatuses(); - + private void collectProofInfo() { List<String> bugs = new LinkedList<String>(); + try { + IPSRoot proofStatus = machine.getPSRoot(); + IPSStatus[] statuses = proofStatus.getStatuses(); - for (IPSStatus status : statuses) { - final int confidence = status.getConfidence(); - boolean broken = status.isBroken(); + for (IPSStatus status : statuses) { + final int confidence = status.getConfidence(); + boolean broken = status.isBroken(); - EProofStatus pstatus = EProofStatus.UNPROVEN; + EProofStatus pstatus = EProofStatus.UNPROVEN; - if (!broken - && (confidence > IConfidence.PENDING && confidence <= IConfidence.REVIEWED_MAX)) - pstatus = EProofStatus.REVIEWED; - if (!broken && confidence == IConfidence.DISCHARGED_MAX) - pstatus = EProofStatus.PROVEN; + if (!broken + && (confidence > IConfidence.PENDING && confidence <= IConfidence.REVIEWED_MAX)) + pstatus = EProofStatus.REVIEWED; + if (!broken && confidence == IConfidence.DISCHARGED_MAX) + pstatus = EProofStatus.PROVEN; - IPOSequent sequent = status.getPOSequent(); - IPOSource[] sources = sequent.getSources(); + IPOSequent sequent = status.getPOSequent(); + IPOSource[] sources = sequent.getSources(); - String name = sequent.getDescription(); + String name = sequent.getDescription(); - ArrayList<SequentSource> s = new ArrayList<SequentSource>( - sources.length); - for (IPOSource source : sources) { + ArrayList<SequentSource> s = new ArrayList<SequentSource>( + sources.length); + for (IPOSource source : sources) { - IRodinElement srcElement = source.getSource(); - if (!srcElement.exists() - || !(srcElement instanceof ILabeledElement)) { - bugs.add(status.getElementName()); - break; - } + IRodinElement srcElement = source.getSource(); + if (!srcElement.exists() + || !(srcElement instanceof ILabeledElement)) { + bugs.add(status.getElementName()); + break; + } - ILabeledElement le = (ILabeledElement) srcElement; - IElementType<? extends IRodinElement> type = srcElement - .getElementType(); - s.add(new SequentSource(type, le.getLabel())); + ILabeledElement le = (ILabeledElement) srcElement; + IElementType<? extends IRodinElement> type = srcElement + .getElementType(); + s.add(new SequentSource(type, le.getLabel())); - if (srcElement instanceof Guard) { - Event srcEvent = (Event) srcElement.getParent(); - String srvEventName = srcEvent.getLabel(); - s.add(new SequentSource(srcEvent.getElementType(), - srvEventName)); - } + if (srcElement instanceof Guard) { + Event srcEvent = (Event) srcElement.getParent(); + String srvEventName = srcEvent.getLabel(); + s.add(new SequentSource(srcEvent.getElementType(), + srvEventName)); + } + } + addProof(new ProofObligation(origin, s, name, pstatus)); } - addProof(new ProofObligation(origin, s, name, pstatus)); + } catch (Exception e) { + bugs.add(e.getLocalizedMessage()); } if (!bugs.isEmpty()) {