From 64cd3e878e3962352e1883ccb7913448eee81b62 Mon Sep 17 00:00:00 2001
From: Jens Bendisposto <jens@bendisposto.de>
Date: Thu, 20 Dec 2012 12:43:56 +0100
Subject: [PATCH] new proof status: reviewed
---
.../prob/eventb/translator/ContextTranslator.java | 11 ++++++++---
.../eventb/translator/internal/EProofStatus.java | 15 +++++++++++++++
.../translator/internal/EventBTranslator.java | 2 +-
.../translator/internal/ModelTranslator.java | 10 +++++++---
.../translator/internal/ProofObligation.java | 6 +++---
5 files changed, 34 insertions(+), 10 deletions(-)
create mode 100644 de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java
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 425266e8..ad5b33af 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -53,6 +53,7 @@ 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.EProofStatus;
import de.prob.eventb.translator.internal.ProofObligation;
import de.prob.eventb.translator.internal.SequentSource;
@@ -135,8 +136,12 @@ public final class ContextTranslator extends AbstractComponentTranslator {
final int confidence = status.getConfidence();
boolean broken = status.isBroken();
- boolean discharged = !broken
- && confidence == IConfidence.DISCHARGED_MAX;
+ EProofStatus pstatus = EProofStatus.UNPROVEN;
+
+ if (!broken && confidence == IConfidence.REVIEWED_MAX)
+ pstatus = EProofStatus.REVIEWED;
+ if (!broken && confidence == IConfidence.DISCHARGED_MAX)
+ pstatus = EProofStatus.PROVEN;
IPOSequent sequent = status.getPOSequent();
IPOSource[] sources = sequent.getSources();
@@ -160,7 +165,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
.getLabel()));
}
- proofs.add(new ProofObligation(origin, s, name, discharged));
+ proofs.add(new ProofObligation(origin, s, name, pstatus));
}
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java b/de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java
new file mode 100644
index 00000000..160bf968
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java
@@ -0,0 +1,15 @@
+package de.prob.eventb.translator.internal;
+
+public enum EProofStatus {
+ UNPROVEN("false"), PROVEN("true"), REVIEWED("reviewed");
+ private final String text;
+
+ private EProofStatus(String text) {
+ this.text = text;
+ }
+
+ @Override
+ public String toString() {
+ return text;
+ }
+}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
index 5f015c24..ed82d8a8 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
@@ -104,7 +104,7 @@ public abstract class EventBTranslator implements ITranslator {
}
pout.closeList();
- pout.printAtom(Boolean.toString(proof.discharged));
+ pout.printAtom(proof.discharged.toString());
pout.closeTerm();
}
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 95973e0f..ead67da6 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
@@ -177,8 +177,12 @@ public class ModelTranslator extends AbstractComponentTranslator {
final int confidence = status.getConfidence();
boolean broken = status.isBroken();
- boolean discharged = !broken
- && confidence == IConfidence.DISCHARGED_MAX;
+ 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;
IPOSequent sequent = status.getPOSequent();
IPOSource[] sources = sequent.getSources();
@@ -202,7 +206,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
s.add(new SequentSource(type, le.getLabel()));
}
- proofs.add(new ProofObligation(origin, s, name, discharged));
+ proofs.add(new ProofObligation(origin, s, name, pstatus));
}
if (!bugs.isEmpty()) {
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java b/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java
index 978df176..39b10069 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java
@@ -9,14 +9,14 @@ public class ProofObligation {
public final IEventBRoot origin;
public final ArrayList<SequentSource> sources;
public final String kind;
- public final boolean discharged;
+ public final EProofStatus discharged;
public ProofObligation(IEventBRoot origin, ArrayList<SequentSource> s,
- String name, boolean discharged) {
+ String name, EProofStatus pstatus) {
this.origin = origin;
this.sources = s;
this.kind = name;
- this.discharged = discharged;
+ this.discharged = pstatus;
}
}
--
GitLab