Model	Type	Original	Parameters	Property	Type	Storm	Storm-static
bluetooth	DTMC	PRISM	1	time	E	11.4	TO / 12.8
coupon	DTMC	PGCL	9-4-5	collect_all_bounded	Pb	5.0	TO / 4.7
coupon	DTMC	PGCL	9-4-5	exp_draws	E	4.2	TO / 4.5
coupon	DTMC	PGCL	15-4-5	collect_all_bounded	Pb	1256.3	TO / 1333.7
coupon	DTMC	PGCL	15-4-5	exp_draws	E	631.8	TO / 609.0
crowds	DTMC	PRISM	5-20	positive	P	2.7	64.6 / 2.9
crowds	DTMC	PRISM	6-20	positive	P	3.1	398.2 / 3.1
egl	DTMC	PRISM	10-2	messagesB	E	6.3	TO / 5.9
egl	DTMC	PRISM	10-2	unfairA	P	3.9	TO / 2.0
egl	DTMC	PRISM	10-8	messagesB	E	23.1	TO / 21.3
egl	DTMC	PRISM	10-8	unfairA	P	27.0	TO / 3.6
haddad-monmege	DTMC	PRISM	100-0.7	exp_steps	E	0.1	0.1 / 0.1
haddad-monmege	DTMC	PRISM	100-0.7	target	P	0.1	0.1 / 0.1
herman	DTMC	PRISM	15	steps	E	TO	TO / 53.6
nand	DTMC	PRISM	40-4	reliable	P	61.8	85.1 / 63.2
nand	DTMC	PRISM	60-4	reliable	P	1085.0	1361.9 / 1093.5
oscillators	DTMC	PRISM	8-10-0.1-1-0.1-1.0	power_consumption	E	379.6	363.5
oscillators	DTMC	PRISM	8-10-0.1-1-0.1-1.0	time_to_synch	E	381.7	362.5
cluster	CTMC	PRISM	128-2000-20	premium_steady	S	TO	TO
cluster	CTMC	PRISM	128-2000-20	qos1	Pb
cluster	CTMC	PRISM	64-2000-20	below_min	Eb
embedded	CTMC	PRISM	8-12	actuators	P	0.7	0.7 / 0.7
embedded	CTMC	PRISM	8-12	up_time	E	0.7	0.7 / 0.7
fms	CTMC	PRISM	8	productivity	S	TO	TO
kanban	CTMC	PRISM	5	throughput	S	TO	TO / TO
majority	CTMC	PRISM	2100	change_state	Pb
mapk_cascade	CTMC	PRISM	4-30	activated_time	E	TO	TO
mapk_cascade	CTMC	PRISM	4-30	reactions	Eb
philosophers	CTMC	GreatSPN	16-1	MaxPrReachDeadlockTB	Pb
philosophers	CTMC	GreatSPN	16-1	MaxPrReachDeadlock	P	1.8	152.7 / 1.5
philosophers	CTMC	GreatSPN	16-1	MinExpTimeDeadlock	E	TO	TO / TO
philosophers	CTMC	GreatSPN	20-1	MaxPrReachDeadlockTB	Pb
philosophers	CTMC	GreatSPN	20-1	MaxPrReachDeadlock	P	2.2	TO / 2.3
philosophers	CTMC	GreatSPN	20-1	MinExpTimeDeadlock	E	ERR	TO
polling	CTMC	PRISM	18-16	s1_before_s2	P	ERR	TO / ERR
speed-ind	CTMC	PRISM	2100	change_state	Pb
beb	MDP	Modest	4-8-7	LineSeized	P	61.8	432.9 / 62.9
beb	MDP	Modest	5-16-15	LineSeized	P	TO	TO
consensus	MDP	PRISM	4-4	disagree	P	12.1	12.5
consensus	MDP	PRISM	4-4	steps_min	E	4.4	4.4
consensus	MDP	PRISM	6-2	disagree	P	6.7	TO / 6.8
consensus	MDP	PRISM	6-2	steps_min	E	3.7	TO / 3.7
csma	MDP	PRISM	3-4	all_before_max	P	10.1	35.7 / 10.0
csma	MDP	PRISM	3-4	time_max	E	26.6	76.3 / 25.3
csma	MDP	PRISM	4-2	all_before_max	P	11.6	21.6 / 10.2
csma	MDP	PRISM	4-2	time_max	E	13.9	26.9 / 12.9
eajs	MDP	PRISM	5-250-11	ExpUtil	E	19.8	140.6 / 18.8
eajs	MDP	PRISM	6-300-13	ExpUtil	E	46.5	435.6 / 44.3
echoring	MDP	Modest	100	MaxOffline1	P	179.7	180.5
elevators	MDP	PPDDL	b-11-9	goal	P	29.0	29.5
exploding-blocksworld	MDP	PPDDL	10	goal	P	TO	TO
firewire	MDP	PRISM	false-36-800	deadline	Pb	60.5	296.9 / 60.6
pacman	MDP	PRISM	100	crash	P	111.2	832.9 / 113.9
pacman	MDP	PRISM	60	crash	P	42.3	361.3 / 39.7
pnueli-zuck	MDP	PRISM	5	live	P	0.9	11.5 / 0.9
pnueli-zuck	MDP	PRISM	10	live	P	2.3	TO / 2.4
rabin	MDP	PRISM	10	live	P	2.2	TO / 2.2
rectangle-tireworld	MDP	PPDDL	11	goal	P	23.1	23.1 / 23.0
resource-gathering	MDP	PRISM	1300-100-100	expgold	Eb	TO	TO / 2.1
resource-gathering	MDP	PRISM	1300-100-100	expsteps	E	120.4	120.4
resource-gathering	MDP	PRISM	1300-100-100	prgoldgem	Pb	TO	TO / TO
tireworld	MDP	PPDDL	45	goal	P	TO	TO
triangle-tireworld	MDP	PPDDL	441	goal	P	TO	TO
wlan	MDP	PRISM	4-0	sent	P	2.3	6.9 / 2.3
wlan	MDP	PRISM	4-0	cost_min	E	10.2	9.8 / 6.8
wlan	MDP	PRISM	5-0	sent	P	3.4	26.4 / 3.3
wlan	MDP	PRISM	5-0	cost_min	E	23.2	36.9 / 21.9
wlan	MDP	PRISM	6-0	sent	P	6.4	107.2 / 6.3
wlan	MDP	PRISM	6-0	cost_min	E	83.7	148.9 / 79.0
zenotravel	MDP	PPDDL	4-2-2	goal	P	7.5	41.7 / 6.9
zeroconf	MDP	PRISM	1000-8-false	correct_max	P	TO	TO
zeroconf	MDP	PRISM	1000-8-false	correct_min	P	55.1	55.3
bitcoin-attack	MA	Modest	20-6	P_MWinMax	Pb
cabinets	MA	Galileo	3-2-true	Unavailability	S	ERR	ERR
cabinets	MA	Galileo	3-2-true	Unreliability	Pb
dpm	MA	Modest	4-8-5	PmaxQueuesFullBound	Pb
dpm	MA	Modest	6-6-5	PminQueue1Full	P	TO	TO
ftpp	MA	Galileo	2-2-true	Unavailability	S	TO	TO
ftwc	MA	Modest	8-5	TimeMax	E	TO	TO
ftwc	MA	Modest	8-5	TimeMin	E	TO	TO
hecs	MA	Galileo	false-1-1	Unreliability	Pb
hecs	MA	Galileo	false-2-2	Unreliability	Pb
hecs	MA	Galileo	false-3-2	Unreliability	Pb
readers-writers	MA	GreatSPN	40	exp_time_many_requests	E	TO	TO
readers-writers	MA	GreatSPN	40	prtb_many_requests	Pb
sms	MA	Galileo	3-true	Unreliability	Pb
sms	MA	Galileo	3-true	Unavailability	S	26.0	54.9 / 24.1
stream	MA	PRISM-MA	1000	exp_buffertime	E	33.6	33.8
stream	MA	PRISM-MA	1000	pr_underrun	P	8.1	8.2
stream	MA	PRISM-MA	1000	pr_underrun_tb	Pb
vgs	MA	Galileo	5-10000	MaxPrReachFailedTB	Pb
vgs	MA	Galileo	5-10000	MinExpTimeFailed	E	0.2	0.2
firewire-pta	PTA	PRISM	30-5000	deadline	Pb
firewire-pta	PTA	PRISM	30-5000	eventually	P	263.4	264.9
repudiation_malicious	PTA	PRISM	20	deadline	Pb
repudiation_malicious	PTA	PRISM	20	eventually	P
wlan-large	PTA	Modest	2	E_or	E	148.8	149.7
wlan-large	PTA	Modest	2	P_max	P	24.6	24.9
zeroconf-pta	PTA	PRISM	200	deadline	Pb
zeroconf-pta	PTA	PRISM	200	incorrect	P	0.4	0.4 / 0.4