Tutorials

How to use smc_storm

Retrieve the available options

smc_storm --help

Examples

Here some examples are provided, to show how to run smc_storm on the exemplary models provided in the models folder:

smc_storm --model leader_sync.3-2.v1.jani --properties-names eventually_elected --batch-size 200
smc_storm --model nand.v1.jani --properties-names reliable --constants "N=20,K=2" --epsilon 0.01 --confidence 0.95 --n-threads 5 --show-statistics
smc_storm --model leader_sync.3-2.v1.jani --properties-names time --traces-file ~/exported_traces.csv --show-statistics --max-n-traces 5
smc_storm --model die.jani --custom-property "P=? [F s=7&d=6]"
smc_storm --model brp.v1.prism --properties-file brp.v1.props --constants "N=16,MAX=2"