#############################################################
	PARAM
#############################################################

For all benchmark models <M> and considered properties <P> we ran the following set of experiments: 

# elimination order: backward, bisimulation: strong, weak, none
./param <M> <P> --lump-method strong --elimination-order backward-opt
./param <M> <P> --lump-method weak --elimination-order backward-opt
./param <M> <P> --lump-method none --elimination-order backward-opt

# elimination order: forward, bisimulation: strong, weak, none
./param <M> <P> --lump-method strong --elimination-order forward
./param <M> <P> --lump-method weak --elimination-order forward
./param <M> <P> --lump-method none --elimination-order forward

# elimination order: forward-reversed, bisimulation: strong, weak, none
./param <M> <P> --lump-method strong --elimination-order forward-reversed
./param <M> <P> --lump-method weak --elimination-order forward-reversed
./param <M> <P> --lump-method none --elimination-order forward-reversed

Note: PARAM supports the elimination orders "backward-opt", "forward", "forward-reversed" and "random" and the bisimulation settings "none", "strong" and "weak".
We have not considered "random" as the elimination order, as results would be nondeterminstic and not reproducible.

#############################################################
	PRISM
#############################################################

For all benchmark models <M> (with parameters <p> and <q>) and considered properties <P> we ran the following set of experiments: 

# elimination order: backward, bisimulation: strong, weak, none
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder bw -parambisim strong
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder bw -parambisim weak
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder bw -parambisim none

# elimination order: backward-reversed, bisimulation: strong, weak, none
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder bwrev -parambisim strong
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder bwrev -parambisim weak
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder bwrev -parambisim none

# elimination order: forward, bisimulation: strong, weak, none
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder fw -parambisim strong
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder fw -parambisim weak
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder fw -parambisim none

# elimination order: forward-reversed, bisimulation: strong, weak, none
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder fwrev -parambisim strong
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder fwrev -parambisim weak
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder fwrev -parambisim none

# elimination order: arbitrary, bisimulation: strong, weak, none
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder arb -parambisim strong
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder arb -parambisim weak
./bin/prism <M> <P> -param <p>=0:1,<q>=0:1 -paramelimorder arb -parambisim none

Note: PARAM supports the elimination orders "bw", "bwrev", "fw", "fwrev", "arb" and "rand" (random) and the bisimulation settings "none", "strong" and "weak".
We have not considered "rand" as the elimination order, as results would be nondeterminstic and not reproducible.

#############################################################
	PROPhESY (the core model checker is called "pstorm")
#############################################################

For all benchmark models <M> (with parameters <p> and <q>) and considered properties <P> we ran the following set of experiments: 

# elimination order: backward, bisimulation: strong, weak, none
./pstorm --symbolic <M> --prop <P> --bisimulation --bisimulation:type strong --sparseelim:order bw --sparseelim:method state
./pstorm --symbolic <M> --prop <P> --bisimulation --bisimulation:type weak --sparseelim:order bw --sparseelim:method state
./pstorm --symbolic <M> --prop <P> --sparseelim:order bw --sparseelim:method state

# elimination order: backward-reversed, bisimulation: strong, weak, none
./pstorm --symbolic <M> --prop <P> --bisimulation --bisimulation:type strong --sparseelim:order bwrev --sparseelim:method state
./pstorm --symbolic <M> --prop <P> --bisimulation --bisimulation:type weak --sparseelim:order bwrev --sparseelim:method state
./pstorm --symbolic <M> --prop <P> --sparseelim:order bwrev --sparseelim:method state

# elimination order: forward, bisimulation: strong, weak, none
./pstorm --symbolic <M> --prop <P> --bisimulation --bisimulation:type strong --sparseelim:order fw --sparseelim:method state
./pstorm --symbolic <M> --prop <P> --bisimulation --bisimulation:type weak --sparseelim:order fw --sparseelim:method state
./pstorm --symbolic <M> --prop <P> --sparseelim:order fw --sparseelim:method state

# elimination order: forward-reversed, bisimulation: strong, weak, none
./pstorm --symbolic <M> --prop <P> --bisimulation --bisimulation:type strong --sparseelim:order fwrev --sparseelim:method state
./pstorm --symbolic <M> --prop <P> --bisimulation --bisimulation:type weak --sparseelim:order fwrev --sparseelim:method state
./pstorm --symbolic <M> --prop <P> --sparseelim:order fwrev --sparseelim:method state

Note: pstorm supports the elimination orders "bw", "bwrev", "fw", "fwrev" and "rand" (random) and the bisimulation settings "none", "strong" and "weak".
We have not considered "rand" as the elimination order, as results would be nondeterminstic and not reproducible.

#############################################################
  Conditional Probabilities (double; non-parametric!)
#############################################################

#############################################################
	PROPhESY (the non-parametric model checker is called "storm")
#############################################################

For all benchmark models <M> and considered properties <P> we ran the following set of experiments: 

# elimination order: backward, bisimulation: strong, weak, none
./storm --symbolic <M> --prop <P> --bisimulation --bisimulation:type strong --sparseelim:order bw --sparseelim:method state
./storm --symbolic <M> --prop <P> --bisimulation --bisimulation:type weak --sparseelim:order bw --sparseelim:method state
./storm --symbolic <M> --prop <P> --sparseelim:order bw --sparseelim:method state

# elimination order: backward-reversed, bisimulation: strong, weak, none
./storm --symbolic <M> --prop <P> --bisimulation --bisimulation:type strong --sparseelim:order bwrev --sparseelim:method state
./storm --symbolic <M> --prop <P> --bisimulation --bisimulation:type weak --sparseelim:order bwrev --sparseelim:method state
./storm --symbolic <M> --prop <P> --sparseelim:order bwrev --sparseelim:method state

# elimination order: forward, bisimulation: strong, weak, none
./storm --symbolic <M> --prop <P> --bisimulation --bisimulation:type strong --sparseelim:order fw --sparseelim:method state
./storm --symbolic <M> --prop <P> --bisimulation --bisimulation:type weak --sparseelim:order fw --sparseelim:method state
./storm --symbolic <M> --prop <P> --sparseelim:order fw --sparseelim:method state

# elimination order: forward-reversed, bisimulation: strong, weak, none
./storm --symbolic <M> --prop <P> --bisimulation --bisimulation:type strong --sparseelim:order fwrev --sparseelim:method state
./storm --symbolic <M> --prop <P> --bisimulation --bisimulation:type weak --sparseelim:order fwrev --sparseelim:method state
./storm --symbolic <M> --prop <P> --sparseelim:order fwrev --sparseelim:method state

#############################################################
	PRISM
#############################################################

For all benchmark models <M> and considered properties <P> we ran the following set of experiments: 

./bin/prism <M> <P> -sparse

#############################################################
	Baier et al. (based on PRISM 4.1)
#############################################################

For all benchmark models <M> and considered properties <P> we ran the following set of experiments: 

./bin/prism <M> <P> -explicit -fixdl -gs