From b0a97f59c842aeba5585a51eb63597ea71fe40d0 Mon Sep 17 00:00:00 2001 From: Sebastian Krings <sebastian@krin.gs> Date: Thu, 18 Apr 2013 14:59:00 +0200 Subject: [PATCH] if the proof status of a theorem as guard is exported for prob, we also export the event name as a source --- .../eventb/translator/internal/ModelTranslator.java | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) 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 45049f26..35069296 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 @@ -36,6 +36,8 @@ import org.eventb.core.ISCWitness; import org.eventb.core.ITraceableElement; import org.eventb.core.ast.FormulaFactory; import org.eventb.core.ast.ITypeEnvironment; +import org.eventb.core.basis.Event; +import org.eventb.core.basis.Guard; import org.eventb.core.seqprover.IConfidence; import org.rodinp.core.IElementType; import org.rodinp.core.IRodinElement; @@ -135,9 +137,9 @@ public class ModelTranslator extends AbstractComponentTranslator { super(machine.getComponentName()); this.machine = machine; origin = machine.getMachineRoot(); - ff = ((ISCMachineRoot) machine).getFormulaFactory(); + ff = machine.getFormulaFactory(); try { - te = ((ISCMachineRoot) machine).getTypeEnvironment(ff); + te = machine.getTypeEnvironment(ff); } catch (RodinDBException e) { final String message = "A Rodin exception occured during translation process. Original Exception: "; throw new TranslationFailedException(machine.getComponentName(), @@ -208,6 +210,13 @@ public class ModelTranslator extends AbstractComponentTranslator { .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)); + } + } addProof(new ProofObligation(origin, s, name, pstatus)); } -- GitLab