Skip to content
Snippets Groups Projects
Commit d5a5e840 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

changes for compatibility with new tlatoolbox

parent 15ff0639
No related branches found
No related tags found
No related merge requests found
Pipeline #139218 failed
...@@ -4,12 +4,12 @@ import de.tla2b.exceptions.ConfigFileErrorException; ...@@ -4,12 +4,12 @@ import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.exceptions.UnificationException; import de.tla2b.exceptions.UnificationException;
import de.tla2b.types.*; import de.tla2b.types.*;
import tla2sany.semantic.*; import tla2sany.semantic.*;
import tlc2.tool.ModelConfig; import tlc2.tool.impl.ModelConfig;
import tlc2.util.Vect; import tlc2.util.Vect;
import tlc2.value.IntValue; import tlc2.value.impl.IntValue;
import tlc2.value.ModelValue; import tlc2.value.impl.ModelValue;
import tlc2.value.SetEnumValue; import tlc2.value.impl.SetEnumValue;
import tlc2.value.Value; import tlc2.value.impl.Value;
import java.util.*; import java.util.*;
...@@ -464,7 +464,7 @@ public class ConfigfileEvaluator { ...@@ -464,7 +464,7 @@ public class ConfigfileEvaluator {
// IntValue iv = (IntValue) o; // IntValue iv = (IntValue) o;
return IntType.getInstance(); return IntType.getInstance();
} else if (o.getClass().getName().equals("tlc2.value.SetEnumValue")) { } else if (o.getClass().getName().equals("tlc2.value.impl.SetEnumValue")) {
SetEnumValue set = (SetEnumValue) o; SetEnumValue set = (SetEnumValue) o;
SetType t = new SetType(new UntypedType()); SetType t = new SetType(new UntypedType());
if (set.isEmpty()) { if (set.isEmpty()) {
...@@ -474,11 +474,11 @@ public class ConfigfileEvaluator { ...@@ -474,11 +474,11 @@ public class ConfigfileEvaluator {
TLAType elemType; TLAType elemType;
if (set.elems.elementAt(0).getClass().getName() if (set.elems.elementAt(0).getClass().getName()
.equals("tlc2.value.ModelValue")) { .equals("tlc2.value.impl.ModelValue")) {
EnumType e = new EnumType(new ArrayList<>()); EnumType e = new EnumType(new ArrayList<>());
for (int i = 0; i < set.size(); i++) { for (int i = 0; i < set.size(); i++) {
if (set.elems.elementAt(i).getClass().getName() if (set.elems.elementAt(i).getClass().getName()
.equals("tlc2.value.ModelValue")) { .equals("tlc2.value.impl.ModelValue")) {
String mv = set.elems.elementAt(i).toString(); String mv = set.elems.elementAt(i).toString();
if (!enumeratedSet.contains(mv)) { if (!enumeratedSet.contains(mv)) {
enumeratedSet.add(mv); enumeratedSet.add(mv);
...@@ -517,7 +517,7 @@ public class ConfigfileEvaluator { ...@@ -517,7 +517,7 @@ public class ConfigfileEvaluator {
t.setSubType(elemType); t.setSubType(elemType);
return t; return t;
} else if (o.getClass().getName().equals("tlc2.value.ModelValue")) { } else if (o.getClass().getName().equals("tlc2.value.impl.ModelValue")) {
ModelValue mv = (ModelValue) o; ModelValue mv = (ModelValue) o;
if (!enumeratedSet.contains(mv.toString())) { if (!enumeratedSet.contains(mv.toString())) {
enumeratedSet.add(mv.toString()); enumeratedSet.add(mv.toString());
...@@ -530,9 +530,9 @@ public class ConfigfileEvaluator { ...@@ -530,9 +530,9 @@ public class ConfigfileEvaluator {
return enumeratedTypes.get(mv.toString()); return enumeratedTypes.get(mv.toString());
} }
} else if (o.getClass().getName().equals("tlc2.value.StringValue")) { } else if (o.getClass().getName().equals("tlc2.value.impl.StringValue")) {
return StringType.getInstance(); return StringType.getInstance();
} else if (o.getClass().getName().equals("tlc2.value.BoolValue")) { } else if (o.getClass().getName().equals("tlc2.value.impl.BoolValue")) {
return BoolType.getInstance(); return BoolType.getInstance();
} else { } else {
throw new ConfigFileErrorException("Unkown ConstantType: " + o throw new ConfigFileErrorException("Unkown ConstantType: " + o
......
...@@ -5,7 +5,7 @@ import de.tla2b.types.TLAType; ...@@ -5,7 +5,7 @@ import de.tla2b.types.TLAType;
import tla2sany.semantic.AbortException; import tla2sany.semantic.AbortException;
import tla2sany.semantic.NumeralNode; import tla2sany.semantic.NumeralNode;
import tla2sany.st.TreeNode; import tla2sany.st.TreeNode;
import tlc2.value.Value; import tlc2.value.impl.Value;
public class TLCValueNode extends NumeralNode implements TranslationGlobals { public class TLCValueNode extends NumeralNode implements TranslationGlobals {
......
package de.tla2b.config; package de.tla2b.config;
import de.tla2b.types.TLAType; import de.tla2b.types.TLAType;
import tlc2.value.Value; import tlc2.value.impl.Value;
public class ValueObj { public class ValueObj {
private Value value; private Value value;
......
...@@ -17,11 +17,14 @@ import de.tla2b.types.*; ...@@ -17,11 +17,14 @@ import de.tla2b.types.*;
import tla2sany.semantic.*; import tla2sany.semantic.*;
import tla2sany.st.Location; import tla2sany.st.Location;
import tlc2.tool.BuiltInOPs; import tlc2.tool.BuiltInOPs;
import tlc2.value.*; import tlc2.value.ValueConstants;
import tlc2.value.impl.*;
import java.util.*; import java.util.*;
import java.util.Map.Entry; import java.util.Map.Entry;
import static tlc2.value.ValueConstants.*;
public class BAstCreator extends BuiltInOPs public class BAstCreator extends BuiltInOPs
implements TranslationGlobals, ASTConstants, BBuildIns, Priorities, ValueConstants { implements TranslationGlobals, ASTConstants, BBuildIns, Priorities, ValueConstants {
......
...@@ -23,7 +23,7 @@ import de.tla2b.util.FileUtils; ...@@ -23,7 +23,7 @@ import de.tla2b.util.FileUtils;
import tla2sany.drivers.SANY; import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj; import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.ModuleNode; import tla2sany.semantic.ModuleNode;
import tlc2.tool.ModelConfig; import tlc2.tool.impl.ModelConfig;
import util.ToolIO; import util.ToolIO;
import java.io.*; import java.io.*;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment