/* This is a model of the task graph considered in Veeraraghavan and Trivedi
In this example we consider two processors with processor sharing between all the
enabled tasks */
# 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);

}

/* We assume that if three tasks are at the same time sharing the two processors
then efficiency drops to 90 % because of context switch overhead */
double factor() {
		if ( enabled("t4") && enabled("t5") && enabled("t3"))
			return(0.9*2./3.);
		if ( enabled("t4") && enabled("t5") && enabled("t6"))
			return(0.9*2./3.);
		if ( enabled("t3") && enabled("t7") && enabled("t8"))
			return(0.9*2./3.);
		if ( enabled("t6") && enabled("t7") && enabled("t8"))
			return(0.9*2./3.);

		return(1);
}

rate_type rate1() { return( 1.0 ); }
rate_type rate2() { return( 0.5 * factor() ); }
rate_type rate3() { return( 1.0 * factor() ); }
rate_type rate4() { return( 0.25 * factor() ); }
rate_type rate5() { return( 0.25 * factor() ); }
rate_type rate6() { return( 0.3333 * factor() ); }
rate_type rate7() { return( 0.142857 * factor() ); }
rate_type rate8() { return( 0.125 * factor() ); }
rate_type rate9() { return( 1.0 ); }

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");
	trans("t5");
	trans("t6");
	trans("t7");
	trans("t8");
	trans("t9");

	ratefun("t1",rate1);
	ratefun("t2",rate2);
	ratefun("t3",rate3);
	ratefun("t4",rate4);
	ratefun("t5",rate5);
	ratefun("t6",rate6);
	ratefun("t7",rate7);
	ratefun("t8",rate8);
	ratefun("t9",rate9);

	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 );
   }


}