From e8d8dd55d6ba5b07764aa05f83e0321b586b81f4 Mon Sep 17 00:00:00 2001 From: Sebastian Krings <sebastian@krin.gs> Date: Thu, 6 Jun 2013 10:42:26 +0200 Subject: [PATCH] disprover: add hypotheses, goal and result to log --- .../eventb/disprover/core/internal/DisproverReasoner.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java index 41e8792c..ca5c5cce 100644 --- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java +++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java @@ -70,16 +70,23 @@ public class DisproverReasoner implements IReasoner { private ICounterExample evaluateSequent(final IProverSequent sequent, final DisproverReasonerInput disproverInput, IProofMonitor pm) throws ProBException, RodinDBException, InterruptedException { + Logger.info("Calling Disprover on Sequent"); Set<Predicate> hypotheses = new HashSet<Predicate>(); for (Predicate predicate : sequent.hypIterable()) { hypotheses.add(predicate); + Logger.info("Disprover: Sending Hypothesis: " + + predicate.toString()); } Predicate goal = sequent.goal(); + Logger.info("Disprover: Sending Goal: " + goal.toString()); IEventBRoot root = getRoot(sequent); + ICounterExample counterExample = DisproverCommand.disprove( Animator.getAnimator(), hypotheses, goal, root, pm); + Logger.info("Disprover: Result: " + counterExample.toString()); + return counterExample; } -- GitLab