/* This example adapted from M.K. Molloy's IEEE TC paper */

# include	"user.h"

parameters() {
	int i;

	iopt(IOP_METHOD,VAL_GASEI);
	iopt(IOP_PR_FULL_MARK,VAL_YES);
	iopt(IOP_PR_MARK_ORDER,VAL_CANONIC);
	iopt(IOP_PR_MC_ORDER,VAL_TOFROM);
	iopt(IOP_PR_MC,VAL_YES);
	iopt(IOP_PR_PROB,VAL_YES);
	iopt(IOP_MC,VAL_CTMC);
	iopt(IOP_PR_RSET,VAL_YES);
	iopt(IOP_PR_RGRAPH,VAL_YES);
	iopt(IOP_ITERATIONS,20000);
	fopt(FOP_ABS_RET_M0,0.0);
	fopt(FOP_PRECISION,0.00000001);

}

net() {
	place("p0");
	init("p0",1);
	place("p1");
	place("p2");
	place("p3");
	place("p4");

	trans("t0");
	trans("t1");
	trans("t2");
	trans("t3");
	trans("t4");
	rateval("t0",1.0);
	rateval("t1",3.0);
	rateval("t2",7.0);
	rateval("t3",9.0);
	rateval("t4",5.0);

	iarc("t0","p0");	oarc("t0","p1");	oarc("t0","p2");
	iarc("t1","p1");	oarc("t1","p3");
	iarc("t2","p2");	oarc("t2","p4");
	iarc("t3","p3");	oarc("t3","p1");
	iarc("t4","p3");	iarc("t4","p4");	oarc("t4","p0");
}

assert() {
	if (mark("p3") > 5)
		return(RES_ERROR);
	else	
		return(RES_NOERR);
}

ac_init() {
	fprintf(stderr,"\nExample from Molloy's Thesis\n\n");
	pr_net_info(); /* information on the net structure */
}

ac_reach() {
	fprintf(stderr,"\nThe reachability graph has been generated\n\n");
	pr_rg_info(); /* information on the reachability graph */
}

/* general marking dependent reward functions */
reward_type	ef0() { return(mark("p0")); }
reward_type	ef1() { return(mark("p1")); }
reward_type	ef2() { return(rate("t2")); }
reward_type	ef3() { return(rate("t3")); }
reward_type	eff() { return(rate("t1") * 1.8 + mark("p3") * 0.7); }

ac_final() {
	pr_mc_info(); /* information about the Markov chain */
	pr_expected("mark(p0)",ef0);
	pr_expected("mark(p1)",ef1);
	pr_expected("rate(t2)",ef2);
	pr_expected("rate(t3)",ef3);
	pr_expected("rate(t1) * 1.8 + mark(p3) * 0.7",eff);
	pr_std_average(); /* default measures */
}