package prism_config

constants C_fair_MD10_MS20_100:
	SRWMod::SRWRP::MaxDist set to 10, 
	SRWMod::SRWRP::MaxSteps from set {20 to 100 by step 10}, and
	SRWMod::SRWRP::Pl set to 0.5
	
constants C_biased_MD10_MS20_100:
	SRWMod::SRWRP::MaxDist set to 10, 
	SRWMod::SRWRP::MaxSteps from set {20 to 100 by step 10}, and
	SRWMod::SRWRP::Pl from set {0.1, 0.3, 0.6, 0.8}
	
defs D_no_recharge:
	pfunction Plus(v, maxv) = {
		return (if (($$v) < ($$maxv)) then ($$v+1) else ($$v) end)
	}
	
	pfunction Minus(v, minv) = {
		return (if (($$v) > ($$minv)) then ($$v-1) else ($$v) end)
	}
	
	pfunction Update(v, maxv, origin) = {
		return (if (($$v) < ($$maxv)) then ($$v+1) else ($$v) end)
	}
	
defs D_recharge:
	pfunction Plus(v, maxv) = {
		return (if (($$v) < ($$maxv)) then ($$v+1) else ($$v) end)
	}
	
	pfunction Minus(v, minv) = {
		return (if (($$v) > ($$minv)) then ($$v-1) else ($$v) end)
	}
	
	pfunction Update(v, maxv, origin) = {
		return (if $$origin then 0 else 
				(if (($$v) < ($$maxv)) then ($$v+1) else ($$v) end)
			end)
	}
	

package SRW_properties

import prism_config::*

label l_stuck = 
	SRWMod::ctrl_ref::stm_ref is in 
		SRWMod::ctrl_ref::stm_ref::Stuck
		
label l_origin = (SRWMod::SRWRP::x == 0)
		
prob property P_deadlock_free:
	not Exists [Finally deadlock]
	with constants C_fair_MD10_MS20_100
	with definitions D_no_recharge
	
prob property P_stuck_not_origin:
	Prob=? of [Finally 
		#l_stuck /\ not #l_origin
	]
	with constants C_fair_MD10_MS20_100
	with definitions D_no_recharge
	
prob property P_stuck_not_origin_recharge:
	Prob=? of [Finally 
		#l_stuck /\ not #l_origin
	]
	with constants C_fair_MD10_MS20_100
	with definitions D_recharge
	
prob property P_stuck_not_origin_biased:
	Prob=? of [Finally 
		#l_stuck /\ not #l_origin
	]
	with constants C_biased_MD10_MS20_100
	with definitions D_no_recharge
	
rewards R_origins = 
	[ SRWMod::ctrl_ref::stm_ref::left.out ] (SRWMod::SRWRP::x == 0) : 1;
	[ SRWMod::ctrl_ref::stm_ref::right.out ] (SRWMod::SRWRP::x == 0) : 1;
endrewards

prob property R_stuck_not_origin:
	Reward {R_origins} =? of [Reachable 
		#l_stuck /\ not #l_origin
	]
	with constants C_fair_MD10_MS20_100
	with definitions D_no_recharge
	
prob property R_stuck_not_origin_recharge:
	Reward {R_origins} =? of [Reachable 
		#l_stuck /\ not #l_origin
	]
	with constants C_fair_MD10_MS20_100
	with definitions D_recharge
	
prob property R_stuck_not_origin_biased:
	Reward {R_origins} =? of [Reachable 
		#l_stuck /\ not #l_origin
	]
	with constants C_biased_MD10_MS20_100
	with definitions D_no_recharge

/*	
rewards R_l = 
	[ SRWMod::ctrl_ref::stm_ref::left.out ] true : 1;
endrewards

rewards R_r = 
	[ SRWMod::ctrl_ref::stm_ref::right.out ] true : 1;
endrewards
*/