diff --git a/build.gradle b/build.gradle index 68144940d3e8b8f8165ea9c3b768cc0f787b3a26..95b17659733ed9d1b571551f9498fd92419028e4 100644 --- a/build.gradle +++ b/build.gradle @@ -35,7 +35,7 @@ dependencies { test { exclude('de/b2tla/tlc/integration/**') } -task integrationtest(type: Test){ +task integrationtests(type: Test){ doFirst{ println("Running integration tests") } scanForTestClasses = true include('de/b2tla/tlc/integration/**') @@ -58,14 +58,3 @@ task b2tla(dependsOn: build) << { } } - -task deploy(dependsOn: build) { - copy { - from('build/libs/') - into('build/b2tla') - include('b2tla-'+project.version+'.jar') - rename('(b2tla)-(.+)', 'B2TLA.jar') - } -} - - diff --git a/src/main/java/de/b2tla/B2TLA.java b/src/main/java/de/b2tla/B2TLA.java index 79837b61ed22c78e0a20ee5e2f988875926a1afe..55c61dca9837a9c84d36b901249ccc4ead2ba38e 100644 --- a/src/main/java/de/b2tla/B2TLA.java +++ b/src/main/java/de/b2tla/B2TLA.java @@ -10,18 +10,16 @@ import java.io.IOException; import java.io.InputStream; import java.io.Writer; import java.util.ArrayList; -import java.util.HashSet; -import java.util.Set; import de.b2tla.Globals; -import tla2tex.FindAlignments; -import util.ToolIO; - import de.b2tla.analysis.UsedStandardModules; import de.b2tla.analysis.UsedStandardModules.STANDARD_MODULES; +import de.b2tla.exceptions.B2TLAIOException; import de.b2tla.exceptions.B2tlaException; +import de.b2tla.exceptions.TypeErrorException; import de.b2tla.tlc.TLCOutput; +import de.b2tla.tlc.TLCOutputInfo; import de.b2tla.tlc.TLCOutput.ERROR; import de.b2tla.util.StopWatch; import de.be4.classicalb.core.parser.exceptions.BException; @@ -34,7 +32,8 @@ public class B2TLA { private String path; private String tlaModule; private String config; - B2TlaTranslator translator; + private B2TlaTranslator translator; + private TLCOutputInfo tlcOutputInfo; public static void main(String[] args) throws IOException { StopWatch.start("Translation"); @@ -42,15 +41,21 @@ public class B2TLA { try { b2tla.progress(args); - } catch (Exception e) { + } catch (BException e) { System.err.println(e.getMessage()); return; + } catch (B2tlaException e) { + System.err.println(e.getMessage()); + System.out.println("Model checking time: 0 sec"); + System.out.println("Result: " + e.getError()); + return; } StopWatch.stop("Translation"); + if (Globals.runTLC) { - ArrayList<String> output = TLCRunner.runTLC( - b2tla.machineName, b2tla.path); - b2tla.evalOutput(output, false); + ArrayList<String> output = TLCRunner.runTLC(b2tla.machineName, + b2tla.path); + b2tla.evalOutput(output, true); } } @@ -75,17 +80,19 @@ public class B2TLA { return null; } - private void evalOutput(ArrayList<String> output, boolean createTraceFile) { TLCOutput tlcOutput = new TLCOutput(machineName, - output.toArray(new String[output.size()])); + output.toArray(new String[output.size()]), tlcOutputInfo); tlcOutput.parseTLCOutput(); + System.out.println("Model checking time: " + tlcOutput.getRunningTime() + + " sec"); + System.out.println("Result: " + tlcOutput.getError()); - StringBuilder trace = tlcOutput.getErrorTrace(); if (tlcOutput.hasTrace() && createTraceFile) { + StringBuilder trace = tlcOutput.getErrorTrace(); String tracefileName = machineName + ".tla.trace"; createFile(path, tracefileName, trace.toString(), "Trace file '" - + path + tracefileName + "'created.", true); + + path + tracefileName + "'created.", false); } } @@ -105,21 +112,21 @@ public class B2TLA { } else if (args[index].toLowerCase().equals("-tool")) { Globals.tool = true; } else if (args[index].charAt(0) == '-') { - throw new B2tlaException("Error: unrecognized option: " + throw new B2TLAIOException("Error: unrecognized option: " + args[index]); } else { if (mainFileName != null) { - throw new B2tlaException( + throw new B2TLAIOException( "Error: more than one input files: " + mainFileName + " and " + args[index]); } mainFileName = args[index]; - + } index++; } if (mainFileName == null) { - throw new B2tlaException("Main machine required!"); + throw new B2TLAIOException("Main machine required!"); } } @@ -133,6 +140,7 @@ public class B2TLA { this.tlaModule = translator.getModuleString(); this.config = translator.getConfigString(); + this.tlcOutputInfo = translator.getTLCOutputInfo(); createFiles(); } @@ -144,7 +152,7 @@ public class B2TLA { name = name.replace("/", File.separator); mainFileName = name; - + if (name.toLowerCase().endsWith(".mch")) { name = name.substring(0, name.length() - 4); } @@ -172,36 +180,45 @@ public class B2TLA { STANDARD_MODULES.Relations)) { createStandardModule(path, STANDARD_MODULES.Relations.toString()); } - + if (translator.getUsedStandardModule().contains( STANDARD_MODULES.Functions)) { createStandardModule(path, STANDARD_MODULES.Functions.toString()); } + + if (translator.getUsedStandardModule().contains( + STANDARD_MODULES.BBuiltIns)) { + createStandardModule(path, STANDARD_MODULES.BBuiltIns.toString()); + } if (translator.getUsedStandardModule().contains( STANDARD_MODULES.FunctionsAsRelations)) { - createStandardModule(path, STANDARD_MODULES.FunctionsAsRelations.toString()); + createStandardModule(path, + STANDARD_MODULES.FunctionsAsRelations.toString()); if (!translator.getUsedStandardModule().contains( STANDARD_MODULES.Functions)) { - createStandardModule(path, STANDARD_MODULES.Functions.toString()); + createStandardModule(path, + STANDARD_MODULES.Functions.toString()); } } - + if (translator.getUsedStandardModule().contains( STANDARD_MODULES.SequencesExtended)) { - createStandardModule(path, STANDARD_MODULES.SequencesExtended.toString()); + createStandardModule(path, + STANDARD_MODULES.SequencesExtended.toString()); } - + if (translator.getUsedStandardModule().contains( STANDARD_MODULES.SequencesAsRelations)) { - createStandardModule(path, STANDARD_MODULES.SequencesAsRelations.toString()); + createStandardModule(path, + STANDARD_MODULES.SequencesAsRelations.toString()); } } private void createStandardModule(String path, String name) { // standard modules are copied from the standardModules folder to the // current directory - + File file = new File(path + name + ".tla"); InputStream is = null; FileOutputStream fos = null; @@ -227,7 +244,7 @@ public class B2TLA { } catch (IOException e) { e.printStackTrace(); } finally { - if(Globals.deleteOnExit){ + if (Globals.deleteOnExit) { file.deleteOnExit(); } try { @@ -291,7 +308,7 @@ public class B2TLA { private File getFile() { File mainFile = new File(mainFileName); if (!mainFile.exists()) { - throw new B2tlaException("The file " + mainFileName + throw new B2TLAIOException("The file " + mainFileName + " does not exist."); } return mainFile; @@ -322,7 +339,7 @@ public class B2TLA { System.out.println(message); } catch (IOException e) { e.printStackTrace(); - throw new B2tlaException(e.getMessage()); + throw new B2TLAIOException(e.getMessage()); } finally { if (deleteOnExit) { file.deleteOnExit(); diff --git a/src/main/java/de/b2tla/B2TlaTranslator.java b/src/main/java/de/b2tla/B2TlaTranslator.java index 53d6c1068a91e7a6085a72cb48f65b32675c1b6d..bf97101bf83de5bd5d69c04fcafda5e16aa01778 100644 --- a/src/main/java/de/b2tla/B2TlaTranslator.java +++ b/src/main/java/de/b2tla/B2TlaTranslator.java @@ -18,6 +18,8 @@ import de.b2tla.analysis.UsedStandardModules; import de.b2tla.analysis.UsedStandardModules.STANDARD_MODULES; import de.b2tla.prettyprint.TLAPrinter; import de.b2tla.tla.Generator; +import de.b2tla.tlc.TLCOutput; +import de.b2tla.tlc.TLCOutputInfo; import de.b2tla.util.StopWatch; import de.be4.classicalb.core.parser.BParser; import de.be4.classicalb.core.parser.exceptions.BException; @@ -31,6 +33,8 @@ public class B2TlaTranslator { private String configString; private String machineName; private ArrayList<STANDARD_MODULES> usedStandardModules; + private TLCOutputInfo tlcOutputInfo; + public B2TlaTranslator(String machineString) throws BException{ this.machineString = machineString; @@ -56,7 +60,6 @@ public class B2TlaTranslator { this.machineName = machineContext.getMachineName(); Typechecker typechecker = new Typechecker(machineContext); - UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder( machineContext); PrecedenceCollector precedenceCollector = new PrecedenceCollector( @@ -89,6 +92,8 @@ public class B2TlaTranslator { moduleString = printer.getStringbuilder().toString(); configString = printer.getConfigString().toString(); + + tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker.getTypes()); } @@ -116,6 +121,10 @@ public class B2TlaTranslator { return machineName; } + public TLCOutputInfo getTLCOutputInfo(){ + return tlcOutputInfo; + } + public boolean containsUsedStandardModule(STANDARD_MODULES module){ return usedStandardModules.contains(module); } diff --git a/src/main/java/de/b2tla/Globals.java b/src/main/java/de/b2tla/Globals.java index c8fab7f42bb3a01224bb5eb57db4e3f261f51f83..d4c48fe61a0adc59ee270bdb3d77abbf9faaad3f 100644 --- a/src/main/java/de/b2tla/Globals.java +++ b/src/main/java/de/b2tla/Globals.java @@ -8,7 +8,6 @@ public class Globals { public static boolean translate = true; public static boolean invariant = true; public static boolean tool = false; - public static boolean setupConstants = false; public static boolean deleteOnExit = false; } diff --git a/src/main/java/de/b2tla/TLCRunner.java b/src/main/java/de/b2tla/TLCRunner.java index dab9de1f4258bb3d38c2cbbf26fd68d3d90240b6..275e3d4597ed23330ca7b3185ac82a41a937836b 100644 --- a/src/main/java/de/b2tla/TLCRunner.java +++ b/src/main/java/de/b2tla/TLCRunner.java @@ -10,10 +10,9 @@ import java.io.PrintStream; import java.util.ArrayList; import java.util.Arrays; import java.util.HashSet; +import java.util.List; import java.util.Set; -import de.b2tla.tlc.ProcessHelper; -import de.b2tla.tlc.TLCOutput; import de.b2tla.util.BTLCPrintStream; import util.SimpleFilenameToStream; @@ -34,6 +33,28 @@ public class TLCRunner { TLC.main(parameters); } + private static Process startJVM(final String optionsAsString, + final String mainClass, final String[] arguments) + throws IOException { + + String separator = System.getProperty("file.separator"); + + String jvm = System.getProperty("java.home") + separator + "bin" + + separator + "java"; + String classpath = System.getProperty("java.class.path"); + + List<String> command = new ArrayList<String>(); + command.add(jvm); + command.add("-cp"); + command.add(classpath); + command.add(mainClass); + command.addAll(Arrays.asList(arguments)); + + ProcessBuilder processBuilder = new ProcessBuilder(command); + Process process = processBuilder.start(); + return process; + } + public static ArrayList<String> runTLCInANewJVM(String machineName, String path) throws IOException { ArrayList<String> list = new ArrayList<String>(); @@ -42,14 +63,12 @@ public class TLCRunner { if (!Globals.deadlockCheck) { list.add("-deadlock"); } - //list.add("-coverage"); - //list.add("1"); - + // list.add("-coverage"); + // list.add("1"); + String[] args = list.toArray(new String[list.size()]); - ProcessHelper helper = new ProcessHelper(); System.out.println("Starting JVM..."); - Process p = helper.startNewJavaProcess("", TLCRunner.class.getName(), - args); + Process p = startJVM("", TLCRunner.class.getCanonicalName(), args); StreamGobbler stdOut = new StreamGobbler(p.getInputStream()); stdOut.start(); @@ -92,41 +111,41 @@ public class TLCRunner { System.setOut(systemOut); ArrayList<String> messages = btlcStream.getArrayList(); - String[] ms =ToolIO.getAllMessages(); + String[] ms = ToolIO.getAllMessages(); System.out.println("--------------------------------"); for (int i = 0; i < ms.length; i++) { - System.out.println(">> "+ms[i]); + System.out.println(">> " + ms[i]); } - + closeThreads(); - //return new ArrayList<String>(Arrays.asList(ms)); + // return new ArrayList<String>(Arrays.asList(ms)); return messages; - - - //TLCOutput tlcOutput = new TLCOutput(machineName, messages); - //tlcOutput.parseTLCOutput(); + + // TLCOutput tlcOutput = new TLCOutput(machineName, messages); + // tlcOutput.parseTLCOutput(); // TLCOutputEvaluator evaluator = new TLCOutputEvaluator(machineName, // messages); - //System.out.println("ERROR: " + tlcOutput.getError()); - //StringBuilder trace = tlcOutput.getErrorTrace(); -// if (tlcOutput.hasTrace()) { -// createfile(path, machineName + ".tla.trace", trace.toString()); -// } + // System.out.println("ERROR: " + tlcOutput.getError()); + // StringBuilder trace = tlcOutput.getErrorTrace(); + // if (tlcOutput.hasTrace()) { + // createfile(path, machineName + ".tla.trace", trace.toString()); + // } } private static void closeThreads() { - Set<Thread> threadSet = new HashSet<Thread>(Thread.getAllStackTraces().keySet()); + Set<Thread> threadSet = new HashSet<Thread>(Thread.getAllStackTraces() + .keySet()); Thread[] threadArray = threadSet.toArray(new Thread[threadSet.size()]); for (int i = 0; i < threadArray.length; i++) { Thread t = threadArray[i]; - //System.out.println(t.getId()+ " "+t.getThreadGroup()); - if(t.getName().equals("RMI Reaper")){ + // System.out.println(t.getId()+ " "+t.getThreadGroup()); + if (t.getName().equals("RMI Reaper")) { t.interrupt(); } } - //System.exit(0); + // System.exit(0); } - + public static void createfile(String dir, String fileName, String text) { File d = new File(dir); d.mkdirs(); diff --git a/src/main/java/de/b2tla/analysis/TypeRestrictor.java b/src/main/java/de/b2tla/analysis/TypeRestrictor.java index 02cf26c926c05e04d4575d1b09df28ea59c1e322..3b3dffd7f5b71f3c54d2714d9185e5c6098d453d 100644 --- a/src/main/java/de/b2tla/analysis/TypeRestrictor.java +++ b/src/main/java/de/b2tla/analysis/TypeRestrictor.java @@ -39,8 +39,7 @@ public class TypeRestrictor extends DepthFirstAdapter { private Hashtable<Node, NodeType> restrictedTypes; private Hashtable<Node, ArrayList<NodeType>> restrictedTypesSet; - - + public TypeRestrictor(Start start, MachineContext machineContext, Typechecker typechecker) { this.machineContext = machineContext; @@ -54,23 +53,21 @@ public class TypeRestrictor extends DepthFirstAdapter { return restrictedTypes; } - public ArrayList<NodeType> getRestrictedTypesSet(Node node){ + public ArrayList<NodeType> getRestrictedTypesSet(Node node) { return restrictedTypesSet.get(node); } - - + private void putRestrictedType(Node identifier, NodeType expression) { ArrayList<NodeType> list = restrictedTypesSet.get(identifier); - - if(list == null){ + + if (list == null) { list = new ArrayList<NodeType>(); list.add(expression); restrictedTypesSet.put(identifier, list); - }else{ + } else { list.add(expression); } - - + if (restrictedTypes.containsKey(identifier)) return; @@ -128,10 +125,9 @@ public class TypeRestrictor extends DepthFirstAdapter { putRestrictedType(r_right, new ElementOfNode(left)); } return; - - + } - + if (n instanceof AConjunctPredicate) { analysePredicate(((AConjunctPredicate) n).getLeft(), list); analysePredicate(((AConjunctPredicate) n).getRight(), list); @@ -149,6 +145,8 @@ public class TypeRestrictor extends DepthFirstAdapter { // e.apply(this); list.add(e); } + // TODO test if the expression is really a implication, currently a + // class cast exception is thrown AImplicationPredicate implication = (AImplicationPredicate) node .getImplication(); analysePredicate(implication.getLeft(), list); @@ -288,7 +286,6 @@ public class TypeRestrictor extends DepthFirstAdapter { } } - @Override public void caseAAnySubstitution(AAnySubstitution node) { HashSet<Node> list = new HashSet<Node>(); diff --git a/src/main/java/de/b2tla/analysis/Typechecker.java b/src/main/java/de/b2tla/analysis/Typechecker.java index dbccc6be3d429670d949eeb6c37e55085ee0c63e..3303df21b228bf12a2136bcaec3982333a7ea7fa 100644 --- a/src/main/java/de/b2tla/analysis/Typechecker.java +++ b/src/main/java/de/b2tla/analysis/Typechecker.java @@ -557,7 +557,6 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { @Override public void caseAIntegerSetExpression(AIntegerSetExpression node) { - System.out.println(node.parent().getClass()); try { SetType found = new SetType(IntegerType.getInstance()); found.unify(getType(node), this); @@ -1090,23 +1089,18 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { @Override public void caseASetExtensionExpression(ASetExtensionExpression node) { - SetType set; - try { - set = new SetType(new UntypedType()).unify(getType(node), this); - } catch (UnificationException e) { - throw new TypeErrorException("Excepted '" + getType(node) - + "' , found 'POW(_A)' in ' {...} '"); - } - + UntypedType u = new UntypedType(); for (PExpression e : node.getExpressions()) { - setType(e, set.getSubtype()); + setType(e, u); } - + BType expected = getType(node); List<PExpression> copy = new ArrayList<PExpression>( node.getExpressions()); for (PExpression e : copy) { e.apply(this); } + BType found = new SetType(getType(copy.get(0))); + unify(expected, found, node); } @Override @@ -1930,7 +1924,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { expected.unify(found, this); } catch (UnificationException e) { throw new TypeErrorException("Excepted '" + expected + "' , found " - + found + "' at " + node.getClass() + "\n " + + found + "' at " + node.getClass().getSimpleName() + "\n " + node.getStartPos()); } } diff --git a/src/main/java/de/b2tla/analysis/UsedStandardModules.java b/src/main/java/de/b2tla/analysis/UsedStandardModules.java index ee7256b949d9257dff30effba14f1b9819cef265..746919603635a62360b8d7ca5fa3691485a98597 100644 --- a/src/main/java/de/b2tla/analysis/UsedStandardModules.java +++ b/src/main/java/de/b2tla/analysis/UsedStandardModules.java @@ -37,6 +37,7 @@ import de.be4.classicalb.core.parser.node.AGeneralConcatExpression; import de.be4.classicalb.core.parser.node.AGeneralIntersectionExpression; import de.be4.classicalb.core.parser.node.AGeneralProductExpression; import de.be4.classicalb.core.parser.node.AGeneralSumExpression; +import de.be4.classicalb.core.parser.node.AGeneralUnionExpression; import de.be4.classicalb.core.parser.node.AGreaterEqualPredicate; import de.be4.classicalb.core.parser.node.AGreaterPredicate; import de.be4.classicalb.core.parser.node.AIdentityExpression; @@ -105,9 +106,7 @@ import de.be4.classicalb.core.parser.node.PExpression; public class UsedStandardModules extends DepthFirstAdapter { public static enum STANDARD_MODULES { - Naturals, Integers, FiniteSets, Sequences, TLC, - BBuiltIns, Relations, FunctionsAsRelations, - Functions, SequencesExtended, SequencesAsRelations + Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations, FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations } private final static ArrayList<STANDARD_MODULES> modules = new ArrayList<UsedStandardModules.STANDARD_MODULES>(); @@ -397,6 +396,10 @@ public class UsedStandardModules extends DepthFirstAdapter { usedStandardModules.add(STANDARD_MODULES.BBuiltIns); } + public void inAGeneralUnionExpression(AGeneralUnionExpression node) { + usedStandardModules.add(STANDARD_MODULES.BBuiltIns); + } + public void inAQuantifiedIntersectionExpression( AQuantifiedIntersectionExpression node) { usedStandardModules.add(STANDARD_MODULES.BBuiltIns); @@ -582,7 +585,7 @@ public class UsedStandardModules extends DepthFirstAdapter { evalSequenceOrRelation(node); } - private void evalSequenceOrRelation(Node node){ + private void evalSequenceOrRelation(Node node) { BType type = typechecker.getType(node); if (type instanceof FunctionType) { usedStandardModules.add(STANDARD_MODULES.Sequences); @@ -590,7 +593,7 @@ public class UsedStandardModules extends DepthFirstAdapter { usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations); } } - + public void inAFirstExpression(AFirstExpression node) { usedStandardModules.add(STANDARD_MODULES.Sequences); } diff --git a/src/main/java/de/b2tla/btypes/BType.java b/src/main/java/de/b2tla/btypes/BType.java index 6663e66321c55a629934fd3e4a0404c8327b0ae2..ad890180f817cc753aa1d4dc6cc233894c179c10 100644 --- a/src/main/java/de/b2tla/btypes/BType.java +++ b/src/main/java/de/b2tla/btypes/BType.java @@ -1,6 +1,5 @@ package de.b2tla.btypes; - public interface BType extends ITypeConstants{ public BType unify(BType other, ITypechecker typechecker); public boolean isUntyped(); diff --git a/src/main/java/de/b2tla/exceptions/B2TLAIOException.java b/src/main/java/de/b2tla/exceptions/B2TLAIOException.java new file mode 100644 index 0000000000000000000000000000000000000000..7c4f56a1b1b8bfc1ab9b4ddb3d8c9e4d0d8ba738 --- /dev/null +++ b/src/main/java/de/b2tla/exceptions/B2TLAIOException.java @@ -0,0 +1,15 @@ +package de.b2tla.exceptions; + +@SuppressWarnings("serial") +public class B2TLAIOException extends B2tlaException{ + + public B2TLAIOException(String e) { + super(e); + } + + @Override + public String getError() { + return "I/O Error"; + } + +} diff --git a/src/main/java/de/b2tla/exceptions/B2tlaException.java b/src/main/java/de/b2tla/exceptions/B2tlaException.java index 3d13b34b7dc14d915227a543e37548625a82b6f8..1561c66c6f3c150888d8520c8c967bfcb45c58f5 100644 --- a/src/main/java/de/b2tla/exceptions/B2tlaException.java +++ b/src/main/java/de/b2tla/exceptions/B2tlaException.java @@ -1,10 +1,12 @@ package de.b2tla.exceptions; @SuppressWarnings("serial") -public class B2tlaException extends RuntimeException { +public abstract class B2tlaException extends RuntimeException { public B2tlaException(String e) { super(e); } + public abstract String getError(); + } diff --git a/src/main/java/de/b2tla/exceptions/ScopeException.java b/src/main/java/de/b2tla/exceptions/ScopeException.java index 9fb42a3a2c9572c20d8c8f5692a5996fe8cf5f7e..ee7a231941a2e5fac3b1640731956a34ae071de8 100644 --- a/src/main/java/de/b2tla/exceptions/ScopeException.java +++ b/src/main/java/de/b2tla/exceptions/ScopeException.java @@ -6,4 +6,10 @@ public class ScopeException extends B2tlaException{ public ScopeException(String e){ super(e); } + + @Override + public String getError() { + return "ScopeException"; + } + } diff --git a/src/main/java/de/b2tla/exceptions/SubstitutionException.java b/src/main/java/de/b2tla/exceptions/SubstitutionException.java index 24d44ad1476f965a2e2d16121530b493bfb5c3f1..12074af2bfede2fb42c10deb07229c29e0ca6dc9 100644 --- a/src/main/java/de/b2tla/exceptions/SubstitutionException.java +++ b/src/main/java/de/b2tla/exceptions/SubstitutionException.java @@ -7,4 +7,9 @@ public class SubstitutionException extends B2tlaException{ super(e); } + @Override + public String getError() { + return "SubstitutionError"; + } + } diff --git a/src/main/java/de/b2tla/exceptions/TypeErrorException.java b/src/main/java/de/b2tla/exceptions/TypeErrorException.java index 49e71aff8cfa00a8ebcf00bf289582dc9ef8a78b..52b29141ce0db07b316ccc8ea82be9b13b49d762 100644 --- a/src/main/java/de/b2tla/exceptions/TypeErrorException.java +++ b/src/main/java/de/b2tla/exceptions/TypeErrorException.java @@ -6,4 +6,9 @@ public class TypeErrorException extends B2tlaException { public TypeErrorException(String e) { super(e); } + + @Override + public String getError() { + return "TypeError"; + } } diff --git a/src/main/java/de/b2tla/exceptions/UnificationException.java b/src/main/java/de/b2tla/exceptions/UnificationException.java index 5caa4e1845aaf8c865b49690120d6f27b01f57d9..1a08bb906cc636723c691c6fdd3ea11378382db6 100644 --- a/src/main/java/de/b2tla/exceptions/UnificationException.java +++ b/src/main/java/de/b2tla/exceptions/UnificationException.java @@ -1,7 +1,7 @@ package de.b2tla.exceptions; @SuppressWarnings("serial") -public class UnificationException extends B2tlaException{ +public class UnificationException extends RuntimeException{ public UnificationException() { super(""); diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java index db9985fa3ac223ab625813d70d55470ea6db0a64..abaa6db7363a0a802dfff10daf96d1e97e31f4aa 100644 --- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java +++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java @@ -1709,8 +1709,9 @@ public class TLAPrinter extends DepthFirstAdapter { @Override public void caseAGeneralUnionExpression(AGeneralUnionExpression node) { inAGeneralUnionExpression(node); - tlaModuleString.append("UNION "); + tlaModuleString.append("Union("); node.getExpression().apply(this); + tlaModuleString.append(")"); outAGeneralUnionExpression(node); } @@ -1718,7 +1719,7 @@ public class TLAPrinter extends DepthFirstAdapter { public void caseAGeneralIntersectionExpression( AGeneralIntersectionExpression node) { inAGeneralIntersectionExpression(node); - tlaModuleString.append("inter("); + tlaModuleString.append("Inter("); node.getExpression().apply(this); tlaModuleString.append(")"); outAGeneralIntersectionExpression(node); @@ -1729,7 +1730,7 @@ public class TLAPrinter extends DepthFirstAdapter { List<PExpression> copy = new ArrayList<PExpression>( node.getIdentifiers()); - tlaModuleString.append("UNION({"); + tlaModuleString.append("Union({"); node.getExpression().apply(this); tlaModuleString.append(": "); printIdentifierList(copy); @@ -1749,7 +1750,7 @@ public class TLAPrinter extends DepthFirstAdapter { List<PExpression> copy = new ArrayList<PExpression>( node.getIdentifiers()); - tlaModuleString.append("INTER({"); + tlaModuleString.append("Inter({"); node.getExpression().apply(this); tlaModuleString.append(": "); printIdentifierList(copy); diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/b2tla/tla/Generator.java index 6a3dcd22c56e07e21fbd41c3948e3c22851776f9..e2765cb568a32686912c8b66c60e515380097023 100644 --- a/src/main/java/de/b2tla/tla/Generator.java +++ b/src/main/java/de/b2tla/tla/Generator.java @@ -127,7 +127,6 @@ public class Generator extends DepthFirstAdapter { configFile.setInit(); tlaModule.addInit(clause.getPredicates()); } else { - Globals.setupConstants = true; tlaModule.addAssume(clause.getPredicates()); } } @@ -231,7 +230,6 @@ public class Generator extends DepthFirstAdapter { } } else { - Globals.setupConstants = true; tlaModule.addAssume(propertiesPerdicate); } } diff --git a/src/main/java/de/b2tla/tlc/ProcessHelper.java b/src/main/java/de/b2tla/tlc/ProcessHelper.java deleted file mode 100644 index 9c2c94465e31f9c1a1cfcc4bae3985d0ffb00167..0000000000000000000000000000000000000000 --- a/src/main/java/de/b2tla/tlc/ProcessHelper.java +++ /dev/null @@ -1,69 +0,0 @@ -package de.b2tla.tlc; - - -//import org.apache.log4j.Logger; -import java.io.File; -import java.io.IOException; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.List; -import java.util.Map; - - -public class ProcessHelper { -//private static Logger log = Logger.getLogger(ProcessHelper.class); -private List<Process> processes; - - -public ProcessHelper() { - processes = new ArrayList< Process >(); - -} - - - -public Process startNewJavaProcess(final String optionsAsString, final String mainClass, final String[] arguments) - throws IOException { - - ProcessBuilder processBuilder = createProcess(optionsAsString, mainClass, arguments); - Process process = processBuilder.start(); - processes.add(process); - //log.debug("Process " + process.toString() + " has started"); - return process; -} - - -private ProcessBuilder createProcess(final String optionsAsString, final String mainClass, final String[] arguments) { - String jvm = System.getProperty("java.home") + File.separator + "bin" + File.separator + "java"; - String classpath = System.getProperty("java.class.path"); - //log.debug("classpath: " + classpath); - // String workingDirectory = System.getProperty("user.dir"); - - String[] options = optionsAsString.split(" "); - List < String > command = new ArrayList <String>(); - command.add(jvm); - command.addAll(Arrays.asList(options)); - command.add(mainClass); - command.addAll(Arrays.asList(arguments)); - - ProcessBuilder processBuilder = new ProcessBuilder(command); - Map< String, String > environment = processBuilder.environment(); - environment.put("CLASSPATH", classpath); - return processBuilder; -} - - -public void killProcess(final Process process) { - process.destroy(); -} - -/** - * Kill all processes. - */ -public void shutdown() { - //log.debug("Killing " + processes.size() + " processes."); - for (Process process : processes) { - killProcess(process); - } -} -} \ No newline at end of file diff --git a/src/main/java/de/b2tla/tlc/TLCOutput.java b/src/main/java/de/b2tla/tlc/TLCOutput.java index 44b007b843e16fabf980c463943058289a84b95e..5e5a6d35ca47d6ce7b4218c4b3837b873379bbee 100644 --- a/src/main/java/de/b2tla/tlc/TLCOutput.java +++ b/src/main/java/de/b2tla/tlc/TLCOutput.java @@ -4,12 +4,15 @@ import java.text.ParseException; import java.text.SimpleDateFormat; import java.util.ArrayList; import java.util.Date; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import de.b2tla.Globals; public class TLCOutput { private final String moduleName; private String[] messages; + private TLCOutputInfo tlcOutputInfo; Date startingTime; Date finishingTime; @@ -19,7 +22,7 @@ public class TLCOutput { String parseError; public static enum ERROR { - Deadlock, Goal, Invariant, ParseError, NoError, Assertion, PropertiesError, EnumerateError + Deadlock, Goal, Invariant, ParseError, NoError, Assertion, PropertiesError, EnumerateError, TLCError } public long getRunningTime() { @@ -28,10 +31,14 @@ public class TLCOutput { } public String getError() { + if(error == ERROR.Invariant){ + return "Invariant Violation"; + } return error.toString(); } public StringBuilder getErrorTrace() { + parseTrace(); return trace; } @@ -39,9 +46,11 @@ public class TLCOutput { return states.size() > 0; } - public TLCOutput(String moduleName, String[] messages) { + public TLCOutput(String moduleName, String[] messages, + TLCOutputInfo tlcOutputInfo) { this.moduleName = moduleName; this.messages = messages; + this.tlcOutputInfo = tlcOutputInfo; } public void parseTLCOutput() { @@ -53,8 +62,8 @@ public class TLCOutput { finishingTime = parseTime(m); } else if (m.startsWith("Error:")) { ERROR e = findError(m); - if(e != null){ - this.error = e; + if (e != null) { + this.error = e; } } else if (m.startsWith("State")) { states.add(m); @@ -67,7 +76,6 @@ public class TLCOutput { this.error = ERROR.NoError; } - System.out.println("Model checking time: " + getRunningTime()); } private void parseTrace() { @@ -75,18 +83,40 @@ public class TLCOutput { // ToolIO.getUserDir()); trace = new StringBuilder(); - if (Globals.setupConstants) { - /** - * There is only one possibility to setup the constants. As a - * consequence ProB has to find the values for the constants so that - * the predicate 1=1 is satisfied. - */ - trace.append("1 = 1 \n"); + + if (tlcOutputInfo.hasConstants()) { + String m1 = states.get(0); + String[] a = m1.split("\n"); + Pattern pattern = Pattern.compile("\\w+"); + String constantSetup = ""; + for (int i = 1; i < a.length; i++) { + String line = a[i]; + Matcher matcher = pattern.matcher(line); + matcher.find(); + String identifier = matcher.group(); + if (tlcOutputInfo.isAConstant(identifier)) { + constantSetup += line + "\n"; + } + } + + if (constantSetup.equals("")) { + /** + * There is only one possibility to setup the constants. As a + * consequence ProB has to find the values for the constants so + * that the predicate 1=1 is satisfied. + */ + trace.append("1 = 1 \n"); + } else { + constantSetup = TLCExpressionParser.parseLine(constantSetup); + trace.append(constantSetup); + trace.append("\n"); + } + } for (int i = 0; i < states.size(); i++) { String m = states.get(i); - System.out.println(m); + // System.out.println(m); String location = m.substring(0, m.indexOf("\n")); // String operationName = moduleMatcher.getName(location); @@ -125,12 +155,11 @@ public class TLCOutput { return ERROR.PropertiesError; } else if (m.equals("Error: TLC threw an unexpected exception.")) { return ERROR.ParseError; - }else if (m.startsWith("Error: Attempted to enumerate")) { - return ERROR.EnumerateError; - }else if (m.startsWith("Error: The behavior up to")){ + } else if (m.startsWith("Error: The behavior up to")) { return null; } - throw new RuntimeException(m); + System.out.println(m); + return ERROR.TLCError; } private static Date parseTime(String m) { diff --git a/src/main/java/de/b2tla/tlc/TLCOutputInfo.java b/src/main/java/de/b2tla/tlc/TLCOutputInfo.java new file mode 100644 index 0000000000000000000000000000000000000000..d6c7932b47866b61ac20c40e33e2cb8e37f5de5c --- /dev/null +++ b/src/main/java/de/b2tla/tlc/TLCOutputInfo.java @@ -0,0 +1,56 @@ +package de.b2tla.tlc; + +import java.util.Hashtable; +import java.util.Iterator; +import java.util.LinkedHashMap; +import java.util.Set; + +import de.b2tla.analysis.MachineContext; +import de.b2tla.analysis.Renamer; +import de.b2tla.btypes.BType; +import de.be4.classicalb.core.parser.node.Node; + +public class TLCOutputInfo { + + Hashtable<String, String> namesMapping; + Hashtable<String, BType> typesTable; + Set<String> constants; + + public String getBName(String tlaName){ + return namesMapping.get(tlaName); + } + + public BType getBType(String tlaName){ + return typesTable.get(tlaName); + } + + public boolean isAConstant(String tlaName){ + return constants.contains(getBName(tlaName)); + } + + public boolean hasConstants(){ + return constants.size()>0; + } + + public TLCOutputInfo(MachineContext machineContext, Renamer renamer, + Hashtable<Node, BType> types) { + + namesMapping = new Hashtable<String, String>(); + typesTable = new Hashtable<String, BType>(); + constants = machineContext.getConstants().keySet(); + + LinkedHashMap<String, Node> identifiers = new LinkedHashMap<String, Node>(); + identifiers.putAll(machineContext.getConstants()); + identifiers.putAll(machineContext.getVariables()); + + for (Iterator<String> iter = identifiers.keySet().iterator(); iter.hasNext();) { + String name = iter.next(); + Node node = identifiers.get(name); + String newName = renamer.getName(node); + namesMapping.put(newName, name); + typesTable.put(newName, types.get(node)); + } + + } + +} diff --git a/src/main/resources/standardModules/BBuiltIns.tla b/src/main/resources/standardModules/BBuiltIns.tla index 68cf656de202080274bb54a7ea807a08ad6c780b..e6713fc3cb275f383b4d0515653173602703c018 100644 --- a/src/main/resources/standardModules/BBuiltIns.tla +++ b/src/main/resources/standardModules/BBuiltIns.tla @@ -1,6 +1,6 @@ ----------------------------- MODULE BBuiltIns ----------------------------- -EXTENDS Integers, FiniteSets +EXTENDS Integers, FiniteSets, TLC RECURSIVE SIGMA(_) SIGMA(S) == LET e == CHOOSE e \in S: TRUE @@ -22,11 +22,20 @@ notSubset(a, b) == ~ (a \subseteq b) notStrictSubset(a, b) == ~ (a \subset b ) -RECURSIVE INTER(_) -INTER(S) == LET e == (CHOOSE e \in S: TRUE) - IN IF Cardinality(S) = 1 - THEN e - ELSE e \cap INTER(S \ {e}) - +RECURSIVE Inter(_) +Inter(S) == IF S = {} + THEN Assert(FALSE, "Applied inter operator to an empty set") + ELSE LET e == (CHOOSE e \in S: TRUE) + IN IF Cardinality(S) = 1 + THEN e + ELSE e \cap Inter(S \ {e}) + +RECURSIVE Union(_) +Union(S) == IF S = {} + THEN {} + ELSE LET e == (CHOOSE e \in S: TRUE) + IN IF Cardinality(S) = 1 + THEN e + ELSE e \cup Inter(S \ {e}) ============================================================================= diff --git a/src/main/resources/standardModules/FunctionsAsRelations.tla b/src/main/resources/standardModules/FunctionsAsRelations.tla index 1e0adfdb36e82e4cffe087718cb8b3f0a0156781..e4218afb915e72218b23f1ea12f2e4f020d74e0d 100644 --- a/src/main/resources/standardModules/FunctionsAsRelations.tla +++ b/src/main/resources/standardModules/FunctionsAsRelations.tla @@ -1,17 +1,20 @@ ------------------------ MODULE FunctionsAsRelations ---------------------------------- -EXTENDS FiniteSets, Relations, Functions +EXTENDS FiniteSets, Functions, TLC, Sequences + +LOCAL RelDom(r) == { x[1] :x \in r} +LOCAL RelRan(r) == { x[2] :x \in r} RelCall(r, x) == - IF Assert(Cardinality(r) = Cardinality(RelDomain(r)), "ERROR") + IF Assert(Cardinality(r) = Cardinality(RelDom(r)), "Applied a function call to the relation: " \o ToString(r)) THEN (CHOOSE y \in r: y[1] = x)[2] ELSE FALSE -MakeRel(f) == {<<x, f[x]>>: x \in DOMAIN f} -Rel(S, S2) == SUBSET (S \times S2) -func(f) == Cardinality(RelDomain(f)) = Cardinality(f) -total(f, dom) == RelDomain(f) = dom -inj(f) == Cardinality(RelRange(f)) = Cardinality(f) -surj(f, ran) == RelRange(f) = ran +LOCAL MakeRel(f) == {<<x, f[x]>>: x \in DOMAIN f} +LOCAL Rel(S, S2) == SUBSET (S \times S2) +LOCAL func(f) == Cardinality(RelDom(f)) = Cardinality(f) +LOCAL total(f, dom) == RelDom(f) = dom +LOCAL inj(f) == Cardinality(RelRan(f)) = Cardinality(f) +LOCAL surj(f, ran) == RelRan(f) = ran RelTotalFunc(S, S2) == {MakeRel(f): f \in [S -> S2]} RelTotalFuncEleOf(S, S2) == {f \in Rel(S,S2): func(f) /\ total(f,S)} diff --git a/src/test/java/de/b2tla/prettyprint/BBuildInsTest.java b/src/test/java/de/b2tla/prettyprint/BBuildInsTest.java index 31c665ce2d5960a12427f76cefe1f49642cc67b7..2882f3bf0b2bf9927455989ac5d20664bf7fa49d 100644 --- a/src/test/java/de/b2tla/prettyprint/BBuildInsTest.java +++ b/src/test/java/de/b2tla/prettyprint/BBuildInsTest.java @@ -81,7 +81,7 @@ public class BBuildInsTest { + "PROPERTIES INTER(z).(z: {1,2} & 1 = 1| {z}) = {} \n" + "END"; String expected = "---- MODULE test ----\n" + "EXTENDS BBuiltIns\n" - + "ASSUME INTER({{z}: z \\in {z \\in {1, 2}: z \\in {1, 2} /\\ 1 = 1}}) = {}\n" + + "ASSUME Inter({{z}: z \\in {z \\in {1, 2}: z \\in {1, 2} /\\ 1 = 1}}) = {}\n" + "===="; compareEquals(expected, machine); } diff --git a/src/test/java/de/b2tla/prettyprint/SetTest.java b/src/test/java/de/b2tla/prettyprint/SetTest.java index 8e362a026e0ee107ea76fcf07636d08f594c2b93..0d5a83a9bf84687342bb2025a2ad9fc4ba409c91 100644 --- a/src/test/java/de/b2tla/prettyprint/SetTest.java +++ b/src/test/java/de/b2tla/prettyprint/SetTest.java @@ -145,9 +145,10 @@ public class SetTest { String machine = "MACHINE test\n" + "PROPERTIES union({{1},{2}}) = {1,2} \n" + "END"; String expected = "---- MODULE test ----\n" - + "ASSUME UNION({{1}, {2}}) = {1, 2}\n" + + "EXTENDS BBuiltIns\n" + + "ASSUME Union({{1}, {2}}) = {1, 2}\n" + "===="; - compare(expected, machine); + assertEquals(expected, translate(machine)); } @@ -157,7 +158,7 @@ public class SetTest { + "PROPERTIES inter({{1},{1,2}}) = {1} \n" + "END"; String expected = "---- MODULE test ----\n" + "EXTENDS BBuiltIns\n" - + "ASSUME inter({{1}, {1, 2}}) = {1}\n" + + "ASSUME Inter({{1}, {1, 2}}) = {1}\n" + "===="; assertEquals(expected, translate(machine)); } @@ -168,7 +169,7 @@ public class SetTest { + "PROPERTIES UNION(z).(z: {1,2} & 1 = 1| {z}) = {1,2} \n" + "END"; String expected = "---- MODULE test ----\n" + "EXTENDS BBuiltIns\n" - + "ASSUME UNION({{z}: z \\in {z \\in {1, 2}: z \\in {1, 2} /\\ 1 = 1}}) = {1, 2}\n" + + "ASSUME Union({{z}: z \\in {z \\in {1, 2}: z \\in {1, 2} /\\ 1 = 1}}) = {1, 2}\n" + "===="; //TODO ERROR in TLA2B compareEquals(expected, machine); @@ -180,7 +181,7 @@ public class SetTest { + "PROPERTIES INTER(z).(z: {1,2} & 1 = 1| {z}) = {} \n" + "END"; String expected = "---- MODULE test ----\n" + "EXTENDS BBuiltIns\n" - + "ASSUME INTER({{z}: z \\in {z \\in {1, 2}: z \\in {1, 2} /\\ 1 = 1}}) = {}\n" + + "ASSUME Inter({{z}: z \\in {z \\in {1, 2}: z \\in {1, 2} /\\ 1 = 1}}) = {}\n" + "===="; System.out.println(expected); compareEquals(expected, machine); diff --git a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java index bd584977bc6d734c37dad534f021abd042c0a976..5a42a2b570eb7d2cc6cd1abd3ed9744353220abb 100644 --- a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java +++ b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java @@ -50,7 +50,7 @@ public class ErrorTest { @Test public void testEnumerationError() throws Exception { String[] a = new String[] { ".\\src\\test\\resources\\error\\EnumerationError.mch" }; - assertEquals(TLCOutput.ERROR.NoError, B2TLA.test(a)); + assertEquals(TLCOutput.ERROR.TLCError, B2TLA.test(a)); } } diff --git a/src/test/resources/test.mch b/src/test/resources/test.mch index 7543aa98697dfd3adb17c019df115e4c076aa15b..e0c483fde856243d45fadfeaf57ecff8d4bfc8a1 100644 --- a/src/test/resources/test.mch +++ b/src/test/resources/test.mch @@ -1,4 +1,3 @@ -MACHINE test -CONSTANTS k -PROPERTIES k = {1} * {2} +MACHINE Test +PROPERTIES inter({{1}}) = {1} END \ No newline at end of file