support not having a por

lip6 · May 3, 2024 · 2f5a149 · 2f5a149
1 parent 3a20832
commit 2f5a149
Showing 1 changed file with 12 additions and 1 deletion.
diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java
@@ -29,6 +29,10 @@ public RandomExplorer(ISparsePetriNet sr) {
 	private int[] computeEnabled(SparseIntArray state) {
 		return wu.computeEnabled(state);
 	}
+
+	public ISparsePetriNet getNet() {
+		return wu.getNet();
+	}
 
 	public int[] runGuidedReachabilityDetection(long nbSteps, SparseIntArray parikhori, SparseIntArray porori,
 			List<Expression> exprs, List<Integer> repr, int timeout, boolean max) {
@@ -37,7 +41,8 @@ public int[] runGuidedReachabilityDetection(long nbSteps, SparseIntArray parikho
 		Map<Integer, List<Integer>> repSet = InvariantCalculator.computeMap(repr);
 		SparseIntArray parikh = InvariantCalculator.transformParikh(parikhori, repSet);
 		parikhori = parikh.clone();
-		int[] por = InvariantCalculator.transformParikh(porori, repSet).toArray(wu.getNet().getTransitionCount());
+		int[] por = null;
+		if (porori != null) por = InvariantCalculator.transformParikh(porori, repSet).toArray(wu.getNet().getTransitionCount());
 
 		long time = System.currentTimeMillis();
 		SparseIntArray state = wu.getInitial();
@@ -55,6 +60,9 @@ public int[] runGuidedReachabilityDetection(long nbSteps, SparseIntArray parikho
 
 		// mode : 0 = RAND, 1 = MAX, 2 = MIN
 		int mode = 0;
+		if (porori == null) {
+			mode = 1;
+		}
 
 		if (list[0] == 0) {
 			if (DEBUG >= 1) {
@@ -93,6 +101,9 @@ public int[] runGuidedReachabilityDetection(long nbSteps, SparseIntArray parikho
 				list = initlist.clone();
 				parikh = parikhori.clone();
 				mode = (mode + 1) % 4;
+				if (porori == null && mode == 0) {
+					mode++;
+				}
 				continue;
 			}