Benchmarking struct (Work in progress)

At InvariantPerformance a benchmark is proposed for testing and comparing invariant calculation by a number of tools, including GreatSPN (gspn), ItsTools, PetriSpot and TINA.struct (with and without the 4ti2 option);

As often in such studies, the choices made among the many available options may be non optimal for some tools, understandably. The study is nethertheless useful as a starting point; many thanks to the authors. We present in this page a revised set of comparisons after fixing some minor issues with the test scripts, tuning parameter choices for TINA.struct, and finally taking advantage of recent improvements of tool struct, prompted by this benchmark.

More precisely:

• A bad interpretation of some struct results ("no flows" wrongly interpreted as a failure instead of "0 flows") is fixed;

• The default TINA.struct options are suitable for teaching purposes but are suboptimal for the large models found in the benchmark; we use instead more suitable options;

• The benchmark has a bias towards large models: The set of petri net models used, taken from those of the MCC includes a proportionally large number of large models (with up to 153 000 nodes) while struct was primarilly intended for more commonly sized models (say with no more than 1000 nodes). Also, neither TINA.struct nor the external 4ti2 tool it may use are optimized for sparse incidence matrices, contrarilly to gspn, Its and PetriSpot tools. A "per model size"; presentation of the results shows results for more typical use case sizes as well;

• While gspn computes the same invariants as TINA.struct, neither PetriSpot nor Its do. The latter two preprocess the incidence matrix of the net to remove most redundant rows or columns (depending if computing place or transition invariants), with the effects of producing invariants of smaller dimensions than |P| or |T|; This obviously prevents fair comparisons with the other tools;

• Finally, we took this opportunity to refresh the code of the struct tool, written about twenty years ago. Without significantly changing the algorithms used, memory usage was optimized at a number of places, resulting in better performances on large models.

To reproduce the results below, proceed as explained in InvariantPerformance but use the scripts run.sh and logs2csv.pl below instead of those provided there:

• run.sh
• logs2csv.pl

Then, to compute the table below, call script reports.sh in folder logs; this produces several markdown files, including file report-c.md, from which the table below is extracted.

Notes: in the tables below:

• the size of a net is the max integer among its |T| and |P|.

• failures are dispatched into:

  • time: cpu time larger than 120s limit;
  • ovf: integer overflow;
  • mem: memory occupation larger than 16Gb limit;
  • unk: unknown (unexpected by the logs2csv script) reason.

sizes in ]0,1000]

sizes in ]0,2000]

sizes in ]0,5000]

sizes in ]0,10000]

sizes in ]0,20000]

sizes in ]0,50000]

sizes in ]0,max]

For benchmarkings semiflow computations instead of flows, use instead scripts (in progress):

• run-semiflows.sh
• logs2csv-semiflows.pl

Computing semiflows is more expensive than computing flows; the current results are:

sizes in ]0,1000]

sizes in ]0,2000]

sizes in ]0,5000]

sizes in ]0,10000]

sizes in ]0,20000]

sizes in ]0,50000]

sizes in ]0,max]

As for flows, GreatSPN and TINA.struct compute the same semiflows ("by the book"), while PetriSpot computes semiflows after a reduction pass removing most redundant places or transitions.