From a2ec771bde9bbeab0827642ef3fbb79b6847d578 Mon Sep 17 00:00:00 2001
From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de>
Date: Tue, 31 Oct 2023 15:37:54 +0100
Subject: [PATCH] Update usages of Prolog Library for Abstract Integer
Representation
---
.gitignore | 1 +
.../core/command/ComputeCoverageCommand.java | 13 ++++++++++---
.../prob/core/command/LtlCheckingCommand.java | 5 ++---
.../prob/core/command/ModelCheckingCommand.java | 9 +++------
.../de/prob/core/domainobjects/Operation.java | 17 +++++++----------
.../core/domainobjects/ltl/CounterExample.java | 9 ++++-----
.../commands/GenerateLocalTestcasesCommand.java | 8 +++-----
.../sap/commands/GenerateTestcaseCommand.java | 6 +++---
.../src/de/prob/ui/ProBGeneralPreferences.java | 10 +++++-----
9 files changed, 38 insertions(+), 40 deletions(-)
diff --git a/.gitignore b/.gitignore
index df249aee..bcc069bd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,6 @@
**/bin/
**/target/
+.idea/
.gradle/
.metadata/
**/pom.xml
diff --git a/de.prob.core/src/de/prob/core/command/ComputeCoverageCommand.java b/de.prob.core/src/de/prob/core/command/ComputeCoverageCommand.java
index 4561a706..960b30a4 100644
--- a/de.prob.core/src/de/prob/core/command/ComputeCoverageCommand.java
+++ b/de.prob.core/src/de/prob/core/command/ComputeCoverageCommand.java
@@ -14,7 +14,7 @@ import de.prob.core.Animator;
import de.prob.exceptions.ProBException;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.IntegerPrologTerm;
+import de.prob.prolog.term.AIntegerPrologTerm;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
@@ -29,9 +29,16 @@ public final class ComputeCoverageCommand implements IComposableCommand {
private final List<String> nodes = new ArrayList<String>();
private final List<String> uncovered = new ArrayList<String>();
+ @Deprecated
public ComputeCoverageResult(final IntegerPrologTerm totalNumberOfNodes,
final IntegerPrologTerm totalNumberOfTransitions, final ListPrologTerm ops, final ListPrologTerm nodes,
final ListPrologTerm uncovered) {
+ this((AIntegerPrologTerm) totalNumberOfNodes, totalNumberOfTransitions, ops, nodes, uncovered);
+ }
+
+ public ComputeCoverageResult(final AIntegerPrologTerm totalNumberOfNodes,
+ final AIntegerPrologTerm totalNumberOfTransitions, final ListPrologTerm ops, final ListPrologTerm nodes,
+ final ListPrologTerm uncovered) {
this.totalNumberOfNodes = totalNumberOfNodes.getValue();
this.totalNumberOfTransitions = totalNumberOfTransitions.getValue();
for (PrologTerm op : ops) {
@@ -83,8 +90,8 @@ public final class ComputeCoverageCommand implements IComposableCommand {
@Override
public void processResult(final ISimplifiedROMap<String, PrologTerm> bindings) throws CommandException {
- IntegerPrologTerm totalNodeNr = (IntegerPrologTerm) bindings.get("TotalNodeNr");
- IntegerPrologTerm totalTransNr = (IntegerPrologTerm) bindings.get("TotalTransSum");
+ AIntegerPrologTerm totalNodeNr = (AIntegerPrologTerm) bindings.get("TotalNodeNr");
+ AIntegerPrologTerm totalTransNr = (AIntegerPrologTerm) bindings.get("TotalTransSum");
ListPrologTerm ops = (ListPrologTerm) bindings.get("OpStat");
ListPrologTerm nodes = (ListPrologTerm) bindings.get("NodeStat");
diff --git a/de.prob.core/src/de/prob/core/command/LtlCheckingCommand.java b/de.prob.core/src/de/prob/core/command/LtlCheckingCommand.java
index ed5320ea..59793d7e 100644
--- a/de.prob.core/src/de/prob/core/command/LtlCheckingCommand.java
+++ b/de.prob.core/src/de/prob/core/command/LtlCheckingCommand.java
@@ -11,8 +11,8 @@ import de.prob.core.domainobjects.Operation;
import de.prob.exceptions.ProBException;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.term.AIntegerPrologTerm;
import de.prob.prolog.term.CompoundPrologTerm;
-import de.prob.prolog.term.IntegerPrologTerm;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
@@ -206,8 +206,7 @@ public final class LtlCheckingCommand implements IComposableCommand {
loopEntry = -1;
} else if (loopStatus.hasFunctor("loop", 1)) {
pathType = PathType.INFINITE;
- loopEntry = ((IntegerPrologTerm) loopStatus.getArgument(1))
- .getValue().intValue();
+ loopEntry = ((AIntegerPrologTerm) loopStatus.getArgument(1)).intValueExact();
} else
throw new CommandException(
"LTL model check returned unexpected loop status: "
diff --git a/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java b/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java
index 5e5858fe..8b160009 100644
--- a/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java
+++ b/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java
@@ -59,12 +59,9 @@ public final class ModelCheckingCommand implements IComposableCommand {
CompoundPrologTerm term = (CompoundPrologTerm) bindings.get("Result");
CompoundPrologTerm stats = (CompoundPrologTerm) bindings.get("Stats");
- int processedTotal = ((IntegerPrologTerm) stats.getArgument(3))
- .getValue().intValue();
- int numStates = ((IntegerPrologTerm) stats.getArgument(1)).getValue()
- .intValue();
- int numTransitions = ((IntegerPrologTerm) stats.getArgument(2))
- .getValue().intValue();
+ int processedTotal = ((AIntegerPrologTerm) stats.getArgument(3)).intValueExact();
+ int numStates = ((AIntegerPrologTerm) stats.getArgument(1)).intValueExact();
+ int numTransitions = ((AIntegerPrologTerm) stats.getArgument(2)).intValueExact();
result = new ModelCheckingResult<Result>(Result.class, term,
processedTotal, numStates, numTransitions);
diff --git a/de.prob.core/src/de/prob/core/domainobjects/Operation.java b/de.prob.core/src/de/prob/core/domainobjects/Operation.java
index 16c341bb..8c586d7e 100644
--- a/de.prob.core/src/de/prob/core/domainobjects/Operation.java
+++ b/de.prob.core/src/de/prob/core/domainobjects/Operation.java
@@ -12,8 +12,8 @@ import java.util.HashMap;
import java.util.List;
import java.util.Map;
+import de.prob.prolog.term.AIntegerPrologTerm;
import de.prob.prolog.term.CompoundPrologTerm;
-import de.prob.prolog.term.IntegerPrologTerm;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
import de.prob.unicode.UnicodeTranslator;
@@ -121,9 +121,8 @@ public final class Operation {
public static Operation fromPrologTerm(final PrologTerm rawOpTerm) {
final CompoundPrologTerm opTerm = (CompoundPrologTerm) rawOpTerm;
- final IntegerPrologTerm pInt = (IntegerPrologTerm) opTerm
- .getArgument(ID);
- final long id = pInt.getValue().longValue();
+ final AIntegerPrologTerm pInt = (AIntegerPrologTerm) opTerm.getArgument(ID);
+ final long id = pInt.longValueExact();
final String name = PrologTerm.atomicString(opTerm.getArgument(NAME));
final EventType type = SPECIAL_EVENTS.get(name);
final String destId = getIdFromPrologTerm(opTerm.getArgument(DST));
@@ -171,8 +170,8 @@ public final class Operation {
.getArgument(ARGS_PRETTY));
this.hashCode = initHashCode();
- final IntegerPrologTerm pInt = (IntegerPrologTerm) term.getArgument(ID);
- this.id = pInt.getValue().longValue();
+ final AIntegerPrologTerm pInt = (AIntegerPrologTerm) term.getArgument(ID);
+ this.id = pInt.longValueExact();
this.eventStack = createEventStack((ListPrologTerm) term
.getArgument(INFOS));
}
@@ -244,10 +243,8 @@ public final class Operation {
}
private static String getIdFromPrologTerm(final PrologTerm destTerm) {
- if (destTerm instanceof IntegerPrologTerm) {
- return ((IntegerPrologTerm) destTerm).getValue().toString();
- }
- return ((CompoundPrologTerm) destTerm).getFunctor();
+ // integer terms have their string representation as functor
+ return destTerm.atomicToString();
}
public long getId() {
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 5d3020a1..39951780 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
@@ -9,8 +9,8 @@ import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.core.command.LtlCheckingCommand.Result;
import de.prob.core.domainobjects.Operation;
import de.prob.logging.Logger;
+import de.prob.prolog.term.AIntegerPrologTerm;
import de.prob.prolog.term.CompoundPrologTerm;
-import de.prob.prolog.term.IntegerPrologTerm;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
@@ -98,8 +98,7 @@ public class CounterExample {
.getArgument(3);
for (int i = 0; i < values.size(); i++) {
- int value = ((IntegerPrologTerm) values.get(i)).getValue()
- .intValue();
+ int value = ((AIntegerPrologTerm) values.get(i)).intValueExact();
// 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);
@@ -140,9 +139,9 @@ public class CounterExample {
Arrays.asList(values));
} else if (arity == 1) {
if (functor.equals("ap") || functor.equals("tp")) {
- IntegerPrologTerm atomic = (IntegerPrologTerm) term
+ AIntegerPrologTerm atomic = (AIntegerPrologTerm) term
.getArgument(1);
- int atomicId = atomic.getValue().intValue();
+ int atomicId = atomic.intValueExact();
final String name = atomicFormulaNames[atomicId];
diff --git a/de.prob.core/src/de/prob/sap/commands/GenerateLocalTestcasesCommand.java b/de.prob.core/src/de/prob/sap/commands/GenerateLocalTestcasesCommand.java
index 8d5d9235..e1c43110 100644
--- a/de.prob.core/src/de/prob/sap/commands/GenerateLocalTestcasesCommand.java
+++ b/de.prob.core/src/de/prob/sap/commands/GenerateLocalTestcasesCommand.java
@@ -12,7 +12,7 @@ import de.prob.core.command.IComposableCommand;
import de.prob.exceptions.ProBException;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.IntegerPrologTerm;
+import de.prob.prolog.term.AIntegerPrologTerm;
import de.prob.prolog.term.PrologTerm;
public class GenerateLocalTestcasesCommand implements IComposableCommand {
@@ -41,10 +41,8 @@ public class GenerateLocalTestcasesCommand implements IComposableCommand {
public void processResult(
final ISimplifiedROMap<String, PrologTerm> bindings)
throws CommandException {
- final int sat = ((IntegerPrologTerm) bindings.get("SAT")).getValue()
- .intValue();
- final int unsat = ((IntegerPrologTerm) bindings.get("UNSAT"))
- .getValue().intValue();
+ final int sat = ((AIntegerPrologTerm) bindings.get("SAT")).intValueExact();
+ final int unsat = ((AIntegerPrologTerm) bindings.get("UNSAT")).intValueExact();
result = new LocalTestcasesResult(sat, unsat);
}
diff --git a/de.prob.core/src/de/prob/sap/commands/GenerateTestcaseCommand.java b/de.prob.core/src/de/prob/sap/commands/GenerateTestcaseCommand.java
index 3ba18c58..5cfa51ce 100644
--- a/de.prob.core/src/de/prob/sap/commands/GenerateTestcaseCommand.java
+++ b/de.prob.core/src/de/prob/sap/commands/GenerateTestcaseCommand.java
@@ -25,7 +25,7 @@ import de.prob.core.command.LoadEventBModelCommand;
import de.prob.exceptions.ProBException;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.IntegerPrologTerm;
+import de.prob.prolog.term.AIntegerPrologTerm;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
import de.prob.sap.exceptions.ParseProblemException;
@@ -133,9 +133,9 @@ public class GenerateTestcaseCommand implements IComposableCommand {
public void processResult(
final ISimplifiedROMap<String, PrologTerm> bindings)
throws CommandException {
- final IntegerPrologTerm pNumberTests = (IntegerPrologTerm) bindings
+ final AIntegerPrologTerm pNumberTests = (AIntegerPrologTerm) bindings
.get(NUMBER_TESTCASES);
- final int numberOfTests = pNumberTests.getValue().intValue();
+ final int numberOfTests = pNumberTests.intValueExact();
final ListPrologTerm pEvents = (ListPrologTerm) bindings
.get(UNCOVERED_EVENTS);
diff --git a/de.prob.ui/src/de/prob/ui/ProBGeneralPreferences.java b/de.prob.ui/src/de/prob/ui/ProBGeneralPreferences.java
index 8ffedede..7562adf1 100644
--- a/de.prob.ui/src/de/prob/ui/ProBGeneralPreferences.java
+++ b/de.prob.ui/src/de/prob/ui/ProBGeneralPreferences.java
@@ -35,8 +35,8 @@ import de.prob.core.command.GetPreferencesCommand;
import de.prob.core.domainobjects.ProBPreference;
import de.prob.exceptions.ProBException;
import de.prob.logging.Logger;
+import de.prob.prolog.term.AIntegerPrologTerm;
import de.prob.prolog.term.CompoundPrologTerm;
-import de.prob.prolog.term.IntegerPrologTerm;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
@@ -154,12 +154,12 @@ public class ProBGeneralPreferences extends FieldEditorPreferencePage implements
BooleanFieldEditor.SEPARATE_LABEL, parent);
} else if (type.hasFunctor("range", 2)) {
final CompoundPrologTerm range = (CompoundPrologTerm) type;
- final BigInteger lower = ((IntegerPrologTerm) range.getArgument(1))
+ final BigInteger lower = ((AIntegerPrologTerm) range.getArgument(1))
.getValue();
- final BigInteger upper = ((IntegerPrologTerm) range.getArgument(2))
+ final BigInteger upper = ((AIntegerPrologTerm) range.getArgument(2))
.getValue();
- field = createIntField(name, desc, parent, lower.intValue(), upper
- .intValue());
+ field = createIntField(name, desc, parent, lower.intValueExact(), upper
+ .intValueExact());
} else if (type.isList()) {
final ListPrologTerm typelist = (ListPrologTerm) type;
final String[][] comboEntries = new String[typelist.size()][2];
--
GitLab