From 7cd70548381b582f2dfc9b1eed497fd87b2f7203 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 27 Aug 2020 14:57:37 +0200
Subject: [PATCH] try improve disprover for null origin project
for Rodin 3.5RC startup
---
.../eventb/disprover/core/DisproverReasoner.java | 15 ++++++++++++---
.../core/command/DisproverLoadCommand.java | 1 +
2 files changed, 13 insertions(+), 3 deletions(-)
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
index 12354709..4a7ce472 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
@@ -107,9 +107,18 @@ public class DisproverReasoner implements IReasoner {
// find the IEventBProject belonging to the sequent
IPOSequent origin = (IPOSequent) sequent.getOrigin();
- IRodinProject project = origin.getRodinProject();
- IEventBProject evbProject = (IEventBProject) project
- .getAdapter(IEventBProject.class);
+
+ IEventBProject evbProject;
+
+ if (origin==null) { // no origin available; seems to happen in Rodin 3.5RC upon startup
+ System.out.println("No origin available for sequent")
+ // throw new InterruptedException(); // Should we do this instead of trying to work with null project?
+ evbProject = null;
+ } else {
+ IRodinProject project = origin.getRodinProject();
+ evbProject = (IEventBProject) project
+ .getAdapter(IEventBProject.class);
+ }
ICounterExample counterExample = DisproverCommand.disprove(
Animator.getAuxAnimator(), evbProject, allHypotheses,
selectedHypotheses, goal, timeoutFactor, context, pm);
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/command/DisproverLoadCommand.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/command/DisproverLoadCommand.java
index faf38c74..d4d437ff 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/command/DisproverLoadCommand.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/command/DisproverLoadCommand.java
@@ -73,6 +73,7 @@ public final class DisproverLoadCommand implements IComposableCommand {
private boolean theoriesUsed() throws TranslationFailedException {
try {
final IRodinElement[] elements;
+ if (project==null) { return false;}
elements = project.getRodinProject().getChildren();
for (IRodinElement element : elements) {
if (element instanceof IRodinFile) {
--
GitLab