Merge pull request #11 from lip6/master

merging

fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/ConcurrentHashDoneProperties.java

@@ -38,4 +38,8 @@ public int size() {
 		return map.size();
 	}
 
+	public Boolean getValue(String prop) {
+		return map.get(prop);
+	}
+
 }

fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/DoneProperties.java

@@ -9,14 +9,15 @@ public interface DoneProperties {
 
 	// A boolean result
 	Boolean put(String prop, Boolean value, String techniques);
+
 	// A numeric result
 	Boolean put(String prop, Integer value, String techniques);
 
-
 	Set<Entry<String, Boolean>> entrySet();
 
 	boolean containsKey(Object arg0);
 
 	Set<String> keySet();
-
+
+	public Boolean getValue(String prop);
 }

fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java

@@ -272,7 +272,7 @@ public int[] runRandomReachabilityDetection (long nbSteps, List<Expression> expr
 	 * @param timeout maximum time for this check, in seconds
 	 * @param bestFirst -1 for random run or the index of the property we want to target with the Best-first heuristic
 	 * @param max if true, we are trying to maximize the expressions (bounds) rather than test their truth value
-	 * @return a set of answers, one per expression in exprs. For "normal" case these are 1 if we found acounter example or 0 otherwise. For bounds these are the max value of the expression.
+	 * @return a set of answers, one per expression in exprs. For "normal" case these are 1 if we found a counter example or 0 otherwise. For bounds these are the max value of the expression.
 	 */
 	public int[] runRandomReachabilityDetection (long nbSteps, List<Expression> exprs, int timeout, int bestFirst, boolean max) {
 		ThreadLocalRandom rand = ThreadLocalRandom.current();
@@ -301,7 +301,7 @@ public int[] runRandomReachabilityDetection (long nbSteps, List<Expression> expr
 			} else {
 				updateMaxVerdicts(exprs, state, verdicts);
 			}
-			if (list[0] == 0){
+			if (list[0] == 0 || ( i >= nbSteps / 3 && nbresets == 0 ) || ( i >= 2*nbSteps/3 && nbresets <= 1) ){
 				//System.out.println("Dead end with self loop(s) found at step " + i);
 				nbresets ++;
 				last = -1;
@@ -365,7 +365,8 @@ public int[] runRandomReachabilityDetection (long nbSteps, List<Expression> expr
 			}
 		}
 		long dur = System.currentTimeMillis() - time + 1; 
-		System.out.println("Incomplete "+(bestFirst>=0?"Best-First ":"")+"random walk after "+ i + "  steps, including "+nbresets+ " resets, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
+		if (nbSteps > 50)
+			System.out.println("Incomplete "+(bestFirst>=0?"Best-First ":"")+"random walk after "+ i + "  steps, including "+nbresets+ " resets, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
 
 		return verdicts;
 	}

fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java

@@ -134,7 +134,7 @@ public Specification rebuildSpecification () {
 		return SpecBuilder.buildSpec(flowPT, flowTP, pnames, tnames, marks);
 	}
 
-	public enum ReductionType { DEADLOCKS, SAFETY, SI_LTL, LTL }
+	public enum ReductionType { DEADLOCKS, SAFETY, SI_LTL, LTL, LIVENESS }
 	public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound {
 		//ruleSeqTrans(trans,places);
 		int initP = pnames.size();
@@ -171,13 +171,16 @@ public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound {
 				totaliter += ruleReduceTrans(rt);
 
 				totaliter += findAndReduceSCCSuffixes(rt) ? 1:0;
-				
+
 				int implicit = ruleImplicitPlace();
 				totaliter +=implicit;
 				if (totaliter > 0 && findFreeSCC(rt))
 					totaliter++;
-
-				totaliter += rulePostAgglo(false,true,rt);
+
+				int agglo = ruleTrivialPostAgglo(rt);
+				totaliter += agglo;
+				if (agglo == 0)
+					totaliter += rulePostAgglo(false,true,rt);
 
 				total += totaliter;
 				if (totaliter > 0) {
@@ -334,7 +337,7 @@ public int ruleRedundantCompositionsBounds() {
 	 * @return the number of transitions discarded by the rule
 	 */
 	private int ruleRedundantCompositions(ReductionType rt) {
-		if (tnames.size() > 20000) {
+		if (tnames.size() > 20000 || rt == ReductionType.LIVENESS) {
 			// quadratic |T| => 10^8 hurts too much 
 			return 0;
 		}
@@ -753,7 +756,7 @@ public int ruleReduceTrans(ReductionType rt) throws NoDeadlockExists {
 			}
 		} 
 
-		if (maxArcValue > 1) {
+		if (maxArcValue > 1 && rt != ReductionType.LIVENESS) {
 			IntMatrixCol tflowPT = flowPT.transpose(); 
 			int modred = 0;
 			// reverse ordered set of tindexes to kill
@@ -904,7 +907,7 @@ private int ensureUnique(IntMatrixCol mPT, IntMatrixCol mTP, List<String> names,
 	}
 
 
-	private int ruleReducePlaces(ReductionType rt, boolean withSyphon, boolean moveTokens) {
+	private int ruleReducePlaces(ReductionType rt, boolean withSyphon, boolean moveTokens) throws DeadlockFound {
 		int totalp = 0;
 		// find constant marking places
 		IntMatrixCol tflowPT = flowPT.transpose();
@@ -920,7 +923,7 @@ private int ruleReducePlaces(ReductionType rt, boolean withSyphon, boolean moveT
 			cstP = new HashSet<>();
 		}
 
-		if (rt != ReductionType.LTL && !keepImage && moveTokens) {
+		if (rt != ReductionType.LTL && !keepImage && moveTokens && rt != ReductionType.LIVENESS) {
 			if (rt == ReductionType.SI_LTL  && marks.stream().mapToInt(i->i).sum() == 1) {
 				int pid = marks.indexOf(1);
 				SparseIntArray from = tflowPT.getColumn(pid);
@@ -980,6 +983,9 @@ private int ruleReducePlaces(ReductionType rt, boolean withSyphon, boolean moveT
 						// always disabled
 						// delete t as well
 						todelTrans.add(from.keyAt(tpos));
+						if (rt == ReductionType.LIVENESS) {
+							throw new DeadlockFound();
+						}
 					}
 				}
 				if (untouchable.get(pid)) {
@@ -1352,7 +1358,103 @@ private boolean inducedBy(int pid, int tcause, IntMatrixCol tflowPT, IntMatrixCo
 
 		return false;
 	}
+	private int ruleTrivialPostAgglo(ReductionType rt) {
+		if (rt == ReductionType.LTL || keepImage) {
+			return 0;
+		}
+		int total = 0;
+		IntMatrixCol tflowPT = flowPT.transpose();
+		IntMatrixCol tflowTP = flowTP.transpose();
+		int initt = tnames.size();
+		long time = System.currentTimeMillis();
+		List<Integer> todel = new ArrayList<>();
+		for (int pid = 0 ; pid < pnames.size() ; pid++) {
+			if (untouchable.get(pid)) {
+				continue;
+			}
+			SparseIntArray fcand = tflowPT.getColumn(pid);
+			SparseIntArray hcand = tflowTP.getColumn(pid);
+			if (fcand.size() == 0 || hcand.size() == 0) {
+				continue;
+			}
+			// refuse to expand anything that is not 1 to 1
+			if (fcand.size() > 1 || hcand.size() > 1) {			
+				continue;
+			}
+			// refuse to do anything other than trivial
+			if (flowTP.getColumn(hcand.keyAt(0)).size() > 1) {
+				continue;
+			}
+
+			// is marked strategy relies on a single output to be triggered
+			boolean isMarked = marks.get(pid) != 0 ; 
+			if (isMarked) {
+				continue;
+			}
+			if (fcand.valueAt(0) != 1 || hcand.valueAt(0) != 1) {
+				continue;
+			}
+
+			List<Integer> Hids = new ArrayList<>();
+			List<Integer> Fids = new ArrayList<>();
+
+			int fid = fcand.keyAt(0);
+			SparseIntArray fPT = flowPT.getColumn(fid);				
+			if (fPT.size() > 1) {
+				// a transition controlled also by someone else than P
+				continue;
+			}
+			Fids.add(fid);
+
+			int hid = hcand.keyAt(0);
+			if (hid == fid) {
+				// Make sure no transition is both input and output for p
+				continue;
+			}
+			Hids.add(hid);
+
+
+			if (touches(Hids) || touches(Fids))
+				continue;
 
+			if (DEBUG>=1) System.out.println("Net is trivially Post-aglomerable in place id "+pid+ " "+pnames.get(pid) + " H->F : " + Hids + " -> " + Fids);
+
+			// substitute output of h by output of f
+			SparseIntArray fTP = flowTP.getColumn(fid);
+			flowTP.setColumn(hid, fTP);
+			// clear f
+			flowPT.setColumn(fid, new SparseIntArray());
+			flowTP.setColumn(fid, new SparseIntArray());			
+			todel.add(fid);
+
+			for (int j=0, je=fTP.size() ; j < je ; j++ ) {
+				int pfed = fTP.keyAt(j);
+				int val = tflowTP.getColumn(pfed).get(fid);
+				tflowTP.getColumn(pfed).put(fid,0);
+				tflowTP.getColumn(pfed).put(hid,val);
+			}
+
+			total++;
+
+			long deltat = System.currentTimeMillis() - time;
+			if (deltat >= 30000) {
+				System.out.println("Performed "+total + " Post agglomeration using trivial condition.");
+				time = System.currentTimeMillis();
+			}
+
+		}
+		if (! todel.isEmpty()) {
+			dropTransitions(todel,"Trivial Post-Agglo cleanup.");
+			System.out.println("Trivial Post-agglo rules discarded "+todel.size()+ " transitions");
+		}
+
+		if (total != 0) {
+			System.out.println("Performed "+total + " trivial Post agglomeration. Transition count delta: " + (initt -tnames.size()));
+		}
+
+		return total;
+
+	}
 	private int rulePostAgglo(boolean doComplex, boolean doSimple, ReductionType rt) {
 		if (rt == ReductionType.LTL) {
 			return 0;
@@ -2011,6 +2113,7 @@ private int ruleFusePlaceByFuture() {
 		}
 
 		if (!toFuse.isEmpty()) {
+			List<Integer> todelp = new ArrayList<>();
 			Set<Integer> todel = new TreeSet<>((x,y)->-Integer.compare(x, y));
 			// now work with the tflowTP to find transitions feeding pj we need to update
 			IntMatrixCol tflowTP = flowTP.transpose();
@@ -2049,15 +2152,28 @@ private int ruleFusePlaceByFuture() {
 				}
 				marks.set(pi, marks.get(pi)+marks.get(pj));
 				marks.set(pj, 0);
-
+				image.set(pi, Expression.op(Op.ADD, image.get(pi), image.get(pj)));
+				if (tokeepImages.get(pj)) {
+					tokeepImages.set(pi);
+					tokeepImages.clear(pj);
+				}
+				todelp.add(pj);
 			}
+
 
-			for (int i : todel) {
-				// System.out.println("removing transition "+tnames.get(i) +" pre:" + flowPT.getColumn(i) +" post:" + flowTP.getColumn(i));
-				flowPT.deleteColumn(i);
-				flowTP.deleteColumn(i);
-				tnames.remove(i);
+			if (! todelp.isEmpty()) {
+				for (int pid : todelp) {
+					SparseIntArray tpt = tflowPT.getColumn(pid);
+					for (int i=0;i<tpt.size();i++) {
+						todel.add(tpt.keyAt(i));
+					}
+				}
+				dropPlaces(todelp, false, "Symmetric choice cleanup.");
 			}
+			if (!todel.isEmpty()) {
+				dropTransitions(new ArrayList<>(todel), false, "Symmetric choice");
+			}
+
 		}
 		return toFuse.size();
 	}
@@ -2218,7 +2334,7 @@ private boolean isStronglyQuasiPersistent(int hid, IntMatrixCol tflowPT, Reducti
 	}
 
 	private boolean findAndReduceSCCSuffixes(ReductionType rt) throws DeadlockFound {
-		if (rt == ReductionType.LTL)
+		if (rt == ReductionType.LTL || rt == ReductionType.LIVENESS)
 			return false;
 		Set<Integer> safeNodes = findSCCSuffixes(this,rt,untouchable);
 		if (safeNodes.size() < getPlaceCount()) {

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/Application.java

@@ -46,9 +46,8 @@
 import fr.lip6.move.gal.mcc.properties.PropertiesToPNML;
 import fr.lip6.move.gal.semantics.IDeterministicNextBuilder;
 import fr.lip6.move.gal.semantics.INextBuilder;
-import fr.lip6.move.gal.structural.DeadlockFound;
+import fr.lip6.move.gal.structural.GlobalPropertySolvedException;
 import fr.lip6.move.gal.structural.InvariantCalculator;
-import fr.lip6.move.gal.structural.NoDeadlockExists;
 import fr.lip6.move.gal.structural.SparsePetriNet;
 import fr.lip6.move.gal.structural.StructuralReduction;
 import fr.lip6.move.gal.structural.expr.Expression;
@@ -694,7 +693,7 @@ private void regeneratePNML(MccTranslator reader, DoneProperties doneProps, Stri
 					System.out.println("For property " + prop.getName() + " final size "
 							+ ((GALTypeDeclaration) copy.getSpec().getTypes().get(0)).getVariables().size());
 				}
-			} catch (NoDeadlockExists | DeadlockFound e) {
+			} catch (GlobalPropertySolvedException e) {
 				e.printStackTrace();
 			}
 		}

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/DeadlockSolver.java

@@ -100,8 +100,8 @@ public static Optional<Boolean> checkStructuralDeadlock(String pwd, String exami
 					br.computeMatrixForm(generators);
 				}
 				try {
-					if (! ReachabilitySolver.applyReductions(sr, reader, ReductionType.DEADLOCKS, solverPath, isSafe,false,true)) 
-						ReachabilitySolver.applyReductions(sr, reader, ReductionType.DEADLOCKS, solverPath, isSafe,true,false);					
+					if (! ReachabilitySolver.applyReductions(sr, ReductionType.DEADLOCKS, solverPath, isSafe, false,true)) 
+						ReachabilitySolver.applyReductions(sr, ReductionType.DEADLOCKS, solverPath, isSafe, true,false);					
 				} catch (DeadlockFound d) {
 					doneProps.put(REACHABILITY_DEADLOCK, true, "TOPOLOGICAL STRUCTURAL_REDUCTION");
 					return Optional.of(true);
@@ -128,7 +128,7 @@ public static Optional<Boolean> checkStructuralDeadlock(String pwd, String exami
 				for (int iter=0 ; iter<2 ; iter++) {
 
 					if (iter == 1) {
-						ReachabilitySolver.applyReductions(sr, reader, ReductionType.DEADLOCKS, solverPath, isSafe,true,false);
+						ReachabilitySolver.applyReductions(sr, ReductionType.DEADLOCKS, solverPath, isSafe, true,false);
 					}
 					RandomExplorer re = new RandomExplorer(sr);
 					long time = System.currentTimeMillis();					

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalDonePropertyPrinter.java

@@ -29,6 +29,10 @@ public String computeTechniques() {
 
 	}
 
+	public boolean shouldTrace() {
+		return makeTrace;
+	}
+
 	@Override
 	public Boolean put(String prop, Boolean value, String techniques) {
 		// System.out.println("FORMULA "+prop+(value?" TRUE":" FALSE")+ " TECHNIQUES
@@ -41,25 +45,23 @@ public Boolean put(String prop, Boolean value, String techniques) {
 
 		case "StableMarking":
 			if (value) {
+				super.put(examination, true, computeTechniques());
 				if (makeTrace)
 					System.out.println("FORMULA " + examination + " TRUE TECHNIQUES " + computeTechniques());
 				throw new GlobalPropertySolverException(examination + " TRUE", true);
 			}
 			break;
 		case "OneSafe":
+		case "Liveness":
+		case "QuasiLiveness": {
 			if (!value) {
+				super.put(examination, false, computeTechniques());
 				if (makeTrace)
 					System.out.println("FORMULA " + examination + " FALSE TECHNIQUES " + computeTechniques());
 				throw new GlobalPropertySolverException(examination + " FALSE", false);
 			}
 			break;
-		case "QuasiLiveness":
-			if (!value) {
-				if (makeTrace)
-					System.out.println("FORMULA " + examination + " FALSE TECHNIQUES " + computeTechniques());
-				throw new GlobalPropertySolverException(examination + " FALSE", false);
-			}
-			break;
+		}
 		}
 
 		return super.put(prop, value, techniques);