Model	Type	Original	Parameters	Property	Type	Storm.sparse	Storm.hybrid	Storm.dd	Storm.ddbisim	Storm.sound	Storm.exact	Storm.automatic
beb	MDP	Modest	4-8-7	LineSeized	P	104.9	15.9	27.0	21.9	117.7	332.2	15.9
beb	MDP	Modest	5-16-15	LineSeized	P	MO	TO	TO	MO	MO	MO	TO
bitcoin-attack	MA	Modest	20-6	P_MWinMax	Pb	0.1	0.5	NS	1.0	0.1	NS	1.0
bluetooth	DTMC	PRISM	1	time	E	TO	MO	6.6	6.7	TO	TO	6.9
cabinets	MA	Galileo	3-2-true	Unavailability	S	36.6	57.7	NS	MO	38.3	MO	36.5
cabinets	MA	Galileo	3-2-true	Unreliability	Pb	23.9	29.9	NS	24.6	25.1	NS	25.4
cluster	CTMC	PRISM	128-2000-20	premium_steady	S	27.3	6.9	NS	54.3	91.7	MO	29.3
cluster	CTMC	PRISM	128-2000-20	qos1	Pb	78.5	67.9	NS	100.7	195.5	NS	79.5
cluster	CTMC	PRISM	64-2000-20	below_min	Eb	109.1	133.2	NS	149.0	386.2	NS	123.9
consensus	MDP	PRISM	4-4	disagree	P	0.8	2.1	72.1	1.8	14.3	9.4	0.9
consensus	MDP	PRISM	4-4	steps_min	E	1.3	3.4	20.6	1.6	3.7	3.4	1.3
consensus	MDP	PRISM	6-2	disagree	P	23.2	26.3	152.9	3.6	175.8	TO	3.6
consensus	MDP	PRISM	6-2	steps_min	E	29.7	51.9	57.9	2.3	112.2	TO	2.3
coupon	DTMC	PGCL	15-4-5	collect_all_bounded	Pb	MO	NS	NS	980.9	MO	MO	929.0
coupon	DTMC	PGCL	15-4-5	exp_draws	E	MO	MO	TO	771.1	MO	MO	812.8
coupon	DTMC	PGCL	9-4-5	collect_all_bounded	Pb	MO	NS	NS	2.4	MO	MO	2.4
coupon	DTMC	PGCL	9-4-5	exp_draws	E	124.1	91.0	89.4	2.1	136.2	MO	2.1
crowds	DTMC	PRISM	5-20	positive	P	10.6	6.0	3.4	1.2	10.1	46.2	1.3
crowds	DTMC	PRISM	6-20	positive	P	72.5	47.0	5.3	1.3	70.8	279.1	1.3
csma	MDP	PRISM	3-4	all_before_max	P	10.6	3.4	8.1	10.9	11.2	25.8	3.3
csma	MDP	PRISM	3-4	time_max	E	10.9	5.1	138.2	7.5	10.9	52.1	5.3
csma	MDP	PRISM	4-2	all_before_max	P	6.4	3.6	17.0	5.6	7.4	17.5	3.6
csma	MDP	PRISM	4-2	time_max	E	6.6	3.7	97.6	5.2	6.6	19.8	3.7
dpm	MA	Modest	4-8-5	PmaxQueuesFullBound	Pb	34.9	999.6	NS	29.5	32.7	NS	29.9
dpm	MA	Modest	6-6-5	PminQueue1Full	P	39.4	44.4	NS	TO	69.6	MO	40.5
eajs	MDP	PRISM	5-250-11	ExpUtil	E	36.8	15.5	61.4	11.9	38.2	95.1	12.0
eajs	MDP	PRISM	6-300-13	ExpUtil	E	119.0	48.3	200.6	27.8	118.7	298.9	27.6
echoring	MDP	Modest	100	MaxOffline1	P	36.3	NS	NS	NS	35.4	135.2	35.4
egl	DTMC	PRISM	10-2	messagesB	E	581.0	456.3	0.9	1.4	MO	MO	1.4
egl	DTMC	PRISM	10-2	unfairA	P	478.8	0.6	0.7	1.7	485.8	MO	1.7
egl	DTMC	PRISM	10-8	messagesB	E	MO	MO	14.0	9.1	MO	MO	9.0
egl	DTMC	PRISM	10-8	unfairA	P	MO	1.3	1.3	17.3	MO	MO	16.6
elevators	MDP	PPDDL	b-11-9	goal	P	5.7	MO	MO	MO	5.7	21.0	5.5
embedded	CTMC	PRISM	8-12	actuators	P	0.1	0.5	NS	0.8	0.8	0.5	0.1
embedded	CTMC	PRISM	8-12	up_time	E	0.1	0.5	NS	0.7	0.8	0.6	0.1
exploding-blocksworld	MDP	PPDDL	10	goal	P	MO	MO	MO	MO	MO	MO	MO
firewire-pta	PTA	PRISM	30-5000	eventually	P	73.0	NS	NS	NS	73.0	176.8	73.5
firewire	MDP	PRISM	false-36-800	deadline	Pb	22.5	NS	NS	17.5	21.2	231.9	18.6
fms	CTMC	PRISM	8	productivity	S	87.4	87.6	NS	TO	TO	MO	78.0
ftpp	MA	Galileo	2-2-true	Unavailability	S	MO	MO	MO	MO	MO	MO	MO
ftwc	MA	Modest	8-5	TimeMax	E	INC	NS	NS	NS	30.6	1588.4	INC
ftwc	MA	Modest	8-5	TimeMin	E	INC	NS	NS	NS	25.9	TO	INC
haddad-monmege	DTMC	PRISM	100-0.7	exp_steps	E	INC	INC	INC	INC	INC	0.1	0.1
haddad-monmege	DTMC	PRISM	100-0.7	target	P	INC	INC	INC	INC	INC	0.1	0.1
hecs	MA	Galileo	false-1-1	Unreliability	Pb	0.2	1.1	NS	1.9	0.2	NS	0.2
hecs	MA	Galileo	false-2-2	Unreliability	Pb	38.2	137.5	NS	MO	38.2	NS	39.0
hecs	MA	Galileo	false-3-2	Unreliability	Pb	MO	MO	MO	MO	MO	MO	MO
herman	DTMC	PRISM	15	steps	E	16.1	2.6	72.0	1.9	16.2	TO	2.8
kanban	CTMC	PRISM	5	throughput	S	45.5	31.5	NS	TO	154.9	MO	29.2
majority	CTMC	PRISM	2100	change_state	Pb	24.0	54.0	NS	58.1	61.5	NS	24.1
mapk_cascade	CTMC	PRISM	4-30	activated_time	E	2.6	2.6	NS	7.7	8.5	TO	2.6
mapk_cascade	CTMC	PRISM	4-30	reactions	Eb	105.3	101.6	NS	106.6	109.9	NS	112.3
nand	DTMC	PRISM	40-4	reliable	P	13.4	6.0	39.1	677.9	13.3	67.3	5.6
nand	DTMC	PRISM	60-4	reliable	P	60.8	26.1	TO	TO	67.0	MO	25.8
oscillators	DTMC	PRISM	8-10-0.1-1-0.1-1.0	power_consumption	E	112.2	MO	MO	MO	138.7	238.6	149.5
oscillators	DTMC	PRISM	8-10-0.1-1-0.1-1.0	time_to_synch	E	137.6	MO	MO	MO	125.6	213.6	125.6
pacman	MDP	PRISM	100	crash	P	289.7	47.5	232.8	MO	291.1	456.6	50.3
pacman	MDP	PRISM	60	crash	P	131.0	20.4	28.0	MO	123.2	178.8	20.8
philosophers	CTMC	GreatSPN	16-1	MaxPrReachDeadlock	P	23.1	0.7	NS	131.9	22.5	120.2	0.7
philosophers	CTMC	GreatSPN	16-1	MaxPrReachDeadlockTB	Pb	38.7	24.6	NS	143.1	51.6	NS	25.0
philosophers	CTMC	GreatSPN	16-1	MinExpTimeDeadlock	E	29.0	15.9	NS	142.3	58.4	TO	16.0
philosophers	CTMC	GreatSPN	20-1	MaxPrReachDeadlock	P	MO	0.9	NS	MO	MO	MO	0.9
philosophers	CTMC	GreatSPN	20-1	MaxPrReachDeadlockTB	Pb	MO	MO	NS	MO	MO	MO	MO
philosophers	CTMC	GreatSPN	20-1	MinExpTimeDeadlock	E	MO	MO	NS	MO	MO	MO	MO
pnueli-zuck	MDP	PRISM	10	live	P	MO	1.1	1.1	MO	MO	MO	1.1
pnueli-zuck	MDP	PRISM	5	live	P	3.2	0.6	0.6	2.3	3.0	8.6	0.6
polling	CTMC	PRISM	18-16	s1_before_s2	P	104.8	10.2	NS	MO	225.7	MO	10.2
rabin	MDP	PRISM	10	live	P	MO	0.9	0.9	4.9	MO	MO	0.9
readers-writers	MA	GreatSPN	40	exp_time_many_requests	E	19.0	53.1	NS	MO	78.8	MO	18.0
readers-writers	MA	GreatSPN	40	prtb_many_requests	Pb	310.3	286.1	NS	MO	324.9	NS	286.0
rectangle-tireworld	MDP	PPDDL	11	goal	P	13.1	18.8	17.6	18.2	13.1	13.0	13.6
resource-gathering	MDP	PRISM	1300-100-100	expgold	Eb	35.8	25.8	1.0	1.3	35.6	TO	26.4
resource-gathering	MDP	PRISM	1300-100-100	expsteps	E	15.4	14.5	112.7	312.9	53.4	100.3	17.0
resource-gathering	MDP	PRISM	1300-100-100	prgoldgem	Pb	63.6	23.9	18.5	349.0	63.1	TO	26.9
sms	MA	Galileo	3-true	Unavailability	S	10.3	7.5	NS	99.7	10.4	44.4	7.6
sms	MA	Galileo	3-true	Unreliability	Pb	0.1	0.7	NS	1.5	0.1	NS	0.1
speed-ind	CTMC	PRISM	2100	change_state	Pb	100.6	110.2	NS	204.0	282.7	NS	110.2
stream	MA	PRISM-MA	1000	exp_buffertime	E	7.8	9.3	NS	218.8	6.3	25.6	7.8
stream	MA	PRISM-MA	1000	pr_underrun	P	1.8	4.4	NS	107.1	2.0	6.5	1.8
stream	MA	PRISM-MA	1000	pr_underrun_tb	Pb	5.0		NS	119.8	5.3	NS	5.4
tireworld	MDP	PPDDL	45	goal	P	TO	TO	1310.1	MO	TO	MO	TO
triangle-tireworld	MDP	PPDDL	441	goal	P	MO	TO	MO	MO	MO	MO	MO
vgs	MA	Galileo	5-10000	MaxPrReachFailedTB	Pb	TO	TO	TO	TO	MO	TO	TO
vgs	MA	Galileo	5-10000	MinExpTimeFailed	E	MO	TO	MO	TO	MO	TO	MO
wlan-large	PTA	Modest	2	E_or	E	31.2	NS	NS	NS	35.2	122.5	31.5
wlan-large	PTA	Modest	2	P_max	P	4.9	NS	NS	NS	5.1	18.8	5.0
wlan	MDP	PRISM	4-0	cost_min	E	2.8	2.7	19.6	124.0	3.2	8.1	2.5
wlan	MDP	PRISM	4-0	sent	P	2.3	1.1	1.1	131.7	2.3	5.2	1.1
wlan	MDP	PRISM	5-0	cost_min	E	11.3	7.1	75.4	863.0	11.0	28.4	7.8
wlan	MDP	PRISM	5-0	sent	P	8.4	1.8	1.8	840.4	8.5	19.5	1.7
wlan	MDP	PRISM	6-0	cost_min	E	48.4	29.5	315.7	TO	46.3	115.6	30.2
wlan	MDP	PRISM	6-0	sent	P	35.7	3.2	3.2	TO	35.1	79.6	3.0
zenotravel	MDP	PPDDL	4-2-2	goal	P	11.6	4.0	3.9	19.4	10.8	24.6	4.1
zeroconf-pta	PTA	PRISM	200	incorrect	P	0.1	NS	NS	NS	0.1	0.1	0.1
zeroconf	MDP	PRISM	1000-8-false	correct_max	P	17.4	18.4	268.6	120.1	23.7	TO	17.2
zeroconf	MDP	PRISM	1000-8-false	correct_min	P	14.0	16.0	672.6	118.4	26.0	47.4	13.1