Command-line interface¶
prodigy¶
Usage
prodigy [OPTIONS] COMMAND [ARGS]...
Options
- --engine <engine>¶
- --strategy <strategy>¶
- --solver <solver>¶
- --template-heuristic <template_heuristic>¶
- --pos-heuristic <pos_heuristic>¶
- --intermediate-results¶
- --stepwise¶
- --no-simplification¶
- --use-latex¶
- --no-normalize¶
- --show-all-invs¶
analyze¶
Analyse a program without asking questions: every loop needs a strategy (–loop or –decisions). Queries are answered with sound intervals.
Usage
prodigy analyze [OPTIONS] PROGRAM_FILE [INPUT_DIST]
Options
- --loop <loop_specs>¶
Strategy for a loop, as ID=STRATEGY[:NAME=VALUE,…], e.g. 0=unroll:iterations=100 or ‘*=evt_synthesis’ for all loops. See prodigy loop_strategies.
- --decisions <decisions_file>¶
JSON file {“0”: {“strategy”: …, “params”: {…}}, “*”: …}.
- --json¶
Print the JSON result.
- --coefficients <coefficients>¶
Number of coefficients per marginal in the result (0 to skip).
- Default:
30
- --steps¶
Record the distribution after each instruction.
- --output <output>¶
Write the JSON result to this file.
Arguments
- PROGRAM_FILE¶
Required argument
- INPUT_DIST¶
Optional argument
check_equality¶
Checks whether a certain loop-free program is an invariant of a specified while loop. :param program_file: the file containing the while-loop :param invariant_file: the provided invariant :return:
Usage
prodigy check_equality [OPTIONS] PROGRAM_FILE OTHER_PROGRAM_FILE
Arguments
- PROGRAM_FILE¶
Required argument
- OTHER_PROGRAM_FILE¶
Required argument
evt_lower_bound¶
Lower induction: verifies that NU is an EVT sub-invariant of finite mass (NU <= Phi(NU) coefficient-wise and NU(1,…,1) < oo) and continues the analysis with the resulting lower bound on the output distribution of the loop. No termination assumption is needed.
Usage
prodigy evt_lower_bound [OPTIONS] PROGRAM_FILE [INPUT_DIST]
Options
- --invariant <invariant>¶
Required EVT sub-invariant nu (a generating function in the program variables).
Arguments
- PROGRAM_FILE¶
Required argument
- INPUT_DIST¶
Optional argument
evt_sandwich¶
Sandwich bounds for a program with one loop: synthesises an EVT sub-invariant of finite mass (lower bound, no termination assumption) and an EVT super-invariant (upper bound) with eventually geometric templates by linear programming, verifies both exactly, and prints two-sided bounds for the queries after the loop.
Usage
prodigy evt_sandwich [OPTIONS] PROGRAM_FILE
Options
- --size <size>¶
Budget for the number of template values of the lower certificate.
- Default:
1200
- --lower <lower_specs>¶
Template shape of the lower certificate ‘rates;periods;tail starts’ (repeatable).
- --upper <upper_specs>¶
Template shape of the upper certificate ‘rates;periods;tail starts’ (repeatable).
- --no-upper¶
Only synthesise the lower certificate.
- --objective <objective>¶
Objective of the upper certificate (auto: exit mass plus the moments of ?Ex queries).
- Default:
'auto'- Options:
auto | mass
- --per-query, --no-per-query¶
Re-optimise the upper certificate for every ?Pr query (default: only if its exit mass is infinite).
- --show-certificates¶
- --json <json_path>¶
Write certificates and bounds to this file.
Arguments
- PROGRAM_FILE¶
Required argument
independent_vars¶
Outputs an under-approximation or the actual result of the pairwise stochastic independence relation.
- param program_file:
the program file of interest
- param compute_exact:
if True, also compute and return the actual stochastic independencies
- return:
under-approximation or the actual relation
Usage
prodigy independent_vars [OPTIONS] PROGRAM_FILE
Options
- --compute-exact¶
Arguments
- PROGRAM_FILE¶
Required argument
invariant_synthesis¶
Tries to synthesize an EVT Invariant for the given input file. Supports a loop-free program to prefix the actual loop describing an initial distribution.
Usage
prodigy invariant_synthesis [OPTIONS] PROGRAM_FILE [INPUT_DIST]
Options
- --invariant <invariant>¶
Arguments
- PROGRAM_FILE¶
Required argument
- INPUT_DIST¶
Optional argument
loop_strategies¶
List the strategies for while loops and their parameters.
Usage
prodigy loop_strategies [OPTIONS]
Options
- --json¶
main¶
Compile the given program and print some information about it.
Usage
prodigy main [OPTIONS] PROGRAM_FILE [INPUT_DIST]
Options
- --show-input-program¶
- --loop <loop_specs>¶
Strategy for a loop, as ID=STRATEGY[:NAME=VALUE,…], e.g. 0=unroll:iterations=100 or ‘*=evt_synthesis’ for all loops. See prodigy loop_strategies. Loops without a decision are asked for.
Arguments
- PROGRAM_FILE¶
Required argument
- INPUT_DIST¶
Optional argument
outline¶
List the loops (with the ids used by –loop) and queries of a program.
Usage
prodigy outline [OPTIONS] PROGRAM_FILE
Options
- --json¶
Arguments
- PROGRAM_FILE¶
Required argument
print-pos-heuristics¶
Usage
prodigy print-pos-heuristics [OPTIONS]
print-strategies¶
Usage
prodigy print-strategies [OPTIONS]
print-template-heuristics¶
Usage
prodigy print-template-heuristics [OPTIONS]
web¶
Start the web GUI (a local web server) and open it in the browser.
Usage
prodigy web [OPTIONS]
Options
- --host <host>¶
- Default:
'127.0.0.1'
- --port <port>¶
- Default:
8080
- --no-browser¶
Do not open a browser window.
- --time-limit <time_limit>¶
Seconds an analysis may run before it is stopped.
- Default:
120.0
- --max-jobs <max_jobs>¶
Analyses running at the same time.
- Default:
2
- --memory-limit <memory_limit>¶
Memory limit per analysis in MB (Linux).
- --examples <examples_dir>¶
Folder with example programs (default: pgfexamples of this checkout or package).
- --allowed-host <allowed_hosts>¶
Additional host name the server may be reached under (when not on localhost).