RegSy (Regular Synthesis) is a synthesis tool that can be used to build functions from specification written in WS1S (or, equivalently, specifications given by automata, thanks to the WS1S-automata connection).

Synthesis for Regular Specifications over Unbounded Domains

Click here for some examples demonstrating the use of RegSy

* Click Here to Download RegSy

• Make sure you have a recent Java distribution
• Make sure you have MONA tool used to build the automaton from WS1S specification. RegSy specifications are currently written as MONA input files

• To run the program use the syntax

./run filename input_tracks

For example, if filename is addition.mona and defines a predicate plus(x,y,z) (corresponding to the relation x + y = z), you can build a program for addition using

./run addition.mona "0 1"

“0 1” means that variables 0 and 1 (x and y) are the input tracks, and z will automatically be the output.

If you wish a program for substraction, you can type

./run addition.mona "0 2"

This way, x and z will be the input tracks, and the system will look for y such that x + y = z (y = z - x).

You can also try

./run addition.mona 2

so that z will be the input track, and once you give z, the system will return some x and y such that x + y = z

Once your function has been synthesized, you can try it on different inputs.

When you run some filename.mona on Regsy, it will automatically save the synthesized function on filename_tracks.sav; you can then run it using

./run -l addition_01.sav

Regsy also have a streaming functionality. You can use it using for instance on:

./run -k 0 not.mona 0

It will assume that the specification is k-causal (in that example, 0-causal) and then you will be able to give a file as input stream, and the program will display the output stream in return. The second 0 corresponds to the input track that you want to use.

• Download and install scala (the code was tested with Scala 2.8 RC2).
• Type

./symbbuild