qCORAL

Command line options

Here are listed the options to qCoral. On the command line, the values for options are specified in the form '--long=value' or '--long value'. The value is mandatory for all options except booleans. Booleans are set to true if no value is specified.

General Options

• --rangeLO lo

Lower bound of search interval. lo must be an integer. Default is -10000.

• --rangeHI hi

Upper bound of search interval. hi must be an integer. Default is 10000.

Model Counting

• --mcSeed num

Seed to be used by the RNG. num must be six "longs", separated by commas. Default value is "990764872,70974053,810762905,153046394,848454615,21597730".

• --mcMinSamplesPerBox num

Minimum number of sampling points to be used for each box. Default is 1000.

• --mcMaxSamples num

Total amount of samples for a single model counter call. Default is 100000.

• --mcDistributeSamples num

Set distinct amounts of samples for each box based on volume. Default is false.

• --mcSkipPaving

Don't use an interval solver before running the model counter. Default is false.

• --mcMergeBoxes

Merge all boxes returned by the interval solver. Default is false.

• --cachePavingResults

Cache RealPaver paving results. Default is false.

• --mathematicaGA

Use global adaptive integration with Mathematica (if false, use monte carlo). Default is false.

• --fixed100Domain

Makes the domain of all variables = [-100,100]. Default is false.

• --domainFile

Read the domain of the variables from the input file. Default is false.

After each constraint, qCoral will read the domain for the variables of that constraint. The domain must be in the format "{$LO,$HI},...". Domains will be attributed to the variables following the order of their IDs. Example:

DLE(DCONST(45),DVAR(r_1));DLE(DVAR(r_1),DCONST(49));DLE(DCONST(80),DVAR(r_2));DLE(DVAR(r_2),DCONST(160));
[{45.0, 90.0}, {80.0, 200.0}]

In this case, the domain of variable $r1 is 45,90, and the domain of $r2 is 80,200.

• --mcUseMathematica

Use Mathematica to compute the volume. Default is false.

• --normalize

Normalize results. Default is true.

• --mcPartitionAndCache

Partition/cache constraints sent to the selected model counter. Default is false.

• --mcDisableCache

disable caching. Default is false.

• --mcCallIntSolPartition

Call interval solver for each partition. Default is false.

• --mcNumExecutions numExecs

Number of times to run the model counter. Default is 1.

• --mcSeedFile file

File with seeds to use for reseeding the rng at the end of each run - make sure to have enough seeds!. Default is "".

• --mcResetRngEachSimulation

Reset rng at the end of each simulation. Default is true.

Interval Solver

• --realPaverLocation path

Path to realPaver executable.

• --intervalSolverPrecision precision

Precision used by the interval solver (1E-precision). precision must be an integer. Default is 3.

• --intervalSolverTimeout timeout

Max time for the interval solver to answer the query (in ms). timeout must be an integer. Default is 2000.