STP

 
process STP[self : 0..MAXUID]

constant

	MAXUID,

	MAXTID,

	MAXSEQ,

	MAXCERT,

	MAXSIGN,

	MAXHASH,

	MAXKEY

input

	self_cert :	array [0..MAXUID] of 0..MAXCERT

function

	Sign(0..MAXKEY, integer) returns 0..MAXSIGN,

	Verify(0..MAXKEY, integer) returns 0..MAXSIGN,

	Hash(integer) returns 0..MAXHASH,

	Unique(0..MAXTID) returns boolean,

	Id(0..MAXCERT) returns 0..MAXUID,

	Key(0..MAXCERT) returns 0..MAXKEY,

	SelfKey(0..MAXCERT) returns 0..MAXKEY

variable

	msgtype :	set {T-start, T-accept, T-data, T-token, T-commit, T-abort, T-fault},

	state :		set {null, sending, receiving, ready, committed, aborted},

	t_state :	array [0..MAXTID] of state init null,

	t_other :	array [0..MAXTID] of 0..MAXUID,

	t_key :		array [0..MAXTID] of 0..MAXKEY,

	t_data :	array [0..MAXTID, 0..MAXSEQ] of integer,

	t_seq :		array [0..MAXTID] of 0..MAXSEQ,

	t_context :	array [0..MAXTID] of 0..MAXHASH,

	cert :		0..MAXCERT,

	data :		integer,

	sign :		0..MAXSIGN,

	context :	0..MAXHASH,

	valid :		boolean

parameter

	tid :		0..MAXTID

begin

	(t_state[tid] = null   Unique(tid))   {Action 0}

	t_other[tid] := any;

	cert := self_cert[t_other[tid]];

	sign := Sign(SelfKey(cert), T-starttidt_other[tid]);

	send T-start(tid, sign, cert) to t_other[tid];

 rcv T-start(tid, sign, cert)   {Action 1}

	valid := (sign = Verify(Key(cert), T-starttidself)   t_state[tid] = null);

	if true  

		skip;

	 (valid)  

		t_state[tid], t_seq[tid], t_context[tid] := receiving, 0, 0;

		t_other[tid], t_key[tid] := Id(cert), Key(cert);

		cert := self_cert[t_other[tid]];

		sign := Sign(SelfKey(cert), T-accepttid);

		send T-accept(tid, sign, cert) to t_other[tid];

	fi

 rcv T-accept(tid,  sign, cert)   {Action 2}

	valid := (sign = Verify(Key(cert), T-accepttid)   t_state[tid] = null);

	if ( valid    (Id(cert) = t_other[tid]))  

		skip;

	 (valid   Id(cert) = t_other[tid])  

		t_state[tid], t_seq[tid], t_context[tid] := sending, 0, 0;

		t_key[tid] := Key(cert);

	fi

 (t_state[tid] = sending)   {Action 3}

	cert := self_cert[t_other[tid]];

	if true  

		data := any;

		sign := Sign(SelfKey(cert), T-datatiddatat_context[tid]);

		send T-data(tid, data, t_context[tid], sign) to t_other[tid];

		t_data[tid, t_seq[tid]] := data;

		t_context[tid] := Hash(datat_context[tid]);

		t_seq[tid] := t_seq[tid] + 1;

	 true  

		sign := Sign(SelfKey(cert), T-tokentidt_context[tid]);

		send T-token(tid, t_context[tid], sign) to t_other[tid];

		t_state[tid] := receiving;

	 true  

		sign = Sign(SelfKey(cert), T-aborttid);

		send T-abort(tid, sign) to t_other[tid];

		t_state[tid] := aborted;

	 true  

		sign = Sign(SelfKey(cert), T-committidt_context[tid]);

		send T-commit(tid, t_context[tid], sign) to t_other[tid];

		t_state[tid] := ready;

	fi

 rcv T-data(tid, data, context, sign)   {Action 4}

	valid := (sign = Verify(t_key[tid], T-datatiddatacontext)   t_state[tid] = receiving);

	if ( valid    (context = t_context[tid]))  

		skip;

	 (valid   context = t_context[tid])  

		t_data[tid, t_seq[tid]] := data;

		t_context[tid] := Hash(datat_context[tid]);

		t_seq[tid] := t_seq[tid] + 1;

	fi

 rcv T-token(tid, context, sign)   {Action 5}

	valid := (sign = Verify(t_key[tid], T-tokentidcontext)   t_state[tid] = receiving);

	if ( valid)  

		skip;

	 (valid     (context = t_context[tid]))  

		cert := self_cert[t_other[tid]];

		sign := Sign(SelfKey(cert), T-aborttid);

		send T-abort(tid, sign) to t_other[tid];

		t_state[tid] := aborted;

	 (valid   context = t_context[tid])  

		t_state[tid] := sending;

	fi

 rcv T-commit(tid, context, sign)   {Action 6}

	valid := (sign = Verify(t_key[tid], T-committidcontext)

		   (t_state[tid] = sending   t_state[tid] = null));

	if ( valid)  

		skip;

	 (valid   t_state[tid] = aborted)  

		cert := self_cert[t_other[tid]];

		sign := Sign(SelfKey(cert), T-aborttid);

		send T-abort(tid, sign) to t_other[tid];

	 (valid   t_state[tid] = committed)  

		cert := self_cert[t_other[tid]];

		sign := Sign(SelfKey(cert), T-committid0);

		send T-commit(tid, 0, sign) to t_other[tid];

	 (valid   t_state[tid] = ready)  

		t_state[tid] := committed;

	 (valid   t_state[tid] = receiving)  

		if true  

			cert := self_cert[t_other[tid]];

			sign := Sign(SelfKey(cert), T-aborttid);

			send T-abort(tid, sign) to t_other[tid];

			t_state[tid] := aborted;

		 (context = t_context[tid])  

			cert := self_cert[t_other[tid]];

			sign := Sign(SelfKey(cert), T-committid0);

			send T-commit(tid, 0, sign) to t_other[tid];

			t_state[tid] := committed;

		fi

	fi

 rcv T-abort(tid, sign)   {Action 7}

	valid := (sign = Verify(t_key[tid], T-aborttid)

		   (t_state[tid] = null   t_state[tid] = committed));

	if ( valid)  

		skip;

	 (valid)  

		t_state[tid] := aborted;

	fi

 rcv T-fault(tid)   {Action 8}

	if (t_state[tid] = null   t_state[tid] = committed   t_state[tid] = aborted)  

		skip;

	 (t_state[tid] = sending   t_state[tid] = receiving)  

		t_state[tid] := aborted;

	 (t_state[tid] = ready)  

		cert := self_cert[t_other[tid]];

		sign := Sign(SelfKey(cert), T-committidt_context[tid]);

		send T-commit(tid, t_context[tid], sign) to t_other[tid];

	fi

end