Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
regsy [2010/06/04 16:34] vkuncak |
regsy [2011/01/12 17:08] (current) vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Regsy: A Synthesizer for Regular Specifications over Unbounded Domains ====== | + | ====== RegSy: A Synthesizer for Regular Specifications over Unbounded Domains ====== |
| - | Regsy (Regular Synthesis) is a synthesis tool that can be used to build functions from specification written in WS1S (or, equivalently, given by automata, thanks to the WS1S-automata connection). | + | 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). |
| + | |||
| + | ==== Paper Describing the Algorithm ===== | ||
| + | |||
| + | [[http://lara.epfl.ch/~kuncak/papers/HamzaETAL10SynthesisforRegularSpecificationsoverUnboundedDomains.html|Synthesis for Regular Specifications over Unbounded Domains]] | ||
| ==== Examples ==== | ==== Examples ==== | ||
| Line 7: | Line 11: | ||
| [[regsy-examples|Click here for some examples demonstrating the use of RegSy]] | [[regsy-examples|Click here for some examples demonstrating the use of RegSy]] | ||
| - | ==== Building Regsy ==== | + | ==== Download ==== |
| - | You can find the source code [[someplace|here]] with a script to build the program as well as a script to run it. | + | * [[http://lara.epfl.ch/~kuncak/regsy.tar.gz|Click Here to Download RegSy]] |
| - | Since this program has been written in [[http://www.scala-lang.org/|scala]] (2.8), you will need it to be able to build. | + | |
| - | To build the program, you can type | + | |
| - | + | ||
| - | ./symbbuild. | + | |
| ==== Running Regsy ==== | ==== Running Regsy ==== | ||
| - | To run the program, you will need [[http://www.brics.dk/mona/|MONA]] to build the automaton from WS1S specification. | + | * Make sure you have a recent Java distribution |
| + | * Make sure you have [[http://www.brics.dk/mona/|MONA]] tool used to build the automaton from WS1S specification. RegSy specifications are currently written as MONA input files | ||
| - | The syntax to run the program is: | + | * To run the program use the syntax |
| ./run filename input_tracks | ./run filename input_tracks | ||
| - | For instance, 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 | + | 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" | ./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. | "0 1" means that variables 0 and 1 (x and y) are the input tracks, and z will automatically be the output. | ||
| Line 37: | Line 38: | ||
| Once your function has been synthesized, you can try it on different inputs. | 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.sav; you can then run it using | + | 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.sav "0 1" | + | ./run -l addition_01.sav |
| Regsy also have a streaming functionality. You can use it using for instance on: | Regsy also have a streaming functionality. You can use it using for instance on: | ||
| Line 46: | Line 47: | ||
| 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. | 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. | ||
| + | |||
| + | ==== Building Regsy ==== | ||
| + | |||
| + | * Download and install [[http://www.scala-lang.org/|scala]] (the code was tested with Scala 2.8 RC2). | ||
| + | * Type | ||
| + | ./symbbuild | ||