From 29a2ede33731e2ea897e189102f215cab819ff81 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 24 Jan 2025 07:56:23 +0100
Subject: [PATCH] minor simplifications
---
src/main/java/de/tlc4b/analysis/Renamer.java | 6 +--
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 6 +--
src/main/java/de/tlc4b/tla/ConfigFile.java | 19 +++-----
.../tla/config/ConfigFileAssignment.java | 12 ++----
.../tla/config/ModelValueAssignment.java | 4 +-
.../config/SetOfModelValuesAssignment.java | 43 +++++--------------
src/main/java/de/tlc4b/tlc/TLCOutputInfo.java | 7 +--
src/main/java/de/tlc4b/tlc/TracePrinter.java | 3 +-
8 files changed, 27 insertions(+), 73 deletions(-)
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index 907739f..d98a9ff 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -147,13 +147,11 @@ public class Renamer extends DepthFirstAdapter {
for (PDefinition e : copy) {
String name = null;
if (e instanceof AExpressionDefinitionDefinition) {
- name = ((AExpressionDefinitionDefinition) e).getName()
- .getText();
+ name = ((AExpressionDefinitionDefinition) e).getName().getText();
} else if (e instanceof APredicateDefinitionDefinition) {
name = ((APredicateDefinitionDefinition) e).getName().getText();
} else if (e instanceof ASubstitutionDefinitionDefinition) {
- name = ((ASubstitutionDefinitionDefinition) e).getName()
- .getText();
+ name = ((ASubstitutionDefinitionDefinition) e).getName().getText();
}
String newName = incName(name);
namesTable.put(e, newName);
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 7c6f951..b43f7a1 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -247,16 +247,14 @@ public class TLAPrinter extends DepthFirstAdapter {
}
}
// CONSTANTS
- ArrayList<ConfigFileAssignment> assignments = configFile
- .getAssignments();
+ List<ConfigFileAssignment> assignments = configFile.getAssignments();
if (!assignments.isEmpty()) {
configFileString.append("CONSTANTS\n");
for (ConfigFileAssignment assignment : assignments) {
configFileString.append(assignment.getString(renamer));
}
}
- if (TLC4BGlobals.useSymmetry()
- && !machineContext.getDeferredSets().isEmpty()) {
+ if (TLC4BGlobals.useSymmetry() && !machineContext.getDeferredSets().isEmpty()) {
configFileString.append("SYMMETRY Symmetry\n");
}
diff --git a/src/main/java/de/tlc4b/tla/ConfigFile.java b/src/main/java/de/tlc4b/tla/ConfigFile.java
index 456c37d..9ae6778 100644
--- a/src/main/java/de/tlc4b/tla/ConfigFile.java
+++ b/src/main/java/de/tlc4b/tla/ConfigFile.java
@@ -1,46 +1,41 @@
package de.tlc4b.tla;
import java.util.ArrayList;
+import java.util.List;
import de.tlc4b.tla.config.ConfigFileAssignment;
-
public class ConfigFile {
- private final ArrayList<ConfigFileAssignment> assignments;
+ private final List<ConfigFileAssignment> assignments;
private int invariantNumber;
private boolean spec;
private boolean init;
private boolean next;
private int assertionsSize;
private boolean goal;
-
-
- public ConfigFile(){
+
+ public ConfigFile() {
this.assignments = new ArrayList<>();
this.invariantNumber = 0;
}
-
- public ArrayList<ConfigFileAssignment> getAssignments() {
+ public List<ConfigFileAssignment> getAssignments() {
return assignments;
}
public boolean isSpec(){
return spec;
}
-
public void setInvariantNumber(int number) {
this.invariantNumber = number;
}
-
public boolean isInit() {
return init;
}
-
public boolean isNext() {
return next;
}
@@ -49,22 +44,18 @@ public class ConfigFile {
assignments.add(assignment);
}
-
public int getInvariantNumber() {
return this.invariantNumber;
}
-
public void setInit() {
this.init = true;
}
-
public void setNext() {
this.next = true;
}
-
public void setAssertionSize(int size) {
assertionsSize = size;
}
diff --git a/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java b/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
index 64b0faf..e74f20d 100644
--- a/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
@@ -2,6 +2,7 @@ package de.tlc4b.tla.config;
import java.util.ArrayList;
import java.util.List;
+import java.util.stream.Collectors;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
@@ -12,14 +13,9 @@ public abstract class ConfigFileAssignment {
public abstract String getString(Renamer renamer);
public String getIdentifier(AIdentifierExpression node) {
- StringBuilder res = new StringBuilder();
-
- List<TIdentifierLiteral> copy = new ArrayList<>(
- node.getIdentifier());
- for (TIdentifierLiteral e : copy) {
- res.append(e.getText());
- }
- return res.toString();
+ return node.getIdentifier().stream()
+ .map(TIdentifierLiteral::getText)
+ .collect(Collectors.joining());
}
}
diff --git a/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java b/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java
index a92f636..d341ca8 100644
--- a/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java
@@ -13,9 +13,7 @@ public class ModelValueAssignment extends ConfigFileAssignment{
public String getString(Renamer renamer) {
AIdentifierExpression id = (AIdentifierExpression) node;
- getIdentifier(id);
String conString = renamer.getNameOfRef(id);
- return conString+ " = "+ conString +"\n";
+ return conString + " = " + conString + "\n";
}
-
}
diff --git a/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java b/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
index 5d0607d..b056554 100644
--- a/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
@@ -1,62 +1,39 @@
package de.tlc4b.tla.config;
-import java.util.List;
-
import de.be4.classicalb.core.parser.node.ADeferredSetSet;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.Node;
-import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.Renamer;
+import java.util.stream.Collectors;
+import java.util.stream.IntStream;
+
/**
*
* This class represents an assignment in the configuration file. The left side
* of the assignment is a constant and the right side a set of model values.
* E.g. k = {k1, k2, k3}
*/
-
public class SetOfModelValuesAssignment extends ConfigFileAssignment {
private final Node node;
private final int size;
public SetOfModelValuesAssignment(Node node, Integer size) {
this.node = node;
- if (size == null) {
- this.size = TLC4BGlobals.getDEFERRED_SET_SIZE();
- } else {
- this.size = size;
- }
-
+ this.size = size == null ? TLC4BGlobals.getDEFERRED_SET_SIZE() : size;
}
public String getString(Renamer renamer) {
- StringBuilder res = new StringBuilder();
-
- StringBuilder conString;
+ String conString;
if (node instanceof ADeferredSetSet) {
- conString = new StringBuilder();
- List<TIdentifierLiteral> copy = ((ADeferredSetSet) node)
- .getIdentifier();
- for (TIdentifierLiteral e : copy) {
- conString.append(e.getText());
- }
- conString = new StringBuilder(renamer.getName(node));
+ conString = renamer.getName(node);
} else {
- AIdentifierExpression id = (AIdentifierExpression) node;
- conString = new StringBuilder(getIdentifier(id));
+ conString = getIdentifier((AIdentifierExpression) node);
}
- res.append(conString).append(" = {");
- for (int j = 1; j < size + 1; j++) {
- res.append(conString).append(j);
- if (j < size) {
- res.append(",");
- }
- }
- res.append("}\n");
-
- return res.toString();
+ return conString + " = {" +
+ IntStream.rangeClosed(1, size).mapToObj(j -> conString + j).collect(Collectors.joining(",")) +
+ "}\n";
}
-
}
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index ed5a7bd..1a5407b 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -63,14 +63,11 @@ public class TLCOutputInfo {
identifiers.putAll(machineContext.getEnumValues());
//TODO add sets of modelvalues
-
- for (Entry<String, Node> entry : identifiers.entrySet()) {
- String name = entry.getKey();
- Node node = entry.getValue();
+ identifiers.forEach((name, node) -> {
String newName = renamer.getNameOfRef(node);
namesMapping.put(newName, name);
typesTable.put(newName, typechecker.getType(node));
- }
+ });
}
}
diff --git a/src/main/java/de/tlc4b/tlc/TracePrinter.java b/src/main/java/de/tlc4b/tlc/TracePrinter.java
index 6e5fd3e..7a4d7dc 100644
--- a/src/main/java/de/tlc4b/tlc/TracePrinter.java
+++ b/src/main/java/de/tlc4b/tlc/TracePrinter.java
@@ -147,8 +147,7 @@ public class TracePrinter {
} else {
BType subtype = ((FunctionType) type).getRange();
res.append("[");
- res.append(parseEnumerationValue(((TupleValue) val).elems,
- subtype));
+ res.append(parseEnumerationValue(((TupleValue) val).elems, subtype));
res.append("]");
}
return res;
--
GitLab