Improving Swarming Using Genetic Algorithms
Description of this page
This page presents:
- the two benchmarks used in this paper
- the settings for the various tools we used
- the details on how to replay the benchmarks
- A comparator of results presented section 1 to 6
Note that all the content of this webpage have been archived
by Zenodo:
[here]
You can download the fork of Spot we use for our experiments [here].
You can download the logs of all the benchmarks we have
used (including DiVinE and LTSmin ones) [here].
You can download the CSV containing all our experiments for
reachability [here].
You can download the CSV containing all our experiments for
deadlock detection [here].
You can download the CSV used for figure 7 [here].
You can download the CSV used for figure 8 [here].
You can download the CSV used for figure 9 [here].
Benchmark Description
This benchmark uses 38 models extracted from the BEEM benchmark.
The table above present all the models we use. We observe that
that every type of model of the classification of Pelanek is represented.
Model | Classification | Type |
adding.6 | puzzle | toy |
anderson.3 | mutex | simple |
at.5 | mutex | simple |
bakery.6 | mutex | simple |
blocks.3 | ps | toy |
brp.6 | communication-protocol | simple |
brp2.6 | communication-protocol | simple |
cambridge.7 | communication-protocol | complex |
collision.4 | communication-protocol | simple |
elevator.4 | controller | simple |
elevator_planning.2 | ps | toy |
extinction.4 | leader-election | simple |
firewire_tree.5 | leader-election | complex |
fischer.5 | mutex | simple |
frogs.5 | puzzle | toy |
hanoi.3 | puzzle | toy |
iprotocol.6 | communication-protocol | complex |
lamport.8 | mutex | simple |
lamport_nonatomic.4 | mutex | simple |
lann.6 | mutex | simple |
leader_election.5 | leader-election | simple |
lifts.7 | controller | complex |
lup.4 | other | simple |
mcs.5 | mutex | simple |
needham.4 | other-protocol | complex |
peterson.5 | mutex | simple |
phils.5 | mutex | toy |
plc.4 | controller | complex |
production_cell.6 | controller | simple |
public_subscribe.4 | other-protocol | complex |
resistance.2 | other | simple |
rether.6 | communication-protocol | simple |
rushhour.4 | puzzle | toy |
schedule_world.2 | ps | simple |
sorter.4 | controller | simple |
synapse.7 | other-protocol | complex |
szymanski.5 | mutex | simple |
telephony.4 | other-protocol | simple |
The benchmark we use for the analysis of the performances of
existing algorithms gains a linear state-space has been built for
this purpose. It consists in a set of processes that can only
progres when they have a token. When a progress have this token,
it can progress for a certain amount of time. During this time
the other processes are frozen. At some point the token is given
to another process. This model can be considered as mutual exclusion.
Replay Benchmark
The easiest way to replay the benchmark is to fetch the Docker
from DockerHub
automatically built
from GitHub/
This Docker contain all tools and models needed to replay
the whole benchmark.
Alternatively, you may consider to install all tools by
yourself. In this case we recomand to follow each steps given in
the . Basically
four tools have to be installed: a patched version of Divine, a
for of Spot, Sylvan and LTSmin.
First of all you need to install the DiVine tool
patched by the LTSmin Team, since we rely on it to generate the
state space of each model. You just have to follow instructions
given in section 10
of [LTSmin
Homepage]. Nonetheless, this tools does not handle
out-of-bound exceptions. Since our algorithms may generate states
that are not reachable, we provided two patches to apply to this
tool to handle this
problem just apply patch1
and patch2. You
also need to
install [LTSmin]
(note that linux binaries are available). Note that these patches
are also aivalable at [here]
Download our fork of
Spot [Here]
or checkout the branch er/interpolate directly from the git
repository [Here].
Then perform the classic classic steps:
- autoreconf -vfi
- ./configure
- make
- make check
Once all previous steps have been done, you should find a
binary file modelcheck in the spot/tests/ltsmin directory. This
is the binary file we use for our experiments. (Note that if you
don't perfom the "make check" step, this binary will not be
produced. Nonetheless, you can build it using "cd tests && make
ltsmin/modelcheck").
Settings
We summarize here the options used for each tool so that you can
replay the whole benchmark:
Spot: the options swarmed-gp-dfs=fitnessfunction are the genetic
algorithm presented in the paper; swarmed-dfs is the
reachability algorithm presented in the paper. We list here
both fitness functions and options that can be combined together
- fitnessfunction=equal: this corresponds to the equality fitness
function mentionned in the paper. A state is selected iff the
number of its successors is equal to the average number of
successors in the initial population.
- fitnessfunction=lessthan: this corresponds to the lessthan fitness
function mentionned in the paper. A state is selected iff the
number of its successors is less or equal to the average number of
successors in the initial population.
- fitnessfunction=lessstrict: a state is selected iff the
number of its successors is less (strict) to the average number of
successors in the initial population.
- fitnessfunction=greaterthan: this corresponds to the greaterthan fitness
function mentionned in the paper. A state is selected iff the
number of its successors is greater or equal to the average number of
successors in the initial population.
- fitnessfunction=greaterstrict: a state is selected iff the
number of its successors is greater (strict) to the average number of
successors in the initial population.
- fitnessfunction=greaterbounded: a state is selected iff the
number of its successors is greater (strict) to the average number of
successors in the initial population.
- -I specify the size of the initial population
- -T specify the thresehold (default is 0.999)
- -G specify the number of generation we use
(default is 3)
- -P specify the size of each new generation
- -p specify the number of threads to use
Divine The options we used are the following:
- metrics for a full exploration
- -i 29 for setting the initial size of the hash
table (the same we fix for other tools)
- -w for specifying the number of threads to use
LTSmin here are the option we use for LTSmin
- dve2lts-mc --strategy=cndfs --threads=... -s 29
--perm=shift calling CNDFS algorithm
- dve2lts-mc --strategy=ufscc --threads=... -s 25
--perm=shift calling the USCC algorithm
- dve2lts-sym --lace-workers=... calling the symbolic algorithm