/* This example models a cluster based computing system with failures and
repairs.  The model also considers arrival and service of jobs in presence of
failures and repairs.  Adapted from Muppala and Trivedi */
# include	"user.h"

int	nproc, nbuff, quorum;
double lambda, mu, delta, beta, gamma, tau, coverage, alpha;

parameters() {

	iopt(IOP_METHOD,VAL_SSSOR);
	iopt(IOP_PR_MARK_ORDER,VAL_CANONIC);
	iopt(IOP_PR_MC_ORDER,VAL_TOFROM);
	iopt(IOP_MC,VAL_CTMC);
	iopt(IOP_PR_RSET,VAL_NO);
	iopt(IOP_PR_RGRAPH,VAL_NO);
	iopt(IOP_ITERATIONS,20000);
	iopt(IOP_CUMULATIVE, VAL_NO);
	fopt(FOP_ABS_RET_M0,0.0);
	fopt(FOP_PRECISION,0.00000001);

	nproc = input("number of processors");
	nbuff = input("number of buffers");
	quorum = input("number of processors required for quorum");
	lambda = 60.0;
	mu = 120.0;
	delta = 360.0;
	alpha = 180.0; /* cluster formation rate */
	beta = 12.0;
	gamma = 0.000167;
	tau = 1.0;
	coverage = 0.9;

}

rate_type dep_rate() {  if ( mark("bufull") < mark("procup") )
                           return(mark("bufull")*mu);
			else
                           return(mark("procup")*mu); }

enabling_type entrupdn() { if ( mark("procup") > quorum )
			      return(1);
			   else
			      return(0); }

enabling_type entrupdn1() { if ( mark("procup") > quorum )
			      return(0);
			   else
			      return(1); }

enabling_type entrdnup() { if ((mark("sysup") == 1 )||(mark("sysdn") == 1))
			      return(1);
			   else
			      return(0); }

enabling_type entrbuf() { return(mark("sysup"));}

enabling_type entrsys() { if (mark("procup") >= quorum)
			      return(1);
			   else
			      return(0); }

net() {
	place("bufree");
	init("bufree",nbuff);
	place("bufull");
	place("sysup");
	init("sysup",1);
	place("sysdn");
	place("procup");
	init("procup",nproc);
	place("proctmp");
	place("procreb");
	place("procrec");
	place("procdn");

	trans("trarr");
	enabling("trarr",entrbuf);
	trans("trdep");
	enabling("trdep",entrbuf);
	trans("trupdn");
	enabling("trupdn",entrupdn);
	trans("trupdn1");
	enabling("trupdn1",entrupdn1);
	trans("truc");
	priority("truc",100);
	trans("trc");
	priority("trc",100);
	trans("trrb");
	trans("trrc");
	trans("trdnup");
	enabling("trdnup",entrdnup);
	trans("trsys");
	priority("trsys", 50);
	enabling("trsys",entrsys);

	rateval("trarr",lambda);
	ratefun("trdep",dep_rate);
	ratedep("trupdn",gamma,"procup");
	ratedep("trupdn1",gamma,"procup");
	probval("trc",coverage);
	probval("truc", 1.0 - coverage);
	rateval("trrb",beta);
	rateval("trrc",delta);
	rateval("trdnup",tau);
	rateval("trsys",alpha);

	iarc("trarr","bufree");	oarc("trarr","bufull");
	iarc("trdep","bufull");	oarc("trdep","bufree");

	iarc("trupdn","procup");	iarc("trupdn","sysup");
	oarc("trupdn","proctmp");

	iarc("trupdn1","procup");	iarc("trupdn1","sysup");
	oarc("trupdn1","procdn");	oarc("trupdn1","sysdn");

	iarc("trc","proctmp");	oarc("trc","procrec");
	iarc("truc","proctmp");	oarc("truc","procreb");

	iarc("trrc","procrec");	oarc("trrc","procdn");
	oarc("trrc","sysup");
	iarc("trrb","procreb");	oarc("trrb","procdn");
	oarc("trrb","sysup");

	iarc("trdnup","procdn");	oarc("trdnup","procup");

	iarc("trsys","sysdn");	oarc("trsys","sysup");
}

assert() {
}

ac_init() {
	fprintf(stderr,
	"\nPerformability model with faulty processor and queueing\n\n");
}

ac_reach() {
	fprintf(stderr,"\nThe reachability graph has been generated\n\n");
}

reward_type	rej_prob_bf() { if(mark("bufree") == 0)
				return(1);
			     else
				return(0);}

reward_type	rej_prob_sd() { return(mark("sysdn"));}
reward_type	rej_prob_rb() { return(mark("procreb"));}
reward_type	rej_prob_rc() { return(mark("procrec"));}
reward_type	rej_prob() { if((mark("bufree") == 0) ||
           	                (mark("sysdn") == 1) ||
           	                (mark("procreb") == 1) ||
           	                (mark("procrec") == 1))
				return(1);
			     else
				return(0);}

ac_final() {

      pr_expected("Rejection Probability(buffer full)",rej_prob_bf);
      pr_expected("Rejection Probability(system down)",rej_prob_sd);
      pr_expected("Rejection Probability(reboot)",rej_prob_rb);
      pr_expected("Rejection Probability(reconfig)",rej_prob_rc);
      pr_expected("Rejection Probability(overall)",rej_prob);

}