Merge branch 'release/1.1.0'

build.gradle

@@ -4,7 +4,7 @@ apply plugin: 'maven'
 apply plugin: 'jacoco'
 apply plugin: 'findbugs'
 
-project.version = '1.0.9'
+project.version = '1.1.0'
 project.group = 'de.hhu.stups'
 project.archivesBaseName = "tla2bAST"
 
@@ -30,17 +30,17 @@ configurations.all {
 
 def parser_version
 if (project.version.endsWith("-SNAPSHOT")) {
-	parser_version = '2.9.7-SNAPSHOT'
+	parser_version = '2.9.13-SNAPSHOT'
 }
 else {
-	parser_version = '2.9.6'
+	parser_version = '2.9.12'
 }
 
 def tlatools_version = '1.0.2'
 
 dependencies {
 
-	compile 'commons-cli:commons-cli:1.2'
+  compile (group: 'commons-cli', name: 'commons-cli', version: '1.4')
   compile (group: 'de.hhu.stups', name: 'tlatools', version: tlatools_version)
   compile (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
   compile (group: 'de.hhu.stups', name: 'parserbase', version: parser_version)

src/main/java/de/tla2b/analysis/BOperation.java

@@ -376,6 +376,10 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 					// Tuple
 					for (int i = 0; i < k.getArgs().length; i++) {
 						OpApplNode var = (OpApplNode) k.getArgs()[i];
+						//findUnchangedVariablesInOpApplNode(var);
+						if(!(var.getOperator() instanceof OpDeclNode)) {
+							throw new RuntimeException(var.getOperator().getName() + " " + var.getLocation());
+						}
 						unchangedVariablesList.add((OpDeclNode) var
 								.getOperator());
 						String name = var.getOperator().getName().toString();

src/main/java/de/tla2b/analysis/SpecAnalyser.java

@@ -33,15 +33,14 @@ import tla2sany.semantic.SymbolNode;
 import tlc2.tool.BuiltInOPs;
 import tlc2.tool.ToolGlobals;
 
-public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
-		ToolGlobals, TranslationGlobals {
+public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobals, TranslationGlobals {
 	private OpDefNode spec;
 	private OpDefNode init;
 	private OpDefNode next;
-	private ArrayList<OpDefNode> invariants = new ArrayList<OpDefNode>();
+	private ArrayList<OpDefNode> invariants = new ArrayList<>();
 
 	private OpDefNode expressionOpdefNode;
-	private Hashtable<String, SymbolNode> namingHashTable = new Hashtable<String, SymbolNode>();
+	private Hashtable<String, SymbolNode> namingHashTable = new Hashtable<>();
 
 	private final ModuleNode moduleNode;
 	private ExprNode nextExpr;
@@ -57,14 +56,14 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 	// set of OpDefNodes which will appear in the resulting B Machine
 	private Set<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
 	// definitions which are used for the type inference algorithm
-	private Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<OpDefNode, FormalParamNode[]>();
+	private Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<>();
 	// additional parameters of an let Operator, these parameters are from the
 	// surrounding operator
-	private ArrayList<String> definitionMacros = new ArrayList<String>();
+	private ArrayList<String> definitionMacros = new ArrayList<>();
 
-	private ArrayList<OpDefNode> recursiveFunctions = new ArrayList<OpDefNode>();
+	private ArrayList<OpDefNode> recursiveFunctions = new ArrayList<>();
 
-	private ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<RecursiveDefinition>();
+	private ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<>();
 
 	private ConfigfileEvaluator configFileEvaluator;
 
@@ -73,8 +72,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		this.bConstants = new ArrayList<OpDeclNode>();
 	}
 
-	public static SpecAnalyser createSpecAnalyser(ModuleNode m,
-			ConfigfileEvaluator conEval) {
+	public static SpecAnalyser createSpecAnalyser(ModuleNode m, ConfigfileEvaluator conEval) {
 		SpecAnalyser specAnalyser = new SpecAnalyser(m);
 		specAnalyser.spec = conEval.getSpecNode();
 		specAnalyser.init = conEval.getInitNode();
@@ -99,8 +97,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		SpecAnalyser specAnalyser = new SpecAnalyser(m);
 		Hashtable<String, OpDefNode> definitions = new Hashtable<String, OpDefNode>();
 		for (int i = 0; i < m.getOpDefs().length; i++) {
-			definitions.put(m.getOpDefs()[i].getName().toString(),
-					m.getOpDefs()[i]);
+			definitions.put(m.getOpDefs()[i].getName().toString(), m.getOpDefs()[i]);
 		}
 		specAnalyser.spec = definitions.get("Spec");
 		specAnalyser.init = definitions.get("Init");
@@ -115,8 +112,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		return specAnalyser;
 	}
 
-	public void start() throws SemanticErrorException, FrontEndException,
-			ConfigFileErrorException, NotImplementedException {
+	public void start()
+			throws SemanticErrorException, FrontEndException, ConfigFileErrorException, NotImplementedException {
 
 		if (spec != null) {
 			evalSpec();
@@ -131,8 +128,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 
 				OpDefNode opDefNode = (OpDefNode) opApplNode.getOperator();
 
-				if (opDefNode.getKind() == UserDefinedOpKind
-						&& !BBuiltInOPs.contains(opDefNode.getName())) {
+				if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())) {
 					int i = invariants.indexOf(inv);
 					invariants.set(i, opDefNode);
 				}
@@ -160,9 +156,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 			OpDeclNode con = bConstants.get(i);
 			if (con.getArity() > 0) {
 				throw new ConfigFileErrorException(
-						String.format(
-								"Constant '%s' must be overriden in the configuration file.",
-								con.getName()));
+						String.format("Constant '%s' must be overriden in the configuration file.", con.getName()));
 			}
 		}
 		findRecursiveConstructs();
@@ -198,8 +192,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 
 	}
 
-	private void processConfigSpec(ExprNode exprNode)
-			throws SemanticErrorException, FrontEndException {
+	private void processConfigSpec(ExprNode exprNode) throws SemanticErrorException, FrontEndException {
 
 		if (exprNode instanceof OpApplNode) {
 			OpApplNode opApp = (OpApplNode) exprNode;
@@ -217,8 +210,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 					}
 					return;
 				}
-				throw new SemanticErrorException(
-						"Can not handle specification conjunction.");
+				throw new SemanticErrorException("Can not handle specification conjunction.");
 			}
 
 			int opcode = BuiltInOPs.getOpCode(opApp.getOperator().getName());
@@ -232,8 +224,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 			if (opcode == OPCODE_box) {
 				SemanticNode boxArg = args[0];
 				if ((boxArg instanceof OpApplNode)
-						&& BuiltInOPs.getOpCode(((OpApplNode) boxArg)
-								.getOperator().getName()) == OPCODE_sa) {
+						&& BuiltInOPs.getOpCode(((OpApplNode) boxArg).getOperator().getName()) == OPCODE_sa) {
 					ExprNode next = (ExprNode) ((OpApplNode) boxArg).getArgs()[0];
 					this.nextExpr = next;
 					return;
@@ -247,8 +238,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 			// temporal
 
 		} else {
-			throw new SemanticErrorException(
-					"Can not handle specification conjunction.");
+			throw new SemanticErrorException("Can not handle specification conjunction.");
 		}
 
 	}
@@ -257,8 +247,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		Set<OpDefNode> set = new HashSet<OpDefNode>(usedDefinitions);
 		for (OpDefNode def : set) {
 			if (def.getInRecursive()) {
-				throw new NotImplementedException(
-						"Recursive definitions are currently not supported: " + def.getName() + "\n" + def.getLocation() );
+				throw new NotImplementedException("Recursive definitions are currently not supported: " + def.getName()
+						+ "\n" + def.getLocation());
 				// bDefinitionsSet.remove(def);
 				// RecursiveDefinition rd = new RecursiveDefinition(def);
 				// recursiveDefinitions.add(rd);

src/main/java/de/tla2b/translation/BDefinitionsFinder.java

@@ -2,6 +2,7 @@ package de.tla2b.translation;
 
 import java.util.ArrayList;
 import java.util.HashSet;
+import java.util.Set;
 
 import tla2sany.semantic.ASTConstants;
 import tla2sany.semantic.AssumeNode;
@@ -15,16 +16,13 @@ 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<OpDefNode>();
+public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
+	private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<>();
 
 	public BDefinitionsFinder(SpecAnalyser specAnalyser) {
 		if (specAnalyser.getConfigFileEvaluator() != null) {
-			bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator()
-					.getConstantOverrideTable().values());
-			bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator()
-					.getOperatorOverrideTable().values());
+			bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator().getConstantOverrideTable().values());
+			bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator().getOperatorOverrideTable().values());
 		}
 
 		for (BOperation op : specAnalyser.getBOperations()) {
@@ -52,15 +50,28 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements
 			bDefinitionsSet.add(def);
 		}
 
-		HashSet<OpDefNode> temp = new HashSet<OpDefNode>(bDefinitionsSet);
+		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("SET_PREF_") || defName.startsWith("HEURISTIC_FUNCTION")
+					|| defName.startsWith("SCOPE") || defName.startsWith("scope_")) {
+				bDefinitionsSet.add(opDef);
+			}
+		}
+
+		HashSet<OpDefNode> temp = new HashSet<>(bDefinitionsSet);
 		for (OpDefNode opDefNode : temp) {
 			visitExprNode(opDefNode.getBody());
 		}
+
 	}
 
+	@Override
 	public void visitUserDefinedNode(OpApplNode n) {
 		OpDefNode def = (OpDefNode) n.getOperator();
 		if (bDefinitionsSet.add(def)) {
+			// visit body only once
 			visitExprNode(def.getBody());
 		}
 		for (ExprOrOpArgNode exprOrOpArgNode : n.getArgs()) {
@@ -68,7 +79,7 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements
 		}
 	}
 
-	public HashSet<OpDefNode> getBDefinitionsSet() {
+	public Set<OpDefNode> getBDefinitionsSet() {
 		return bDefinitionsSet;
 	}
 

src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java

@@ -13,22 +13,18 @@ import de.tla2b.analysis.SpecAnalyser;
 import de.tla2b.global.BBuiltInOPs;
 import de.tla2b.global.TranslationGlobals;
 
-public class UsedDefinitionsFinder extends AbstractASTVisitor implements
-		ASTConstants, ToolGlobals, TranslationGlobals {
-
-	private final HashSet<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
+public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
 
+	private final HashSet<OpDefNode> usedDefinitions = new HashSet<>();
 
 	public UsedDefinitionsFinder(SpecAnalyser specAnalyser) {
 
 		if (specAnalyser.getConfigFileEvaluator() != null) {
-			Collection<OpDefNode> cons = specAnalyser.getConfigFileEvaluator()
-					.getConstantOverrideTable().values();
+			Collection<OpDefNode> cons = specAnalyser.getConfigFileEvaluator().getConstantOverrideTable().values();
 			for (OpDefNode def : cons) {
 				visitExprNode(def.getBody());
 			}
-			Collection<OpDefNode> ops = specAnalyser.getConfigFileEvaluator()
-					.getOperatorOverrideTable().values();
+			Collection<OpDefNode> ops = specAnalyser.getConfigFileEvaluator().getOperatorOverrideTable().values();
 			for (OpDefNode def : cons) {
 				visitExprNode(def.getBody());
 			}
@@ -59,6 +55,15 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements
 				visitExprNode(def.getBody());
 			}
 		}
+
+		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("SET_PREF_")) {
+				usedDefinitions.add(opDef);
+			}
+		}
 	}
 
 	public HashSet<OpDefNode> getUsedDefinitions() {
@@ -70,15 +75,12 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements
 		super.visitUserDefinedNode(n);
 
 		OpDefNode def = (OpDefNode) n.getOperator();
-		ModuleNode moduleNode = def.getSource()
-				.getOriginallyDefinedInModuleNode();
+		ModuleNode moduleNode = def.getSource().getOriginallyDefinedInModuleNode();
 		if (moduleNode.getName().toString().equals("TLA2B")) {
 			return;
 		}
 		if (BBuiltInOPs.contains(def.getName())
-				&& STANDARD_MODULES.contains(def.getSource()
-						.getOriginallyDefinedInModuleNode().getName()
-						.toString())) {
+				&& STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
 			return;
 		}
 		if (usedDefinitions.add(def)) {

src/main/java/de/tla2b/types/StructType.java

@@ -81,8 +81,9 @@ public class StructType extends AbstractHasFollowers {
 	}
 
 	public boolean compare(TLAType o) {
-		if (this.contains(o) || o.contains(this))
+		if (this.contains(o) || o.contains(this)) {
 			return false;
+		}
 		if (o.getKind() == UNTYPED)
 			return true;
 
@@ -119,32 +120,32 @@ public class StructType extends AbstractHasFollowers {
 		}
 
 		if (o instanceof StructType) {
-			StructType s = (StructType) o;
+			StructType otherStruct = (StructType) o;
 			boolean extendStruct = false;
 
-			if (this.incompleteStruct && s.incompleteStruct) {
+			if (this.incompleteStruct && otherStruct.incompleteStruct) {
 				extendStruct = false;
 			} else if (this.incompleteStruct) {
-				if (s.types.keySet().containsAll(this.types.keySet())) {
+				if (otherStruct.types.keySet().containsAll(this.types.keySet())) {
 					extendStruct = false;
 				} else {
 					extendStruct = true;
 				}
-			} else if (s.incompleteStruct) {
-				if (this.types.keySet().containsAll(s.types.keySet())) {
+			} else if (otherStruct.incompleteStruct) {
+				if (this.types.keySet().containsAll(otherStruct.types.keySet())) {
 					extendStruct = false;
 				} else {
 					extendStruct = true;
 				}
 			} else {
-				extendStruct = !s.types.keySet().equals(this.types.keySet());
+				extendStruct = !otherStruct.types.keySet().equals(this.types.keySet());
 			}
-			this.extensible = this.extensible || s.extensible || extendStruct;
+			this.extensible = this.extensible || otherStruct.extensible || extendStruct;
 
-			Iterator<String> keys = s.types.keySet().iterator();
+			Iterator<String> keys = otherStruct.types.keySet().iterator();
 			while (keys.hasNext()) {
 				String fieldName = (String) keys.next();
-				TLAType sType = s.types.get(fieldName);
+				TLAType sType = otherStruct.types.get(fieldName);
 				if (this.types.containsKey(fieldName)) {
 					TLAType res = this.types.get(fieldName).unify(sType);
 					this.types.put(fieldName, res);

src/main/java/de/tla2bAst/Translator.java

@@ -346,7 +346,7 @@ public class Translator implements TranslationGlobals {
 	public static RecursiveMachineLoader parseAllMachines(final Start ast, final File f, final BParser bparser)
 			throws BCompoundException {
 		final RecursiveMachineLoader rml = new RecursiveMachineLoader(f.getParent(), bparser.getContentProvider());
-		rml.loadAllMachines(f, ast, bparser.getSourcePositions(), bparser.getDefinitions());
+		rml.loadAllMachines(f, ast, bparser.getDefinitions());
 		return rml;
 	}
 

src/test/java/de/tla2b/main/MainTest.java

 package de.tla2b.main;
 
+import java.io.File;
+
 import org.junit.Test;
 
 import de.tla2b.TLA2B;
@@ -8,8 +10,9 @@ public class MainTest {
 
 	@Test
 	public void testClub() throws Exception {
-		String file = "src/test/resources/regression/Club/Club.tla";
-		TLA2B.main(new String[] { file });
+		String dir = "src/test/resources/regression/Club/";
+		TLA2B.main(new String[] { dir + "Club.tla" });
+		new File(dir + "Club_tla.txt").deleteOnExit();
 	}
 
 }

src/test/java/de/tla2b/prettyprintb/DefinitionsTest.java

@@ -33,4 +33,22 @@ public class DefinitionsTest {
 				+ "END";
 		compare(expected, module);
 	}
+	
+	@Test
+	public void testGoalDefinition() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "VARIABLES x, y \n"
+				+ "Init == x = 1 /\\ y = 1 \n"
+				+ "GOAL == 1=1 \n"
+				+ "=================================";
+		
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS GOAL == 1 = 1;"
+				+ "VARIABLES x, y\n"
+				+ "INVARIANT x : INTEGER & y : INTEGER \n"
+				+ "INITIALISATION  x, y:(x = 1 & y = 1) \n"
+				+ "END";
+		compare(expected, module);
+	}
 }

src/test/java/de/tla2b/prettyprintb/SpecialDefinitions.java

+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class SpecialDefinitions {
+
+	
+	@Test
+	public void testVisualisationDefinition() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CUSTOM_GRAPH_NODES == { <<a,<<\"lightgray\",b>> >> : a\\in 1..2 , b \\in 1..2} \n"
+				+ "CUSTOM_GRAPH_EDGES == 1..10 \n"
+				+ "=================================";
+		
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS CUSTOM_GRAPH_NODES == UNION(a,b).(a : 1 .. 2 & b : 1 .. 2 | {(a|->(\"lightgray\"|->b))}); \n"
+				+ "CUSTOM_GRAPH_EDGES == 1 .. 10;"
+				+ "END";
+		compare(expected, module);
+	}
+}