**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.

PresTAF comes with a GENEPI plugin. This plugin can be used in any tool based on the generic solver for Presburger formulas proposed by GENEPI. Among these tools there is:

- FAST the model-checker based on acceleration techniques developed by J. Leroux [2];
- and distiller, the solver for the Armoise language.

To our knowledge, PresTAF is the only tool that is able to synthesize [3] a Presburger formula (using the Armoise high-level language) from a binary automaton.

## 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).

The benchmarks related to comparisons of plugins are given on the pages of FASTer and distiller. 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.

In the tables below, columns have the following meaning:

*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 states[4] 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.

[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.