// Running example MDP (see Figure 2, p.6)
// and DRA for LTL property "F G go" (see Figure 10, p.36)

mdp

// MDP M
module M

	// s=i for state s_i
	s : [0..3];
	
	[go] s=0 -> (s'=1);
	[safe] s=1 -> 0.7:(s'=0) + 0.3:(s'=2);
	[risk] s=1 -> 0.5:(s'=2) + 0.5:(s'=3);
	[finish] s=2 -> (s'=2);
	[stop] s=3 -> (s'=3);
	[reset] s=3 -> (s'=0);

endmodule

// DRA A_ltl for LTL property "F G go"
// This is encoded as a PRISM module to allow action-based LTL 
// model checking: PRISM only supports state-based LTL currently
module A_ltl

	// q=i for state q_i
	q : [0..1] init 0;

	[go] q=0 -> (q'=1);
	[safe] q=0 -> (q'=0);
	[risk] q=0 -> (q'=0);
	[finish] q=0 -> (q'=0);
	[stop] q=0 -> (q'=0);
	[reset] q=0 -> (q'=0);

	[go] q=1 -> (q'=1);
	[safe] q=1 -> (q'=0);
	[risk] q=1 -> (q'=0);
	[finish] q=1 -> (q'=0);
	[stop] q=1 -> (q'=0);
	[reset] q=1 -> (q'=0);

endmodule

// Accepting pair (L_1,K_1) = ({q_0},{q_1}) for the DRA
label "L1" = q=0;
label "K1" = q=1;