PAWS is a tool to analyse the behaviour of weighted automata and conditional transition systems. At its core PAWS is based on a generic implementation of algorithms for checking language equivalence in weighted automata and bisimulation in conditional transition systems. The tool is designed in such a way that arbitrary user-deﬁned semirings can be employed. New semirings can be generated during run-time and the user can rely on numerous automatisation techniques to help with creating new semiring structures to use with PAWS’ algorithms. Basic semirings such as distributive complete lattices and ﬁelds of fractions can be deﬁned by specifying few parameters, more exotic semirings can be built from other semirings or deﬁned from scratch using a built-in semiring generator tool. In the most general case, users can deﬁne new semirings by programming (in C#) the base operations of the semiring and a procedure to solve linear equations and use their newly generated semiring in the analysis methods offered by PAWS.
The development of this tool is part of the BEMEGA project (related publications).
Getting started with PAWS
In order to run PAWS, download it via the provided linke and unzip the files. After that you need to run the Analysis_Part.exe file in PAWS/Analysis_Part/bin/. For semiring generation you can switch to the generator component using the "Save and Generator" button.
PAWS is implemented in C# and can be compiled for 32-bit version without any restrictions. 64-bit Compiling works only without the GraphViz library. It should be noted that manually implemented semirings, in the config files also have to be added, if one wants to use these within the semiring generator.
External Libaries and Projects
Currently, only a minimal tutorial is included, which is available pressing the "Help" button in the semiring generator. A more detailled description or manual will be published at a later time.
Input and output
For loading and storing weighted automatas or generated semirings PAWS is using the MSDN serialization of C#. At the moment serialization for lattices on BDD is not supported. For source code generation we use CodeDOM.