Wring

Software

Here is a link to wring-1.1.0  (dated 21 Jun 01) by Fabio Somenzi. Wring is a perl script to translate LTL  formulae to generalized Buechi automata.  It is based on the paper

Fabio Somenzi and Roderick Bloem, Efficient Buechi automata from LTL Formulae, CAV'00, pp.248-263, 2000 (postscript, copyright Springer Verlag).

Wring takes an LTL formula and produces a dot or verilog representation of a corresponding automaton.  It is meant to produce small automata.

The software includes a reimplementation of Gerth, Peled, Vardi and Wolper's GPVW and GPVW+ algorithms, and of Daniele, Giunchiglia and Vardi's LTL2AUT.  It should be understood that any errors or inadvertent inefficiencies in the reimplementation are solely our responsibility, not that of the original authors.

Wring works in three stages: rewriting, translation, and simulation-based minimization.  The first and last stages can be turned off or on at will, and the middle stage can be set to GPVW, GPVW+, LTL2AUT or Boolean optimization.  In this way one can obtain a good picture of the relative strengths of the various methods.

New

Wring-1.1.0 improves Wring-1.0.0 in the following ways.

• It fixes two bugs in Wring-1.0.0 that yield incorrect results. (Thanks Heikki Tauriainen.)
• Wring now outputs verilog monitors.
• Wring now can read Buechi automata written in the format used by Buechi::ToString. This means that it can read back in its own output.

Difference with Paper

The third stage makes use of don't-care information.  For some states it does not matter in which fair sets they occur; this gives the optimizer more freedom.  Unfortunately, there was a mistake in the initial implementation, and the current, corrected version uses don't-care information less efficiently.  Hence, we see small differences with respect to the tables of  the paper. We mention the two most important revisions:

• In Table 1, the overall performance of Wring is 121 states, 232 transitions, 22 fairness constraints (was: 122, 231, 22).
• In Table 2, the last line becomes: 5689 states, 10141 transitions, 492 fair sets, 1548 initial, 395 weak,  526 teminal,  578.0s. (was: 5648 states, 10053 transitions, 492 fair sets, 1535 initial, 390 weak,  537 teminal,  631.0s.)

Variability in Results

In doing experiments, you will notice small differences between runs on different architectures and between runs with different parameters, even if they mean the same.  This happens because some heuristics are order dependent, and hash tables get read out in different orders on different architectures and when their placement in the address space is different.

Benchmarks

The tar archive also contains several benchmarks.  One, Test/table.ltl is the set used in Table 1, as ``formulas in common use and from the literature''.  The set of 1000 random formulas that we used for Table 2 is available as Test/l1000-15-3-05.ltl.  A random formula generator, inspired by the one by Daniele, Giunchiglia, and Vardi, is also included.

Future

Our long-term plan is to integrate wring into vis.

For additional information, please contact Fabio Somenzi or Roderick Bloem.