Implements better reduced functions for partial order reductions
[Read all the issue before anything else, there may be some interesting tips]
Currently, branch er/por-next implements partial order reduction for an on-the-fly exploration of the model. Thus, the following work must be done on a branch with er/por-next as upstream since er/por-next is not yet merged in next.
Preliminary work:
-
You must install the divine tool patched by the LTSmin team. You just have to follow the instructions that are in tests/ltsmin/README
Only install divine for now, you may want to install Spins later. Note: If you use MacOSX you may have some troubles with Flags, just ask for help. -
You must download divine models from http://paradise.fi.muni.cz/beem/
or the subset from our ATVA'16 paperhttps://www.lrde.epita.fr/~renault/benchs/ATVA-2016/REF.tgz
. Note that you can also have a look to our benchmarkhttps://www.lrde.epita.fr/~renault/benchs/ATVA-2016/results.html
to have an idea of what is a consistent benchmark. -
Ensure that divine is correctly installed in you PATH. Running make check
should now execute (some of) the tests fromtests/ltsmin
directory. Moreover, now runningdivine compile --ltsmin model.dve
should produce two files :model.dve.cpp
andmodel.dve2C
. The first file is the translation frommodel.dve
to language C: please open this file to have a look, you will see that there is no magic trick. The second file is only a shared library.
Warmup:
Have a look to spot/ltsmin/porinfos.hh
and spot/ltsmin/porinfos.cc
. These files provide all informations required
when performing partial order reductions. Have a look to the compute_reduced_set
function: it compute a reduced set
of successors (as described page 21 of pater.11.misc.pdf). This function takes two arguments enabled
and for_spins_state
.
-
for_spins_state
: represents is the state for which we want to compute a reduced set of successor -
enabled
: represents the id of all the outgoing transitions from this state
The goal of compute_reduced_set
is to return a boolean vector indicating, for each transition in enable
, wether
this transition belongs to the reduced set or not.
Todo:
-
Implements the stubborn_set_ns
as page 27 of pater.11.misc.pdf. Note that this algorithm may use information computed by divine but not imported by spot. Just import them in theltsmin.cc
file. -
Allows compute_reduced_set
to dispatch on your reduced set or the one already implemented in spot. The tooltests/ltsmin/modelcheck
should be able to choose one of the algorithm from the command line. Note thatmodelcheck
is quite ugly for now, we have to work on that... -
Test your algorithm. To do that cd tests && make ltsmin/modelcheck && ./ltsmin/modelcheck -sm -por=source model.dve 'true'
. At this point we should discuss but you can use the benchmark of ATVA'16 to compare relative performances. Note: do not choose-por=none
or-por=full
since you will probably not see any impact. -
Improve efficiency of your algorithm by avoiding multiple redundant computations. Keep your original algorithm so that you will be able to compare the relative performances.
Note, step 2 may implies that you have a look to :
-
spot/ltsmin/proviso.hh
which presents a lot of provisos as described in our ATVA'16 paper. -
spot/ltsmin/dfs_stats.hh
allows a (parametric) exploration of the state space. -
spot/ltsmin/dfs_inspector.hh
a kind of wrapper
Don't be afraid! :) AFAIK is just (ugly) c++. When you reach this particular point just ask for help I will explain you things that are related to steps 2 and 3.
Going further:
-
page 14 of pater.11.misc.pdf talk about persistent set. They are the first technique of partial order reductions. Implement them an compare -
File at https://wwwhome.ewi.utwente.nl/~laarman/papers/guard_por_journal.pdf
seems to be a journal version of Pater's work. In this paper new heuristics seems to be proposed. Adapt them and compare. By the way, this paper is shorter than pater master thesis, but may be more clear (from the mathematical point of view). Depending on your affinities you may prefer to read one or the other.