// Trivial test of parametric model checking
// (also tests a bugfix in the results testing when the result is just a lone parameter)

dtmc

const double p;

module M

	// local state
	s : [0..7] init 0;
	
	[] s=0 -> p : (s'=1) + 1-p : (s'=2);
	[] s>0 -> true;
	
endmodule