Skip to content
Snippets Groups Projects
Commit a5e8c82a authored by dgelessus's avatar dgelessus
Browse files

Use Utils.isProBSpecialDefinitionName instead of hardcoding the names

parent ecb506e1
No related branches found
No related tags found
No related merge requests found
Pipeline #112042 passed
...@@ -4,17 +4,20 @@ import java.util.ArrayList; ...@@ -4,17 +4,20 @@ import java.util.ArrayList;
import java.util.HashSet; import java.util.HashSet;
import java.util.Set; 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.ASTConstants;
import tla2sany.semantic.AssumeNode; import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.ExprNode; import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode; import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.OpApplNode; import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode; import tla2sany.semantic.OpDefNode;
import tlc2.tool.ToolGlobals; 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 { public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<>(); private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<>();
...@@ -52,14 +55,8 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstan ...@@ -52,14 +55,8 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstan
for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) { for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) {
String defName = opDef.getName().toString(); String defName = opDef.getName().toString();
// GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, // GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, etc.
if (defName.equals("GOAL") || defName.startsWith("ANIMATION_") || defName.startsWith("CUSTOM_GRAPH_") if (Utils.isProBSpecialDefinitionName(defName)) {
|| 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_")) {
bDefinitionsSet.add(opDef); bDefinitionsSet.add(opDef);
} }
} }
......
...@@ -3,15 +3,18 @@ package de.tla2b.translation; ...@@ -3,15 +3,18 @@ package de.tla2b.translation;
import java.util.Collection; import java.util.Collection;
import java.util.HashSet; 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.ASTConstants;
import tla2sany.semantic.ModuleNode; import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode; import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode; import tla2sany.semantic.OpDefNode;
import tlc2.tool.ToolGlobals; 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 { public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
...@@ -58,15 +61,8 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTCons ...@@ -58,15 +61,8 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTCons
for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) { for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) {
String defName = opDef.getName().toString(); String defName = opDef.getName().toString();
// GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, // GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, etc.
if (defName.equals("GOAL") || defName.startsWith("ANIMATION_FUNCTION") if (Utils.isProBSpecialDefinitionName(defName)) {
|| 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_")) {
usedDefinitions.add(opDef); usedDefinitions.add(opDef);
} }
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment