Merge pull request #16 from lip6/master

merge

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

@@ -42,4 +42,8 @@ public Boolean getValue(String prop) {
 		return map.get(prop);
 	}
 
+	@Override
+	public boolean isFinished() {
+		return false;
+	}
 }

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

@@ -20,4 +20,6 @@ public interface DoneProperties {
 	Set<String> keySet();
 
 	public Boolean getValue(String prop);
+
+	boolean isFinished();
 }

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

@@ -62,7 +62,8 @@ public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikh
 		for (; i < nbSteps ; i++) {			
 			long dur = System.currentTimeMillis() - time + 1; 
 			if (dur > 1000 * timeout) {
-				System.out.println("Interrupted Parikh walk after "+ i + "  steps, including "+nbresets+ " resets, run timeout after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
+				System.out.println("Interrupted Parikh walk after "+ i + "  steps, including "+nbresets+ " resets, run timeout after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties (out of " + exprs.size()
+				+ ") seen :" + Arrays.stream(verdicts).sum() +(DEBUG >=1 ? (" reached state " + state):"") );
 				return verdicts;
 			}
 			if (!max) {
@@ -138,7 +139,11 @@ public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikh
 		}
 
 		long dur = System.currentTimeMillis() - time + 1; 
-		System.out.println("Incomplete Parikh walk after "+ i + " steps, including "+nbresets+ " resets, run finished after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + new SparseIntArray(verdicts) + " could not realise parikh vector " + (DEBUG >=1 ? parikhori : "")+ (DEBUG >=1 ? (" reached state " + state):"") );
+		System.out.println("Incomplete Parikh walk after " + i + " steps, including " + nbresets
+				+ " resets, run finished after " + dur + " ms. (steps per millisecond=" + (i / dur) + " )"
+				+ " properties (out of " + exprs.size()
+				+ ") seen :" + Arrays.stream(verdicts).sum() + " could not realise parikh vector "
+				+ (DEBUG >= 1 ? parikhori : "") + (DEBUG >= 1 ? (" reached state " + state) : ""));
 		return verdicts;
 	}
 
@@ -366,7 +371,10 @@ public int[] runRandomReachabilityDetection (long nbSteps, List<Expression> expr
 		}
 		long dur = System.currentTimeMillis() - time + 1; 
 		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):"") );
+			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 (out of " + exprs.size()
+					+ ") seen :" + Arrays.stream(verdicts).sum() + (DEBUG >= 1 ? (" reached state " + state) : ""));
 
 		return verdicts;
 	}

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

@@ -532,7 +532,7 @@ public void readFrom(StructuralReduction sr) {
 	public List<Expression> readFrom(StructuralReduction sr, List<Expression> original) {
 		this.flowPT = sr.getFlowPT();
 		this.flowTP = sr.getFlowTP();
-		this.marks = sr.getMarks();
+		this.marks = new ArrayList<>(sr.getMarks());
 		this.maxArcValue = sr.getMaxArcValue();
 		this.tnames = sr.getTnames();
 		int [] perm = new int [pnames.size()];

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

@@ -102,6 +102,10 @@ public void setKeepImage(boolean keepImage) {
 		this.keepImage = keepImage;
 	}
 
+	public BitSet getTokeepImages() {
+		return tokeepImages;
+	}
+
 	private int findMax(IntMatrixCol mat) {
 		int max =0;
 		for (int ti = 0 ; ti < mat.getColumnCount() ; ti++) {
@@ -136,7 +140,7 @@ public Specification rebuildSpecification () {
 		return SpecBuilder.buildSpec(flowPT, flowTP, pnames, tnames, marks);
 	}
 
-	public enum ReductionType { DEADLOCKS, SAFETY, SI_LTL, LTL, LIVENESS }
+	public enum ReductionType { DEADLOCKS, SAFETY, SI_LTL, LTL, LIVENESS, STATESPACE }
 	public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound {
 		//ruleSeqTrans(trans,places);
 		int initP = pnames.size();
@@ -149,6 +153,16 @@ public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound {
 		int totaliter=0;
 		int iter =0;
 
+		if (rt == ReductionType.STATESPACE) {
+			// pretty basic stuff only
+			total += ruleReducePlaces(rt,false,false);
+			total += ruleReduceTrans(rt);
+			total += ruleRedundantCompositions(rt);
+			total += ruleReducePlaces(rt,false,false);
+			total += ruleReduceTrans(rt);			
+			return total;
+		}
+
 		if (findFreeSCC(rt)) {
 			total++;
 			totaliter += ruleReduceTrans(rt);
@@ -237,6 +251,10 @@ public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound {
 				totaliter += findAndReduceSCCSuffixes(rt) ? 1 :0;
 			}
 			totaliter += ruleReducePlaces(rt,true,false);						
+			if (totaliter ==0) {
+				totaliter += ruleRedundantCompositions(rt);
+			}
+
 			if (totaliter == 0 && rt == ReductionType.SAFETY) {
 				totaliter += ruleFreeAgglo(false);
 			}
@@ -246,12 +264,12 @@ public int reduce (ReductionType rt) throws NoDeadlockExists, DeadlockFound {
 			if (totaliter == 0 && rt == ReductionType.SAFETY) {
 				totaliter += rulePartialFreeAgglo();
 			}			
-			if (totaliter == 0 && rt == ReductionType.SAFETY) {
+			if (totaliter == 0 && (rt == ReductionType.SAFETY || (rt == ReductionType.SI_LTL && ! keepImage)) ) {
+				// this rule is almost legitimate for SI_LTL
+				// but not quite
 				totaliter += rulePartialPostAgglo(rt);
 			}						
-			if (totaliter ==0) {
-				totaliter += ruleRedundantCompositions(rt);
-			}
+
 			if (totaliter ==0) {
 				totaliter += ruleReducePlaces(rt,false,true);
 			}
@@ -727,14 +745,14 @@ public int ruleFreeAgglo(boolean doComplex) {
 
 	public int ruleReduceTrans(ReductionType rt) throws NoDeadlockExists {
 		int reduced = 0;
-		if (rt == ReductionType.SAFETY) {
+		if (rt == ReductionType.SAFETY || rt == ReductionType.STATESPACE) {
 
 			List<Integer> todrop = new ArrayList<>();
 			for (int i = tnames.size()-1 ;  i >= 0 ; i--) {
-				if (rt == ReductionType.SAFETY && flowPT.getColumn(i).equals(flowTP.getColumn(i))) {
+				if ( (rt == ReductionType.SAFETY || rt == ReductionType.STATESPACE) && flowPT.getColumn(i).equals(flowTP.getColumn(i))) {
 					// transitions with no effect => no use to safety
 					todrop.add(i);
-				} else if (flowTP.getColumn(i).size() == 0 && ! touches(i)) {
+				} else if (rt == ReductionType.SAFETY && flowTP.getColumn(i).size() == 0 && ! touches(i)) {
 					// sink transitions that are stealing tokens from the net are not helpful
 					// they lead to strictly weaker nets
 					todrop.add(i);
@@ -997,7 +1015,7 @@ private int ruleReducePlaces(ReductionType rt, boolean withSyphon, boolean moveT
 				if (DEBUG >= 2) cstP.add(pid);
 				totalp++;
 			} else if (from.size() == 0) {
-				if (untouchable.get(pid)) {
+				if (rt==ReductionType.STATESPACE || untouchable.get(pid)) {
 					continue;
 				}
 				prem.add(dropPlace(pid, tflowPT, tflowTP));
@@ -1014,7 +1032,9 @@ private int ruleReducePlaces(ReductionType rt, boolean withSyphon, boolean moveT
 			FlowPrinter.drawNet(sr2, "Constant places reduction"+ (withPreFire ? " with pre firing/single continuation ":"")+ prem, cstP, todelTrans);
 			//FlowPrinter.drawNet(this, "Constant places reduction REAL RESULT"+ (withPreFire ? " with pre firing/single continuation ":"")+ prem, cstP, todelTrans);
 		}
-		int deltap = ensureUnique(tflowPT, tflowTP, pnames, marks, true);
+		int deltap = 0;
+		if (rt != ReductionType.STATESPACE)
+			deltap = ensureUnique(tflowPT, tflowTP, pnames, marks, true);
 		totalp += deltap;
 		if (deltap > 0) {
 			// reconstruct updated flow matrices
@@ -1625,6 +1645,8 @@ private int rulePostAgglo(boolean doComplex, boolean doSimple, ReductionType rt)
 				}
 				if (!ok)
 					continue;				
+			} else if (rt==ReductionType.SI_LTL && touches(Fids)) {
+				continue;
 			}
 
 			if (DEBUG>=1) System.out.println("Net is Post-agglomerable in place id "+pid+ " "+pnames.get(pid) + " H->F : " + Hids + " -> " + Fids);
@@ -2064,7 +2086,9 @@ private int ruleFusePlaceByFuture(ReductionType rt) {
 					continue;
 				SparseIntArray piouts = tflowPT.getColumn(pi);
 
-
+				boolean tokeepi = false;
+				if (keepImage)
+					tokeepi=tokeepImages.get(pi);
 				for (int j = i+ 1 ; j < list.size() ; j++ ) {					
 					int pj = list.get(j);
 					if (untouchable.get(pj)) {
@@ -2075,6 +2099,9 @@ private int ruleFusePlaceByFuture(ReductionType rt) {
 					}
 					if (toFuse.containsKey(pj)) 
 						continue;
+					if (keepImage && tokeepi !=tokeepImages.get(pj)) {
+						continue;
+					}
 					SparseIntArray pjouts = tflowPT.getColumn(pj);
 					// so, pi and pj have the same number of outputs
 					int ti = 0;
@@ -2171,11 +2198,7 @@ private int ruleFusePlaceByFuture(ReductionType rt) {
 				}
 				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);
-				}
+				image.set(pi, Expression.op(Op.ADD, image.get(pi), image.get(pj)));				
 				todelp.add(pj);
 			}
 
@@ -2847,4 +2870,12 @@ public boolean isSafe() {
 	public void setSafe(boolean isSafe) {
 		this.isSafe = isSafe;
 	}
+
+
+	public boolean isKeepImage() {
+		return keepImage;
+	}
+
+
+
 }

fr.lip6.move.gal/src/fr/lip6/move/serialization/BasicGalSerializer.java

@@ -113,8 +113,10 @@ public void serialize (EObject modelElement, OutputStream stream) {
 	}
 
 	public void close() {
-		pw.flush();
-		pw.close();
+		if (pw != null) {
+			pw.flush();
+			pw.close();
+		}
 		pw = null;
 	}
 

fr.lip6.move.gal/src/fr/lip6/move/serialization/SerializationUtil.java

@@ -91,8 +91,12 @@ public static void systemToFile(Specification system, final String filename) thr
 
 			FileOutputStream os = new FileOutputStream(filename);
 			BasicGalSerializer bser = new BasicGalSerializer();
-			bser.serialize(system, new BufferedOutputStream(os));
+			BufferedOutputStream buff = new BufferedOutputStream(os);
+			bser.serialize(system, buff);
 //			system.eResource().save(os, map);
+			bser.close();
+			buff.flush();
+			buff.close();
 			os.close();
 
 //			java.lang.System.out.println("Done");

pins/fr.lip6.move.gal.gal2pins/src/fr/lip6/move/gal/gal2pins/Gal2PinsTransformerNext.java

@@ -1,6 +1,7 @@
 package fr.lip6.move.gal.gal2pins;
 
 import java.io.ByteArrayOutputStream;
+import java.io.File;
 import java.io.IOException;
 import java.io.PrintWriter;
 import java.util.List;
@@ -46,6 +47,7 @@
 
 public class Gal2PinsTransformerNext {
 
+	private static final int DEBUG = 0;
 	private List<List<INext>> transitions;
 	private IDeterministicNextBuilder dnb;
 	private Gal2SMTFrontEnd gsf;
@@ -57,6 +59,8 @@ public void setSmtConfig(Gal2SMTFrontEnd gsf) {
 	}
 
 	private void buildBodyFile(String path) throws IOException {
+		File fpath = new File(path);
+		if (DEBUG==0) fpath.deleteOnExit();
 		PrintWriter pw = new PrintWriter(path);
 
 		pw.println("#include <ltsmin/pins.h>");
@@ -118,6 +122,8 @@ private void buildBodyFile(String path) throws IOException {
 
 
 	private void buildHeader(String path) throws IOException {
+		File fpath = new File(path);
+		if (DEBUG==0) fpath.deleteOnExit();
 		PrintWriter pw = new PrintWriter(path);
 		pw.print(
 				"#include <ltsmin/pins.h>\n"+

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

@@ -27,7 +27,14 @@ public void join() throws InterruptedException {
 			runnerThread.join();
 		}		
 	}
+	@Override
+	public void join(long millis) throws InterruptedException {
+		if (runnerThread != null) {
+			runnerThread.join(millis);
+		}		
+	}
 
+
 	@Override
 	public void configure(Specification z3Spec, DoneProperties doneProps) throws IOException {
 		this.spec = z3Spec ;

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

@@ -51,6 +51,7 @@
 import fr.lip6.move.gal.structural.InvariantCalculator;
 import fr.lip6.move.gal.structural.SparsePetriNet;
 import fr.lip6.move.gal.structural.StructuralReduction;
+import fr.lip6.move.gal.structural.StructuralReduction.ReductionType;
 import fr.lip6.move.gal.structural.expr.Expression;
 import fr.lip6.move.gal.structural.smt.DeadlockTester;
 import fr.lip6.move.gal.util.IntMatrixCol;
@@ -305,6 +306,17 @@ public Object startNoEx(IApplicationContext context) throws Exception {
 			if (totaltok > 0) {
 				reader.setMissingTokens(totaltok);
 			}
+			{
+				SparsePetriNet spn = reader.getSPN();
+				StructuralReduction sr = new StructuralReduction(spn);
+				ReachabilitySolver.applyReductions(sr,ReductionType.STATESPACE,solverPath,true,true);
+
+				// Breaks max token per marking metric.
+				int curtok = spn.getMarks().stream().mapToInt(i->i).sum();
+				int newtok = sr.getMarks().stream().mapToInt(i->i).sum();				
+				spn.readFrom(sr);
+				reader.setMissingTokens( (curtok-newtok) + reader.countMissingTokens());
+			}
 			System.out.println("Final net has " + reader.getSPN().getPlaceCount() + " places and "
 					+ reader.getSPN().getTransitionCount() + " transitions.");
 			reader.rebuildSpecification(doneProps);
@@ -453,8 +465,8 @@ public Object startNoEx(IApplicationContext context) throws Exception {
 				// || examination.startsWith("CTL")
 				if (!reader.getSpec().getProperties().isEmpty()) {
 					System.out.println("Using solver " + solver + " to compute partial order matrices.");
-					LTSminRunner ltsRunner = new LTSminRunner(solverPath, solver, doPOR, onlyGal, reader.getFolder(),
-							timeout / reader.getSpec().getProperties().size(), reader.getSPN().isSafe());
+					LTSminRunner ltsRunner = new LTSminRunner(solverPath, solver, doPOR, onlyGal, timeout / reader.getSpec().getProperties().size(),
+							reader.getSPN().isSafe());
 					ltsRunner.configure(EcoreUtil.copy(reader.getSpec()), doneProps);
 					ltsRunner.setNet(reader.getSPN());
 					runners.add(ltsRunner);
@@ -491,6 +503,8 @@ public Object startNoEx(IApplicationContext context) throws Exception {
 					ReachabilitySolver.checkInInitial(reader.getHLPN(), doneProps);
 
 					SparsePetriNet skel = reader.getHLPN().skeleton();
+					skel.getProperties().removeIf(p -> ! fr.lip6.move.gal.structural.expr.Simplifier.allEnablingsAreNegated(p.getBody()));
+
 					reader.setSpn(skel,true);
 					ReachabilitySolver.checkInInitial(reader.getSPN(), doneProps);
 					new AtomicReducerSR().strongReductions(solverPath, reader, doneProps);
@@ -620,9 +634,10 @@ public Object startNoEx(IApplicationContext context) throws Exception {
 			if (onlyGal || doLTSmin) {
 				if (!reader.getSpec().getProperties().isEmpty()) {
 					System.out.println("Using solver " + solver + " to compute partial order matrices.");
-					IRunner ltsminRunner = new LTSminRunner(solverPath, solver, doPOR, onlyGal, reader.getFolder(),
-							timeout / reader.getSpec().getProperties().size(), reader.getSPN().isSafe());
+					LTSminRunner ltsminRunner = new LTSminRunner(solverPath, solver, doPOR, onlyGal, timeout / reader.getSpec().getProperties().size(),
+							reader.getSPN().isSafe());
 					ltsminRunner.configure(EcoreUtil.copy(reader.getSpec()), doneProps);
+					ltsminRunner.setNet(reader.getSPN());
 					runners.add(ltsminRunner);
 					ltsminRunner.solve(this);
 				}

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

@@ -72,4 +72,9 @@ public Boolean put(String prop, Integer value, String techniques) {
 		//
 		return super.put(prop, value, techniques);
 	}
+
+	@Override
+	public boolean isFinished() {
+		return containsKey(examination);
+	}
 }