search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
51 stars 30 forks source link

Move remaining sequential tool functionality to multi-core tool #24

Open Meijuh opened 9 years ago

Meijuh commented 9 years ago

pins2lts-mc.c contains rudimentary support for LTS storage (full vectors) en POR (alleen stack proviso)

To eliminate the sequential tool, we have to: add the color/queue proviso in the multi-core tool distinguish state revisiting algorithms (NDFSs) and limit their combination with POR to single threaded cases only write LTSs in index format (extend PBFS with local resizing hash/tree tables and transition communication) Th SCC algorithm will be lost, but more efficient versions are available for the multi-core tool in a local branch

Meijuh commented 6 years ago

using BDDs as state storage is also not supported in the mc backend, what else?

alaarman commented 6 years ago

This functionality (BDD storage) is superseded by the -sym tool.

alaarman commented 6 years ago

The POR / proviso combinations have by now all been implemented in the Multi-core tool. I do not know what the index file format is needed.

The -seq backend can be removed in my opinion, but @jacopol might not agree anymore.