Jeroen Meijer
Jeroen Meijer
(any) is represented using a reserved value that could collide with a state slot Additionally, negative integers can be printed into an ETF but not parsed again
Add a function to the PINS interface that pretty prints all types (also non-enum) in the model. This allows the printing of state and transition labels according to the frontend...
Add a base text to ltsmin-standards.h
Subsumption can reduce the number of groups, which can be beneficial for partial order reduction. However, the regrouping is only loaded after the POR layer. This should be reversed and...
Currently the ETF format does not support read, write and copy dependencies. Furthermore guards should also be stored explicitly in the ETF file.
Currently pins2lts-sym can only store and load the transition relation from a file. Guards should also be stored and loaded. E.g. the vector sets `guard_false` and `guard_true` should be loaded...
The current allocator in the multi-process environment (--procs=P) is a hack. It claims a large piece of anonymous pages using mmap at pre-fork time. Memory allocations are handled by giving...
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...
For easy inspection of state spaces it would be useful to have dot output. Example code can be found in pins2lts-seq. If implemented in IO-lib, the output format will be...