These are a small number of notes about SpinBatch, but don't expected too much of documentation.
- There are some useful defines in "batch.c", for compiler and location of Spin.
- I know, it was a quick and dirty job. Deal with it.
- To compile the batch program, just type "make"
- To use the resulting binary, call "spinbatch [batch-file]", with batch file a text file with the following key value pairs:
iterate-int [variable name] [lower bound] [upper bound] [optional: step]
define [variable name] [value] (for strings escape the " manually by typing \"
model [model file] (e.g. model some-model.pml)
memory [max-memory in megabytes]
search depth-first|breath-first whichever way you like
basic to enable basic checking of the model, including assertions
progress to check for liveness and progress states
safety [some ltl formulae] eg "safety (value <= 10)". Multiple ltl formulaes can be specified. Their are automatically compiled into the version.
logilfe [some log file] specify a file to write detailed logs to.
shortest to enable iterative search for the shortest path
mailto [mail adres] automatically mail the output of a run to the specified mail adres
mailsubject [some subject] in case of multiple runs, makes filtering in your mail box easier
multicore [number of cores] specify how many cores you want to use (read the documentation of Spin on the implications on the validity of the results)
- If a run goes wrong, the debug information is automatically generated and written to the a logfile with the format "name-number.log" and, if present, the trail file to "name-number.trail". The model used is written to "name-number.model" (preprocessed model).
- If you have any questions or remarks, you can direct them to Bernard van Gastel.
- I would appericate if you use this software or made improvements that you let me know, and if possible send me the changes so I can make them available for others to use.
- There is ofcourse no warrenty associated with this software, use on your own risk.
iterate-int SKEW 0 10 1
iterate-int SW_LENGTH 1 10 1
iterate-int THRESHOLD 0 10 1
define BALANCED_HASH_LENGTH 8
safety (ether >= 0)
You can download the program here. Good luck!