// Trust models for user-centric networks from
// M. Kwiatkowska, D. Parker and A. Simaitis
// Strategic analysis of trust models for user-centric networks. 
// In: Proc. SR’13. EPTCS, vol. 112, pp. 53–60 (2013)
// (have simplified the reward structures)

// originally based on the trust model of
// A. Bogliolo, P. Polidori, A. Aldini, W. Moreira, P. Mendes, M. Yildiz, C. Ballester, and J.-M. Seigneur. 
// Virtual Currency and Reputation-Based Cooperation Incentives in User-Centric Networks. 
// In: Proc. IWCMC-2012, Cyprus, 2012

// turn-based stochastic game
smg

const int K; // number of services
const int td; // trust model

// model parameters
const double alpha_all = 0.8; // recommendation influence parameter
const int st_init_all = med; // initial service trust for all providers
const int reduct_all = td; // trust decrease for all providers
const bool hide_all = false; // allow information hiding
const double cancel = 0.05; // probability to cancel fair request
const bool init_know_all = true; // sharing of initial trust
const double die_prob = 0; // probability provider dies after serving a request
const int cmax = 10; // maximum service cost 
const int cmin = 2; // minimum service cost

player requester1
requester1, [pay11], [nopay11], [pay21], [nopay21], [pay31], [nopay31], [try11], [try21], [try31], [buy]
endplayer

player provider1
provider1, [accept11], [refuse11], [reveal11], [notreveal11]
endplayer

player provider2
provider2, [accept21], [refuse21], [reveal21], [notreveal21]
endplayer

player provider3
provider3, [accept31], [refuse31], [reveal31], [notreveal31]
endplayer

// probability to share information
formula rev_prob = know21&(trust11>trust21) | know31&(trust11>trust31) ? 0 : 1;

module requester1

	x1 : [0..43] init 0;  // states of the module
	//ns1 : [0..K] init 0; // number of requested services
	ps1 : [0..K] init 0; // number of payed services
	nps1 : [0..K] init 0; // number of unpayed services

	unpaid1 : bool init false;

	// choose service provider
	[try11] x1=0 & (y1+y2+y3=0) & ps1+nps1 < K -> (x1'=11) & (unpaid1'=false);
	[try21] x1=0 & (y1+y2+y3=0) & ps1+nps1 < K -> (x1'=21) & (unpaid1'=false);
	[try31] x1=0 & (y1+y2+y3=0) & ps1+nps1 < K -> (x1'=31) & (unpaid1'=false);
	// or buy the service off-market
	[buy] x1=0 & (y1+y2+y3=0) -> (x1'=41) & (unpaid1'=false);
	
	// finished sending requests
	[] x1=0 & (y1+y2+y3=0) & (ps1+nps1=K) -> (x1'=1) & (unpaid1'=false);
	[] x1=1 -> true;

	// reply from first requester and then decide to pay or not
	[accept11] x1=11 -> (x1'=12);
	[refuse11] x1=11 -> (x1'=13);
	[pay11] x1=12 -> (x1'=0) & (ps1'=min(K,ps1+1));
	[nopay11] x1=12 -> (x1'=0) & (nps1'=min(K,nps1+1)) & (unpaid1'=true); 
	[] x1=13 -> (x1'=0);
	// reply from second requester and then decide to pay or not
	[accept21] x1=21 -> (x1'=22);
	[refuse21] x1=21 -> (x1'=23);
	[pay21] x1=22 -> (x1'=0) & (ps1'=min(K,ps1+1));
	[nopay21] x1=22 -> (x1'=0) & (nps1'=min(K,nps1+1)) & (unpaid1'=true); 
	[] x1=23 -> (x1'=0);
	// reply from third requester and then decide to pay or not
	[accept31] x1=31 -> (x1'=32);
	[refuse31] x1=31 -> (x1'=33);
	[pay31] x1=32 -> (x1'=0) & (ps1'=min(K,ps1+1));
	[nopay31] x1=32 -> (x1'=0) & (nps1'=min(K,nps1+1)) & (unpaid1'=true); 
	[] x1=33 -> (x1'=0);
	// finish paying off-market
	[] x1=41 -> (x1'=0) & (ps1'=min(K,ps1+1));

endmodule

label "finished" = x1=1; // requester finished

// factor alpha of the cost formula
const double alpha1 = alpha_all;
const double alpha2 = alpha_all; 
const double alpha3 = alpha_all;
// trust formula
formula trusteq1 = min(top, !know21 & !know31 ? trust11 : floor(alpha1*trust11 + (1-alpha1)*recommend));
formula recommend = ((know21 ? trust21 : 0) + (know31 ? trust31 : 0)) / ((know21 ? 1 : 0) + (know31 ? 1 : 0));

// initial knowledge parameters
const bool init_know11 = init_know_all;
const bool init_know21 = init_know_all;
const bool init_know31 = init_know_all;

// initial trust parameters
const int dt_init1 = st_init_all; // dispositional trust
const int st_init1 = st_init_all; // service trust level 
const int trust_init1 = dt_init1; // initial trust
const int tth_init1 = high; // trust threshold (see the cost formula)

const int dt_init2 = st_init_all;
const int st_init2 = st_init_all;
const int trust_init2 = dt_init2; 
const int tth_init2 = high;

const int dt_init3 = st_init_all;
const int st_init3 = st_init_all;
const int trust_init3 = dt_init3; 
const int tth_init3 = high;


// trust reduction rates (0:NULL; 1:-1; 2:-2)
const int reduct1 = reduct_all;
const int reduct2 = reduct_all;
const int reduct3 = reduct_all;

// enable information withholding
// info about requester 1
const bool hide11 = hide_all;
const bool hide21 = hide_all;
const bool hide31 = hide_all; 

module provider1

	alive1 : bool init true;

	y1 : [0..4] init 0; // states of the module
	st1 : [0..level] init st_init1; // service trust level
	dt1 : [0..level] init dt_init1; // dispositional trust
	tth1 : [0..level] init tth_init1; // trust threshold (see the cost formula)

	trust11 : [0..level] init trust_init1; // trust towards the requester
	know11: bool init init_know11; // interaction flag

	// initiate connection with requester
	[try11] alive1 & (y1=0) -> ((trusteq1 < st1) ? 1 : 0) + ((trusteq1 < st1) ? 0 : 1) * cancel : (y1'=4) 
                            +  (1-(((trusteq1 < st1) ? 1 : 0) + ((trusteq1 < st1) ? 0 : 1) * cancel)) : (y1'=3);
	[try11] !alive1 & y1=0 -> (y1'=4);

	// accept or refuse requester1
	[accept11] (y1=3) & (trusteq1 >= st1) -> (y1'=1);  
	//[refuse11] (y1=4) & (trusteq1 < st1) -> (y1'=0); 
	[refuse11] (y1=4) -> (y1'=0); 

	// settle payment with requester1
	[pay11] (y1=1) -> (y1'=2) & (trust11' = (trust11 < top ? trust11+1 : top));
	[nopay11] (reduct1=1) & (y1=1) -> (y1'=2) & (trust11' = (trust11 > null ? trust11-1 : null));
	[nopay11] (reduct1=2) &(y1=1) -> (y1'=2) & (trust11' = (trust11 > null ? trust11-2 : null));
	[nopay11] (reduct1=0) & (y1=1) -> (y1'=2) & (trust11'=null);

	// decide to reveal info about requester to other providers or not
	[reveal11] (y1=2) ->  (1-die_prob) * rev_prob : (y1'=0) & (know11'=true) 
	                    + (1-die_prob) * (1-rev_prob) : (y1'=0) & (know11'=false)
			            + die_prob : (y1'=0) & (alive1'=false) & (trust11'=trust_init1) & (know11'=false);
	[notreveal11] hide11 & (y1=2) -> (y1'=0) & (know11'=false);

endmodule

module provider2 = provider1 [y1=y2, st1=st2, dt1=dt2, tth1=tth2, trust11=trust21, know11=know21, alive1=alive2,
                               alpha1=alpha2, trust21=trust11, know21=know11, // renaming parameters trust formula
                               dt_init1=dt_init2, st_init1=st_init2, 
                               trust_init1=trust_init2, tth_init1=tth_init2, try11=try21, init_know11=init_know21,                              
                               accept11=accept21, refuse11=refuse21, pay11=pay21, nopay11=nopay21,
			                   reduct1=reduct2, reveal11=reveal21, notreveal11=notreveal21,
			                   hide11=hide21]
endmodule

module provider3 = provider1 [y1=y3, st1=st3, dt1=dt3, tth1=tth3, trust11=trust31, know11=know31, alive1=alive3,
                               alpha1=alpha3, trust31=trust11, know31=know11, // renaming parameters trust formula 
                               dt_init1=dt_init3, st_init1=st_init3, 
                               trust_init1=trust_init3, tth_init1=tth_init3,try11=try31, init_know11=init_know31,                                 
                               accept11=accept31, refuse11=refuse31, pay11=pay31, nopay11=nopay31,
                               reduct1=reduct3, reveal11=reveal31, notreveal11=notreveal31,
                               hide11=hide31]
endmodule

// trust level aliases
const int level = 10;
const int null = 0;
const int low = 2;
const int med = 5;
const int high = 8;
const int top = 10;

// highest price in the market
formula max_price = max((trust11 < tth1) ? cmin + ceil(((cmax - cmin) / tth1) * (tth1 - trust11)) : cmin, 
			(trust21 < tth2) ? cmin + ceil(((cmax - cmin) / tth2) * (tth2 - trust21)) : cmin,
 			(trust31 < tth3) ? cmin + ceil(((cmax - cmin) / tth3) * (tth3 - trust31)) : cmin);
//formula max_price = cmax;

// maximum difference between trust
// changed to action reward
formula max_diff = max(max(trust11-trust21,trust21-trust11), max(trust11-trust31,trust31-trust11), max(trust21-trust31,trust31-trust21));

//  cost of obtaining services
rewards "cost"
	!unpaid1 & y1=2 : (trust11 < tth1) ? cmin + ceil(((cmax - cmin) / tth1) * (tth1 - trust11)) : cmin; 
	!unpaid1 & y2=2 : (trust21 < tth2) ? cmin + ceil(((cmax - cmin) / tth2) * (tth2 - trust21)) : cmin;
	!unpaid1 & y3=2 : (trust31 < tth3) ? cmin + ceil(((cmax - cmin) / tth3) * (tth3 - trust31)) : cmin;
	x1=41 : max_price;
endrewards

// obtain an paid service
rewards "payed"
	!unpaid1 & y1=2 : 1;
	!unpaid1 & y2=2 : 1;
	!unpaid1 & y3=2 : 1;
endrewards
// obtain an unpaid service
rewards "nopayed"
	unpaid1 & y1=2 : 1;
	unpaid1 & y2=2 : 1;
	unpaid1 & y3=2 : 1;
endrewards
// total services
rewards "accepted"
	[accept11] true : 1;
	[accept21] true : 1;
	[accept31] true : 1;
endrewards