From b80a56fa121a4db33c5081981e883524ecfae0f0 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 24 Jan 2025 07:38:27 +0100
Subject: [PATCH] delete UtilMethods class
filter more description nodes at the beginning
---
.../de/tlc4b/analysis/MachineContext.java | 7 +--
.../java/de/tlc4b/analysis/Typechecker.java | 10 ++--
.../analysis/UnsupportedConstructsFinder.java | 18 ++++++
.../typerestriction/TypeRestrictor.java | 9 +--
.../de/tlc4b/btypes/EnumeratedSetElement.java | 4 +-
src/main/java/de/tlc4b/util/UtilMethods.java | 57 -------------------
6 files changed, 29 insertions(+), 76 deletions(-)
delete mode 100644 src/main/java/de/tlc4b/util/UtilMethods.java
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 92de466..ff19458 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -16,9 +16,6 @@ import de.tlc4b.exceptions.ScopeException;
import de.tlc4b.ltl.LTLBPredicate;
import de.tlc4b.ltl.LTLFormulaVisitor;
-import static de.tlc4b.util.UtilMethods.getIdentifierExpression;
-import static de.tlc4b.util.UtilMethods.getOperation;
-
public class MachineContext extends DepthFirstAdapter {
private String machineName;
@@ -391,7 +388,7 @@ public class MachineContext extends DepthFirstAdapter {
private void extractIdentifierExpressions(List<PExpression> copy, Map<String, Node> addToMap) {
for (PExpression e : copy) {
- AIdentifierExpression identifier = getIdentifierExpression(e);
+ AIdentifierExpression identifier = (AIdentifierExpression) e;
String name = Utils.getTIdentifierListAsString(identifier.getIdentifier());
exist(identifier.getIdentifier());
addToMap.put(name, identifier);
@@ -557,7 +554,7 @@ public class MachineContext extends DepthFirstAdapter {
List<POperation> copy = new ArrayList<>(node.getOperations());
// first collect all operations
for (POperation e : copy) {
- AOperation op = getOperation(e);
+ AOperation op = (AOperation) e;
String name = Utils.getTIdentifierListAsString(op.getOpName());
// existString(name);
if (operations.containsKey(name)) {
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index b76c6da..01baa17 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -30,8 +30,6 @@ import de.tlc4b.exceptions.UnificationException;
import de.tlc4b.ltl.LTLBPredicate;
import de.tlc4b.ltl.LTLFormulaVisitor;
-import static de.tlc4b.util.UtilMethods.getIdentifierExpression;
-
/**
* TODO we need a second run over the AST to check if all local variables have a
* type. This run should be performed after the normal model checking task.
@@ -181,25 +179,25 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAConstantsMachineClause(AConstantsMachineClause node) {
List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
- copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType()));
+ copy.forEach(e -> setType(e, new UntypedType()));
}
@Override
public void caseAAbstractConstantsMachineClause(AAbstractConstantsMachineClause node) {
List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
- copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType()));
+ copy.forEach(e -> setType(e, new UntypedType()));
}
@Override
public void caseAVariablesMachineClause(AVariablesMachineClause node) {
List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
- copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType()));
+ copy.forEach(e -> setType(e, new UntypedType()));
}
@Override
public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
- copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType()));
+ copy.forEach(e -> setType(e, new UntypedType()));
}
/**
diff --git a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
index eaeb668..1860cd3 100644
--- a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
+++ b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
@@ -88,4 +88,22 @@ public class UnsupportedConstructsFinder extends DepthFirstAdapter {
node.getPredicate().apply(this);
node.replaceBy(node.getPredicate());
}
+
+ @Override
+ public void caseADescriptionExpression(ADescriptionExpression node) {
+ node.getExpression().apply(this);
+ node.replaceBy(node.getExpression());
+ }
+
+ @Override
+ public void caseADescriptionOperation(ADescriptionOperation node) {
+ node.getOperation().apply(this);
+ node.replaceBy(node.getOperation());
+ }
+
+ @Override
+ public void caseADescriptionSet(ADescriptionSet node) {
+ node.getSet().apply(this);
+ node.replaceBy(node.getSet());
+ }
}
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 479abd5..2d2a7d6 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -53,7 +53,6 @@ import de.tlc4b.analysis.Typechecker;
import de.tlc4b.btypes.BType;
import de.tlc4b.exceptions.NotSupportedException;
import de.tlc4b.ltl.LTLFormulaVisitor;
-import de.tlc4b.util.UtilMethods;
public class TypeRestrictor extends DepthFirstAdapter {
@@ -500,12 +499,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
AIdentifierExpression id = (AIdentifierExpression) e;
String localVariableName = Utils.getTIdentifierListAsString(id.getIdentifier());
throw new NotSupportedException(
- "Unable to restrict the type '"
- + conType
- + "' of identifier '"
- + localVariableName
+ "Unable to restrict the type '" + conType + "' of identifier '" + localVariableName
+ "' to a finite set. TLC is not able to handle infinite sets.\n"
- + UtilMethods.getPositionAsString(e));
+ + (e.getStartPos() == null ? "### Unknown position."
+ : "### Line " + e.getStartPos().getLine() + ", Column " + e.getEndPos().getPos()));
}
tree = conType.createASTNode(typechecker);
diff --git a/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java b/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
index e20b807..05cfb6a 100644
--- a/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
+++ b/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
@@ -2,9 +2,9 @@ package de.tlc4b.btypes;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.util.ASTBuilder;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.exceptions.UnificationException;
-import de.tlc4b.util.UtilMethods;
public class EnumeratedSetElement implements BType {
private final String name;
@@ -58,7 +58,7 @@ public class EnumeratedSetElement implements BType {
}
public PExpression createASTNode(Typechecker typechecker) {
- AIdentifierExpression id = UtilMethods.createAIdentifierExpression(name);
+ AIdentifierExpression id = ASTBuilder.createIdentifier(name);
typechecker.setType(id, new SetType(this));
return id;
}
diff --git a/src/main/java/de/tlc4b/util/UtilMethods.java b/src/main/java/de/tlc4b/util/UtilMethods.java
deleted file mode 100644
index 2e824b3..0000000
--- a/src/main/java/de/tlc4b/util/UtilMethods.java
+++ /dev/null
@@ -1,57 +0,0 @@
-package de.tlc4b.util;
-
-import java.util.ArrayList;
-
-import de.be4.classicalb.core.parser.node.*;
-import de.hhu.stups.sablecc.patch.SourcePosition;
-
-public class UtilMethods {
-
- public static AIdentifierExpression createAIdentifierExpression(String name) {
- TIdentifierLiteral literal = new TIdentifierLiteral(name);
- ArrayList<TIdentifierLiteral> idList = new ArrayList<>();
- idList.add(literal);
- return new AIdentifierExpression(idList);
- }
-
- public static AIdentifierExpression getIdentifierExpression(PExpression e) {
- AIdentifierExpression identifier;
- if (e instanceof ADescriptionExpression) {
- identifier = getIdentifierExpression(((ADescriptionExpression) e).getExpression());
- } else if (e instanceof AIdentifierExpression) {
- identifier = (AIdentifierExpression) e;
- } else {
- throw new IllegalStateException("Unexpected expression type: " + e);
- }
- return identifier;
- }
-
- public static AOperation getOperation(POperation e) {
- AOperation op;
- if (e instanceof ADescriptionOperation) {
- op = getOperation(((ADescriptionOperation) e).getOperation());
- } else if (e instanceof AOperation) {
- op = (AOperation) e;
- } else {
- throw new IllegalStateException("Unexpected operation type: " + e);
- }
- return op;
- }
-
- public static String getPositionAsString(Node node) {
- StringBuilder sb = new StringBuilder();
- SourcePosition startPos = node.getStartPos();
- SourcePosition endPos = node.getEndPos();
- if (startPos == null) {
- sb.append("### Unknown position.");
- } else {
- sb.append("### Line ");
- sb.append(startPos.getLine());
- sb.append(", Column ");
- sb.append(endPos.getPos());
- }
-
- return sb.toString();
- }
-
-}
--
GitLab