SATAF/PresTAF libraries

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.