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:49] vkuncak |
regsy [2011/01/12 17:08] vkuncak |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| 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). | 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 34: | 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: | ||