Skip to content

Commit eeee649

Browse files
yanntmyanntm
committed
progress wrapper and use KERS v2
1 parent 5d606bb commit eeee649

2 files changed

Lines changed: 61 additions & 54 deletions

File tree

‎petrispot/fr.lip6.move.petrispot.runner/src/fr/lip6/move/petrispot/runner/KERSFormatIO.java‎

Lines changed: 22 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,12 @@ public static void write(IntMatrixCol matrix, DataOutputStream out) throws IOExc
9090
if (nnz == 0) continue;
9191
writeIntLE(out, ci);
9292
writeIntLE(out, nnz);
93+
// Contiguous row indices block
94+
for (int i = 0; i < nnz; i++) {
95+
writeIntLE(out, col.keyAt(i));
96+
}
97+
// Contiguous values block
9398
for (int i = 0; i < nnz; i++) {
94-
writeIntLE(out, col.keyAt(i));
9599
writeLongLE(out, (long) col.valueAt(i));
96100
}
97101
}
@@ -129,20 +133,30 @@ public static IntMatrixCol read(DataInputStream in) throws IOException {
129133

130134
// Stream column entries until sentinel 0xFFFFFFFF (== -1 as signed int)
131135
int colIdx;
136+
int[] rowBuf = new int[0];
137+
long[] valBuf = new long[0];
138+
132139
while ((colIdx = readIntLE(in)) != -1) {
133140
int nnz = readIntLE(in);
141+
// Grow scratch buffers only when needed
142+
if (nnz > rowBuf.length) {
143+
rowBuf = new int[nnz];
144+
valBuf = new long[nnz];
145+
}
146+
// Read contiguous row-indices block, then contiguous values block
147+
for (int i = 0; i < nnz; i++) rowBuf[i] = readIntLE(in);
148+
for (int i = 0; i < nnz; i++) valBuf[i] = readLongLE(in);
149+
134150
// Pre-allocate exactly nnz slots — avoids all GrowingArrayUtils resizing
135151
SparseIntArray col = new SparseIntArray(nnz);
136152
for (int i = 0; i < nnz; i++) {
137-
int row = readIntLE(in);
138-
long val = readLongLE(in);
139-
int ival = (int) val;
140-
if (ival != val) {
141-
log.warning("KERS value " + val + " at col=" + colIdx
142-
+ " row=" + row + " overflows int; truncated.");
153+
int ival = (int) valBuf[i];
154+
if (ival != valBuf[i]) {
155+
log.warning("KERS value " + valBuf[i] + " at col=" + colIdx
156+
+ " row=" + rowBuf[i] + " overflows int; truncated.");
143157
}
144158
// Row indices sorted ascending in file: append is O(1) — no binary search
145-
col.append(row, ival);
159+
col.append(rowBuf[i], ival);
146160
}
147161
// Replace the empty column allocated by IntMatrixCol constructor
148162
matrix.setColumn(colIdx, col);

‎petrispot/fr.lip6.move.petrispot.runner/src/fr/lip6/move/petrispot/runner/PetriSpotRunner.java‎

Lines changed: 39 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
11
package fr.lip6.move.petrispot.runner;
22

3+
import java.io.File;
34
import java.io.IOException;
45
import java.nio.file.Files;
5-
import java.nio.file.Path;
6+
import java.util.ArrayList;
7+
import java.util.List;
68
import java.util.concurrent.TimeoutException;
79
import java.util.logging.Logger;
810

@@ -21,13 +23,16 @@
2123
* <li>Write it to a temporary KERS file.</li>
2224
* <li>Invoke petri64 with the appropriate mode flag.</li>
2325
* <li>Read the output KERS file and return the result matrix.</li>
24-
* <li>Clean up temporary files.</li>
26+
* <li>Clean up temporary files (unless DEBUG &gt;= 1).</li>
2527
* </ol>
2628
*/
2729
public class PetriSpotRunner {
2830

2931
private static final Logger log = Logger.getLogger("fr.lip6.move.gal");
3032

33+
/** Set to 1 to keep intermediate files for inspection; 2 for extra verbose output. */
34+
private static final int DEBUG = 0;
35+
3136
/** Default timeout in seconds for the PetriSpot binary. */
3237
private static final long DEFAULT_TIMEOUT_S = 120;
3338

@@ -54,65 +59,61 @@ public enum InvariantMode {
5459
* @return the result matrix (columns = invariants/flows), or {@code null} on failure
5560
*/
5661
public static IntMatrixCol computeInvariants(SparsePetriNet spn, InvariantMode mode, long timeout) {
57-
// Step 1 – build incidence matrix: effect = post - pre = -1*flowPT + 1*flowTP
58-
IntMatrixCol incidence = IntMatrixCol.sumProd(-1, spn.getFlowPT(), 1, spn.getFlowTP());
59-
60-
Path workDir = null;
62+
List<File> todel = new ArrayList<>();
63+
// Default: empty matrix — safe for all callers (means "no invariants found")
64+
IntMatrixCol result = new IntMatrixCol(0, 0);
6165
try {
66+
// Step 1 – build incidence matrix: effect = post - pre = -1*flowPT + 1*flowTP
67+
IntMatrixCol incidence = IntMatrixCol.sumProd(-1, spn.getFlowPT(), 1, spn.getFlowTP());
68+
6269
// Step 2 – write incidence matrix to a temp KERS file
63-
workDir = Files.createTempDirectory("petrispot-");
64-
Path inputKers = workDir.resolve("input.kers");
65-
Path outputKers = workDir.resolve("output.kers");
70+
File inputKers = Files.createTempFile("petrispot-input-", ".kers").toFile();
71+
File outputKers = Files.createTempFile("petrispot-output-", ".kers").toFile();
72+
todel.add(inputKers);
73+
todel.add(outputKers);
6674

67-
KERSFormatIO.write(incidence, inputKers);
75+
KERSFormatIO.write(incidence, inputKers.toPath());
6876

6977
// Step 3 – build command line
7078
String binaryPath = BinaryToolsPlugin.getPetriURI().getPath();
7179
CommandLine cl = new CommandLine();
7280
cl.addArg(binaryPath);
73-
cl.addArg("--loadKERS=" + inputKers.toAbsolutePath());
81+
cl.addArg("--loadKERS=" + inputKers.getCanonicalPath());
7482
cl.addArg(modeFlag(mode));
75-
cl.addArg("--basisKERS=" + outputKers.toAbsolutePath());
76-
cl.setWorkingDir(workDir.toFile());
83+
cl.addArg("--basisKERS=" + outputKers.getCanonicalPath());
7784

78-
log.info("Invoking PetriSpot: " + cl);
85+
System.out.println("Running PetriSpot : " + cl);
7986
long t0 = System.currentTimeMillis();
8087

8188
// Step 4 – invoke and monitor
8289
int exitCode = Runner.runTool(timeout, cl);
83-
log.info("PetriSpot finished in " + (System.currentTimeMillis() - t0) + " ms, exit=" + exitCode);
8490

8591
if (exitCode != 0) {
86-
log.warning("PetriSpot returned non-zero exit code " + exitCode + " for mode " + mode);
87-
return null;
92+
System.out.println("PetriSpot run failed in " + (System.currentTimeMillis() - t0)
93+
+ " ms. Status: " + exitCode);
94+
} else if (!outputKers.exists() || outputKers.length() == 0) {
95+
System.out.println("PetriSpot produced no output file for mode " + mode);
96+
} else {
97+
// Step 5 – parse result
98+
if (DEBUG >= 1) System.out.println("Successful run of PetriSpot took "
99+
+ (System.currentTimeMillis() - t0) + " ms. Input: "
100+
+ inputKers.getCanonicalPath() + " Output: " + outputKers.getCanonicalPath());
101+
result = KERSFormatIO.read(outputKers.toPath());
102+
if (DEBUG >= 2) System.out.println("PetriSpot result matrix: " + result);
88103
}
89-
90-
if (!Files.exists(outputKers)) {
91-
log.warning("PetriSpot produced no output file for mode " + mode);
92-
return null;
93-
}
94-
95-
// Step 5 – parse result
96-
return KERSFormatIO.read(outputKers);
97-
98104
} catch (TimeoutException e) {
99-
log.warning("PetriSpot timed out after " + timeout + " s (" + mode + ")");
100-
return null;
105+
System.out.println("PetriSpot timed out after " + timeout + " s (" + mode + ")");
101106
} catch (InterruptedException e) {
102107
Thread.currentThread().interrupt();
103-
log.warning("PetriSpot invocation interrupted (" + mode + ")");
104-
return null;
108+
System.out.println("PetriSpot invocation interrupted (" + mode + ")");
105109
} catch (IOException e) {
106-
log.warning("PetriSpot I/O error (" + mode + "): " + e.getMessage());
107-
return null;
110+
System.out.println("PetriSpot I/O error (" + mode + "): " + e.getMessage());
108111
} finally {
109-
// Step 6 – cleanup
110-
if (workDir != null) {
111-
deleteQuietly(workDir.resolve("input.kers"));
112-
deleteQuietly(workDir.resolve("output.kers"));
113-
deleteQuietly(workDir);
114-
}
112+
if (DEBUG == 0)
113+
for (File f : todel)
114+
f.delete();
115115
}
116+
return result;
116117
}
117118

118119
/**
@@ -137,12 +138,4 @@ private static String modeFlag(InvariantMode mode) {
137138
default: throw new IllegalArgumentException("Unknown mode: " + mode);
138139
}
139140
}
140-
141-
private static void deleteQuietly(Path p) {
142-
try {
143-
Files.deleteIfExists(p);
144-
} catch (IOException e) {
145-
// best-effort cleanup
146-
}
147-
}
148141
}

0 commit comments

Comments
 (0)