| model | Yes | n/a | string | Model file, e.g. `models/brp/brp.sm` |

| property | Yes | n/a | string | File to load properties from |

| N | No | 100 | int. or list of integers | Number of solution vectors. A list can be passed as e.g., `[100,200]` |

| beta | No | [0.9,0.99,0.999] | float or list of floats | Confidence level. A list can be passed as e.g., `[0.9,0.99]` |

| rho_list | No | --depends-- | float of floats | Lists of the costs or relaxation to use, e.g. `[0.2,0.5,0.75,1.5]` |

| param_file | No | parameters.xlsx | string | File to load parameter distributions from |

| prop_file | No | properties.xlsx | string | File to load properties from |

| no-bisim | No | False | bool | If this argument is added, bisimulation is disabled |

| seed | No | 1 | int | Random seed |

| Nvalidate | No | 0 | int | Number of solution vectors to use in computing empirical containment probabilities (as in Table 2 in [1]) |

| dft_checker | No | concrete | string | Type of DFT model checker to use (either `concrete` or `parametric`) |

| precision | No | 0 | float >= 0 | If specified (and if bigger than zero), approximate model checker is used |

| naive_baseline | No | False | bool | If this argument is added, comparison with a naive Monte Carlo baseline is performed |

| export_stats| No | None | string | If this argument is added, benchmark statistics are exported to the specified file |

| refine | No | False | bool | If this argument is added, the iterative refinement scheme is enabled |

| refine_precision | No | 0 | float | Refinement precision to be used for refining solutions (0 means refining to exact solution vectors) |

| plot_timebounds | No | None | str | List of two timebounds to create 2D plot for (note: these should be present in the properties Excel file!) |

| curve_plot_mode | No | conservative | str | If `conservative`, overapproximation of curves are plotted over time; if `optimistic`, underapproximations are plotted |

| pareto_pieces | No | 0 | int | If nonzero, a pareto front is plotted, with a front consisting of the specified number of linear pieces |

| model | Yes | n/a | string | Model file, e.g. `models/brp/brp.sm` |

| property | Yes | n/a | string | File to load properties from |

| threshold | Yes | n/a | float in [0,1] | Threshold for the specification to compare against |

| comparator | Yes | n/a | string | Is either `geq` or `leq`, or a list of strings, e.g. `'("geq","leq")'` |

| num_samples | Yes | n/a | (list of) integers | Number of parameter samples to use, e.g. `1000` or `'(1000,5000)'` |

| bisimulation | No | `strong` | string | Bisimulation mode. Can be `strong`, `weak`, or `none` |

| num_iter | No | 1 | integer | Number of iterations, given as integer |

| eta | No | None | (list if) floats in [0,1] | Fix the satisfaction probability (and compute the probability level). Either a float, e.g. `0.8` or a list of floats, e.g. `'(0.8, 0.9)'` |

| beta | No | None | (list if) floats in [0,1] | Fix the confidence probability (and compute the satisfaction level). Either a float, e.g. `0.99` or a list of floats, e.g. `'(0.99, 0.999)'` |

| outfile | No | `outfile` | string | Prefix of the output file for storing results, without extension (the extension, `.csv` or `.txt`, is automatically added). |

| weather | No | 0 | string | Dedicated argument for the drone benchmark in [1]. Can be `uniform`, `y-pos-bias`, or `x-neg-bias` |