Skip to content
Snippets Groups Projects
Commit b0a97f59 authored by Sebastian Krings's avatar Sebastian Krings
Browse files

if the proof status of a theorem as guard is exported for prob, we also export...

if the proof status of a theorem as guard is exported for prob, we also export the event name as a source
parent 60f5b509
No related branches found
No related tags found
No related merge requests found
...@@ -36,6 +36,8 @@ import org.eventb.core.ISCWitness; ...@@ -36,6 +36,8 @@ import org.eventb.core.ISCWitness;
import org.eventb.core.ITraceableElement; import org.eventb.core.ITraceableElement;
import org.eventb.core.ast.FormulaFactory; import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment; 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.eventb.core.seqprover.IConfidence;
import org.rodinp.core.IElementType; import org.rodinp.core.IElementType;
import org.rodinp.core.IRodinElement; import org.rodinp.core.IRodinElement;
...@@ -135,9 +137,9 @@ public class ModelTranslator extends AbstractComponentTranslator { ...@@ -135,9 +137,9 @@ public class ModelTranslator extends AbstractComponentTranslator {
super(machine.getComponentName()); super(machine.getComponentName());
this.machine = machine; this.machine = machine;
origin = machine.getMachineRoot(); origin = machine.getMachineRoot();
ff = ((ISCMachineRoot) machine).getFormulaFactory(); ff = machine.getFormulaFactory();
try { try {
te = ((ISCMachineRoot) machine).getTypeEnvironment(ff); te = machine.getTypeEnvironment(ff);
} catch (RodinDBException e) { } catch (RodinDBException e) {
final String message = "A Rodin exception occured during translation process. Original Exception: "; final String message = "A Rodin exception occured during translation process. Original Exception: ";
throw new TranslationFailedException(machine.getComponentName(), throw new TranslationFailedException(machine.getComponentName(),
...@@ -208,6 +210,13 @@ public class ModelTranslator extends AbstractComponentTranslator { ...@@ -208,6 +210,13 @@ public class ModelTranslator extends AbstractComponentTranslator {
.getElementType(); .getElementType();
s.add(new SequentSource(type, le.getLabel())); 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)); addProof(new ProofObligation(origin, s, name, pstatus));
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment