SYNOPSIS

spgsolver [OPTIONS] <game>

OPTIONS

Symbolic Parity Game Solver Options

--attr=default|chain|par|par2

Choose attractor function.

Available attractor functions:

default

Straightforward attractor computation.

chain

Chaining attractor, applies transition groups in a different order than default in computing an attractor level.

par

Spawns parallel tasks to compute forward and backward steps for each attractor level.

par2

Spawns more parallel tasks than par, by applying forward steps in parallel to the result of the backward steps of the different transition groups.

--saturating-attractor

Use saturation in the chaining attractor.

--pg-write-dot

Write dot files to disk during parity game solving for debugging.

Vector Set Options

--vset=TYPE

Select type of vector set: ldd64, ldd, list, tree, fdd, ddd, sylvan, or lddmc. With ldd64, the 64-bit ListDD list encoding is used (non-ATerm based). With ldd, the 32-bit ListDD list encoding is used (non-ATerm based). With list, ATermDD with list encoding is used. With tree, ATermDD with tree encoding is used. With fdd, BuDDy FDDs are used. With ddd, libDDD SDDs are used. With sylvan, the parallel BDD package Sylvan is used. With lddmc, the parallel LDD package LDDmc is used. Defaults to first available type in the list.

ListDD Options

--ldd32-step=STEP

The internal tables of ListDD resize according to the Fibonacci series. This option sets the initial size to the Fibonacci number STEP. Defaults to 30.

--ldd32-cache=DIFF

Set Fibonacci difference DIFF between the cache and nodes (DIFF may be negative). Defaults to 1.

ListDD Options

--ldd-step=STEP

The internal tables of ListDD resize according to the Fibonacci series. This option sets the initial size to the Fibonacci number STEP. Defaults to 30.

--ldd-cache=DIFF

Set Fibonacci difference DIFF between the cache and nodes (DIFF may be negative). Defaults to 1.

BuDDy Options

--cache-ratio=RATIO

Set cache ration. Defaults to 64.

--max-increase=NUMBER

Set maximum increase. Defaults to 1,000,000.

--min-free-nodes=PERCENTAGE

Sets the minimum percentage of free nodes as integer between 0 and 100. Defaults to 20.

--fdd-bits=BITS

Sets the number of bits for each FDD variable. Defaults to 16.

--fdd-reorder=STRATEGY

Sets the strategy for dynamic variable reordering. Valid options are none, win2, win2ite, win3, win3ite, sift, siftite, random. Refer to the BuDDy manual for details. Defaults to none.

Sylvan Options

--sylvan-threads=NUMBER

Set number of workers. Defaults to 1.

*--sylvan-dqsize Sets the size of the (static) task queue for work stealing in Wool to N. Defaults to 100000.

--sylvan-tablesize=NUMBER

Sets the size of the BDD table to 1<<N nodes. Defaults to 23. Maximum of 29.

--sylvan-cachesize=NUMBER

Set the size of the memoization table to 1<<N entries. Defaults to 23.

--sylvan-bits=BITS

Sets the number of bits for each integer in the state vector. Defaults to 16.

--sylvan-granularity=NUMBER

Controls memoization table usage. Only use the memoization table every 1/N BDD levels. Defaults to 1, i.e., always use the table.

LDDmc Options

--lddmc-tablesize=NUMBER

Sets the size of the BDD table to 1<<N nodes. Defaults to 23. Maximum of 29.

--lddmc-cachesize=NUMBER

Set the size of the memoization table to 1<<N entries. Defaults to 23.

Lace Options

--lace-workers=NUMBER

Set number of Lace workers (threads for parallelization). Defaults to the number of available cores if parallel algorithms are used, 1 otherwise.

--lace-dqsize=NUMBER

Set length of Lace task queue. Defaults to 40960000.

--lace-stacksize=NUMBER

Set size of program stack in kilo bytes. Defaults to 0, which means using the default stack size.

General Options

-v

Increase the level of verbosity

-q

Be quiet; do not print anything to the terminal.

--debug=<file.c>

Enable debugging output for file.c (option allowed multiple times).

--version

Print version string of this tool.

-h, --help

Print help text

--usage

Print short usage summary.

EXIT STATUS

0

Successful termination.

255

Some error occurred.

SEE ALSO