From a5e8c82aabb1733bd7c2727f9935b4c7d11bf055 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Wed, 26 Apr 2023 10:10:37 +0200 Subject: [PATCH] Use Utils.isProBSpecialDefinitionName instead of hardcoding the names --- .../tla2b/translation/BDefinitionsFinder.java | 21 ++++++++---------- .../translation/UsedDefinitionsFinder.java | 22 ++++++++----------- 2 files changed, 18 insertions(+), 25 deletions(-) diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java index d853a5e..2c7cbc8 100644 --- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java +++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java @@ -4,17 +4,20 @@ import java.util.ArrayList; import java.util.HashSet; import java.util.Set; +import de.be4.classicalb.core.parser.util.Utils; +import de.tla2b.analysis.AbstractASTVisitor; +import de.tla2b.analysis.BOperation; +import de.tla2b.analysis.SpecAnalyser; +import de.tla2b.global.TranslationGlobals; + import tla2sany.semantic.ASTConstants; import tla2sany.semantic.AssumeNode; import tla2sany.semantic.ExprNode; import tla2sany.semantic.ExprOrOpArgNode; import tla2sany.semantic.OpApplNode; import tla2sany.semantic.OpDefNode; + import tlc2.tool.ToolGlobals; -import de.tla2b.analysis.AbstractASTVisitor; -import de.tla2b.analysis.BOperation; -import de.tla2b.analysis.SpecAnalyser; -import de.tla2b.global.TranslationGlobals; public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals { private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<>(); @@ -52,14 +55,8 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstan for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) { String defName = opDef.getName().toString(); - // GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, - if (defName.equals("GOAL") || defName.startsWith("ANIMATION_") || defName.startsWith("CUSTOM_GRAPH_") - || defName.startsWith("ASSERT_CTL") || defName.startsWith("ASSERT_LTL") - || defName.startsWith("SET_PREF_") || defName.startsWith("HEURISTIC_FUNCTION") - || defName.startsWith("VISB_SVG_") // VISB_SVG_OBJECTS, VISB_SVG_UPDATES, VISB_SVG_HOVERS - || defName.equals("VISB_JSON_FILE") - || defName.startsWith("GAME_") // GAME_OVER, GAME_PLAYER, GAME_MCTS_RUNS - || defName.startsWith("SCOPE") || defName.startsWith("scope_")) { + // GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, etc. + if (Utils.isProBSpecialDefinitionName(defName)) { bDefinitionsSet.add(opDef); } } diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java index 321ad57..b947fcc 100644 --- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java +++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java @@ -3,15 +3,18 @@ package de.tla2b.translation; import java.util.Collection; import java.util.HashSet; +import de.be4.classicalb.core.parser.util.Utils; +import de.tla2b.analysis.AbstractASTVisitor; +import de.tla2b.analysis.SpecAnalyser; +import de.tla2b.global.BBuiltInOPs; +import de.tla2b.global.TranslationGlobals; + import tla2sany.semantic.ASTConstants; import tla2sany.semantic.ModuleNode; import tla2sany.semantic.OpApplNode; import tla2sany.semantic.OpDefNode; + import tlc2.tool.ToolGlobals; -import de.tla2b.analysis.AbstractASTVisitor; -import de.tla2b.analysis.SpecAnalyser; -import de.tla2b.global.BBuiltInOPs; -import de.tla2b.global.TranslationGlobals; public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals { @@ -58,15 +61,8 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTCons for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) { String defName = opDef.getName().toString(); - // GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, - if (defName.equals("GOAL") || defName.startsWith("ANIMATION_FUNCTION") - || defName.startsWith("ANIMATION_IMG") - || defName.startsWith("ASSERT_LTL") || defName.startsWith("ASSERT_CTL") - || defName.startsWith("VISB_SVG_") // VISB_SVG_OBJECTS, VISB_SVG_UPDATES, VISB_SVG_HOVERS - || defName.equals("VISB_JSON_FILE") - || defName.startsWith("GAME_") // GAME_OVER, GAME_PLAYER, GAME_MCTS_RUNS - || defName.startsWith("SET_PREF_") || defName.startsWith("HEURISTIC_FUNCTION") - || defName.startsWith("SCOPE") || defName.startsWith("scope_")) { + // GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, etc. + if (Utils.isProBSpecialDefinitionName(defName)) { usedDefinitions.add(opDef); } } -- GitLab