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.
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)