hopefully last issues with indexes...

Author: yanntm

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/UpperBoundsSolver.java

@@ -266,8 +266,6 @@ public static List<Integer> applyReductions(MccTranslator reader, DoneProperties
 
 					printBounds("After Parikh guided walk", maxSeen, maxStruct);
 					checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL PARIKH_GUIDED_WALK");
-				if (spn.getProperties().removeIf(p -> doneProps.containsKey(p.getName())))
-					iter++;
 				if (spn.getProperties().isEmpty())
 					break;
 
@@ -309,7 +307,9 @@ public static List<Integer> applyReductions(MccTranslator reader, DoneProperties
 				spn.testInInitial();
 				spn.removeConstantPlaces();
 				spn.simplifyLogic();			
-
+				
+				
+				
 				if (checkStatus(spn, tocheck, maxStruct, maxSeen, doneProps, "TOPOLOGICAL STRUCTURAL_REDUCTION") > 0) {
 					printBounds("after structural reductions", maxSeen, maxStruct);
 					iter++;
@@ -318,6 +318,15 @@ public static List<Integer> applyReductions(MccTranslator reader, DoneProperties
 					return Collections.emptyList();
 				}
 
+				if (spn.getProperties().size() != tocheck.size()) {
+					System.out.println("Inconsistency detected : number of properties changed after reduction without any verdict. This should not happen.");
+				} else {
+					tocheck.clear();
+					for (Property prop : spn.getProperties()) {
+						tocheck.add(prop.getBody());
+					}
+				}
+				
 				if (!isBounded.isPresent()) {
 					// check if we still have inf upper bounds
 					int hasInf = -1;
@@ -348,7 +357,7 @@ public static List<Integer> applyReductions(MccTranslator reader, DoneProperties
 							long total = 10000; // 10 seconds 
 							while (System.currentTimeMillis() - start < total) {
 								int[] verdicts = cw.runRandomReachabilityDetection(nbsteps, tocheck, (int) (total - (start - System.currentTimeMillis())) / 1000, -1, true, maxState);							
-								iter += interpretVerdict(tocheck, spn, doneProps, verdicts,"COVER",maxSeen,maxStruct);
+								iter += interpretVerdict(tocheck, spn, doneProps, verdicts,"COVER", maxSeen, maxStruct);
 								if (DEBUG >= 1) printBounds("after cover walk", maxSeen, maxStruct);
 								if (maxSeen.size() == 0) {
 									break;
@@ -466,9 +475,6 @@ private static void testWithReachability(MccTranslator ori, List<Integer> maxSee
 				}
 			}
 			if (done) {
-				ori.getSPN().getProperties().remove(id);
-				maxSeen.remove(id);
-				maxStruct.remove(id);
 				seen++;
 			}
 		}
@@ -672,13 +678,11 @@ public static void approximateStructuralBoundsUsingInvariants(ISparsePetriNet sr
 	}
 
 	public static void computeToCheck(SparsePetriNet spn, List<Expression> tocheck, DoneProperties doneProps) {
-		int j=0;
 		tocheck.clear();
 		for (fr.lip6.move.gal.structural.Property p : spn.getProperties()) {
 			if (! doneProps.containsKey(p.getName()) && p.getType() == PropertyType.BOUNDS) {
 				tocheck.add(p.getBody());
 			}
-			j++;
 		}			
 	}