SATAF/PresTAF libraries¶
Description¶
SATAF is a library implementing Shared Automata. This data-structure has been proposed by J.-M. Couvreur in [ 1 ]. The prototype of J.-M. Couvreur, called PresTAF (written in Java), has been rewritten using the C language and splitted into two libraries:- SATAF that is the core implementation of the shared-automata data-structure;
- and PresTAF that is an implementation of a Presburger solver/synthesizer based on shared-automata.
- FAST the model-checker based on acceleration techniques developed by J. Leroux [ 2 ] ;
- and Alambic, the solver for the Armoise language.
PresTAF is the very first tool that is able to synthesize [ 3 ] a Presburger formula (using the Armoise high-level language) from a binary automaton.
Documentations about the programming interfaces of these libraries can be found following these links: SATAF and PresTAF.
Downloads¶
You can download these libraries from the Download area. The last stable release of these libraries are :
SATAF 1.4 and PresTAF 1.6
Source code is also available via our version control system (GIT):
- Using the HTTP protocol, sources are freely available for read only access:
git clone http://altarica.labri.fr/git/sataf.git
git clone http://altarica.labri.fr/git/prestaf.git - Using a SSH authorized access, the repository is accessible for read and write synchronizations:
git clone git@altarica.labri.fr:sataf.git
git clone git@altarica.labri.fr:prestaf.git
In order to use SATAF and PresTAF libraries you will need to install CCL.
Benchmarks¶
As written above, the PresTAF library comes with a GENEPI plugin. Using this plugin we have submitted the PresTAF solver to two kinds benchmarks:- First we compare performances of our plugin to others using FASTer and distiller.
- Second we measure performances of the Presburger formula synthesizer (see TaPAS).
Below we give two tables that gather the results of the formula synthesizer used on automata obtained by two different kinds of computation:
- In the first case, automata are computed from an Armoise formula.
- In the second case, automata are obtained with FASTer after a long sequence of operations that corresponds to the computation of a fixpoint a state space.
Each process (distiller or FASTer) was allocated a budget of 4.5 GB and 5 minutes of CPU times. ERR indicates an abnormal termination of the program due to the consumption of its memory or time limit. The benchmarks was executed on a 64 bits machine equipped with an Intel® Xeon® 2.33 GHz CPU and 8 GB of memory. CPU Execution times are expressed in seconds and were computed with the time command of the bash shell.
- file is the input file. Files used for the benchmark are distributed within the packages of distiller or FASTer;
- formula size in nodes is the number of nodes of the syntactic tree encoding the generated formula;
- formula size in chars is the size of file generated for the formula;
- automata size is the number of states4 of the shared-automaton used for the computation;
- total time is the total amount of time until termination of the process;
- synthesis time is the time passed to synthesis the formula.
PresTAF plugin used to solve Armoise formulas¶
| File | formula size in nodes | formula size in chars | automata size | total time | synthesis time |
| bench-01 | 63 | 344 | 4620 | 10.16 | 10.01 |
| bench-02 | 155 | 628 | 147378 | 8.23 | 7.25 |
| bench-03 | 6893 | 29060 | 10158 | 10.13 | 9.86 |
| bench-04 | 44 | 304 | 51135 | 2.08 | 1.68 |
| bench-05 | 67 | 364 | 2715 | 22.58 | 20.93 |
| bench-06 | 248 | 910 | 16530 | 1.91 | 0.35 |
| bench-07 | 372 | 1710 | 4320 | 1.84 | 1.6 |
| bench-08 | 75 | 396 | 33335 | 2.13 | 1.15 |
| bench-09 | 71 | 392 | 63154 | 2.42 | 1.97 |
| bench-10 | 48 | 295 | 315 | 0.23 | 0.06 |
| bench-11 | 17 | 200 | 3 | 0.19 | 0 |
| bench-12 | 85 | 478 | 9 | 0.19 | 0 |
| bench-13 | 40 | 282 | 946 | 0.31 | 0.13 |
| bench-14 | 225 | 1029 | 1024 | 0.85 | 0.65 |
PresTAF plugin used to compute reachable sets of states with FASTer¶
| File | formula size in nodes | formula size in chars | automata size | total time | synthesis time |
| barber | 365 | 1600 | 36 | 0.36 | 0 |
| berkeley | 239 | 1189 | 29 | 0.24 | 0 |
| BoigelotLegayWolperCAV03.without_strategy | 369 | 1327 | 523 | 25.50 | 0.03 |
| BoigelotLegayWolperCAV03.with_strategy | 369 | 1327 | 523 | 6.06 | 0.03 |
| canibals_v2 | ERR | ||||
| centralserver | 793 | 3167 | 75 | 2.52 | 0.01 |
| consistency | 719 | 2949 | 90 | 71.51 | 0.03 |
| consistencyInv | 3380 | 12503 | 205 | 0.69 | 0.25 |
| consprod | 4679 | 17548 | 353 | 2.48 | 0.01 |
| consprodjava | 12895 | 48470 | 1967 | 16.16 | 2.38 |
| consprodjavaN | 12895 | 48470 | 1967 | 16.12 | 2.38 |
| consprodjavaNInv | 6222 | 22100 | 308 | 2.97 | 0.41 |
| csm | 721 | 2812 | 66 | 4.67 | 0.02 |
| csmInv | 3813 | 13901 | 140 | 0.73 | 0.03 |
| dekker | 2767 | 10053 | 200 | 4.22 | 0.01 |
| DRAGON | 258 | 1224 | 23 | 0.35 | 0 |
| efm | 195 | 936 | 26 | 0.33 | 0 |
| FIREFLY | 226 | 1116 | 28 | 0.25 | 0 |
| fms | 12173 | 43804 | 528 | 14.03 | 1.52 |
| fmsInv | 12173 | 43804 | 528 | 13.82 | 1.32 |
| futurbus | 798 | 3369 | 106 | 0.52 | 0.03 |
| gb | ERR | ||||
| ILLINOIS | 201 | 985 | 22 | 0.30 | 0 |
| incdec | ERR | ||||
| incdecInv | 26232 | 88914 | 1047 | 60.14 | 19.33 |
| kanban | 483 | 1949 | 31 | 2.17 | 0 |
| lamport | 359 | 1519 | 25 | 0.67 | 0 |
| lastinfirstserved | 560 | 2275 | 68 | 0.46 | 0 |
| lift | 881 | 3817 | 73 | 0.51 | 0.01 |
| manufacturing | 130 | 541 | 9 | 3.91 | 0 |
| MESI | 188 | 935 | 18 | 0.24 | 0 |
| MOESI | 270 | 1295 | 33 | 0.26 | 0.02 |
| multipoll | 10626 | 39934 | 612 | 3.11 | 0.63 |
| peterson | 588 | 2329 | 39 | 1.18 | 0 |
| PRODUCER-CONSUMMER | 77 | 389 | 35 | 0.23 | 0 |
| readwrit | 733 | 2917 | 93 | 6.15 | 0 |
| rtp | 225 | 1027 | 11 | 0.44 | 0 |
| swimmingpool.cheated | ERR | ||||
| swimmingpool | ERR | ||||
| swimmingpoolInv | ERR | ||||
| SYNAPSE | 162 | 816 | 18 | 0.21 | 0 |
| ticket2i | 1251 | 5048 | 133 | 0.28 | 0.01 |
| ticket3i | 5601 | 22332 | 609 | 0.46 | 0.04 |
| train | 37 | 325 | 1 | 0.56 | 0 |
| ttp2 | 126511 | 502715 | 17373 | 72.80 | 41.97 |
| ttp | 92890 | 366993 | 17971 | 49.88 | 26.32 |
1 Jean-Michel Couvreur. A BDD-like Implementation of an Automata Package. In Revised Selected Papers of the 9th International Conference on Implementation and Application of Automata (CIAA'04), Kingston, Ontario, Canada, July 2004, LNCS 3317, pages 310-311. Springer, 2005. PS, PDF.
2 Jérôme Leroux. Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l'outil FAST. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2003. PS
3 Jérôme Leroux. A polynomial time presburger criterion and synthesis for number decision diagrams. In LICS, pages 147–156. IEEE Comp. Soc., 2005.
4 Shared-automata are minimal and complete.