From 674f5e9ab9502e11266eb8d8ffabc7b37fece070 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 9 Jan 2015 17:31:49 +0100
Subject: [PATCH] Implemented 'partial invariant evaluation'

---
 src/main/java/de/tlc4b/TLC4B.java             |  3 +-
 src/main/java/de/tlc4b/TLC4BGlobals.java      | 11 +++
 src/main/java/de/tlc4b/Translator.java        | 63 +++++++------
 .../InvariantPreservationAnalysis.java        | 62 +++++++++++++
 .../UnchangedVariablesFinder.java             |  4 +
 .../java/de/tlc4b/prettyprint/TLAPrinter.java | 93 ++++++++++++++++++-
 6 files changed, 205 insertions(+), 31 deletions(-)
 create mode 100644 src/main/java/de/tlc4b/analysis/unchangedvariables/InvariantPreservationAnalysis.java

diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index a32cac0..88638b8 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/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) {
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 7bd7335..27fd599 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/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() {
@@ -126,6 +129,14 @@ public class TLC4BGlobals {
 	public static boolean isDeleteOnExit() {
 		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;
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 2f16221..cce5b3a 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/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;
@@ -47,7 +48,7 @@ public class Translator {
 		start = parser.parse(machineString, false);
 		final Ast2String ast2String2 = new Ast2String();
 		start.apply(ast2String2);
-		//System.out.println(ast2String2.toString());
+		// System.out.println(ast2String2.toString());
 	}
 
 	public Translator(String machineString, String ltlFormula)
@@ -58,48 +59,52 @@ public class Translator {
 		start = parser.parse(machineString, false);
 		final Ast2String ast2String2 = new Ast2String();
 		start.apply(ast2String2);
-		//System.out.println(ast2String2.toString());
+		// 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());
-		
-		if(constantSetup!= null){
+		rml.loadAllMachines(machineFile, start, null, parser.getDefinitions(),
+				parser.getPragmas());
+
+		if (constantSetup != null) {
 			BParser con = new BParser();
 			Start start2 = null;
 			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();
 			start2.apply(ast2String2);
-			//System.out.println(ast2String2.toString());
+			// System.out.println(ast2String2.toString());
 		}
-		
-	    final Ast2String ast2String2 = new Ast2String();
+
+		final Ast2String ast2String2 = new Ast2String();
 		start.apply(ast2String2);
-		//System.out.println(ast2String2.toString());
+		// System.out.println(ast2String2.toString());
 	}
 
 	public void translate() {
 		new NotSupportedConstructs(start);
-		
+
 		new DefinitionsEliminator(start);
 
 		MachineContext machineContext = new MachineContext(machineName, start,
@@ -117,26 +122,30 @@ public class Translator {
 		ConstantsEvaluator constantsEvaluator = new ConstantsEvaluator(
 				machineContext);
 
+		InvariantPreservationAnalysis invariantPreservationAnalysis = new InvariantPreservationAnalysis(
+				machineContext, constantsEvaluator.getInvariantList(),
+				unchangedVariablesFinder);
+
 		TypeRestrictor typeRestrictor = new TypeRestrictor(start,
 				machineContext, typechecker);
 
 		PrecedenceCollector precedenceCollector = new PrecedenceCollector(
 				start, typechecker, machineContext, typeRestrictor);
-		
+
 		DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(
 				machineContext);
-		
+
 		Generator generator = new Generator(machineContext, typeRestrictor,
 				constantsEvaluator, deferredSetSizeCalculator, typechecker);
 		generator.generate();
 
 		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();
-		
+
 		PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator
 				.getTlaModule().getOperations(), machineContext);
 		primedNodesMarker.start();
@@ -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() {
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/InvariantPreservationAnalysis.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/InvariantPreservationAnalysis.java
new file mode 100644
index 0000000..44c8777
--- /dev/null
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/InvariantPreservationAnalysis.java
@@ -0,0 +1,62 @@
+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);
+		}
+	}
+
+}
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
index 6f9a66b..0fe4427 100644
--- a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
+++ b/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){
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 1be55ae..6e3fe3c 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/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");
 	}
 
-- 
GitLab