Skip to content

Commit 398c3ea

Browse files
committed
Wrapper for PetriSpot. Still WIP
1 parent 3d0fb2d commit 398c3ea

16 files changed

Lines changed: 753 additions & 0 deletions

File tree

fr.lip6.move.gal.parent/pom.xml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,10 @@
100100
<module>../ltl/fr.lip6.ltl.jhoaf</module>
101101
<module>../ltl/fr.lip6.ltl.tgba</module>
102102

103+
<!-- PetriSpot : Petri net invariants solver -->
104+
<module>../petrispot/fr.lip6.petrispot.binaries</module>
105+
<module>../petrispot/fr.lip6.move.petrispot.runner</module>
106+
103107
<!-- LTSmin interactions : launching and configuration -->
104108
<module>../ltsmin/fr.lip6.move.gal.ltsmin.preference</module>
105109
<module>../ltsmin/fr.lip6.move.gal.ltsmin.binaries</module>
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<classpath>
3+
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-21"/>
4+
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
5+
<classpathentry kind="src" path="src"/>
6+
<classpathentry kind="output" path="target/classes"/>
7+
</classpath>
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/target/
Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<projectDescription>
3+
<name>fr.lip6.move.petrispot.runner</name>
4+
<comment></comment>
5+
<projects>
6+
</projects>
7+
<buildSpec>
8+
<buildCommand>
9+
<name>org.eclipse.jdt.core.javabuilder</name>
10+
<arguments>
11+
</arguments>
12+
</buildCommand>
13+
<buildCommand>
14+
<name>org.eclipse.pde.ManifestBuilder</name>
15+
<arguments>
16+
</arguments>
17+
</buildCommand>
18+
<buildCommand>
19+
<name>org.eclipse.pde.SchemaBuilder</name>
20+
<arguments>
21+
</arguments>
22+
</buildCommand>
23+
<buildCommand>
24+
<name>org.eclipse.m2e.core.maven2Builder</name>
25+
<arguments>
26+
</arguments>
27+
</buildCommand>
28+
</buildSpec>
29+
<natures>
30+
<nature>org.eclipse.m2e.core.maven2Nature</nature>
31+
<nature>org.eclipse.pde.PluginNature</nature>
32+
<nature>org.eclipse.jdt.core.javanature</nature>
33+
</natures>
34+
</projectDescription>
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
eclipse.preferences.version=1
2+
encoding/<project>=UTF-8
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
activeProfiles=
2+
eclipse.preferences.version=1
3+
resolveWorkspaceProjects=true
4+
version=1
Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
# KERS — Kernel/Elimination Result Sparse format
2+
3+
KERS is a compact binary format for sparse integer matrices.
4+
It is used by PetriSpot both for **input** (incidence matrices) and **output** (invariant bases),
5+
enabling efficient program-to-program transfer without going through PNML or ASCII representations.
6+
7+
## Design goals
8+
9+
- Single format for input and output: the caller reads the result the same way it wrote the input.
10+
- Suitable for large models: 10⁵ × 10⁵ matrices with millions of non-zeros load in milliseconds.
11+
- No external dependencies: plain binary, no compression, no serialisation library.
12+
- Self-describing dimensions: a reader can allocate correctly before parsing any entries.
13+
14+
## File structure
15+
16+
All multi-byte integers are **little-endian**.
17+
18+
### Header (16 bytes)
19+
20+
| Offset | Size | Type | Description |
21+
|--------|------|--------|------------------------------------|
22+
| 0 | 4 | char[4]| Magic: `K` `E` `R` `S` (0x4B 0x45 0x52 0x53) |
23+
| 4 | 1 | uint8 | Version: `1` |
24+
| 5 | 1 | uint8 | Flags: reserved, must be `0` |
25+
| 6 | 4 | uint32 | `nrows` — number of rows |
26+
| 10 | 4 | uint32 | `ncols` — number of columns |
27+
| 14 | 2 || Padding (zero) |
28+
29+
### Body — column entries
30+
31+
Only non-empty columns are written, in **ascending column order**.
32+
33+
For each non-empty column:
34+
35+
| Size | Type | Description |
36+
|------|--------|------------------------------------------|
37+
| 4 | uint32 | Column index (0-based) |
38+
| 4 | uint32 | `nnz` — number of non-zero entries in this column |
39+
| 4×nnz | uint32 | Row index (0-based, repeated nnz times as `(row, value)` pairs — see below) |
40+
41+
Each entry is a `(row_index, value)` pair:
42+
43+
| Size | Type | Description |
44+
|------|--------|-------------------|
45+
| 4 | uint32 | Row index (0-based)|
46+
| 8 | int64 | Value (signed) |
47+
48+
Row indices within a column are **sorted in ascending order**.
49+
This allows readers to use `append()` (amortised O(1)) rather than `put()` (O(log n)).
50+
51+
### Terminator
52+
53+
After the last column, a 4-byte sentinel marks end of data:
54+
55+
| Size | Type | Value |
56+
|------|--------|--------------|
57+
| 4 | uint32 | `0xFFFFFFFF` |
58+
59+
## Semantic conventions
60+
61+
### Input matrix (incidence matrix)
62+
63+
When used as input to PetriSpot via `--loadKERS`:
64+
65+
- `nrows` = number of **variables** (places for P-flows, transitions for T-flows)
66+
- `ncols` = number of **constraints** (transitions for P-flows, places for T-flows)
67+
- The matrix is the **incidence matrix** C = flowTP − flowPT
68+
- For T-flows/T-semiflows, pass the same C; PetriSpot transposes internally
69+
70+
### Output matrix (invariant basis)
71+
72+
When written by PetriSpot via `--basisKERS`:
73+
74+
- `nrows` = number of variables (same as input)
75+
- `ncols` = number of basis vectors (invariants)
76+
- Each column is one basis vector: a sparse integer vector in the null space of C
77+
78+
No constant terms are stored (constants depend on the initial marking and are not part of the basis).
79+
80+
## Usage with PetriSpot
81+
82+
```
83+
# Export incidence matrix of a Petri net in KERS format
84+
petri64 -i model.pnml --exportAsKERS=model.kers
85+
86+
# Compute P-semiflows from a KERS matrix, export result as KERS
87+
petri64 --loadKERS=model.kers --Psemiflows --basisKERS=basis.kers
88+
89+
# Equivalent: compute directly from PNML, export basis
90+
petri64 -i model.pnml --Psemiflows --basisKERS=basis.kers
91+
```
92+
93+
## kersconv — ASCII conversion utility
94+
95+
`kersconv` is a small companion tool for inspecting and constructing KERS files without PetriSpot.
96+
It is built alongside the `petri*` binaries by the autoconf/automake build system.
97+
98+
### Usage
99+
100+
```
101+
kersconv --decode <input.kers> [output.txt] # KERS binary → ASCII (stdout if no output file)
102+
kersconv --encode <input.txt> <output.kers> # ASCII → KERS binary
103+
```
104+
105+
### ASCII format
106+
107+
The text representation is the same as `--exportAsMatrix`:
108+
109+
```
110+
<nrows> <ncols>
111+
<rowIdx> <colIdx>:<val> <colIdx>:<val> ...
112+
...
113+
```
114+
115+
- First line: matrix dimensions.
116+
- Each subsequent line encodes one **non-empty row**: the row index followed by space-separated `colIdx:value` pairs.
117+
- Empty rows are omitted.
118+
- Values are signed integers.
119+
120+
### Example
121+
122+
```sh
123+
# Inspect a basis file
124+
kersconv --decode basis.kers
125+
126+
# Roundtrip: decode then re-encode
127+
kersconv --decode basis.kers basis.txt
128+
kersconv --encode basis.txt basis2.kers
129+
```
130+
131+
### Consistency with PNML-based output
132+
133+
When comparing `--loadKERS` output to direct PNML computation, the invariant **coefficients and
134+
count are identical**. The following differences are expected and by design:
135+
136+
| Property | PNML path | KERS path |
137+
|---|---|---|
138+
| Variable names | Real place/transition names from PNML | `x0`, `x1`, … (no name table in binary format) |
139+
| RHS constant | Dot product with initial marking (e.g., `= 1`) | Always `0` (no marking stored in KERS) |
140+
| Log lines | Includes parsing and model info | Only computation lines |
141+
| "Computed" line | `Computed N P flows in T ms.` | `Computed N P flows in T ms.` (same) |
142+
143+
For pure **flows** (as opposed to semiflows), `= 0` on the RHS is mathematically correct regardless.
144+
For **semiflows**, the PNML path annotates each invariant with the conserved quantity value
145+
(the invariant dotted with the initial marking), which is unavailable in the KERS path.
146+
147+
## Size estimate
148+
149+
For a matrix with `N` non-zero entries:
150+
- Header: 16 bytes
151+
- Per non-empty column header: 8 bytes
152+
- Per entry: 12 bytes (4 row + 8 value)
153+
- Terminator: 4 bytes
154+
155+
Total ≈ 16 + 8×ncols_nonempty + 12×N bytes.
156+
157+
For N = 10⁶ entries: approximately **12 MB**.
158+
159+
## Overflow behaviour
160+
161+
PetriSpot ships three binaries: `petri32` (int), `petri64` (long), `petri128` (long long).
162+
All three read and write values as `int64` in the file.
163+
When reading into a narrower type (e.g. `petri32`), values outside `[-2³¹, 2³¹-1]` trigger
164+
a warning on stderr and are truncated. Use `petri64` or `petri128` for large coefficients.
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
Manifest-Version: 1.0
2+
Bundle-ManifestVersion: 2
3+
Bundle-Name: PetriSpot Runner
4+
Bundle-SymbolicName: fr.lip6.move.petrispot.runner;singleton:=true
5+
Bundle-Version: 1.0.0.qualifier
6+
Bundle-RequiredExecutionEnvironment: JavaSE-21
7+
Bundle-Vendor: LIP6
8+
Require-Bundle: fr.lip6.move.gal.structural;bundle-version="1.0.0",
9+
fr.lip6.move.gal.process;bundle-version="1.0.0",
10+
fr.lip6.petrispot.binaries;bundle-version="1.0.0"
11+
Export-Package: fr.lip6.move.petrispot.runner

0 commit comments

Comments
 (0)