PRINSYS - PRobabilistic INvariant SYnthesiS
About
PRINSYS is a novel tool for invariant generation for probabilistic programs. It takes a constraint-based approach and relies on quantifier elimination techniques to obtain the results. PRINSYS is under constant development so check back for news soon!
Below you will find short download instructions and a quick manual which explains how to obtain the results from our paper (currently under review).
If you have any questions or suggestions, do not hesitate to contact: Friedrich Gretz (fgretz at cs dot rwth-aachen.de)
Download
See here for download and installation instructions.
Case Studies
See here for examples.
Quick manual (GUI)
Download the tar.gz archive, unpack it and navigate to the working directory. Then start PRINSYS by typing
./start.sh
This is how the GUI looks like. You have the option to save and load sessions (last opened pcgl file, used templates/assumptions etc.).
The debug console is located on the bottom where we can see the results, errors etc.
First we have to set the tool paths (Reduce, SLFQ and dot). So click on the "Configuration" tab.
Now type in the paths to the executables of the tools. Let's move on to the "File" tab.
Here we have a text editor with basic functions (save,load,program graph generation).
Let us load a pgcl program (e.g. duelling cowboys) by clicking on the "Load" button.
The editor shows us the program code now. We want to generate the program graph by clicking on the "Generate Graph" button.
After generating the graph, a new tab "Program Graph" has been enabled. You can zoom in/out to view the graph.
The "Invariant Generation" tab is where we can use templates and assumptions for our pgcl program. Let's put this template into the Template box:
[turn=0 and continue=0]*(1) + [turn=0 and continue-1=0]*(alpha) + [turn-1=0 and continue-1=0]*(beta)
Now click on the "Generate Constraints" button and after a while the generated constraints appear on the "Constraints" field!
Quick manual (command line interface)
Navigate to the working directory of PRINSYS and type
./start.sh
This should give you
Enter a command. Type 'm' to see a list of available commands.
Type m to get an overview of tour possibilities:
Please choose an action:
[l] load a pGCL file
[g] generate a program graph for the currently loaded program
[t] enter a template invariant
[i] generate constraints for a valid invariant
[q] quit
These options also describe the workflow. First let us load a file. Therefore choose l, you will see a list of programs that are shipped along with PRINSYS. Press 2 to select the duelling cowboys example.
Enter the path to the file or choose a file from the list below by entering its number.
[0] biased_coin.pgcl
[1] binomial_update.pgcl
[2] cowboys.pgcl
[3] geometric_loop11_param.pgcl
[4] geometric_loop12_param.pgcl
[5] geometric_loop22_param.pgcl
2
pgcl_programs/cowboys.pgcl successfully parsed!
Press t to type in a template invariant:
Enter a template of the form [linear term <= 0 and linear term < 0 and ...]*(linear term)
[turn=0 and continue=0]*(1) + [turn=0 and continue-1=0]*(alpha) + [turn-1=0 and continue-1=0]*(beta)
Note that all comparisons are written wrt. to 0. So instead of writing continue=1 write continue-1=0. This restriction is due to the simple parser. In the next release this will be more convenient.
Hit i to get constraints over alpha and beta which describe all invariant instances of the given template.
22/01/2012 8:33:33 PM constraintGenerator.DirectConstraintGenerator getFOconstraints
INFO: Quantifier Elimination using REDLOG took 535 ms
22/01/2012 8:33:33 PM java.util.logging.LogManager$RootLogger log
INFO: Consecution condition yields:
a*beta - a + alpha - beta <= 0 and alpha*b - alpha + beta <= 0
22/01/2012 8:33:35 PM constraintGenerator.DirectConstraintGenerator getFOconstraints
INFO: Quantifier Elimination using REDLOG took 208 ms
22/01/2012 8:33:35 PM java.util.logging.LogManager$RootLogger log
INFO: 0 <= I condition yields:
alpha >= 0 and beta >= 0
22/01/2012 8:33:36 PM constraintGenerator.DirectConstraintGenerator getFOconstraints
INFO: Quantifier Elimination using REDLOG took 240 ms
22/01/2012 8:33:36 PM java.util.logging.LogManager$RootLogger log
INFO: I <= 1 condition yields:
alpha - 1 <= 0 and beta - 1 <= 0
With the last command q PRINSYS shuts down.
To generate the invariants for the geometric distribution examples use the following template:
[0<=0]*(1*x) + [flip=0]*(alpha)
The parser enforces to write us some expression between the [ ] so 0<=0 represents true here. This again is due to the simple parser and will become more convenient with the next update.
21 Oct. 2012