Passel instructions

1) Run the file passel.exe

2) Select an input file from the list (the file must be in a subdirectory labeled input, the path for input files is displayed at the top of the console output)

3) Browse to the output folder and select the appropriate log file.  A summary of invariants proved or disproved appears at the very bottom of the log file.




Other details:

A variety of examples appear in the input folder, please check them out to see different versions of SATS, Fischer's protcol, simplified Bakery, etc. that we verified (as well as buggy versions of the protocols).

Feel free to play with the examples as you like, although the parser does not have great error checking yet (particularly with the dynamics, e.g., you could input some nonlinear dynamics, but that won't work), so try to match the syntax in the examples.






Runtime details:

I ran my experiments on a Windows 7 (64-bit) laptop with a quad-core I7 processor running at 2.0GHz and 8GB RAM (however, the program is compiled in 32-bit, and the Z3 DLL is also 32-bit).

You can read more about Z3 at its homepage, and please note any copyrights Microsoft has on it: http://research.microsoft.com/en-us/um/redmond/projects/z3/

The program is written in C# and reles on the .NET libraries.






Future:

The current input file selection method is a little strange, but was easiest for me to debug the program in Visual Studio, but this will change to the more standard file input format.