added symmetry reduction

src/main/java/de/tlc4b/TLC4B.java

@@ -71,24 +71,31 @@ public class TLC4B {
 
 	}
 
-
 	private void printResults(TLCResults results, boolean createTraceFile) {
 		// options
 		System.out.println("Used Options");
 		System.out.println("| Number of workers: " + TLC4BGlobals.getWorkers());
 		System.out.println("| Invariants check: " + TLC4BGlobals.isInvariant());
-		System.out.println("| Deadlock check: " + TLC4BGlobals.isDeadlockCheck());
+		System.out.println("| Deadlock check: "
+				+ TLC4BGlobals.isDeadlockCheck());
 		System.out.println("| Assertion check: " + TLC4BGlobals.isAssertion());
 		System.out.println("| Find Goal check: " + TLC4BGlobals.isGOAL());
-		System.out.println("| LTL formulas check: " + TLC4BGlobals.isCheckLTL());
-		System.out.println("| Partial invariant evaluation: " + TLC4BGlobals.isPartialInvariantEvaluation());
-		System.out.println("| Lazy constants setup: " + !TLC4BGlobals.isForceTLCToEvalConstants());
-		System.out.println("| Agressive well-definedness check: " + TLC4BGlobals.checkWelldefinedness());
-		System.out.println("| Prob constant setup: " + TLC4BGlobals.isProBconstantsSetup());
-		System.out.println("| Symmetry used: " + TLC4BGlobals.useSymmetry());
+		System.out
+				.println("| LTL formulas check: " + TLC4BGlobals.isCheckLTL());
+		System.out.println("| Partial invariant evaluation: "
+				+ TLC4BGlobals.isPartialInvariantEvaluation());
+		System.out.println("| Lazy constants setup: "
+				+ !TLC4BGlobals.isForceTLCToEvalConstants());
+		System.out.println("| Agressive well-definedness check: "
+				+ TLC4BGlobals.checkWelldefinedness());
+		System.out.println("| Prob constant setup: "
+				+ TLC4BGlobals.isProBconstantsSetup());
+		System.out.println("| Symmetry reduction: "
+				+ TLC4BGlobals.useSymmetry());
 		System.out.print("| MIN Int: " + TLC4BGlobals.getMIN_INT());
 		System.out.print(" | MAX Int: " + TLC4BGlobals.getMAX_INT());
-		System.out.println(" | Deferret set size: " + TLC4BGlobals.getDEFERRED_SET_SIZE());
+		System.out.println(" | Standard deferret set size: "
+				+ TLC4BGlobals.getDEFERRED_SET_SIZE());
 		System.out.println("--------------------------------");
 		System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing")
 				+ " ms");
@@ -96,7 +103,8 @@ public class TLC4B {
 				+ " ms");
 		System.out.println("Model checking time: "
 				+ results.getModelCheckingTime() + " sec");
-		//System.out.println("Number of workers: " + TLCGlobals.getNumWorkers());
+		// System.out.println("Number of workers: " +
+		// TLCGlobals.getNumWorkers());
 		System.out.println("States analysed: "
 				+ results.getNumberOfDistinctStates());
 		System.out.println("Transitions fired: "
@@ -162,6 +170,8 @@ public class TLC4B {
 				TLC4BGlobals.setAssertionCheck(false);
 			} else if (args[index].toLowerCase().equals("-wdcheck")) {
 				TLC4BGlobals.setWelldefinednessCheck(true);
+			} else if (args[index].toLowerCase().equals("-symmetry")) {
+				TLC4BGlobals.setSymmetryUse(true);
 			} else if (args[index].toLowerCase().equals("-tool")) {
 				TLC4BGlobals.setTool(false);
 			} else if (args[index].toLowerCase().equals("-tmp")) {

src/main/java/de/tlc4b/analysis/Renamer.java

@@ -67,6 +67,7 @@ public class Renamer extends DepthFirstAdapter {
 		KEYWORDS.add("WF_");
 		KEYWORDS.add("WITH");
 		KEYWORDS.add("STATE");
+		KEYWORDS.add("DEF");
 
 		KEYWORDS.add("Init");
 		KEYWORDS.add("Next");

src/main/java/de/tlc4b/analysis/UsedStandardModules.java

@@ -132,6 +132,12 @@ public class UsedStandardModules extends DepthFirstAdapter {
 		this.usedStandardModules = new HashSet<STANDARD_MODULES>();
 		this.typechecker = typechecker;
 
+		
+		
+		if (TLC4BGlobals.useSymmetry()) {
+			usedStandardModules.add(STANDARD_MODULES.TLC);
+		}
+		
 		List<PDefinition> definitions = tlaModule.getAllDefinitions();
 		if (definitions != null) {
 			for (PDefinition pDefinition : definitions) {

src/main/java/de/tlc4b/prettyprint/TLAPrinter.java

 package de.tlc4b.prettyprint;
 
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.HashSet;
 import java.util.Iterator;
 import java.util.LinkedList;
@@ -98,11 +99,35 @@ public class TLAPrinter extends DepthFirstAdapter {
 		printSpecFormula();
 		printLTLFormulas();
 
+		printSymmetry();
+		
+		
 		tlaModuleString.append("====");
 
 		printConfig();
 	}
 
+	private void printSymmetry() {
+
+		if(TLC4BGlobals.useSymmetry() && machineContext.getDeferredSets().size()>0){
+			
+			tlaModuleString.append("Symmetry == ");
+			Collection<Node> values = machineContext.getDeferredSets().values();
+			ArrayList<Node> array = new ArrayList<Node>(values);
+			for (int i = 0; i < array.size(); i++) {
+				Node node = array.get(i);
+				tlaModuleString.append("Permutations(");
+				node.apply(this);
+				tlaModuleString.append(")");
+				if(i<array.size()-1){
+					tlaModuleString.append(" \\cup ");
+				}
+			}
+			tlaModuleString.append("\n");
+			//Symmetry == Permutations(Clients) \cup Permutations(Resources)
+		}
+	}
+
 	private void printSpecFormula() {
 
 		if (this.configFile.isSpec()) {
@@ -235,6 +260,11 @@ public class TLAPrinter extends DepthFirstAdapter {
 				configFileString.append(assignments.get(i).getString(renamer));
 			}
 		}
+		if(TLC4BGlobals.useSymmetry()&& machineContext.getDeferredSets().size()>0){
+			configFileString.append("SYMMETRY Symmetry\n");
+		}
+		
+		
 		if (TLC4BGlobals.isPartialInvariantEvaluation()) {
 			configFileString.append("CONSTANTS\n");
 			configFileString.append("Init_action = Init_action\n");