Merge pull request #3 from lip6/master

merging main code

.github/workflows/build.yml

@@ -39,5 +39,5 @@ jobs:
           # You should create a personal access token and store it in your repository
           token: ${{ secrets.NOTIF_PAT }}
           repo: ITS-commandline
-          owner: bnslmn
-          event_type: rebuild
+          owner: yanntm
+          event_type: rebuild

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

@@ -0,0 +1,41 @@
+package fr.lip6.move.gal.mcc.properties;
+
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Set;
+import java.util.concurrent.ConcurrentHashMap;
+
+public class ConcurrentHashDoneProperties implements DoneProperties {
+	private Map<String,Boolean> map = new ConcurrentHashMap<>();
+
+	@Override
+	public boolean containsKey(Object arg0) {
+		return map.containsKey(arg0);
+	}
+
+	@Override
+	public Set<Entry<String, Boolean>> entrySet() {
+		return map.entrySet();
+	}
+
+	@Override
+	public Boolean put(String prop, Boolean value, String techniques) {
+		return map.put(prop, value);
+	}
+
+	@Override
+	public Boolean put(String prop, Integer value, String techniques) {
+		return map.put(prop, true);
+	}
+
+	@Override
+	public Set<String> keySet() {
+		return map.keySet();
+	}
+
+	@Override
+	public int size() {
+		return map.size();
+	}
+
+}

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

@@ -0,0 +1,22 @@
+package fr.lip6.move.gal.mcc.properties;
+
+import java.util.Map.Entry;
+import java.util.Set;
+
+public interface DoneProperties {
+
+	int size();
+
+	// 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();
+
+}

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

@@ -37,16 +37,15 @@ private static Logger getLog() {
 	 * @return true if we had to introduce a special "one" place to represent constants.
 	 * @throws IOException
 	 */
-	public static boolean transform(SparsePetriNet spn, String path, Map<String, Boolean> doneProps) throws IOException {
+	public static boolean transform(SparsePetriNet spn, String path, DoneProperties doneProps) throws IOException {
 		long time = System.currentTimeMillis();
 		PrintWriter pw = new PrintWriter(new File(path));
 		pw.append("<?xml version=\"1.0\" encoding=\"utf-8\"?>\n");
 
 		pw.append("<property-set xmlns=\"http://mcc.lip6.fr/\">\n");
 		boolean usesConstants = false;
 		for (Property prop : spn.getProperties()) {
-			Boolean res = doneProps.get(prop.getName());
-			if (res == null) {
+			if (! doneProps.containsKey(prop.getName())) {
 				pw.append("  <property>\n" + 
 						"    <id>"+ prop.getName() +"</id>\n" + 
 						"    <description>Automatically generated</description>\n" + 

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

@@ -7,10 +7,12 @@ public class HLPlace {
 	int startIndex;
 	private int [] initial;
 	private boolean isConstant = false;
-	public HLPlace(String name, int start, int [] initial) {
+	private String sort;
+	public HLPlace(String name, int start, int [] initial, String sname) {
 		this.name = name;
 		this.startIndex = start;
 		this.initial = initial;
+		this.sort = sname;
 	}
 	public String getName() {
 		return name;
@@ -28,4 +30,7 @@ public boolean isConstant() {
 	public int[] getInitial() {
 		return initial;
 	}
+	public String getSort() {
+		return sort;
+	}
 }

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

@@ -123,7 +123,7 @@ public void updateEnabled (SparseIntArray state, int [] enabled, int tfired) {
 			}
 		}
 	}
-	public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikhori, List<Expression> exprs, List<Integer> repr, int timeout) {
+	public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikhori, List<Expression> exprs, List<Integer> repr, int timeout, boolean max) {
 		ThreadLocalRandom rand = ThreadLocalRandom.current();
 
 		Map<Integer, List<Integer>> repSet = computeMap(repr);		
@@ -155,11 +155,15 @@ public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikh
 				System.out.println("Interrupted Parikh walk after "+ i + "  steps, including "+nbresets+ " resets, run timeout after "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ " properties seen :" + Arrays.toString(verdicts) +(DEBUG >=1 ? (" reached state " + state):"") );
 				return verdicts;
 			}
-
-			if (! updateVerdicts(exprs, state, verdicts)) {
-				System.out.println("Finished Parikh walk after "+ i + "  steps, including "+nbresets+ " resets, run visited all " +exprs.size()+ " properties in "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ (DEBUG >=1 ? (" reached state " + state):"") );				
-				return verdicts;
+			if (!max) {
+				if (! updateVerdicts(exprs, state, verdicts)) {
+					System.out.println("Finished Parikh walk after "+ i + "  steps, including "+nbresets+ " resets, run visited all " +exprs.size()+ " properties in "+ dur +" ms. (steps per millisecond="+ (i/dur) +" )"+ (DEBUG >=1 ? (" reached state " + state):"") );				
+					return verdicts;
+				}
+			} else {
+				updateMaxVerdicts(exprs, state, verdicts);
 			}
+
 			if (list[0] == 0){
 				//System.out.println("Dead end with self loop(s) found at step " + i);
 				nbresets ++;
@@ -407,18 +411,18 @@ public int[] runRandomReachabilityDetection (long nbSteps, List<Expression> expr
 				}
 			} else {
 				// heuristically follow a successor with "Best-first search"
-				int minDist = Integer.MAX_VALUE;
+				int minDist = max ? 0 :Integer.MAX_VALUE;
 				List<Integer>  mini = new ArrayList<>();
 				List<SparseIntArray> bestSucc = new ArrayList<>();
 				for (int ti = 1 ; ti-1 < list[0] && i < nbSteps; ti++) {
 					SparseIntArray succ = fire(list[ti],state);
-					int distance = exprs.get(bestFirst).evalDistance(succ, false);
-					if (distance < minDist) {
+					int distance = exprs.get(bestFirst).evalDistance(succ, false);					
+					if ( (!max && distance < minDist) || (max && distance > minDist)) {
 						mini.clear();
 						bestSucc.clear();
 						minDist = distance;
 					}
-					if (distance <= minDist) {
+					if ((!max && distance <= minDist) || (max && distance >= minDist)) {
 						mini.add(list[ti]);
 						bestSucc.add(succ);
 					}