Skip to content
Snippets Groups Projects
Commit 82831a57 authored by Lukas Ladenberger's avatar Lukas Ladenberger
Browse files

Merge branch 'develop' of github.com:bendisposto/prob into develop

parents 75e0dc59 77f79834
Branches
No related tags found
No related merge requests found
Showing
with 352 additions and 213 deletions
......@@ -14,10 +14,6 @@ Export-Package: de.be4.classicalb.core.parser,
de.be4.classicalb.core.parser.exceptions,
de.be4.classicalb.core.parser.node;x-friends:="de.prob.eventb.disprover.core",
de.be4.ltl.core.parser,
de.prob.animationscript.parser.analysis,
de.prob.animationscript.parser.lexer,
de.prob.animationscript.parser.node,
de.prob.animationscript.parser.parser;uses:="de.prob.animationscript.parser.lexer,de.prob.animationscript.parser.analysis,de.prob.animationscript.parser.node",
de.prob.core;
uses:="de.prob.core.domainobjects.eval,
de.prob.parserbase,
......
No preview for this file type
......@@ -190,9 +190,10 @@ public class EvaluationGetValuesCommand implements IComposableCommand {
final CompoundPrologTerm vc = (CompoundPrologTerm) valueTerm;
final String valString = ((CompoundPrologTerm) vc
.getArgument(1)).getFunctor();
value = new EvaluationResult(
FormulaTranslator.translate(valString), true, false,
false, false);
final String translated = valString.length() == 0 ? ""
: FormulaTranslator.translate(valString);
value = new EvaluationResult(translated, true, false, false,
false);
} else if (valueTerm.hasFunctor("e", 1)) {
final CompoundPrologTerm vc = (CompoundPrologTerm) valueTerm;
final String error = ((CompoundPrologTerm) vc.getArgument(1))
......
......@@ -97,4 +97,35 @@ public abstract class CounterExampleBinaryOperator extends
int size = getFirstArgument().getValues().size();
return pos < size ? pos : pos - (size - loopEntry);
}
protected int indexOfUnknownState(
final List<CounterExampleValueType> firstCheckedValues,
final List<CounterExampleValueType> secondCheckedValues,
boolean past) {
int unknownStateIndex = -1;
if (past) {
for (int i = firstCheckedValues.size() - 1; i >= 0; i--) {
if (firstCheckedValues.get(i).equals(
CounterExampleValueType.UNKNOWN)
&& secondCheckedValues.get(i).equals(
CounterExampleValueType.UNKNOWN)) {
unknownStateIndex = i;
break;
}
}
} else {
for (int i = 0; i < firstCheckedValues.size(); i++) {
if (firstCheckedValues.get(i).equals(
CounterExampleValueType.UNKNOWN)
&& secondCheckedValues.get(i).equals(
CounterExampleValueType.UNKNOWN)) {
unknownStateIndex = i;
break;
}
}
}
return unknownStateIndex;
}
}
......@@ -4,7 +4,7 @@ import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.logging.Logger;
/**
* Provides an "And" operator.
* Provides an "and" operator.
*
* @author Andriy Tolstoy
*
......@@ -24,8 +24,8 @@ public final class CounterExampleConjunction extends
pathType, loopEntry, firstArgument);
CounterExampleNegation notSecondArgument = new CounterExampleNegation(
pathType, loopEntry, secondArgument);
CounterExampleDisjunction or = new CounterExampleDisjunction(pathType, loopEntry,
notFirstArgument, notSecondArgument);
CounterExampleDisjunction or = new CounterExampleDisjunction(pathType,
loopEntry, notFirstArgument, notSecondArgument);
not = new CounterExampleNegation(pathType, loopEntry, or);
}
......@@ -69,9 +69,9 @@ public final class CounterExampleConjunction extends
if (firstValue == CounterExampleValueType.FALSE
|| secondValue == CounterExampleValueType.FALSE) {
result = CounterExampleValueType.FALSE;
} else if (firstValue == CounterExampleValueType.UNDEFINED
|| secondValue == CounterExampleValueType.UNDEFINED) {
result = CounterExampleValueType.UNDEFINED;
} else if (firstValue == CounterExampleValueType.UNKNOWN
|| secondValue == CounterExampleValueType.UNKNOWN) {
result = CounterExampleValueType.UNKNOWN;
}
return result;
......
......@@ -3,7 +3,7 @@ package de.prob.core.domainobjects.ltl;
import de.prob.core.command.LtlCheckingCommand.PathType;
/**
* Provides an "Or" operator.
* Provides an "or" operator.
*
* @author Andriy Tolstoy
*
......@@ -54,9 +54,9 @@ public final class CounterExampleDisjunction extends
if (firstValue == CounterExampleValueType.TRUE
|| secondValue == CounterExampleValueType.TRUE) {
result = CounterExampleValueType.TRUE;
} else if (firstValue == CounterExampleValueType.UNDEFINED
|| secondValue == CounterExampleValueType.UNDEFINED) {
result = CounterExampleValueType.UNDEFINED;
} else if (firstValue == CounterExampleValueType.UNKNOWN
|| secondValue == CounterExampleValueType.UNKNOWN) {
result = CounterExampleValueType.UNKNOWN;
}
return result;
......
......@@ -8,7 +8,7 @@ import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.logging.Logger;
/**
* Provides a "Finally" operator.
* Provides a "finally" operator.
*
* @author Andriy Tolstoy
*
......@@ -43,7 +43,7 @@ public final class CounterExampleFinally extends CounterExampleUnaryOperator {
}
private CounterExampleValueType calculateFinallyOperator(final int position) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
List<CounterExampleValueType> checkedValues = new ArrayList<CounterExampleValueType>(
argument.getValues());
......
......@@ -8,7 +8,7 @@ import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.logging.Logger;
/**
* Provides a "Globally" operator.
* Provides a "globally" operator.
*
* @author Andriy Tolstoy
*
......@@ -75,7 +75,7 @@ public final class CounterExampleGlobally extends CounterExampleUnaryOperator {
}
private CounterExampleValueType calculateGlobally(final int position) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
List<CounterExampleValueType> checkedValues = new ArrayList<CounterExampleValueType>(
argument.getValues());
......
......@@ -8,7 +8,7 @@ import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.logging.Logger;
/**
* Provides a "History" operator.
* Provides a "history" operator.
*
* @author Andriy Tolstoy
*
......@@ -22,8 +22,8 @@ public final class CounterExampleHistory extends CounterExampleUnaryOperator {
final CounterExampleProposition argument) {
super("H", "History", pathType, loopEntry, argument);
CounterExampleNegation notArgument = new CounterExampleNegation(pathType,
loopEntry, argument);
CounterExampleNegation notArgument = new CounterExampleNegation(
pathType, loopEntry, argument);
CounterExampleOnce onceOperator = new CounterExampleOnce(pathType,
loopEntry, notArgument);
......@@ -59,7 +59,7 @@ public final class CounterExampleHistory extends CounterExampleUnaryOperator {
}
private CounterExampleValueType calculateHistoryOperator(final int position) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
List<CounterExampleValueType> checkedValues = new ArrayList<CounterExampleValueType>(
argument.getValues());
......@@ -73,7 +73,7 @@ public final class CounterExampleHistory extends CounterExampleUnaryOperator {
if (index != -1) {
result = CounterExampleValueType.FALSE;
} else {
if (!checkedValues.contains(CounterExampleValueType.UNDEFINED)) {
if (!checkedValues.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.TRUE;
}
}
......
......@@ -3,7 +3,7 @@ package de.prob.core.domainobjects.ltl;
import de.prob.core.command.LtlCheckingCommand.PathType;
/**
* Provides an "Imply" operator.
* Provides an "imply" operator.
*
* @author Andriy Tolstoy
*
......
......@@ -3,7 +3,7 @@ package de.prob.core.domainobjects.ltl;
import de.prob.core.command.LtlCheckingCommand.PathType;
/**
* Provides a "Not" operator.
* Provides a "not" operator.
*
* @author Andriy Tolstoy
*
......@@ -32,7 +32,7 @@ public final class CounterExampleNegation extends CounterExampleUnaryOperator {
public static CounterExampleValueType calculateNotOperator(
final CounterExampleValueType value) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
if (value == CounterExampleValueType.TRUE) {
result = CounterExampleValueType.FALSE;
......
......@@ -6,7 +6,7 @@ import java.util.List;
import de.prob.core.command.LtlCheckingCommand.PathType;
/**
* Provides a "Next" operator.
* Provides a "next" operator.
*
* @author Andriy Tolstoy
*
......@@ -24,7 +24,7 @@ public final class CounterExampleNext extends CounterExampleUnaryOperator {
}
private CounterExampleValueType calculateNextOperator(int position) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
List<CounterExampleValueType> checkedValues = new ArrayList<CounterExampleValueType>(
argument.getValues());
......
......@@ -8,7 +8,7 @@ import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.logging.Logger;
/**
* Provides an "Once" operator.
* Provides an "once" operator.
*
* @author Andriy Tolstoy
*
......@@ -48,7 +48,7 @@ public final class CounterExampleOnce extends CounterExampleUnaryOperator {
}
private CounterExampleValueType calculateOnceOperator(final int position) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
List<CounterExampleValueType> checkedValues = new ArrayList<CounterExampleValueType>(
argument.getValues());
......@@ -62,7 +62,7 @@ public final class CounterExampleOnce extends CounterExampleUnaryOperator {
if (index != -1) {
result = CounterExampleValueType.TRUE;
} else {
if (!checkedValues.contains(CounterExampleValueType.UNDEFINED)) {
if (!checkedValues.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.FALSE;
}
}
......
......@@ -6,6 +6,7 @@ import java.util.ArrayList;
import java.util.List;
import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.logging.Logger;
/**
* Provides an abstract class for all types of propositions.
......@@ -105,11 +106,13 @@ public abstract class CounterExampleProposition {
if (index != -1) {
int pos = isPastOperator ? index : index + position;
pos = calculatePosition(pos);
Logger.assertProB("Position invalid", pos >= 0);
positions.add(pos);
} else {
for (int i = 0; i < checkedSize; i++) {
int pos = isPastOperator ? position - i : position + i;
pos = calculatePosition(pos);
Logger.assertProB("Position invalid", pos >= 0);
positions.add(pos);
}
}
......
......@@ -7,7 +7,7 @@ import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.logging.Logger;
/**
* Provides a "Release" operator.
* Provides a "release" operator.
*
* @author Andriy Tolstoy
*
......@@ -38,9 +38,10 @@ public final class CounterExampleRelease extends CounterExampleBinaryOperator {
@Override
protected CounterExampleValueType calculate(final int position) {
CounterExampleValueType value = calculateReleaseOperator(position);
final CounterExampleValueType value = calculateReleaseOperator(position);
List<CounterExampleValueType> notUntilValues = notUntil.getValues();
final List<CounterExampleValueType> notUntilValues = notUntil
.getValues();
Logger.assertProB("Release invalid",
value == notUntilValues.get(position));
......@@ -49,7 +50,7 @@ public final class CounterExampleRelease extends CounterExampleBinaryOperator {
}
private CounterExampleValueType calculateReleaseOperator(final int position) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
List<CounterExampleValueType> firstCheckedValues = new ArrayList<CounterExampleValueType>(
getFirstArgument().getValues());
......@@ -80,36 +81,49 @@ public final class CounterExampleRelease extends CounterExampleBinaryOperator {
if (firstIndex != -1) {
// look for a state with a false value in second argument
secondCheckedValues = secondCheckedValues
.subList(0, firstIndex + 1);
secondIndex = secondCheckedValues
secondIndex = secondCheckedValues.subList(0, firstIndex + 1)
.indexOf(CounterExampleValueType.FALSE);
if (secondIndex == -1) {
trueOrUnknown = true;
if (pathType != PathType.REDUCED) {
result = CounterExampleValueType.TRUE;
} else {
// look for the state with an unknown value in second
// argument
if (secondCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
firstCheckedValues = firstCheckedValues.subList(0,
firstIndex + 1);
secondCheckedValues = secondCheckedValues.subList(0,
firstIndex + 1);
// look for a state with an unknown value in first and
// second argument
final int unknownStateIndex = indexOfUnknownState(
firstCheckedValues, secondCheckedValues, false);
if (unknownStateIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(0,
unknownStateIndex + 1);
secondCheckedValues = secondCheckedValues.subList(0,
unknownStateIndex + 1);
firstIndex = -1;
} else {
// look for the state with an unknown value in second
// argument
if (!secondCheckedValues
.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.TRUE;
} else {
firstIndex = -1;
}
}
}
} else {
// look for a state with a false value in second argument
if (!secondCheckedValues.contains(CounterExampleValueType.FALSE)) {
if (pathType != PathType.REDUCED) {
// all states of first argument are invalid and all states of second
// argument are valid on a finite or an infinite path
if (pathType != PathType.REDUCED
&& !secondCheckedValues
.contains(CounterExampleValueType.FALSE)) {
trueOrUnknown = true;
result = CounterExampleValueType.TRUE;
}
firstCheckedValues.clear();
}
}
......@@ -122,36 +136,41 @@ public final class CounterExampleRelease extends CounterExampleBinaryOperator {
firstCheckedValues = firstCheckedValues.subList(0, secondIndex);
firstIndex = -1;
if (pathType != PathType.REDUCED) {
// look for a state with an unknown value in first argument
if (!firstCheckedValues
.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.FALSE;
} else {
// look for a state with an unknown value in first argument
if (firstCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
// look for a state with an unknown value in first and
// second argument
final int unknownStateIndex = indexOfUnknownState(
firstCheckedValues,
secondCheckedValues.subList(0, secondIndex), false);
if (unknownStateIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(0,
unknownStateIndex + 1);
secondCheckedValues = secondCheckedValues.subList(0,
unknownStateIndex + 1);
} else {
secondCheckedValues = secondCheckedValues.subList(0,
secondIndex + 1);
secondIndex = -1;
} else {
result = CounterExampleValueType.FALSE;
}
secondIndex = -1;
}
} else {
if (pathType != PathType.REDUCED) {
result = CounterExampleValueType.FALSE;
} else {
for (int i = 0; i < firstCheckedValues.size(); i++) {
if (firstCheckedValues.get(i).equals(
CounterExampleValueType.UNDEFINED)
&& secondCheckedValues.get(i).equals(
CounterExampleValueType.UNDEFINED)) {
firstCheckedValues = firstCheckedValues.subList(0,
i + 1);
secondCheckedValues = secondCheckedValues.subList(
0, i + 1);
// look for a state with an unknown value in first and
// second argument
final int unknownStateIndex = indexOfUnknownState(
firstCheckedValues, secondCheckedValues, false);
break;
}
}
if (unknownStateIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(0,
unknownStateIndex + 1);
secondCheckedValues = secondCheckedValues.subList(0,
unknownStateIndex + 1);
}
}
}
......
package de.prob.core.domainobjects.ltl;
import java.util.ArrayList;
import java.util.List;
import de.prob.core.command.LtlCheckingCommand.PathType;
/**
* Provides a "Since" operator.
* Provides a "since" operator.
*
* @author Andriy Tolstoy
*
......@@ -26,18 +27,18 @@ public final class CounterExampleSince extends CounterExampleBinaryOperator {
@Override
protected CounterExampleValueType calculate(final int position) {
CounterExampleValueType result = calculateSinceOperator(position);
final CounterExampleValueType result = calculateSinceOperator(position);
return result;
}
private CounterExampleValueType calculateSinceOperator(final int position) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
// remove all future values
List<CounterExampleValueType> firstCheckedValues = getFirstArgument()
.getValues().subList(0, position + 1);
List<CounterExampleValueType> secondCheckedValues = getSecondArgument()
.getValues().subList(0, position + 1);
List<CounterExampleValueType> firstCheckedValues = new ArrayList<CounterExampleValueType>(
getFirstArgument().getValues().subList(0, position + 1));
List<CounterExampleValueType> secondCheckedValues = new ArrayList<CounterExampleValueType>(
getSecondArgument().getValues().subList(0, position + 1));
int firstIndex = -1;
......@@ -49,78 +50,102 @@ public final class CounterExampleSince extends CounterExampleBinaryOperator {
if (secondIndex != -1) {
// look for a state with a false value in first argument
firstCheckedValues = firstCheckedValues.subList(secondIndex + 1,
position + 1);
firstIndex = firstCheckedValues
.lastIndexOf(CounterExampleValueType.FALSE);
firstIndex = firstCheckedValues.subList(secondIndex + 1,
firstCheckedValues.size()).lastIndexOf(
CounterExampleValueType.FALSE);
if (firstIndex == -1) {
trueOrUnknown = true;
if (pathType != PathType.REDUCED) {
result = CounterExampleValueType.TRUE;
// look for a state with an unknown value in first and
// second argument
int unknownStateIndex = indexOfUnknownState(
firstCheckedValues.subList(secondIndex + 1,
firstCheckedValues.size()),
secondCheckedValues.subList(secondIndex + 1,
secondCheckedValues.size()), true);
if (unknownStateIndex != -1) {
unknownStateIndex += (secondIndex + 1);
firstCheckedValues = firstCheckedValues.subList(
unknownStateIndex, firstCheckedValues.size());
secondCheckedValues = secondCheckedValues.subList(
unknownStateIndex, secondCheckedValues.size());
secondIndex = -1;
} else {
firstCheckedValues = firstCheckedValues.subList(
secondIndex + 1, firstCheckedValues.size());
// look for the state with an unknown value in first
// argument
if (firstCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
if (!firstCheckedValues
.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.TRUE;
} else {
secondCheckedValues = secondCheckedValues.subList(
secondIndex, position + 1);
secondIndex, secondCheckedValues.size());
secondIndex = -1;
} else {
result = CounterExampleValueType.TRUE;
}
}
}
}
if (!trueOrUnknown) {
firstCheckedValues = getFirstArgument().getValues().subList(0,
position + 1);
secondCheckedValues = getSecondArgument().getValues().subList(0,
position + 1);
// look for a state with a false value in first argument
firstIndex = firstCheckedValues
.lastIndexOf(CounterExampleValueType.FALSE);
if (firstIndex != -1) {
secondCheckedValues = secondCheckedValues.subList(firstIndex,
position + 1);
secondCheckedValues.size());
secondIndex = -1;
if (pathType != PathType.REDUCED) {
// look for a state with an unknown value in second argument
if (!secondCheckedValues
.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.FALSE;
} else {
// look for a state with an unknown value in second argument
if (secondCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
firstCheckedValues = firstCheckedValues.subList(firstIndex,
firstCheckedValues.size());
// look for a state with an unknown value in first and
// second argument
int unknownStateIndex = indexOfUnknownState(
firstCheckedValues, secondCheckedValues, true);
if (unknownStateIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(
firstIndex, position + 1);
firstIndex = -1;
} else {
result = CounterExampleValueType.FALSE;
unknownStateIndex, firstCheckedValues.size());
secondCheckedValues = secondCheckedValues.subList(
unknownStateIndex, secondCheckedValues.size());
}
firstIndex = -1;
}
} else {
if (!firstCheckedValues
.contains(CounterExampleValueType.UNDEFINED)
// all states of first argument are valid and all states of
// second argument are invalid
if (!firstCheckedValues.contains(CounterExampleValueType.FALSE)
&& !firstCheckedValues
.contains(CounterExampleValueType.UNKNOWN)
&& !secondCheckedValues
.contains(CounterExampleValueType.TRUE)
&& !secondCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.FALSE;
firstCheckedValues.clear();
} else {
for (int i = firstCheckedValues.size() - 1; i >= 0; i--) {
if (firstCheckedValues.get(i).equals(
CounterExampleValueType.UNDEFINED)
&& secondCheckedValues.get(i).equals(
CounterExampleValueType.UNDEFINED)) {
firstCheckedValues = firstCheckedValues.subList(i,
position + 1);
secondCheckedValues = secondCheckedValues.subList(
i, position + 1);
// look for a state with an unknown value in first and
// second argument
final int unknownStateIndex = indexOfUnknownState(
firstCheckedValues, secondCheckedValues, true);
break;
}
if (unknownStateIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(
unknownStateIndex, firstCheckedValues.size());
secondCheckedValues = secondCheckedValues.subList(
unknownStateIndex, secondCheckedValues.size());
}
}
}
......
......@@ -4,7 +4,14 @@ import java.util.List;
import de.prob.core.command.LtlCheckingCommand.PathType;
public class CounterExampleTransition extends CounterExamplePredicate {
/**
* Provides transitions.
*
* @author Andriy Tolstoy
*
*/
public final class CounterExampleTransition extends CounterExamplePredicate {
public CounterExampleTransition(final String name, final PathType pathType,
final int loopEntry, final List<CounterExampleValueType> values) {
super(name, pathType, loopEntry, values);
......
package de.prob.core.domainobjects.ltl;
import java.util.ArrayList;
import java.util.List;
import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.logging.Logger;
/**
* Provides a "Trigger" operator.
* Provides a "trigger" operator.
*
* @author Andriy Tolstoy
*
......@@ -37,9 +38,10 @@ public final class CounterExampleTrigger extends CounterExampleBinaryOperator {
@Override
protected CounterExampleValueType calculate(final int position) {
CounterExampleValueType value = calculateTriggerOperator(position);
final CounterExampleValueType value = calculateTriggerOperator(position);
List<CounterExampleValueType> notSinceValues = notSince.getValues();
final List<CounterExampleValueType> notSinceValues = notSince
.getValues();
Logger.assertProB("Trigger invalid",
value == notSinceValues.get(position));
......@@ -48,13 +50,13 @@ public final class CounterExampleTrigger extends CounterExampleBinaryOperator {
}
private CounterExampleValueType calculateTriggerOperator(final int position) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
// remove all future values
List<CounterExampleValueType> firstCheckedValues = getFirstArgument()
.getValues().subList(0, position + 1);
List<CounterExampleValueType> secondCheckedValues = getSecondArgument()
.getValues().subList(0, position + 1);
List<CounterExampleValueType> firstCheckedValues = new ArrayList<CounterExampleValueType>(
getFirstArgument().getValues().subList(0, position + 1));
List<CounterExampleValueType> secondCheckedValues = new ArrayList<CounterExampleValueType>(
getSecondArgument().getValues().subList(0, position + 1));
int secondIndex = -1;
......@@ -66,85 +68,107 @@ public final class CounterExampleTrigger extends CounterExampleBinaryOperator {
if (firstIndex != -1) {
// look for a state with a false value in second argument
secondCheckedValues = secondCheckedValues.subList(firstIndex,
position + 1);
secondIndex = secondCheckedValues
.lastIndexOf(CounterExampleValueType.FALSE);
secondIndex = secondCheckedValues.subList(firstIndex,
secondCheckedValues.size()).lastIndexOf(
CounterExampleValueType.FALSE);
if (secondIndex == -1) {
trueOrUnknown = true;
if (pathType != PathType.REDUCED) {
result = CounterExampleValueType.TRUE;
// look for a state with an unknown value in first and
// second argument
int unknownStateIndex = indexOfUnknownState(
firstCheckedValues.subList(firstIndex,
firstCheckedValues.size()),
secondCheckedValues.subList(firstIndex,
secondCheckedValues.size()), true);
if (unknownStateIndex != -1) {
unknownStateIndex += firstIndex;
firstCheckedValues = firstCheckedValues.subList(
unknownStateIndex, firstCheckedValues.size());
secondCheckedValues = secondCheckedValues.subList(
unknownStateIndex, secondCheckedValues.size());
firstIndex = -1;
} else {
secondCheckedValues = secondCheckedValues.subList(
firstIndex, secondCheckedValues.size());
// look for the state with an unknown value in second
// argument
if (secondCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
if (!secondCheckedValues
.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.TRUE;
} else {
firstCheckedValues = firstCheckedValues.subList(
firstIndex, position + 1);
firstIndex, firstCheckedValues.size());
firstIndex = -1;
} else {
result = CounterExampleValueType.TRUE;
}
}
}
} else {
if (!firstCheckedValues.contains(CounterExampleValueType.UNDEFINED)
// all states of first argument are invalid and all states of second
// argument are valid on a finite or an infinite path
if (!firstCheckedValues.contains(CounterExampleValueType.UNKNOWN)
&& !secondCheckedValues
.contains(CounterExampleValueType.FALSE)
&& !secondCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
.contains(CounterExampleValueType.UNKNOWN)) {
trueOrUnknown = true;
result = CounterExampleValueType.TRUE;
firstCheckedValues.clear();
}
}
if (!trueOrUnknown) {
firstCheckedValues = getFirstArgument().getValues().subList(0,
position + 1);
secondCheckedValues = getSecondArgument().getValues().subList(0,
position + 1);
// look for a state with a false value in second argument
secondIndex = secondCheckedValues
.lastIndexOf(CounterExampleValueType.FALSE);
if (secondIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(
secondIndex + 1, position + 1);
secondIndex + 1, firstCheckedValues.size());
firstIndex = -1;
if (pathType != PathType.REDUCED) {
// look for a state with an unknown value in first argument
if (!firstCheckedValues
.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.FALSE;
} else {
// look for a state with an unknown value in first argument
if (firstCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
// look for a state with an unknown value in first and
// second argument
int unknownStateIndex = indexOfUnknownState(
firstCheckedValues,
secondCheckedValues.subList(secondIndex + 1,
secondCheckedValues.size()), true);
if (unknownStateIndex != -1) {
secondCheckedValues = secondCheckedValues.subList(
secondIndex, position + 1);
secondIndex = -1;
secondIndex + 1, secondCheckedValues.size());
firstCheckedValues = firstCheckedValues.subList(
unknownStateIndex, firstCheckedValues.size());
secondCheckedValues = secondCheckedValues.subList(
unknownStateIndex, secondCheckedValues.size());
} else {
result = CounterExampleValueType.FALSE;
secondCheckedValues = secondCheckedValues.subList(
secondIndex, secondCheckedValues.size());
}
secondIndex = -1;
}
} else {
if (pathType != PathType.REDUCED) {
result = CounterExampleValueType.FALSE;
} else {
for (int i = firstCheckedValues.size() - 1; i >= 0; i--) {
if (firstCheckedValues.get(i).equals(
CounterExampleValueType.UNDEFINED)
&& secondCheckedValues.get(i).equals(
CounterExampleValueType.UNDEFINED)) {
firstCheckedValues = firstCheckedValues.subList(i,
position + 1);
secondCheckedValues = secondCheckedValues.subList(
i, position + 1);
// look for a state with an unknown value in first and
// second argument
final int unknownStateIndex = indexOfUnknownState(
firstCheckedValues, secondCheckedValues, true);
break;
}
}
if (unknownStateIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(
unknownStateIndex, firstCheckedValues.size());
secondCheckedValues = secondCheckedValues.subList(
unknownStateIndex, secondCheckedValues.size());
}
}
}
......
......@@ -6,7 +6,7 @@ import java.util.List;
import de.prob.core.command.LtlCheckingCommand.PathType;
/**
* Provides an "Until" operator.
* Provides an "until" operator.
*
* @author Andriy Tolstoy
*
......@@ -19,14 +19,20 @@ public final class CounterExampleUntil extends CounterExampleBinaryOperator {
super("U", "Until", pathType, loopEntry, firstArgument, secondArgument);
}
public CounterExampleUntil(final PathType pathType,
final CounterExampleProposition firstArgument,
final CounterExampleProposition secondArgument) {
this(pathType, -1, firstArgument, secondArgument);
}
@Override
protected CounterExampleValueType calculate(final int position) {
CounterExampleValueType result = calculateUntilOperator(position);
final CounterExampleValueType result = calculateUntilOperator(position);
return result;
}
private CounterExampleValueType calculateUntilOperator(final int position) {
CounterExampleValueType result = CounterExampleValueType.UNDEFINED;
CounterExampleValueType result = CounterExampleValueType.UNKNOWN;
List<CounterExampleValueType> firstCheckedValues = new ArrayList<CounterExampleValueType>(
getFirstArgument().getValues());
......@@ -57,25 +63,39 @@ public final class CounterExampleUntil extends CounterExampleBinaryOperator {
if (secondIndex != -1) {
// look for a state with a false value in first argument
firstCheckedValues = firstCheckedValues.subList(0, secondIndex);
firstIndex = firstCheckedValues
.indexOf(CounterExampleValueType.FALSE);
firstIndex = firstCheckedValues.subList(0, secondIndex).indexOf(
CounterExampleValueType.FALSE);
if (firstIndex == -1) {
trueOrUnknown = true;
if (pathType != PathType.REDUCED) {
result = CounterExampleValueType.TRUE;
} else {
// look for the state with an unknown value in first
// argument
if (firstCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
firstCheckedValues = firstCheckedValues.subList(0,
secondIndex + 1);
secondCheckedValues = secondCheckedValues.subList(0,
secondIndex + 1);
// look for a state with an unknown value in first and
// second argument
final int unknownStateIndex = indexOfUnknownState(
firstCheckedValues, secondCheckedValues, false);
if (unknownStateIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(0,
unknownStateIndex + 1);
secondCheckedValues = secondCheckedValues.subList(0,
unknownStateIndex + 1);
secondIndex = -1;
} else {
firstCheckedValues = firstCheckedValues.subList(0,
secondIndex);
// look for a state with an unknown value in first argument
if (!firstCheckedValues
.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.TRUE;
} else {
secondIndex = -1;
}
}
}
......@@ -91,35 +111,48 @@ public final class CounterExampleUntil extends CounterExampleBinaryOperator {
firstIndex + 1);
secondIndex = -1;
if (pathType != PathType.REDUCED) {
// look for a state with an unknown value in second argument
if (!secondCheckedValues
.contains(CounterExampleValueType.UNKNOWN)) {
result = CounterExampleValueType.FALSE;
} else {
// look for a state with an unknown value in second argument
if (secondCheckedValues
.contains(CounterExampleValueType.UNDEFINED)) {
firstCheckedValues = firstCheckedValues.subList(0,
firstIndex + 1);
firstIndex = -1;
} else {
result = CounterExampleValueType.FALSE;
// look for a state with an unknown value in first and
// second argument
final int unknownStateIndex = indexOfUnknownState(
firstCheckedValues, secondCheckedValues, false);
if (unknownStateIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(0,
unknownStateIndex + 1);
secondCheckedValues = secondCheckedValues.subList(0,
unknownStateIndex + 1);
}
}
} else {
if (pathType != PathType.REDUCED) {
// all states of first argument are valid and all states of
// second argument are invalid on a finite or an infinite path
if (pathType != PathType.REDUCED
&& !firstCheckedValues
.contains(CounterExampleValueType.FALSE)
&& !secondCheckedValues
.contains(CounterExampleValueType.TRUE)) {
result = CounterExampleValueType.FALSE;
firstCheckedValues.clear();
} else {
for (int i = 0; i < firstCheckedValues.size(); i++) {
if (firstCheckedValues.get(i).equals(
CounterExampleValueType.UNDEFINED)
&& secondCheckedValues.get(i).equals(
CounterExampleValueType.UNDEFINED)) {
firstCheckedValues = firstCheckedValues.subList(0,
i + 1);
secondCheckedValues = secondCheckedValues.subList(
0, i + 1);
// look for a state with an unknown value in first and
// second argument
final int unknownStateIndex = indexOfUnknownState(
firstCheckedValues, secondCheckedValues, false);
break;
}
if (unknownStateIndex != -1) {
firstCheckedValues = firstCheckedValues.subList(0,
unknownStateIndex + 1);
secondCheckedValues = secondCheckedValues.subList(0,
unknownStateIndex + 1);
}
}
}
......
package de.prob.core.domainobjects.ltl;
public enum CounterExampleValueType {
TRUE, FALSE, UNDEFINED;
TRUE, FALSE, UNKNOWN;
@Override
public String toString() {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment