Improving Swarming Using Genetic Algorithms

Description of this page

This page presents:

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.

ModelClassificationType
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:

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
  • Divine The options we used are the following:
  • LTSmin here are the option we use for LTSmin