Testing CLIs.

[sjunges]

Originally by TQ:

For testing the CLI re-implementation, I compiled a list of commands that should cover most of the functionality affected by this PR. I diffed the outputs for old vs. new implementation and manually checked that they are consistent.

Here is my command list for future reference.

set -e # fail on first error

STORMBIN=./build/bin
TESTFILES=./resources/examples/testfiles

$STORMBIN/storm;
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]'
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --prism2jani
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' -bisim
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --exact
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --exact -bisim
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --buildstateval --exportresult res.json; cat res.json; rm res.json
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P>0.5 [ F "one"]' --counterexample
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --exportbuild crowds5_5.drn; head -n20 crowds5_5.drn; rm crowds5_5.drn
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --exact --exportbuild crowds5_5.drn; head -n20 crowds5_5.drn; rm crowds5_5.drn
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine hybrid
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine hybrid --ddlib cudd
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine hybrid --exact
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd --exact
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd -bisim
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd -bisim --exact
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd-to-sparse
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd-to-sparse -bisim
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine automatic
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine expl
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine abs
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine abs --abstraction:method games
$STORMBIN/storm --explicit-drn $TESTFILES/ma/jobscheduler.drn --prop 'Tmax=? [F "all_jobs_finished" ]'

$STORMBIN/storm --prism $TESTFILES/imdp/robot.prism -const delta=0.01 --buildfull;
$STORMBIN/storm --prism $TESTFILES/imdp/robot.prism -const delta=0.01 --buildfull --exportbuild robot.drn; cat robot.drn; rm robot.drn
$STORMBIN/storm --prism $TESTFILES/imdp/robot.prism -const delta=0.1 --buildfull --prop 'Pmax=? [F "goal1"]' --minmax:method vi;

$STORMBIN/storm-pars --prism $TESTFILES/pdtmc/parametric_die_2.pm --prop 'P=? [ F "one" ]' --mode solutionfunction
$STORMBIN/storm-pars --prism $TESTFILES/pdtmc/parametric_die_2.pm --prop 'P=? [ F "one" ]' --mode solutionfunction --engine dd

$STORMBIN/storm-pomdp --prism $TESTFILES/pomdp/maze2.prism -const sl=0 --prop 'Rmin=? [F "goal"]' --buildfull --belief-exploration
$STORMBIN/storm-pomdp --prism $TESTFILES/pomdp/maze2.prism -const sl=0 --prop 'Rmin=? [F "goal"]' --buildfull --belief-exploration --exact


echo "done"

Originally posted by @tquatmann in #739 (comment)

[tquatmann]

Here is another snippet for testing DRN import/export that might be useful (taken from #862 )

mkdir -p tmp
rm tmp/*

set -e
STORM=./build/bin/storm
EXAMPLES=./resources/examples/testfiles

# brp (DTMC)

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-double.drn
grep double tmp/brp-double.drn
$STORM -drn tmp/brp-double.drn
$STORM -drn tmp/brp-double.drn --exact
$STORM -drn tmp/brp-double.drn --parametric

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-double.drn.xz
$STORM -drn tmp/brp-double.drn.xz

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-double.drn.gz
$STORM -drn tmp/brp-double.drn.gz

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-exact.drn --exact
grep rational tmp/brp-exact.drn
$STORM -drn tmp/brp-exact.drn
$STORM -drn tmp/brp-exact.drn --exact
$STORM -drn tmp/brp-exact.drn --parametric

# polling (MA)

$STORM --prism $EXAMPLES/ma/polling.ma -const N=3,Q=3 --exportbuild tmp/pol-double.drn --buildchoicelab
grep double tmp/pol-double.drn
$STORM -drn tmp/pol-double.drn
$STORM -drn tmp/pol-double.drn --buildchoicelab
$STORM -drn tmp/pol-double.drn --exact
$STORM -drn tmp/pol-double.drn --parametric

# robot (IMDP)
$STORM --prism $EXAMPLES/imdp/robot.prism -const delta=0.5 --exportbuild tmp/robot-double.drn
grep "double-interval" tmp/robot-double.drn
$STORM -drn tmp/robot-double.drn

# nand (PDTMC)
$STORM --prism $EXAMPLES/pdtmc/nand-5-2.pm --exportbuild tmp/nand-par.drn --parametric
grep "parametric" tmp/nand-par.drn
$STORM -drn tmp/nand-par.drn --parametric

[tquatmann]

Similarly for UMB (#875 )

mkdir -p tmp
rm tmp/*

set -e
STORM=./cmake-build-debug/bin/storm
EXAMPLES=./resources/examples/testfiles

# brp (DTMC)

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-double.umb --buildfull
$STORM -umb tmp/brp-double.umb
$STORM -umb tmp/brp-double.umb --exact

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-double-none.umb --compression none
$STORM -umb tmp/brp-double-none.umb

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-double-xz.umb --compression xz
$STORM -umb tmp/brp-double-xz.umb

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-exact.umb --exact
$STORM -umb tmp/brp-exact.umb
$STORM -umb tmp/brp-exact.umb --exact

# polling (MA)

$STORM --prism $EXAMPLES/ma/polling.ma -const N=3,Q=3 --exportbuild tmp/pol-double.umb --buildchoicelab
$STORM -umb tmp/pol-double.umb
$STORM -umb tmp/pol-double.umb --buildchoicelab
$STORM -umb tmp/pol-double.umb --exact

# robot (IMDP)
$STORM --prism $EXAMPLES/imdp/robot.prism -const delta=0.5 --exportbuild tmp/robot-double.umb
$STORM -umb tmp/robot-double.umb

# maze (POMDP
$STORM --prism $EXAMPLES/pomdp/maze2.prism -const sl=0.5 --exportbuild tmp/maze2-double.umb --buildfull --buildchoicelab
$STORM -umb tmp/maze2-double.umb --buildchoicelab

$STORM --prism $EXAMPLES/pomdp/maze2.prism -const sl=0.5 --exportbuild tmp/maze2-rational.umb --exact --buildfull --buildchoicelab
$STORM -umb tmp/maze2-rational.umb --buildchoicelab