Frequently Asked Questions

  1. What does ALPAGA mean ?

    Algorithms for Parity Games (thanks to Gilles Geeraerts for this name)

  2. Why is the logo a llama ?

    Alpaga is the french word for alpaca, a kind of llama.

  3. What is the link between ALPAGA and ALASKA ? Why are the tools not merged ?

    The two tools share a lot of things:

    • Some common concepts : the use of antichains based fixpoint for gaining efficiency;
    • A common set of technologies: Python and Pycudd;
    • A programmer : Martin De Wulf, which is currently the only one for Alpaga, but has also participated to Alaska, although the main programmer for Alaska is Nicolas Maquet;
    • A common domain name : antichains.be (and a good part of the website too, since the initial designer is the same).

    In the mean time, there are lots of differences:

    • The problems solved are distinct (although there exists some intersection);
    • As a consequence, the input languages are different. Alaska allows analysis of LTL formula, Alternating Buechi Automata and Nusmv Models, while Alpaga defines its own minimal input language.
    • The two tools do not share a single line of code. It could be thought that we should share data structures for manipulating antichains, but in fact, we would not gain much time by doing this. Indeed, the time used to implement antichains operations (intersection, union, insertion and inclusion test) is really small compared to the time used for designing the encoding of automata, models and games in Binary Decision Diagrams. A future rework of the architecture of the tools could lead to a merge, but that remains uncertain.

  4. Wich technologies do Alpaga rely on ?

    The tool is programmed in Python and heavily relies on the use of the CUDD binary decision diagram package (by Fabio Somenzi), through the use of a binding named PyCUDD (by Steve Haynal and Aravind Vijayakumar).