Improving Swarming Using Genetic Algorithms
| Main Author: | Etienne Renault |
|---|---|
| Format: | info software |
| Terbitan: |
, 2020
|
| Online Access: |
https://zenodo.org/record/3707234 |
Daftar Isi:
- This archive contains the necessary command to setup a docker environment used for the benchmark. This archive was generated automatically from this GitHub repository and is also publicly available in DockerHub (with updates every time the GitHub repository changes). The docker provides: The version of spot used for the benchmark The (doubly) patched version of divine used to check bounds The latest version of sylvan so that we can use latest saturation techniques The latest version of LTSmin patched to work with the latest sylvan version All the models we used for the benchmark. When running the docker, all tools have been automatically installed. You can replay a specific run against a given model (available in the directory model) by running For Spot algorithms - modelcheck -p <nb_th> --swarmed-dfs -m <model_name> : the SOTA parallel DFS (swarming) - modelcheck -p <nb_th> --swarmed-gp-dfs=lessthan -m <model_name> : The GP DFS presented in the paper - modelcheck -p <nb_th> --swarmed-gp-deadlock=lessthan -m <model_name> : The deadlock GP DFS presented in the paper Note that: - nb_th **must be strictly** greater than 1 for swarmed-gp* algorithms - option -x 0.7 spaws 0.7 percent of threads with the GP strategy - option -I 1000 sets the initial population to 100 - option -P 50 sets the size of each new population - option -T 0.999 sets the threshold for mutations to 0.999 - more options are available, see --help For LTSMIN algorithms - dve2lts-sym --saturation=sat --order=bfs-prev --lace-workers=<nb_th> -rf <model_name>: The symbolic algorithm of LTSmin (settings fixed with LTSmin team) - dve2lts-mc --perm=shift --threads=<nb_th> <model_name> : The explicit algorithm (settings fixed with LTSmin team)