Examples

Online store

An online store has the following contract: buyers can iteratively add items to a shopping cart; when at least one item has been added, a buyer can proceed to the checkout. Then, the client can either cancel the order, or pay. In the latter case, the store can accept the payment (ok), or decline it (no, in which case it lets the user try again), or it can abort the transaction.

onlinestore.co2

onlinestore.java

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
single package it.unica.co2.site

honesty Store

/*
 * contract
 */
contract C {
	addToCart? int . Cadd
}

contract Cadd {
	addToCart? int . Cadd 
	+ checkout? . Cpay
}

contract Cpay {
	pay? string . (
		ok! 
		(+) no!.Cpay 
		(+) abort!
	) 
	+ cancel?
}

/*
 * specification
 */
specification Store {
	tell x C . 
	receive@x addToCart?[n:int] . Padd(x,n)
}

specification Padd (x:session, total:int) {
	receive {
		@x addToCart?[n:int] -> Padd(x, total+n)
		@x checkout? -> Ppay(x, total)
	}
}

specification Ppay (x:session, amount:int) {
	receive { 
		@x pay?[s:string] -> Pack(x,amount) 
		@x cancel?
	}
}

specification Pack (x:session, amount:int) {
	if amount<100 
	then send@x ok! 
	else send@x no!.Ppay(x,amount)
}
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
package it.unica.co2.site.onlinestore;


import static it.unica.co2.api.contract.utils.ContractFactory.*;
import it.unica.co2.api.contract.ContractDefinition;
import it.unica.co2.api.contract.Recursion;
import it.unica.co2.api.contract.SessionType;
import it.unica.co2.api.contract.Sort;
import it.unica.co2.api.process.CO2Process;
import it.unica.co2.api.process.Participant;
import it.unica.co2.honesty.HonestyChecker;
import co2api.ContractException;
import co2api.ContractExpiredException;
import co2api.Message;
import co2api.Public;
import co2api.Session;
import co2api.SessionI;
import co2api.TimeExpiredException;

/*
 * auto-generated by co2-plugin
 * creation date: 02-12-2016 15:33:55
 */
@SuppressWarnings("unused")
public class Main {
	
	private static final String username = "eclipse@co2.unica.it";
	private static final String password = "eclipse";
	
	
	/*
	 * contracts declaration
	 */
	static final ContractDefinition C = def("C");
	static final ContractDefinition Cadd = def("Cadd");
	static final ContractDefinition Cpay = def("Cpay");
	
	/*
	 * contracts initialization
	 */
	static {
		C.setContract(externalSum().add("addToCart", Sort.integer(), ref(Cadd)));
		Cadd.setContract(externalSum().add("addToCart", Sort.integer(), ref(Cadd)).add("checkout", Sort.unit(), ref(Cpay)));
		Cpay.setContract(externalSum().add("pay", Sort.string(), internalSum().add("ok", Sort.unit()).add("no", Sort.unit(), ref(Cpay)).add("abort", Sort.unit())).add("cancel", Sort.unit()));
	}
	
	
	public static class Store extends Participant {
		
		private static final long serialVersionUID = 1L;
		
		public Store(String username, String password) {
			super(username, password);
		}
		
		@Override
		public void run() {
			Session<SessionType> x = tellAndWait(Main.C);
			
			logger.info("waiting on 'x' for actions [addToCart]");
			Message msg = x.waitForReceive("addToCart"); 
			
			logger.info("received [addToCart]");
			Integer n;
			try {
				n = Integer.parseInt(msg.getStringValue());
			}
			catch (NumberFormatException e) {
				throw new RuntimeException(e);
			}
			processCall(Padd.class, username, password ,x, n); 
		}
	}
	
	public static class Padd extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private Integer total;
		
		public Padd(String username, String password, SessionI<SessionType> x, Integer total) {
			super(username, password);
			this.x=x;
			this.total=total;
		}
		
		@Override
		public void run() {
			logger.info("waiting on 'x' for actions [addToCart, checkout]");
			Message msg = x.waitForReceive("addToCart", "checkout"); 
			
			switch (msg.getLabel()) {
				case "addToCart":
					logger.info("received ["+msg.getLabel()+"]");
					Integer n;
					try {
						n = Integer.parseInt(msg.getStringValue());
					}
					catch (NumberFormatException e) {
						throw new RuntimeException(e);
					}
					processCall(Padd.class, username, password ,x, (total+n)); 
					break;
				case "checkout":
					logger.info("received ["+msg.getLabel()+"]");
					processCall(Ppay.class, username, password ,x, total); 
					break;
			}
		}
	}
	
	public static class Ppay extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private Integer amount;
		
		public Ppay(String username, String password, SessionI<SessionType> x, Integer amount) {
			super(username, password);
			this.x=x;
			this.amount=amount;
		}
		
		@Override
		public void run() {
			logger.info("waiting on 'x' for actions [pay, cancel]");
			Message msg = x.waitForReceive("pay", "cancel"); 
			
			switch (msg.getLabel()) {
				case "pay":
					logger.info("received ["+msg.getLabel()+"]");
					String s;
					s = msg.getStringValue();
					processCall(Pack.class, username, password ,x, amount); 
					break;
				case "cancel":
					logger.info("received ["+msg.getLabel()+"]");
					break;
			}
		}
	}
	
	public static class Pack extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private Integer amount;
		
		public Pack(String username, String password, SessionI<SessionType> x, Integer amount) {
			super(username, password);
			this.x=x;
			this.amount=amount;
		}
		
		@Override
		public void run() {
			if ((amount<100)) { 
				logger.info("sending action 'ok'");
				x.sendIfAllowed("ok"); 
			}
			else {
				logger.info("sending action 'no'");
				x.sendIfAllowed("no"); 
				
				processCall(Ppay.class, username, password ,x, amount); 
			}
		}
	}
	
	public static void main(String[] args) {
		HonestyChecker.isHonest(Store.class, Main.username, Main.password);
		//new Thread(new Store(Main.username, Main.password)).start();
	}
}

Recursive Online Store

store-rec.co2

store-rec.java

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
single package it.unica.co2.site

honesty StoreRec

contract Crec {  
    addToCart? string . Crec
    + checkout? . ( 
           price! int . (accept? + reject?)
           (+) unavailable!
    )
}

contract D { req! string . ( ok? + no? ) }

specification StoreRec { tell x Crec . Loop(x) }
specification Loop(x:session) {
    receive {
        @x addToCart?[item:string] -> Loop(x)
        @x checkout? -> Checkout(x)
    }
}
specification Checkout(x:session) {
    tell y D .
        send@y req![*:string] .
        receive {
            @y ok?  -> send@x price![*:int] . receive {
                    @x accept?
                    @x reject?
                }
            @y no?  -> send@x unavailable!
            after * -> (
                send@x unavailable! |
                receive@y ok? no? 
            )                
        }
    after * -> send@x unavailable!
}
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
package it.unica.co2.site.storerec;


import static it.unica.co2.api.contract.utils.ContractFactory.*;
import it.unica.co2.api.contract.ContractDefinition;
import it.unica.co2.api.contract.Recursion;
import it.unica.co2.api.contract.SessionType;
import it.unica.co2.api.contract.Sort;
import it.unica.co2.api.process.CO2Process;
import it.unica.co2.api.process.Participant;
import it.unica.co2.honesty.HonestyChecker;
import co2api.ContractException;
import co2api.ContractExpiredException;
import co2api.Message;
import co2api.Public;
import co2api.Session;
import co2api.SessionI;
import co2api.TimeExpiredException;

/*
 * auto-generated by co2-plugin
 * creation date: 02-12-2016 15:23:53
 */
@SuppressWarnings("unused")
public class Main {
	
	private static final String username = "eclipse@co2.unica.it";
	private static final String password = "eclipse";
	
	static final Integer intPlaceholder = 42;
	static final String stringPlaceholder = "42";
	
	
	/*
	 * contracts declaration
	 */
	static final ContractDefinition Crec = def("Crec");
	static final ContractDefinition D = def("D");
	
	/*
	 * contracts initialization
	 */
	static {
		Crec.setContract(externalSum().add("addToCart", Sort.string(), ref(Crec)).add("checkout", Sort.unit(), internalSum().add("price", Sort.integer(), externalSum().add("accept", Sort.unit()).add("reject", Sort.unit())).add("unavailable", Sort.unit())));
		D.setContract(internalSum().add("req", Sort.string(), externalSum().add("ok", Sort.unit()).add("no", Sort.unit())));
	}
	
	
	public static class StoreRec extends Participant {
		
		private static final long serialVersionUID = 1L;
		
		public StoreRec(String username, String password) {
			super(username, password);
		}
		
		@Override
		public void run() {
			Session<SessionType> x = tellAndWait(Main.Crec);
			
			processCall(Loop.class, username, password ,x); 
		}
	}
	
	public static class Loop extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		
		public Loop(String username, String password, SessionI<SessionType> x) {
			super(username, password);
			this.x=x;
		}
		
		@Override
		public void run() {
			logger.info("waiting on 'x' for actions [addToCart, checkout]");
			Message msg = x.waitForReceive("addToCart", "checkout"); 
			
			switch (msg.getLabel()) {
				case "addToCart":
					logger.info("received ["+msg.getLabel()+"]");
					String item;
					item = msg.getStringValue();
					processCall(Loop.class, username, password ,x); 
					break;
				case "checkout":
					logger.info("received ["+msg.getLabel()+"]");
					processCall(Checkout.class, username, password ,x); 
					break;
			}
		}
	}
	
	public static class Checkout extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		
		public Checkout(String username, String password, SessionI<SessionType> x) {
			super(username, password);
			this.x=x;
		}
		
		@Override
		public void run() {
			Public<SessionType> pbl_y = tell(Main.D, Main.intPlaceholder*1000); 
			
			try {
				Session<SessionType> y = pbl_y.waitForSession();
				
				logger.info("sending action 'req'");
				y.sendIfAllowed("req", Main.stringPlaceholder); //TODO: remove the placeholder/s
				
				try {
					logger.info("waiting on 'y' for actions [ok, no]");
					Message msg = y.waitForReceive(Main.intPlaceholder*1000, "ok", "no"); //TODO: remove the placeholder/s
					
					switch (msg.getLabel()) {
						case "ok":
							logger.info("received ["+msg.getLabel()+"]");
							logger.info("sending action 'price'");
							x.sendIfAllowed("price", Main.intPlaceholder); //TODO: remove the placeholder/s
							
							logger.info("waiting on 'x' for actions [accept, reject]");
							Message msg1 = x.waitForReceive("accept", "reject"); 
							
							switch (msg1.getLabel()) {
								case "accept":
									logger.info("received ["+msg1.getLabel()+"]");
									break;
								case "reject":
									logger.info("received ["+msg1.getLabel()+"]");
									break;
							}
							break;
						case "no":
							logger.info("received ["+msg.getLabel()+"]");
							logger.info("sending action 'unavailable'");
							x.sendIfAllowed("unavailable"); 
							break;
					}
				}
				catch (TimeExpiredException e) {
					
					parallel(()->{
						logger.info("sending action 'unavailable'");
						x.sendIfAllowed("unavailable"); 
					});
					
					parallel(()->{
						logger.info("waiting on 'y' for actions [ok, no]");
						Message msg2 = y.waitForReceive("ok", "no"); 
						
						switch (msg2.getLabel()) {
							case "ok":
							case "no":
								logger.info("received ["+msg2.getLabel()+"]");
								break;
						}
					});
				}
				
			}
			catch(ContractExpiredException e1) {
				//retract y
				logger.info("sending action 'unavailable'");
				x.sendIfAllowed("unavailable"); 
			}
		}
	}
	
	public static void main(String[] args) {
		HonestyChecker.isHonest(StoreRec.class, Main.username, Main.password);
		//new Thread(new StoreRec(Main.username, Main.password)).start();
	}
}

Voucher distribution system

A store offers buyers two payments options: clickPay or clickVoucher. If a buyer chooses clickPay, the store requires it to pay; otherwise, the store check the validity of the voucher interacting with an online voucher distribution system (V). If V validates the voucher (ok), the buyer can use it (voucher), otherwise (no) it must pay the store.

voucher.co2

voucher.java

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
single package it.unica.co2.site

honesty P

/*
 * contracts
 */
contract CB {
	clickPay? . pay? string
	+ clickVoucher? . (
		reject! . pay? string 
		(+) accept! . voucher? string
	)
}
contract CV {
	ok? + no?
}

/*
 * specification
 */
specification P {
	tell x CB .
	receive {
		@x  clickPay? -> (receive@x pay?[code:string])	
		@x  clickVoucher? -> (
			tell y CV . 
			Q(x,y) 
			after * -> send@x reject! . receive@x pay?[code:string]
		)
	}
}

specification Q ( x:session , y:session ) {
	receive {
		@y ok? -> send@x accept! . receive@x voucher?[v:string]
		@y no? -> send@x reject! . receive@x pay?[code:string]
		after * -> R(x,y) 
	}
}

specification R ( x:session , y:session ) {
	send@x reject! . receive@x pay?[code:string]
	| receive@y ok? no?
}
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
package it.unica.co2.site.voucher;


import static it.unica.co2.api.contract.utils.ContractFactory.*;
import it.unica.co2.api.contract.ContractDefinition;
import it.unica.co2.api.contract.Recursion;
import it.unica.co2.api.contract.SessionType;
import it.unica.co2.api.contract.Sort;
import it.unica.co2.api.process.CO2Process;
import it.unica.co2.api.process.Participant;
import it.unica.co2.honesty.HonestyChecker;
import co2api.ContractException;
import co2api.ContractExpiredException;
import co2api.Message;
import co2api.Public;
import co2api.Session;
import co2api.SessionI;
import co2api.TimeExpiredException;

/*
 * auto-generated by co2-plugin
 * creation date: 02-12-2016 15:31:31
 */
@SuppressWarnings("unused")
public class Main {
	
	private static final String username = "eclipse@co2.unica.it";
	private static final String password = "eclipse";
	
	static final Integer intPlaceholder = 42;
	
	
	/*
	 * contracts declaration
	 */
	static final ContractDefinition CB = def("CB");
	static final ContractDefinition CV = def("CV");
	
	/*
	 * contracts initialization
	 */
	static {
		CB.setContract(externalSum().add("clickPay", Sort.unit(), externalSum().add("pay", Sort.string())).add("clickVoucher", Sort.unit(), internalSum().add("reject", Sort.unit(), externalSum().add("pay", Sort.string())).add("accept", Sort.unit(), externalSum().add("voucher", Sort.string()))));
		CV.setContract(externalSum().add("ok", Sort.unit()).add("no", Sort.unit()));
	}
	
	
	public static class P extends Participant {
		
		private static final long serialVersionUID = 1L;
		
		public P(String username, String password) {
			super(username, password);
		}
		
		@Override
		public void run() {
			Session<SessionType> x = tellAndWait(Main.CB);
			
			logger.info("waiting on 'x' for actions [clickPay, clickVoucher]");
			Message msg = x.waitForReceive("clickPay", "clickVoucher"); 
			
			switch (msg.getLabel()) {
				case "clickPay":
					logger.info("received ["+msg.getLabel()+"]");
					logger.info("waiting on 'x' for actions [pay]");
					Message msg1 = x.waitForReceive("pay"); 
					
					logger.info("received [pay]");
					String code;
					code = msg1.getStringValue();
					break;
				case "clickVoucher":
					logger.info("received ["+msg.getLabel()+"]");
					Public<SessionType> pbl_y = tell(Main.CV, Main.intPlaceholder*1000); 
					
					try {
						Session<SessionType> y = pbl_y.waitForSession();
						
						processCall(Q.class, username, password ,x, y); 
					}
					catch(ContractExpiredException e) {
						//retract y
						logger.info("sending action 'reject'");
						x.sendIfAllowed("reject"); 
						
						logger.info("waiting on 'x' for actions [pay]");
						Message msg2 = x.waitForReceive("pay"); 
						
						logger.info("received [pay]");
						String code1;
						code1 = msg2.getStringValue();
					}
					break;
			}
		}
	}
	
	public static class Q extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private SessionI<SessionType> y;
		
		public Q(String username, String password, SessionI<SessionType> x, SessionI<SessionType> y) {
			super(username, password);
			this.x=x;
			this.y=y;
		}
		
		@Override
		public void run() {
			try {
				logger.info("waiting on 'y' for actions [ok, no]");
				Message msg = y.waitForReceive(Main.intPlaceholder*1000, "ok", "no"); //TODO: remove the placeholder/s
				
				switch (msg.getLabel()) {
					case "ok":
						logger.info("received ["+msg.getLabel()+"]");
						logger.info("sending action 'accept'");
						x.sendIfAllowed("accept"); 
						
						logger.info("waiting on 'x' for actions [voucher]");
						Message msg1 = x.waitForReceive("voucher"); 
						
						logger.info("received [voucher]");
						String v;
						v = msg1.getStringValue();
						break;
					case "no":
						logger.info("received ["+msg.getLabel()+"]");
						logger.info("sending action 'reject'");
						x.sendIfAllowed("reject"); 
						
						logger.info("waiting on 'x' for actions [pay]");
						Message msg2 = x.waitForReceive("pay"); 
						
						logger.info("received [pay]");
						String code;
						code = msg2.getStringValue();
						break;
				}
			}
			catch (TimeExpiredException e) {
				processCall(R.class, username, password ,x, y); 
			}
			
		}
	}
	
	public static class R extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private SessionI<SessionType> y;
		
		public R(String username, String password, SessionI<SessionType> x, SessionI<SessionType> y) {
			super(username, password);
			this.x=x;
			this.y=y;
		}
		
		@Override
		public void run() {
			
			parallel(()->{
				logger.info("sending action 'reject'");
				x.sendIfAllowed("reject"); 
				
				logger.info("waiting on 'x' for actions [pay]");
				Message msg = x.waitForReceive("pay"); 
				
				logger.info("received [pay]");
				String code;
				code = msg.getStringValue();
			});
			
			parallel(()->{
				logger.info("waiting on 'y' for actions [ok, no]");
				Message msg1 = y.waitForReceive("ok", "no"); 
				
				switch (msg1.getLabel()) {
					case "ok":
					case "no":
						logger.info("received ["+msg1.getLabel()+"]");
						break;
				}
			});
		}
	}
	
	public static void main(String[] args) {
		HonestyChecker.isHonest(P.class, Main.username, Main.password);
		//new Thread(new P(Main.username, Main.password)).start();
	}
}

Blackjack

blackjack.co2

blackjack.java

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
single package it.unica.co2.site

honesty P

/*
 * contracts
 */
// between the dealer and the player
contract Cp {
	hit?. (card! int.Cp (+) lose! (+) abort!)   
	+ stand? . (win! (+) lose! (+) abort!)
}

// between the dealer and the desk service
contract Cd { 
	next!. card?int .Cd (+) abort! 
}

/*
 * specification
 */
specification P {
	tell xd Cd .	
	tell xp Cp . Pplay(xp, xd, 0) 
	after * -> send@xd abort!
}

specification Pplay(xp:session, xd:session, np:int) {
	
	receive {
		@xp  hit? -> send@xd next! . Pdeck(xp, xd, np)
		@xp  stand? -> Qstand(xp,xd,np,0)
		after * -> send@xd abort! . PabortP(xp) 
	}
}

specification Pdeck(xp:session, xd:session, np:int) {
	receive {
		@xd card?[n:int] -> Pcard(xp,xd,np+n,n)
		after * -> send@xp abort! . PabortD(xd)
	}
}

specification Pcard(xp:session, xd:session, np:int, n:int) {
	if np<21
	then send@xp card![n] . Pplay(xp,xd,np)
	else send@xp lose! . PabortD(xd)
}

specification Qstand(xp:session, xd:session, np:int, nd:int) {
	if nd<21
	then send@xd next! . Qdeck(xp,xd,np,nd)
	else send@xp win! . send@xd abort!
}

specification Qdeck(xp:session, xd:session, np:int, nd:int) {
	receive {
		@xd card?[n:int] -> Qcard(xp,xd,np,nd)
		after * -> send@xp abort!. PabortD(xd)
	}
}

specification Qcard(xp:session, xd:session, np:int, nd:int) {
	if nd<np
	then Qstand(xp,xd,np,nd)
	else send@xp lose! . PabortD(xd)
}

specification PabortP(xp:session) {
	receive@xp  hit? stand?. send@xp abort!
}

specification PabortD(xd:session) {
	send@xd abort! 
	| receive@xd card?[n:int] . send@xd abort!
}
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
package it.unica.co2.site.blackjack;


import static it.unica.co2.api.contract.utils.ContractFactory.*;
import it.unica.co2.api.contract.ContractDefinition;
import it.unica.co2.api.contract.Recursion;
import it.unica.co2.api.contract.SessionType;
import it.unica.co2.api.contract.Sort;
import it.unica.co2.api.process.CO2Process;
import it.unica.co2.api.process.Participant;
import it.unica.co2.honesty.HonestyChecker;
import co2api.ContractException;
import co2api.ContractExpiredException;
import co2api.Message;
import co2api.Public;
import co2api.Session;
import co2api.SessionI;
import co2api.TimeExpiredException;

/*
 * auto-generated by co2-plugin
 * creation date: 02-12-2016 15:25:41
 */
@SuppressWarnings("unused")
public class Main {
	
	private static final String username = "eclipse@co2.unica.it";
	private static final String password = "eclipse";
	
	static final Integer intPlaceholder = 42;
	
	
	/*
	 * contracts declaration
	 */
	static final ContractDefinition Cp = def("Cp");
	static final ContractDefinition Cd = def("Cd");
	
	/*
	 * contracts initialization
	 */
	static {
		Cp.setContract(externalSum().add("hit", Sort.unit(), internalSum().add("card", Sort.integer(), ref(Cp)).add("lose", Sort.unit()).add("abort", Sort.unit())).add("stand", Sort.unit(), internalSum().add("win", Sort.unit()).add("lose", Sort.unit()).add("abort", Sort.unit())));
		Cd.setContract(internalSum().add("next", Sort.unit(), externalSum().add("card", Sort.integer(), ref(Cd))).add("abort", Sort.unit()));
	}
	
	
	public static class P extends Participant {
		
		private static final long serialVersionUID = 1L;
		
		public P(String username, String password) {
			super(username, password);
		}
		
		@Override
		public void run() {
			Session<SessionType> xd = tellAndWait(Main.Cd);
			
			Public<SessionType> pbl_xp = tell(Main.Cp, Main.intPlaceholder*1000); 
			
			try {
				Session<SessionType> xp = pbl_xp.waitForSession();
				
				processCall(Pplay.class, username, password ,xp, xd, 0); 
			}
			catch(ContractExpiredException e) {
				//retract xp
				logger.info("sending action 'abort'");
				xd.sendIfAllowed("abort"); 
			}
		}
	}
	
	public static class Pplay extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xp;
		private SessionI<SessionType> xd;
		private Integer np;
		
		public Pplay(String username, String password, SessionI<SessionType> xp, SessionI<SessionType> xd, Integer np) {
			super(username, password);
			this.xp=xp;
			this.xd=xd;
			this.np=np;
		}
		
		@Override
		public void run() {
			try {
				logger.info("waiting on 'xp' for actions [hit, stand]");
				Message msg = xp.waitForReceive(Main.intPlaceholder*1000, "hit", "stand"); //TODO: remove the placeholder/s
				
				switch (msg.getLabel()) {
					case "hit":
						logger.info("received ["+msg.getLabel()+"]");
						logger.info("sending action 'next'");
						xd.sendIfAllowed("next"); 
						
						processCall(Pdeck.class, username, password ,xp, xd, np); 
						break;
					case "stand":
						logger.info("received ["+msg.getLabel()+"]");
						processCall(Qstand.class, username, password ,xp, xd, np, 0); 
						break;
				}
			}
			catch (TimeExpiredException e) {
				logger.info("sending action 'abort'");
				xd.sendIfAllowed("abort"); 
				
				processCall(PabortP.class, username, password ,xp); 
			}
			
		}
	}
	
	public static class Pdeck extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xp;
		private SessionI<SessionType> xd;
		private Integer np;
		
		public Pdeck(String username, String password, SessionI<SessionType> xp, SessionI<SessionType> xd, Integer np) {
			super(username, password);
			this.xp=xp;
			this.xd=xd;
			this.np=np;
		}
		
		@Override
		public void run() {
			try {
				logger.info("waiting on 'xd' for actions [card]");
				Message msg = xd.waitForReceive(Main.intPlaceholder*1000, "card"); //TODO: remove the placeholder/s
				
				logger.info("received [card]");
				Integer n;
				try {
					n = Integer.parseInt(msg.getStringValue());
				}
				catch (NumberFormatException e) {
					throw new RuntimeException(e);
				}
				processCall(Pcard.class, username, password ,xp, xd, (np+n), n); 
			}
			catch (TimeExpiredException e1) {
				logger.info("sending action 'abort'");
				xp.sendIfAllowed("abort"); 
				
				processCall(PabortD.class, username, password ,xd); 
			}
			
		}
	}
	
	public static class Pcard extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xp;
		private SessionI<SessionType> xd;
		private Integer np;
		private Integer n;
		
		public Pcard(String username, String password, SessionI<SessionType> xp, SessionI<SessionType> xd, Integer np, Integer n) {
			super(username, password);
			this.xp=xp;
			this.xd=xd;
			this.np=np;
			this.n=n;
		}
		
		@Override
		public void run() {
			if ((np<21)) { 
				logger.info("sending action 'card'");
				xp.sendIfAllowed("card", n); 
				
				processCall(Pplay.class, username, password ,xp, xd, np); 
			}
			else {
				logger.info("sending action 'lose'");
				xp.sendIfAllowed("lose"); 
				
				processCall(PabortD.class, username, password ,xd); 
			}
		}
	}
	
	public static class Qstand extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xp;
		private SessionI<SessionType> xd;
		private Integer np;
		private Integer nd;
		
		public Qstand(String username, String password, SessionI<SessionType> xp, SessionI<SessionType> xd, Integer np, Integer nd) {
			super(username, password);
			this.xp=xp;
			this.xd=xd;
			this.np=np;
			this.nd=nd;
		}
		
		@Override
		public void run() {
			if ((nd<21)) { 
				logger.info("sending action 'next'");
				xd.sendIfAllowed("next"); 
				
				processCall(Qdeck.class, username, password ,xp, xd, np, nd); 
			}
			else {
				logger.info("sending action 'win'");
				xp.sendIfAllowed("win"); 
				
				logger.info("sending action 'abort'");
				xd.sendIfAllowed("abort"); 
			}
		}
	}
	
	public static class Qdeck extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xp;
		private SessionI<SessionType> xd;
		private Integer np;
		private Integer nd;
		
		public Qdeck(String username, String password, SessionI<SessionType> xp, SessionI<SessionType> xd, Integer np, Integer nd) {
			super(username, password);
			this.xp=xp;
			this.xd=xd;
			this.np=np;
			this.nd=nd;
		}
		
		@Override
		public void run() {
			try {
				logger.info("waiting on 'xd' for actions [card]");
				Message msg = xd.waitForReceive(Main.intPlaceholder*1000, "card"); //TODO: remove the placeholder/s
				
				logger.info("received [card]");
				Integer n;
				try {
					n = Integer.parseInt(msg.getStringValue());
				}
				catch (NumberFormatException e) {
					throw new RuntimeException(e);
				}
				processCall(Qcard.class, username, password ,xp, xd, np, nd); 
			}
			catch (TimeExpiredException e1) {
				logger.info("sending action 'abort'");
				xp.sendIfAllowed("abort"); 
				
				processCall(PabortD.class, username, password ,xd); 
			}
			
		}
	}
	
	public static class Qcard extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xp;
		private SessionI<SessionType> xd;
		private Integer np;
		private Integer nd;
		
		public Qcard(String username, String password, SessionI<SessionType> xp, SessionI<SessionType> xd, Integer np, Integer nd) {
			super(username, password);
			this.xp=xp;
			this.xd=xd;
			this.np=np;
			this.nd=nd;
		}
		
		@Override
		public void run() {
			if ((nd<np)) { 
				processCall(Qstand.class, username, password ,xp, xd, np, nd); 
			}
			else {
				logger.info("sending action 'lose'");
				xp.sendIfAllowed("lose"); 
				
				processCall(PabortD.class, username, password ,xd); 
			}
		}
	}
	
	public static class PabortP extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xp;
		
		public PabortP(String username, String password, SessionI<SessionType> xp) {
			super(username, password);
			this.xp=xp;
		}
		
		@Override
		public void run() {
			logger.info("waiting on 'xp' for actions [hit, stand]");
			Message msg = xp.waitForReceive("hit", "stand"); 
			
			switch (msg.getLabel()) {
				case "hit":
				case "stand":
					logger.info("received ["+msg.getLabel()+"]");
					logger.info("sending action 'abort'");
					xp.sendIfAllowed("abort"); 
					break;
			}
		}
	}
	
	public static class PabortD extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xd;
		
		public PabortD(String username, String password, SessionI<SessionType> xd) {
			super(username, password);
			this.xd=xd;
		}
		
		@Override
		public void run() {
			
			parallel(()->{
				logger.info("sending action 'abort'");
				xd.sendIfAllowed("abort"); 
			});
			
			parallel(()->{
				logger.info("waiting on 'xd' for actions [card]");
				Message msg = xd.waitForReceive("card"); 
				
				logger.info("received [card]");
				Integer n;
				try {
					n = Integer.parseInt(msg.getStringValue());
				}
				catch (NumberFormatException e) {
					throw new RuntimeException(e);
				}
				logger.info("sending action 'abort'");
				xd.sendIfAllowed("abort"); 
			});
		}
	}
	
	public static void main(String[] args) {
		HonestyChecker.isHonest(P.class, Main.username, Main.password);
		//new Thread(new P(Main.username, Main.password)).start();
	}
}

Travel Agency

travelagency.co2

travelagency.java

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
single package it.unica.co2.site

honesty P

/*
 * contracts
 */
// between the travel agency and the customer
contract Cu {
	tripDets? string. budget? int . (quote! int. pay? . (commit! (+) abort!) (+) abort!)
}

// between the travel agency and the flying company
contract Cf {
	flightDets! string . D
}

// between the travel agency and the hotel reservation service
contract Ch {
	hotelDets! string . D
}

contract D {
	quote? int . (
		pay! . (confirm? . ( commit! (+) abort! ) )
		(+) abort!
	)
}

/*
 * specification
 */
specification P {
	tell xu Cu . 
	receive@xu tripDets?[yt:string] . 
	receive@xu budget?[bud:int] . P1(xu,yt,bud)
}

specification P1 (xu: session, yt:string, bud:int) {
	tellAndReturn xf Cf.
	tellAndReturn xh Ch . (
		send@xf flightDets![yt]
		| send@xh hotelDets![yt]
		| Pquote(xu,xf,xh,bud)	
	)
}

specification Pquote (xu:session, xf:session, xh:session, bud:int) {
	receive {
		@xf quote?[n:int] -> Pquote1(xu,xf,xh,n,bud)
		@xh quote?[n:int] -> Pquote1(xu,xh,xf,n,bud) 
		after * -> Pabort(xu,xh,xf)
	}
}

specification Pquote1 (x:session, x1:session, x2:session, quote:int, budget:int) {
	if quote<budget
	then Pquote2(x,x1,x2,quote,budget)
	else Pabort(x,x1,x2)
}

specification Pquote2 (x:session, x1:session, x2:session, quote:int, budget:int) {
	receive {
		@x2 quote?[quote2:int] -> 
			if quote+quote2<budget
			then Ppay(x,x1,x2,quote+quote2)
			else Pabort(x,x1,x2)
		after * -> Pabort(x,x1,x2)
	}
}

specification Pabort (x:session, x1:session, x2:session) {
	send@x abort! | send@x1 abort! | send@x2 abort! |
	receive@x pay? |
	receive@x1 quote?[n:int] | receive@x2 quote?[n:int] | 
	receive@x1 confirm? | receive@x2 confirm?
}

specification Ppay (x:session, x1:session, x2:session, amount:int) {
	send@x quote![amount] . (
		receive {
			@x pay? -> Pconfirm1(x,x1,x2)
			after * -> Pabort(x,x1,x2)
		}
	)
}

specification Pconfirm1 (x:session, x1:session, x2:session) {
	send@x1 pay!. send@x2 pay! . (
		receive { 
			@x1 confirm? -> Pconfirm2(x,x1,x2)
			after * -> Pabort(x,x1,x2)
		}
	)
}

specification Pconfirm2 (x:session, x1:session, x2:session) {
	receive {
		@x2 confirm? -> Pcommit(x,x1,x2)
		after * -> Pabort(x,x1,x2)
	}
}

specification Pcommit (x:session, x1:session, x2:session) {
	send@x commit! . 
	send@x1 commit! . 
	send@x2 commit!
}
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
package it.unica.co2.site.travelagency;


import static it.unica.co2.api.contract.utils.ContractFactory.*;
import it.unica.co2.api.contract.ContractDefinition;
import it.unica.co2.api.contract.Recursion;
import it.unica.co2.api.contract.SessionType;
import it.unica.co2.api.contract.Sort;
import it.unica.co2.api.process.CO2Process;
import it.unica.co2.api.process.Participant;
import it.unica.co2.honesty.HonestyChecker;
import co2api.ContractException;
import co2api.ContractExpiredException;
import co2api.Message;
import co2api.Public;
import co2api.Session;
import co2api.SessionI;
import co2api.TimeExpiredException;

/*
 * auto-generated by co2-plugin
 * creation date: 02-12-2016 15:21:15
 */
@SuppressWarnings("unused")
public class Main {
	
	private static final String username = "eclipse@co2.unica.it";
	private static final String password = "eclipse";
	
	static final Integer intPlaceholder = 42;
	
	
	/*
	 * contracts declaration
	 */
	static final ContractDefinition Cu = def("Cu");
	static final ContractDefinition Cf = def("Cf");
	static final ContractDefinition Ch = def("Ch");
	static final ContractDefinition D = def("D");
	
	/*
	 * contracts initialization
	 */
	static {
		Cu.setContract(externalSum().add("tripDets", Sort.string(), externalSum().add("budget", Sort.integer(), internalSum().add("quote", Sort.integer(), externalSum().add("pay", Sort.unit(), internalSum().add("commit", Sort.unit()).add("abort", Sort.unit()))).add("abort", Sort.unit()))));
		Cf.setContract(internalSum().add("flightDets", Sort.string(), ref(D)));
		Ch.setContract(internalSum().add("hotelDets", Sort.string(), ref(D)));
		D.setContract(externalSum().add("quote", Sort.integer(), internalSum().add("pay", Sort.unit(), externalSum().add("confirm", Sort.unit(), internalSum().add("commit", Sort.unit()).add("abort", Sort.unit()))).add("abort", Sort.unit())));
	}
	
	
	public static class P extends Participant {
		
		private static final long serialVersionUID = 1L;
		
		public P(String username, String password) {
			super(username, password);
		}
		
		@Override
		public void run() {
			Session<SessionType> xu = tellAndWait(Main.Cu);
			
			logger.info("waiting on 'xu' for actions [tripDets]");
			Message msg = xu.waitForReceive("tripDets"); 
			
			logger.info("received [tripDets]");
			String yt;
			yt = msg.getStringValue();
			logger.info("waiting on 'xu' for actions [budget]");
			Message msg1 = xu.waitForReceive("budget"); 
			
			logger.info("received [budget]");
			Integer bud;
			try {
				bud = Integer.parseInt(msg1.getStringValue());
			}
			catch (NumberFormatException e) {
				throw new RuntimeException(e);
			}
			processCall(P1.class, username, password ,xu, yt, bud); 
		}
	}
	
	public static class P1 extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xu;
		private String yt;
		private Integer bud;
		
		public P1(String username, String password, SessionI<SessionType> xu, String yt, Integer bud) {
			super(username, password);
			this.xu=xu;
			this.yt=yt;
			this.bud=bud;
		}
		
		@Override
		public void run() {
			Public<SessionType> xf = tell(Main.Cf);
			
			Public<SessionType> xh = tell(Main.Ch);
			
			
			parallel(()->{
				logger.info("sending action 'flightDets'");
				xf.sendIfAllowed("flightDets", yt); 
			});
			
			parallel(()->{
				logger.info("sending action 'hotelDets'");
				xh.sendIfAllowed("hotelDets", yt); 
			});
			
			parallel(()->{
				processCall(Pquote.class, username, password ,xu, xf, xh, bud); 
			});
		}
	}
	
	public static class Pquote extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> xu;
		private SessionI<SessionType> xf;
		private SessionI<SessionType> xh;
		private Integer bud;
		
		public Pquote(String username, String password, SessionI<SessionType> xu, SessionI<SessionType> xf, SessionI<SessionType> xh, Integer bud) {
			super(username, password);
			this.xu=xu;
			this.xf=xf;
			this.xh=xh;
			this.bud=bud;
		}
		
		@Override
		public void run() {
			try {
				multipleSessionReceiver()
					.add(
						xf, 
						(msg) -> {
							Integer n;
							try {
								n = Integer.parseInt(msg.getStringValue());
							}
							catch (NumberFormatException e) {
								throw new RuntimeException(e);
							}
							processCall(Pquote1.class, username, password ,xu, xf, xh, n, bud); 
						}, 
						"quote"
					)
					.add(
						xh, 
						(msg) -> {
							Integer n1;
							try {
								n1 = Integer.parseInt(msg.getStringValue());
							}
							catch (NumberFormatException e1) {
								throw new RuntimeException(e1);
							}
							processCall(Pquote1.class, username, password ,xu, xh, xf, n1, bud); 
						}, 
						"quote"
					)
					.waitForReceive(Main.intPlaceholder*1000) 
				;
			}
			catch (TimeExpiredException e2) {
				processCall(Pabort.class, username, password ,xu, xh, xf); 
			}
			
		}
	}
	
	public static class Pquote1 extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private SessionI<SessionType> x1;
		private SessionI<SessionType> x2;
		private Integer quote;
		private Integer budget;
		
		public Pquote1(String username, String password, SessionI<SessionType> x, SessionI<SessionType> x1, SessionI<SessionType> x2, Integer quote, Integer budget) {
			super(username, password);
			this.x=x;
			this.x1=x1;
			this.x2=x2;
			this.quote=quote;
			this.budget=budget;
		}
		
		@Override
		public void run() {
			if ((quote<budget)) { 
				processCall(Pquote2.class, username, password ,x, x1, x2, quote, budget); 
			}
			else {
				processCall(Pabort.class, username, password ,x, x1, x2); 
			}
		}
	}
	
	public static class Pquote2 extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private SessionI<SessionType> x1;
		private SessionI<SessionType> x2;
		private Integer quote;
		private Integer budget;
		
		public Pquote2(String username, String password, SessionI<SessionType> x, SessionI<SessionType> x1, SessionI<SessionType> x2, Integer quote, Integer budget) {
			super(username, password);
			this.x=x;
			this.x1=x1;
			this.x2=x2;
			this.quote=quote;
			this.budget=budget;
		}
		
		@Override
		public void run() {
			try {
				logger.info("waiting on 'x2' for actions [quote]");
				Message msg = x2.waitForReceive(Main.intPlaceholder*1000, "quote"); //TODO: remove the placeholder/s
				
				logger.info("received [quote]");
				Integer quote2;
				try {
					quote2 = Integer.parseInt(msg.getStringValue());
				}
				catch (NumberFormatException e) {
					throw new RuntimeException(e);
				}
				if (((quote+quote2)<budget)) { 
					processCall(Ppay.class, username, password ,x, x1, x2, (quote+quote2)); 
				}
				else {
					processCall(Pabort.class, username, password ,x, x1, x2); 
				}
			}
			catch (TimeExpiredException e1) {
				processCall(Pabort.class, username, password ,x, x1, x2); 
			}
			
		}
	}
	
	public static class Pabort extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private SessionI<SessionType> x1;
		private SessionI<SessionType> x2;
		
		public Pabort(String username, String password, SessionI<SessionType> x, SessionI<SessionType> x1, SessionI<SessionType> x2) {
			super(username, password);
			this.x=x;
			this.x1=x1;
			this.x2=x2;
		}
		
		@Override
		public void run() {
			
			parallel(()->{
				logger.info("sending action 'abort'");
				x.sendIfAllowed("abort"); 
			});
			
			parallel(()->{
				logger.info("sending action 'abort'");
				x1.sendIfAllowed("abort"); 
			});
			
			parallel(()->{
				logger.info("sending action 'abort'");
				x2.sendIfAllowed("abort"); 
			});
			
			parallel(()->{
				logger.info("waiting on 'x' for actions [pay]");
				Message msg = x.waitForReceive("pay"); 
				
				logger.info("received [pay]");
			});
			
			parallel(()->{
				logger.info("waiting on 'x1' for actions [quote]");
				Message msg1 = x1.waitForReceive("quote"); 
				
				logger.info("received [quote]");
				Integer n;
				try {
					n = Integer.parseInt(msg1.getStringValue());
				}
				catch (NumberFormatException e) {
					throw new RuntimeException(e);
				}
			});
			
			parallel(()->{
				logger.info("waiting on 'x2' for actions [quote]");
				Message msg2 = x2.waitForReceive("quote"); 
				
				logger.info("received [quote]");
				Integer n1;
				try {
					n1 = Integer.parseInt(msg2.getStringValue());
				}
				catch (NumberFormatException e1) {
					throw new RuntimeException(e1);
				}
			});
			
			parallel(()->{
				logger.info("waiting on 'x1' for actions [confirm]");
				Message msg3 = x1.waitForReceive("confirm"); 
				
				logger.info("received [confirm]");
			});
			
			parallel(()->{
				logger.info("waiting on 'x2' for actions [confirm]");
				Message msg4 = x2.waitForReceive("confirm"); 
				
				logger.info("received [confirm]");
			});
		}
	}
	
	public static class Ppay extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private SessionI<SessionType> x1;
		private SessionI<SessionType> x2;
		private Integer amount;
		
		public Ppay(String username, String password, SessionI<SessionType> x, SessionI<SessionType> x1, SessionI<SessionType> x2, Integer amount) {
			super(username, password);
			this.x=x;
			this.x1=x1;
			this.x2=x2;
			this.amount=amount;
		}
		
		@Override
		public void run() {
			logger.info("sending action 'quote'");
			x.sendIfAllowed("quote", amount); 
			
			try {
				logger.info("waiting on 'x' for actions [pay]");
				Message msg = x.waitForReceive(Main.intPlaceholder*1000, "pay"); //TODO: remove the placeholder/s
				
				logger.info("received [pay]");
				processCall(Pconfirm1.class, username, password ,x, x1, x2); 
			}
			catch (TimeExpiredException e) {
				processCall(Pabort.class, username, password ,x, x1, x2); 
			}
			
		}
	}
	
	public static class Pconfirm1 extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private SessionI<SessionType> x1;
		private SessionI<SessionType> x2;
		
		public Pconfirm1(String username, String password, SessionI<SessionType> x, SessionI<SessionType> x1, SessionI<SessionType> x2) {
			super(username, password);
			this.x=x;
			this.x1=x1;
			this.x2=x2;
		}
		
		@Override
		public void run() {
			logger.info("sending action 'pay'");
			x1.sendIfAllowed("pay"); 
			
			logger.info("sending action 'pay'");
			x2.sendIfAllowed("pay"); 
			
			try {
				logger.info("waiting on 'x1' for actions [confirm]");
				Message msg = x1.waitForReceive(Main.intPlaceholder*1000, "confirm"); //TODO: remove the placeholder/s
				
				logger.info("received [confirm]");
				processCall(Pconfirm2.class, username, password ,x, x1, x2); 
			}
			catch (TimeExpiredException e) {
				processCall(Pabort.class, username, password ,x, x1, x2); 
			}
			
		}
	}
	
	public static class Pconfirm2 extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private SessionI<SessionType> x1;
		private SessionI<SessionType> x2;
		
		public Pconfirm2(String username, String password, SessionI<SessionType> x, SessionI<SessionType> x1, SessionI<SessionType> x2) {
			super(username, password);
			this.x=x;
			this.x1=x1;
			this.x2=x2;
		}
		
		@Override
		public void run() {
			try {
				logger.info("waiting on 'x2' for actions [confirm]");
				Message msg = x2.waitForReceive(Main.intPlaceholder*1000, "confirm"); //TODO: remove the placeholder/s
				
				logger.info("received [confirm]");
				processCall(Pcommit.class, username, password ,x, x1, x2); 
			}
			catch (TimeExpiredException e) {
				processCall(Pabort.class, username, password ,x, x1, x2); 
			}
			
		}
	}
	
	public static class Pcommit extends Participant {
		
		private static final long serialVersionUID = 1L;
		private SessionI<SessionType> x;
		private SessionI<SessionType> x1;
		private SessionI<SessionType> x2;
		
		public Pcommit(String username, String password, SessionI<SessionType> x, SessionI<SessionType> x1, SessionI<SessionType> x2) {
			super(username, password);
			this.x=x;
			this.x1=x1;
			this.x2=x2;
		}
		
		@Override
		public void run() {
			logger.info("sending action 'commit'");
			x.sendIfAllowed("commit"); 
			
			logger.info("sending action 'commit'");
			x1.sendIfAllowed("commit"); 
			
			logger.info("sending action 'commit'");
			x2.sendIfAllowed("commit"); 
		}
	}
	
	public static void main(String[] args) {
		HonestyChecker.isHonest(P.class, Main.username, Main.password);
		//new Thread(new P(Main.username, Main.password)).start();
	}
}