Tempest_in_Action/tempest-devel/resources/examples/testfiles/ma/jobscheduler.drn

// Exported by storm
// Original model type: Markov Automaton
@type: Markov Automaton
@parameters

@reward_models
avg_waiting_time 
@nr_states
17
@model
state 0 !0 [1] init
	action 0 [0]
		1 : 1
	action 1 [0]
		2 : 1
	action 2 [0]
		3 : 1
state 1 !3 [1]
	action 0 [0]
		4 : 0.333333
		5 : 0.666667
state 2 !4 [1]
	action 0 [0]
		4 : 0.25
		6 : 0.75
state 3 !5 [1]
	action 0 [0]
		5 : 0.4
		6 : 0.6
state 4 !0 [0.666667] one_job_finished slowest_before_fastest
	action 0 [0]
		7 : 1
state 5 !0 [0.666667] one_job_finished
	action 0 [0]
		8 : 1
state 6 !0 [0.666667] one_job_finished
	action 0 [0]
		9 : 1
state 7 !5 [0.666667] one_job_finished slowest_before_fastest
	action 0 [0]
		10 : 0.4
		11 : 0.6
state 8 !4 [0.666667] one_job_finished
	action 0 [0]
		10 : 0.25
		12 : 0.75
state 9 !3 [0.666667] one_job_finished
	action 0 [0]
		11 : 0.333333
		12 : 0.666667
state 10 !0 [0.333333] half_of_jobs_finished slowest_before_fastest
	action 0 [0]
		13 : 1
state 11 !0 [0.333333] half_of_jobs_finished
	action 0 [0]
		14 : 1
state 12 !0 [0.333333] half_of_jobs_finished
	action 0 [0]
		15 : 1
state 13 !3 [0.333333] half_of_jobs_finished slowest_before_fastest
	action 0 [0]
		16 : 1
state 14 !2 [0.333333] half_of_jobs_finished
	action 0 [0]
		16 : 1
state 15 !1 [0.333333] half_of_jobs_finished
	action 0 [0]
		16 : 1
state 16 !1 [0] all_jobs_finished deadlock
	action 0 [0]
		16 : 1