diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index 9efea70a50f7580fa3719a2f91c954de2e1deef0..51094754bc91e5e537d432e4a02fdad1a847da3f 100644 --- a/src/main/java/de/tlc4b/TLC4B.java +++ b/src/main/java/de/tlc4b/TLC4B.java @@ -13,17 +13,25 @@ import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.util.Map; import java.util.Map.Entry; -import java.util.concurrent.*; +import java.util.concurrent.ExecutionException; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; +import java.util.concurrent.TimeUnit; +import java.util.concurrent.TimeoutException; import de.be4.classicalb.core.parser.exceptions.BCompoundException; -import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES; -import de.tlc4b.exceptions.TLC4BIOException; import de.tlc4b.exceptions.TLC4BException; +import de.tlc4b.exceptions.TLC4BIOException; import de.tlc4b.exceptions.TranslationException; import de.tlc4b.tlc.TLCOutputInfo; import de.tlc4b.tlc.TLCResults; import de.tlc4b.util.StopWatch; -import org.apache.commons.cli.*; + +import org.apache.commons.cli.CommandLine; +import org.apache.commons.cli.DefaultParser; +import org.apache.commons.cli.HelpFormatter; +import org.apache.commons.cli.Options; +import org.apache.commons.cli.ParseException; import static de.tlc4b.TLC4BCliOptions.*; import static de.tlc4b.TLC4BCliOptions.TLCOption.*; @@ -448,8 +456,8 @@ public class TLC4B { } private void createStandardModules() { - for (STANDARD_MODULES module : translator.getStandardModuleToBeCreated()) { - createStandardModule(buildDir, module.toString()); + for (String module : translator.getStandardModuleToBeCreated()) { + createStandardModule(buildDir, module); } } diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java index 159f16730f1e0c56280684b4d75679d534047211..b79bbdd4d3134f0512d565b9e33a425a359325aa 100644 --- a/src/main/java/de/tlc4b/Translator.java +++ b/src/main/java/de/tlc4b/Translator.java @@ -2,8 +2,8 @@ package de.tlc4b; import java.io.File; import java.io.IOException; -import java.util.HashSet; import java.util.Map; +import java.util.Set; import de.be4.classicalb.core.parser.BParser; import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader; @@ -21,7 +21,6 @@ import de.tlc4b.analysis.Renamer; import de.tlc4b.analysis.Typechecker; import de.tlc4b.analysis.UnsupportedConstructsFinder; import de.tlc4b.analysis.UsedStandardModules; -import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES; import de.tlc4b.analysis.transformation.DefinitionsEliminator; import de.tlc4b.analysis.transformation.SeesEliminator; import de.tlc4b.analysis.transformation.SequenceSubstitutionsEliminator; @@ -44,7 +43,7 @@ public class Translator { private String machineName; private String ltlFormula; private PPredicate constantsSetup; - private HashSet<STANDARD_MODULES> standardModulesToBeCreated; + private Set<String> standardModulesToBeCreated; private TLCOutputInfo tlcOutputInfo; private String translatedLTLFormula; @@ -193,11 +192,7 @@ public class Translator { return tlcOutputInfo; } - public boolean containsUsedStandardModule(STANDARD_MODULES module) { - return standardModulesToBeCreated.contains(module); - } - - public HashSet<UsedStandardModules.STANDARD_MODULES> getStandardModuleToBeCreated() { + public Set<String> getStandardModuleToBeCreated() { return standardModulesToBeCreated; } diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java index b6e2feed50c7a02500df80dd6a83f18f18cf58b4..173d50df689f1750d25a2550d6b979977666a1d7 100644 --- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java +++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java @@ -4,6 +4,7 @@ import java.util.ArrayList; import java.util.HashSet; import java.util.List; import java.util.Set; +import java.util.stream.Collectors; import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter; import de.be4.classicalb.core.parser.node.AAddExpression; @@ -103,8 +104,7 @@ import de.tlc4b.btypes.SetType; import de.tlc4b.tla.TLAModule; public class UsedStandardModules extends DepthFirstAdapter { - - public enum STANDARD_MODULES { + private enum STANDARD_MODULES { Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations, FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations, ExternalFunctions, Foo } @@ -149,7 +149,7 @@ public class UsedStandardModules extends DepthFirstAdapter { start.apply(this); } - public ArrayList<STANDARD_MODULES> getExtendedModules() { + public List<String> getExtendedModules() { ArrayList<STANDARD_MODULES> list = new ArrayList<>(extendedStandardModules); if (list.contains(STANDARD_MODULES.Integers)) { list.remove(STANDARD_MODULES.Naturals); @@ -159,10 +159,10 @@ public class UsedStandardModules extends DepthFirstAdapter { Integer i2 = modules.indexOf(s2); return i1.compareTo(i2); }); - return list; + return list.stream().map(STANDARD_MODULES::name).collect(Collectors.toList()); } - public HashSet<STANDARD_MODULES> getStandardModulesToBeCreated() { + public Set<String> getStandardModulesToBeCreated() { // dependencies of standard modules HashSet<STANDARD_MODULES> res = new HashSet<>(); for (STANDARD_MODULES module : extendedStandardModules) { @@ -199,7 +199,7 @@ public class UsedStandardModules extends DepthFirstAdapter { } } - return res; + return res.stream().map(STANDARD_MODULES::name).collect(Collectors.toSet()); } @Override diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java index 6cdce49751216c449d6cf60c7b238d73206d7ba2..64da8fd456397e7796aa4d4ed6afe723566b0ebb 100644 --- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java +++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java @@ -299,15 +299,10 @@ public class TLAPrinter extends DepthFirstAdapter { } private void printExtendedModules() { - if (!usedStandardModules.getExtendedModules().isEmpty()) { + List<String> extendedModules = usedStandardModules.getExtendedModules(); + if (!extendedModules.isEmpty()) { moduleStringAppend("EXTENDS "); - for (int i = 0; i < usedStandardModules.getExtendedModules().size(); i++) { - if (i > 0) { - moduleStringAppend(", "); - } - moduleStringAppend(usedStandardModules.getExtendedModules() - .get(i).toString()); - } + moduleStringAppend(String.join(", ", extendedModules)); moduleStringAppend("\n"); } }