Given a source file qrcu.spin, one can use the following commands:
The optimizations produced by -DSAFETY greatly speed things up, so you should use it when you can. An example situation where you cannot use -DSAFETY is when checking for livelocks (AKA ``non-progress cycles'') via -DNP.
If you aren't sure whether your machine has enough memory, run top in one window and ./pan in another. Keep the focus on the ./pan window so that you can quickly kill execution if need be. As soon as CPU time drops much below 100%, kill ./pan. If you have removed focus from the window running ./pan, you may wait a long time for the windowing system to grab enough memory to do anything for you.
Don't forget to capture the output, especially if you are working on a remote machine,
If your model includes forward-progress checks, you will likely need to enable ``weak fairness'' via the -f command-line argument to ./pan. If your forward-progress checks involve accept labels, you will also need the -a argument.