From af71deea53d61f65c9ea0c21086e4b1f0e91231a Mon Sep 17 00:00:00 2001
From: Ivaylo Dobrikov <dobrikov@cs.uni-duesseldorf.de>
Date: Fri, 31 Oct 2014 16:09:38 +0100
Subject: [PATCH] Fixed a bug in the LTL viewer of Rodin (see comments in the
commit).
---
.../domainobjects/ltl/CounterExample.java | 23 ++++++++++++++-----
1 file changed, 17 insertions(+), 6 deletions(-)
diff --git a/de.prob.core/src/de/prob/core/domainobjects/ltl/CounterExample.java b/de.prob.core/src/de/prob/core/domainobjects/ltl/CounterExample.java
index 4c6990ac..4c45e0f2 100644
--- a/de.prob.core/src/de/prob/core/domainobjects/ltl/CounterExample.java
+++ b/de.prob.core/src/de/prob/core/domainobjects/ltl/CounterExample.java
@@ -51,10 +51,11 @@ public class CounterExample {
.asList(modelCheckingResult.getInitPathOps()));
ceSize = modelCheckingResult.getCounterexample().size();
+ final String[] atomicFormulaNames = createAtomicNames(modelCheckingResult);
+
final List<ArrayList<Boolean>> predicateValues = createStates(modelCheckingResult
- .getCounterexample());
+ .getCounterexample(), atomicFormulaNames);
- final String[] atomicFormulaNames = createAtomicNames(modelCheckingResult);
propositionRoot = createExample(modelCheckingResult.getStructure(),
atomicFormulaNames, predicateValues);
propositionRoot.setVisible(true);
@@ -73,10 +74,17 @@ public class CounterExample {
return res;
}
- private List<ArrayList<Boolean>> createStates(final ListPrologTerm example) {
+ private List<ArrayList<Boolean>> createStates(final ListPrologTerm example, String[] atomicFormulaNames) {
List<ArrayList<Boolean>> predicateValues = new ArrayList<ArrayList<Boolean>>();
- for (int i = 0; i < example.size(); i++) {
+ // A bug fix from 31.10.2014: changed the termination condition from
+ // 'i < example.size()' to 'i < atomicFormulaNames.length'. The statement
+ // predicateValues.get(i).add(value == 0 ? false : true) in the inner for-loop (lines 98-105)
+ // crashed once the reported counter-example 'example' had less atoms as atomic propositions,
+ // e.g. for 'G ({x/=1} & {y<=10})' with 'example = [atom(0,[0,1],none)]' an IndexOutOfBounds-Exception
+ // had been thrown. Note that the bug-fix has been not thoroughly tested and there may be other issues
+ // that may occur.
+ for (int i = 0; i < atomicFormulaNames.length; i++) {
predicateValues.add(new ArrayList<Boolean>());
}
@@ -92,12 +100,15 @@ public class CounterExample {
for (int i = 0; i < values.size(); i++) {
int value = ((IntegerPrologTerm) values.get(i)).getValue()
.intValue();
- predicateValues.get(i).add(value == 0 ? false : true);
+ // Doesn't have to be a 'predicateValues.get(index)' and not
+ // 'predicateValues.get(i)' (predicateValues is a list of boolean lists)
+ //predicateValues.get(index).add(value == 0 ? false : true);
+ predicateValues.get(i).add(value == 0 ? false : true);
}
final Operation operation = NONE.equals(operationTerm) ? null
: Operation.fromPrologTerm(operationTerm);
- final CounterExampleState ceState = new CounterExampleState(index,
+ final CounterExampleState ceState = new CounterExampleState(index,
stateId, operation);
states.add(ceState);
index++;
--
GitLab