Implemented 'partial invariant evaluation'

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

@@ -84,7 +84,6 @@ public class TLC4B {
 				+ results.getNumberOfTransitions());
 		System.out.println("Result: " + results.getResultString());
 
-		
 		if (results.hasTrace() && createTraceFile) {
 			String trace = results.getTrace();
 			String tracefileName = machineFileNameWithoutFileExtension
@@ -156,6 +155,8 @@ public class TLC4B {
 				TLC4BGlobals.setCreateTraceFile(false);
 			} else if (args[index].toLowerCase().equals("-del")) {
 				TLC4BGlobals.setDeleteOnExit(true);
+			} else if (args[index].toLowerCase().equals("-parinveval")) {
+				TLC4BGlobals.setPartialInvariantEvaluation(true);
 			} else if (args[index].toLowerCase().equals("-maxint")) {
 				index = index + 1;
 				if (index == args.length) {

src/main/java/de/tlc4b/TLC4BGlobals.java

@@ -11,6 +11,7 @@ public class TLC4BGlobals {
 	private static boolean checkLTL;
 	private static boolean checkWD;
 	private static boolean proBconstantsSetup;
+	private static boolean partialInvariantEvaluation;
 
 	private static boolean deleteFilesOnExit;
 
@@ -65,6 +66,8 @@ public class TLC4BGlobals {
 		runTestscript = false;
 		testingMode = false;
 		createTraceFile = true;
+		
+		partialInvariantEvaluation = false;
 	}
 
 	public static boolean isCreateTraceFile() {
@@ -127,6 +130,14 @@ public class TLC4BGlobals {
 		return deleteFilesOnExit;
 	}
 	
+	public static boolean isPartialInvariantEvaluation(){
+		return partialInvariantEvaluation;
+	}
+	
+	public static void setPartialInvariantEvaluation(boolean b){
+		partialInvariantEvaluation = b;
+	}
+
 	public static void setDEFERRED_SET_SIZE(int dEFERRED_SET_SIZE) {
 		DEFERRED_SET_SIZE = dEFERRED_SET_SIZE;
 	}

src/main/java/de/tlc4b/Translator.java

@@ -23,6 +23,7 @@ import de.tlc4b.analysis.UsedStandardModules;
 import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
 import de.tlc4b.analysis.transformation.DefinitionsEliminator;
 import de.tlc4b.analysis.typerestriction.TypeRestrictor;
+import de.tlc4b.analysis.unchangedvariables.InvariantPreservationAnalysis;
 import de.tlc4b.analysis.unchangedvariables.UnchangedVariablesFinder;
 import de.tlc4b.prettyprint.TLAPrinter;
 import de.tlc4b.tla.Generator;
@@ -61,18 +62,20 @@ public class Translator {
 		// System.out.println(ast2String2.toString());
 	}
 
-	public Translator(String machineName, File machineFile, String ltlFormula, String constantSetup)
-			throws IOException, BException {
+	public Translator(String machineName, File machineFile, String ltlFormula,
+			String constantSetup) throws IOException, BException {
 		this.machineName = machineName;
 		this.ltlFormula = ltlFormula;
 
 		BParser parser = new BParser(machineName);
 		start = parser.parseFile(machineFile, false);
 
-		// Definitions of definitions files are injected in the ast of the main machine
+		// Definitions of definitions files are injected in the ast of the main
+		// machine
 		final RecursiveMachineLoader rml = new RecursiveMachineLoader(
 				machineFile.getParent(), parser.getContentProvider());
-		rml.loadAllMachines(machineFile, start, null, parser.getDefinitions(), parser.getPragmas());
+		rml.loadAllMachines(machineFile, start, null, parser.getDefinitions(),
+				parser.getPragmas());
 
 		if (constantSetup != null) {
 			BParser con = new BParser();
@@ -80,11 +83,13 @@ public class Translator {
 			try {
 				start2 = con.parse("#FORMULA " + constantSetup, false);
 			} catch (BException e) {
-				System.err.println("An error occured while parsing the constants setup predicate.");
+				System.err
+						.println("An error occured while parsing the constants setup predicate.");
 				throw e;
 			}
 
-			APredicateParseUnit parseUnit = (APredicateParseUnit) start2.getPParseUnit();
+			APredicateParseUnit parseUnit = (APredicateParseUnit) start2
+					.getPParseUnit();
 			this.constantsSetup = parseUnit.getPredicate();
 
 			final Ast2String ast2String2 = new Ast2String();
@@ -117,6 +122,10 @@ public class Translator {
 		ConstantsEvaluator constantsEvaluator = new ConstantsEvaluator(
 				machineContext);
 
+		InvariantPreservationAnalysis invariantPreservationAnalysis = new InvariantPreservationAnalysis(
+				machineContext, constantsEvaluator.getInvariantList(),
+				unchangedVariablesFinder);
+
 		TypeRestrictor typeRestrictor = new TypeRestrictor(start,
 				machineContext, typechecker);
 
@@ -132,8 +141,8 @@ public class Translator {
 
 		generator.getTlaModule().sortAllDefinitions(machineContext);
 
-		UsedStandardModules usedModules = new UsedStandardModules(start, typechecker,
-				typeRestrictor, generator.getTlaModule());
+		UsedStandardModules usedModules = new UsedStandardModules(start,
+				typechecker, typeRestrictor, generator.getTlaModule());
 
 		usedStandardModules = usedModules.getUsedModules();
 
@@ -145,13 +154,13 @@ public class Translator {
 		TLAPrinter printer = new TLAPrinter(machineContext, typechecker,
 				unchangedVariablesFinder, precedenceCollector, usedModules,
 				typeRestrictor, generator.getTlaModule(),
-				generator.getConfigFile(), primedNodesMarker, renamer);
+				generator.getConfigFile(), primedNodesMarker, renamer, invariantPreservationAnalysis);
 		printer.start();
 		moduleString = printer.getStringbuilder().toString();
 		configString = printer.getConfigString().toString();
 
-		tlcOutputInfo = new TLCOutputInfo(machineContext, renamer,
-				typechecker, generator.getTlaModule(), generator.getConfigFile());
+		tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker,
+				generator.getTlaModule(), generator.getConfigFile());
 	}
 
 	public String getMachineString() {

src/main/java/de/tlc4b/analysis/unchangedvariables/InvariantPreservationAnalysis.java

+package de.tlc4b.analysis.unchangedvariables;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.Hashtable;
+
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.Node;
+import de.tlc4b.analysis.MachineContext;
+
+public class InvariantPreservationAnalysis extends DepthFirstAdapter {
+	protected final Hashtable<Node, HashSet<Node>> foundVariablesTable;
+	private final MachineContext machineContext;
+
+	// results
+	private final Hashtable<Node, HashSet<Node>> preservingOperationsTable;
+
+	// temp
+	private HashSet<Node> foundVariables;
+
+	public ArrayList<Node> getPreservingOperations(Node invariant) {
+		return new ArrayList<Node>(preservingOperationsTable.get(invariant));
+	}
+
+	public InvariantPreservationAnalysis(MachineContext machineContext,
+			ArrayList<Node> invariants, UnchangedVariablesFinder unchangedFinder) {
+		this.foundVariablesTable = new Hashtable<Node, HashSet<Node>>();
+		this.machineContext = machineContext;
+
+		this.preservingOperationsTable = new Hashtable<Node, HashSet<Node>>();
+
+		for (Node inv : invariants) {
+			foundVariables = new HashSet<Node>();
+			inv.apply(this);
+			foundVariablesTable.put(inv, foundVariables);
+		}
+
+		for (Node inv : invariants) {
+			HashSet<Node> preservingOperations = new HashSet<Node>();
+			HashSet<Node> usedVariables = foundVariablesTable.get(inv);
+			for (Node op : machineContext.getOperations().values()) {
+				HashSet<Node> assignedVariables = unchangedFinder
+						.getAssignedVariables(op);
+				HashSet<Node> temp = new HashSet<Node>(usedVariables);
+				temp.retainAll(assignedVariables);
+				if (temp.size() == 0) {
+					preservingOperations.add(op);
+				}
+			}
+			preservingOperationsTable.put(inv, preservingOperations);
+		}
+	}
+
+	public void inAIdentifierExpression(AIdentifierExpression node) {
+		Node identifier = machineContext.getReferenceNode(node);
+		if (machineContext.getVariables().containsValue(identifier)) {
+			foundVariables.add(identifier);
+		}
+	}
+
+}

src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java

@@ -58,6 +58,10 @@ public class UnchangedVariablesFinder extends DepthFirstAdapter {
 		return unchangedVariablesTable.get(node);
 	}
 	
+	public HashSet<Node> getAssignedVariables(Node node){
+		return assignedIdentifiersTable.get(node);
+	}
+	
 	public boolean hasUnchangedVariables(Node node){
 		HashSet<Node> set = unchangedVariablesTable.get(node);
 		if(set== null){

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

@@ -6,9 +6,11 @@ import java.util.Iterator;
 import java.util.LinkedList;
 import java.util.List;
 
+import tlc2.TLCGlobals;
 import de.be4.classicalb.core.parser.Utils;
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
 import de.be4.classicalb.core.parser.node.*;
+import de.tlc4b.TLC4B;
 import de.tlc4b.TLC4BGlobals;
 import de.tlc4b.analysis.MachineContext;
 import de.tlc4b.analysis.PrecedenceCollector;
@@ -17,6 +19,7 @@ import de.tlc4b.analysis.Renamer;
 import de.tlc4b.analysis.Typechecker;
 import de.tlc4b.analysis.UsedStandardModules;
 import de.tlc4b.analysis.typerestriction.TypeRestrictor;
+import de.tlc4b.analysis.unchangedvariables.InvariantPreservationAnalysis;
 import de.tlc4b.analysis.unchangedvariables.UnchangedVariablesFinder;
 import de.tlc4b.btypes.BType;
 import de.tlc4b.btypes.FunctionType;
@@ -55,6 +58,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 	private ConfigFile configFile;
 	private PrimedNodesMarker primedNodesMarker;
 	private Renamer renamer;
+	private final InvariantPreservationAnalysis invariantPreservationAnalysis;
 
 	public TLAPrinter(MachineContext machineContext, Typechecker typechecker,
 			UnchangedVariablesFinder unchangedVariablesFinder,
@@ -62,7 +66,8 @@ public class TLAPrinter extends DepthFirstAdapter {
 			UsedStandardModules usedStandardModules,
 			TypeRestrictor typeRestrictor, TLAModule tlaModule,
 			ConfigFile configFile, PrimedNodesMarker primedNodesMarker,
-			Renamer renamer) {
+			Renamer renamer,
+			InvariantPreservationAnalysis invariantPreservationAnalysis) {
 		this.typechecker = typechecker;
 		this.machineContext = machineContext;
 		this.missingVariableFinder = unchangedVariablesFinder;
@@ -73,6 +78,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 		this.configFile = configFile;
 		this.primedNodesMarker = primedNodesMarker;
 		this.renamer = renamer;
+		this.invariantPreservationAnalysis = invariantPreservationAnalysis;
 
 		this.tlaModuleString = new StringBuilder();
 		this.configFileString = new StringBuilder();
@@ -230,6 +236,31 @@ public class TLAPrinter extends DepthFirstAdapter {
 				configFileString.append(assignments.get(i).getString(renamer));
 			}
 		}
+		if(TLC4BGlobals.isPartialInvariantEvaluation()){
+			configFileString.append("CONSTANTS\n");
+			configFileString.append("Init1 = Init1\n");
+			
+			ArrayList<POperation> operations = tlaModule.getOperations();
+			StringBuilder sb = new StringBuilder();
+			sb.append("{");
+			for (int i = 0; i < operations.size(); i++) {
+				AOperation node = (AOperation) operations.get(i);
+				String name = renamer.getNameOfRef(node);
+				configFileString.append(name + "1 = ");
+				configFileString.append(name + "1");
+				configFileString.append("\n");
+				sb.append(name + "1");
+				if(i < operations.size()-1){
+					sb.append(", ");
+				}
+			}
+			sb.append("}");
+			configFileString.append("OpSet = ");
+			configFileString.append(sb);
+			configFileString.append("\n");
+			configFileString.append("VIEW myView");
+		}
+		
 	}
 
 	public void moduleStringAppend(String str) {
@@ -288,6 +319,20 @@ public class TLAPrinter extends DepthFirstAdapter {
 	}
 
 	private void printConstants() {
+		if (TLC4BGlobals.isPartialInvariantEvaluation()) {
+			ArrayList<POperation> operations = tlaModule.getOperations();
+			tlaModuleString.append("CONSTANTS OpSet, Init1, ");
+			for (int i = 0; i < operations.size(); i++) {
+				AOperation node = (AOperation) operations.get(i);
+				String name = renamer.getNameOfRef(node);
+				tlaModuleString.append(name + "1");
+
+				if (i < operations.size() - 1)
+					tlaModuleString.append(", ");
+			}
+			tlaModuleString.append("\n");
+		}
+		/******************/
 		ArrayList<Node> list = this.tlaModule.getConstants();
 		if (list.size() == 0)
 			return;
@@ -322,17 +367,50 @@ public class TLAPrinter extends DepthFirstAdapter {
 		tlaModuleString.append("VARIABLES ");
 		for (int i = 0; i < vars.size(); i++) {
 			vars.get(i).apply(this);
-			if (i < vars.size() - 1)
+			if (i < vars.size() - 1) {
 				tlaModuleString.append(", ");
 			}
+
+		}
+		if (TLC4BGlobals.isPartialInvariantEvaluation()) {
+			tlaModuleString.append(", lastOp");
+		}
 		tlaModuleString.append("\n");
+
+		if (TLC4BGlobals.isPartialInvariantEvaluation()) {
+			tlaModuleString.append("myView == <<");
+			for (int i = 0; i < vars.size(); i++) {
+				vars.get(i).apply(this);
+				if (i < vars.size() - 1)
+					tlaModuleString.append(", ");
+			}
+			tlaModuleString.append(">>\n");
+		}
 	}
 
 	private void printInvariant() {
 		ArrayList<Node> invariants = this.tlaModule.getInvariantList();
 		for (int i = 0; i < invariants.size(); i++) {
+			Node inv = invariants.get(i);
 			tlaModuleString.append("Invariant" + (i + 1) + " == ");
-			invariants.get(i).apply(this);
+			if (TLC4BGlobals.isPartialInvariantEvaluation()) {
+				ArrayList<Node> operations = invariantPreservationAnalysis
+						.getPreservingOperations(inv);
+				if (operations.size() > 0) {
+					tlaModuleString.append("lastOp \\in {");
+					for (int j = 0; j < operations.size(); j++) {
+						Node op = operations.get(j);
+						String name = renamer.getNameOfRef(op);
+						tlaModuleString.append(name);
+						tlaModuleString.append("1");
+						if (j < operations.size() - 1) {
+							tlaModuleString.append(", ");
+						}
+					}
+					tlaModuleString.append("} \\/ ");
+				}
+			}
+			inv.apply(this);
 			tlaModuleString.append("\n");
 		}
 	}
@@ -365,6 +443,9 @@ public class TLAPrinter extends DepthFirstAdapter {
 			if (init instanceof ADisjunctPredicate) {
 				tlaModuleString.append(")");
 			}
+			if (TLC4BGlobals.isPartialInvariantEvaluation()) {
+				tlaModuleString.append(" /\\ lastOp = Init1 ");
+			}
 			if (i < inits.size() - 1)
 				tlaModuleString.append("\n\t/\\ ");
 		}
@@ -965,6 +1046,12 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 		printUnchangedConstants();
 
+		if (TLC4BGlobals.isPartialInvariantEvaluation()) {
+			tlaModuleString.append(" /\\ lastOp' = ");
+			tlaModuleString.append(name);
+			tlaModuleString.append("1");
+		}
+
 		tlaModuleString.append("\n\n");
 	}