Wendy - Synthesizing partners for services

Wendy is a tool to synthesize partners for services. This includes a finite characterization of all partners (called "operating guidelines"). Wendy uses a vast set of reduction rules to synthesize (small) partners. These rules may, however, not preserve all partners of the service under consideration, but will synthesize a partner if one exists.

Download Wendy

Version history

Wendy has been developed for quite some time now. See the ChangeLog for details or try out the older versions.

License

Wendy is open source software, licensed under the AGPL3+.

Install Wendy

Requirements

Installing and running Wendy requires a bunch of other tools:

Compiling requires:

  • GCC - The GCC compiler

Testing requires:

  • Autotools test suite - Part of the GNU Auto-Tools for automated Tests
  • LCOV - LCOV is a graphical front-end for GCC's coverage testing tool gcov. It collects gcov data for multiple source files and creates HTML pages containing the source code annotated with coverage information.
  • Valgrind - Valgrind is an instrumentation framework for building dynamic analysis tools. There are Valgrind tools that can automatically detect many memory management and threading bugs, and profile your programs in detail.

Contributing requires:

  • Bison - Gnu parser generator - Bison is a general-purpose parser generator that converts an annotated context-free grammar into a deterministic LR or generalized LR (GLR) parser employing LALR(1) parser tables.
  • GNU Gengetopt - Gengetopt generates a C function that uses getopt_long function to parse the command line options, to validate them and fills a struct .
  • flex: The Fast Lexical Analyzer - Flex is a tool for generating scanners. A scanner, sometimes called a tokenizer, is a program which recognizes lexical patterns in text. The flex program reads user-specified input files, or its standard input if no file names are given, for a description of a scanner to generate.

Quick install

Extract the tar ball into a folder of your choice, and follow the steps below.

  1. Configure
    ./configure
  2. Compile
    make
  3. Test (optional, but recommended)
    make check
  4. Install
    sudo make install

Manual

Wendy's manual explains usage, features, and a brief scientifical background.

Documentation

Wendy's documentation aims at the developer in you. If you are interested in implementation details this is the right place for you to look.

Maintainer

The current maintainer of Wendy is Niels Lohmann.

Authors

Niels Lohmann implemented the original core functionality of Wendy (operating guidelines), Daniela Weinberg implemented reduction techniques as well as the synthesis of livelock free strategies, and Christian Sura implemented the functions to cover open nets nodes

Contributors

Several people have committed time, code, and advice to the development of Wendy.

  • Niels Lohmann (312 commits)
  • Daniela Weinberg (64 commits)
  • Christian Gierds (8 commits)
  • Christian Sura (8 commits)
  • Kathrin Kaschner (7 commits)
  • Richard Müller (4 commits)
  • Jan Sürmeli (2 commits)
  • Stephan Mennicke (1 commit)
  • Andreas Lehmann (1 commit)

Acknowledgements

Wendy's development team thanks:

  • Thanks to Marc Voorhoeve for reporting some bugs running Wendy in a native (non-Cygwin) Windows environment.
  • Thanks to Christian Gierds for testing Wendy with strange nets that revealed several really subtle bugs.
  • Thanks to Dirk Fahland for pointing out a problem in the STL sorting algorithm which led to a segmentation fault.
  • Thanks to Mike Hordecki for a post on Stack Overflow with a portable preprocessor macro to iterate C++ containers (see 'src/util.h').