From 144e947a7e34b8ea0e1beb338970cc36f85d56da Mon Sep 17 00:00:00 2001
From: Yann Thierry-Mieg <Yann.Thierry-Mieg@lip6.fr>
Date: Sun, 31 Mar 2024 16:44:12 +0200
Subject: [PATCH] more tracing + error checking.

---
 .../application/solver/UpperBoundsSolver.java | 62 +++++++++++--------
 1 file changed, 37 insertions(+), 25 deletions(-)

diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/UpperBoundsSolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/UpperBoundsSolver.java
index 69bd04172a..e44e1ae92b 100644
--- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/UpperBoundsSolver.java
+++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/UpperBoundsSolver.java
@@ -82,6 +82,7 @@ public static List<Integer> treatSkeleton(MccTranslator reader, DoneProperties d
 			invar = InvariantCalculator.computePInvariants(sumMatrix);
 		}
 		approximateStructuralBoundsUsingInvariants(sr, invar, tocheck, maxStruct);
+		printBounds("after Invariants on skeleton", maxSeen, maxStruct);
 		
 		checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL CPN_APPROX INITIAL_STATE");
 		
@@ -99,7 +100,7 @@ public static List<Integer> treatSkeleton(MccTranslator reader, DoneProperties d
 			List<SparseIntArray> paths = DeadlockTester.findStructuralMaxWithSMT(tocheck, maxSeen, maxStruct, sr, repr, new ArrayList<>(), 5, true);
 			
 			//interpretVerdict(tocheck, spn, doneProps, new int[tocheck.size()], solverPath, maxSeen, maxStruct);
-			printBounds("after SMT", maxSeen, maxStruct);
+			printBounds("after SMT on skeleton", maxSeen, maxStruct);
 			
 			checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL SAT_SMT CPN_APPROX INITIAL_STATE");
 		return maxStruct;
@@ -135,16 +136,24 @@ public static List<Integer> applyReductions(MccTranslator reader, DoneProperties
 			List<Integer> maxSeen = new ArrayList<>(tocheckIndexes.size());
 			{
 				SparseIntArray m0 = new SparseIntArray(spn.getMarks());
-				for (Expression tc:tocheck) {
-					maxSeen.add(tc.eval(m0));
-					if (spn.isSafe() && tc.getOp() == Op.PLACEREF) {
-						maxStruct.add(1);
-					} else {
+				if (spn.isSafe()) {
+					SparseIntArray ones = new SparseIntArray(spn.getMarks().size());
+					for (int i=0,ie=spn.getPlaceCount();i<ie; i++) {
+						ones.append(i, 1);
+					}
+					for (Expression tc:tocheck) {
+						maxSeen.add(tc.eval(m0));
+						maxStruct.add(tc.eval(ones));
+					}
+					printBounds("Initiallly, because the net is safe", maxSeen, maxStruct);
+				} else {
+					for (Expression tc:tocheck) {
+						maxSeen.add(tc.eval(m0));
 						maxStruct.add(-1);
 					}
+					printBounds("Initially", maxSeen, maxStruct);
 				}
 			}
-			boolean hasSkel = false;
 			if (initMaxStruct != null) {
 				for (int i=0; i < maxStruct.size() ; i++) {
 					int init=initMaxStruct.get(i); 
@@ -152,13 +161,15 @@ public static List<Integer> applyReductions(MccTranslator reader, DoneProperties
 						maxStruct.set(i, init);
 					}
 				}
-				hasSkel = true;
+				printBounds("Adding known information on max bounds.", maxSeen, maxStruct);
 			}
 			
 			checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL INITIAL_STATE");
 			
 			List<Integer> lastMaxSeen = null;
 			
+			printBounds("Before main loop", maxSeen, maxStruct);
+			
 			boolean first = true;
 			do {
 				iter =0;
@@ -170,23 +181,19 @@ public static List<Integer> applyReductions(MccTranslator reader, DoneProperties
 				}
 				StructuralReduction sr = new StructuralReduction(spn);
 				
-				if (!hasSkel) {
-					// the invariants themselves
-					Set<SparseIntArray> invar ;
-					{
-						// effect matrix
-						List<Integer> repr = new ArrayList<>();
-						IntMatrixCol sumMatrix = InvariantCalculator.computeReducedFlow(spn, repr);
-						invar = InvariantCalculator.computePInvariants(sumMatrix);
-					}
-					approximateStructuralBoundsUsingInvariants(sr, invar, tocheck, maxStruct);
-					
-					printBounds("after invariants", maxSeen, maxStruct);
-				//	FlowPrinter.drawNet(sr, "After Invariants");
-					checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL INITIAL_STATE");
-				} else {
-					hasSkel = false;
+				// the invariants themselves
+				Set<SparseIntArray> invar ;
+				{
+					// effect matrix
+					List<Integer> repr = new ArrayList<>();
+					IntMatrixCol sumMatrix = InvariantCalculator.computeReducedFlow(spn, repr);
+					invar = InvariantCalculator.computePInvariants(sumMatrix);
 				}
+				approximateStructuralBoundsUsingInvariants(sr, invar, tocheck, maxStruct);
+
+				printBounds("after invariants", maxSeen, maxStruct);
+				//	FlowPrinter.drawNet(sr, "After Invariants");
+				checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL INITIAL_STATE");
 				
 				lastMaxSeen = new ArrayList<>(maxSeen);
 				RandomExplorer re = new RandomExplorer(sr);
@@ -560,7 +567,7 @@ private static void testWithReachability(MccTranslator ori, List<Integer> maxSee
 				seen++;
 			}
 		}
-		printBounds("After reachability solving "+seen+"queries.", maxSeen, maxStruct);
+		printBounds("After reachability solving "+seen+" queries.", maxSeen, maxStruct);
 	}
 
 	private static void printBounds(String rule, List<Integer> maxSeen, List<Integer> maxStruct) {
@@ -571,6 +578,11 @@ private static void printBounds(String rule, List<Integer> maxSeen, List<Integer
 		printOmegas(maxStruct, sb);
 		
 		System.out.println("Current structural bounds on expressions ("+ rule + ") : " + sb.toString());
+		for (int i=0; i< maxSeen.size() ; i++) {
+			if (maxStruct.get(i) >= 0 && maxSeen.get(i) > maxStruct.get(i)) {
+				System.out.println("Inconsistency detected : max struct is less than max seen for bound index "+i);
+			}
+		}
 	}
 
 	public static void printOmegas(List<Integer> bounds, StringBuilder sb) {