spgsolver(1)

SYNOPSIS

spgsolver [OPTIONS] <game>

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

--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.
vset-cache-diff=diff: Influences the size of operations cache when counting precisely with bignums: cache size = floor((2log(nodes-to-count) + <diff>)^2). More precisely; LTSmin will bitshift <diff> bits to the left or right on the number of nodes in the vector set, depending on the signedness of <diff>. The default is 0, meaning that if the cache is full the number of bignums in memory will be equal to the number of nodes in the vector set. The default value seems to work well, even when the number vectors in the vector set is very large relative to the number of nodes. If the number of vectors relative to the number of nodes is lower, <diff> may be decreased. The user may want to set <diff> as low as possible (to save memory), while keeping the operations cache effective. Bignums are not floating point numbers and may thus consume a lot of memory.

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

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

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

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