/* This example is adapted from the paper by Veeraraghavan and Trivedi on
hierarchical performance appearing in the Princeton workshop proceedings.
This corresponds to the task graph execution with two processors schedule A */
# include	"user.h"

parameters() {

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

}

enabling_type et4() { if ( mark("p3") == 1 ) return(0); else return(1); }
enabling_type et5() { if ( mark("p3") == 1 ) return(0); else return(1); }
enabling_type et6() { if ( mark("p2") >= 1  || mark("p3") >= 1 ||
                    mark("p4") >= 1  || mark("p5") >= 1 ||
                    mark("p8") >= 1 ) return(0);
		else return(1); }

net() {
	place("p1");
	init("p1",1);
	place("p2");
	place("p3");
	place("p4");
	place("p5");
	place("p6");
	place("p7");
	place("p8");
	place("p9");
	place("pfin");
	place("procsr");
	init("procsr",2);

	trans("t1");
	trans("t2");
	trans("t3");
	trans("t4");
	enabling("t4",et4);
	trans("t5");
	enabling("t5",et5);
	trans("t6");
	enabling("t6",et6);
	trans("t7");
	trans("t8");
	trans("t9");

	rateval("t1",1.0);
	rateval("t2",0.5);
	rateval("t3",1.0);
	rateval("t4",0.25);
	rateval("t5",0.25);
	rateval("t6",0.3333);
	rateval("t7",0.142857);
	rateval("t8",0.125);
	rateval("t9",1.0);

	iarc("t1","p1");	oarc("t1","p2");	oarc("t1","p3");
	iarc("t1","procsr");	oarc("t1","procsr");
	iarc("t2","p2");	oarc("t2","p4");	oarc("t2","p5");
	iarc("t2","procsr");	oarc("t2","procsr");
	iarc("t3","p3");	oarc("t3","p6");
	iarc("t3","procsr");	oarc("t3","procsr");
	iarc("t4","p4");	oarc("t4","p7");	oarc("t4","p8");
	iarc("t4","procsr");	oarc("t4","procsr");
	iarc("t5","p5");	oarc("t5","p7");	oarc("t5","p8");
	iarc("t5","procsr");	oarc("t5","procsr");
	iarc("t6","p6");	oarc("t6","p9");
	iarc("t6","procsr");	oarc("t6","procsr");
	miarc("t7","p7",2);	oarc("t7","p9");
	iarc("t7","procsr");	oarc("t7","procsr");
	miarc("t8","p8",2);	oarc("t8","p9");
	iarc("t8","procsr");	oarc("t8","procsr");
	miarc("t9","p9",3);	oarc("t9","pfin");
	iarc("t9","procsr");	oarc("t9","procsr");
}

assert() {
}

ac_init() {
	fprintf(stderr,"\nA Task Graph from Princeton Paper\n\n");
	pr_net_info();
}

ac_reach() {
	pr_rg_info();
}

reward_type dfpfun() { return( 1.0 - mark("pfin")); }

ac_final() {
   double time_pt;

   for ( time_pt = 5.0; time_pt <= 75.0; time_pt += 5.0 )
   {
	time_value (time_pt);
	pr_expected( "DFP:", dfpfun );
   }

}