Instructions for installing and using GPUexplore

GPUexplore can be compiled using the included Makefile. After compiling, any of the models from the models package can be used as input, after some preprocessing has been performed.

Preparing input

GPUexplore accepts input files in the GPF format. These can be generated from the models included in the models package, which are in the EXP format. Included in the models package is a python script named to perform this conversion.

Running GPUexplore

GPUexplore supports the following commandline options:

GPUexplore <model> [-b <num_blocks>] [-t <num_threads>] [-k <kernel_iter>] [-q <hash_table_size>] [-v <num>] [--por [--cycle-proviso]] [-d|-p]
Generate the state space of <model>.gpf (without extension), using the options specified:
-b                number of blocks to use
-t                number of threads per block
-k                number of iterations per kernel launch
-q                size of the hash table in number of 32 bit integers
-v                verbosity: 0 is quiet, 1 prints the iterations, 2 prints the number of states, 3 prints state vectors
--por             apply partial-order reduction
--cycle-proviso   apply the cycle proviso during POR
-d                check for deadlocks
-p                check for safety property (should be embedded in the model)