#define BB	1

#define QSZ	2

mtype = { close, aclose, dial, adial, talk, htalk,
	numb, numbis, answer, trans, transok, atalk, nak, hangup,
	sysclose, opent, opend, ioattn, call, cnak };

chan h_envirn = [QSZ] of { byte };
chan h_normal = [QSZ] of { byte };
chan h_extern = [QSZ] of { byte };
chan c_normal = [QSZ] of { byte };
chan c_extern = [QSZ] of { byte };
chan c_envirn = [QSZ] of { byte };

active proctype host()
{
	xr h_normal;
	xr h_extern;
	xs c_normal;
	xs h_envirn;
end:
closed:
	do
	:: h_normal?close    -> c_normal!aclose
	:: h_normal?aclose
	:: h_normal?adial
	:: h_normal?talk     -> c_normal!close; goto lclosed
	:: h_normal?atalk
	:: h_normal?nak      -> c_normal!close
	:: h_extern?opent    -> c_normal!talk; goto watalk
	:: h_extern?opend    -> c_normal!dial; goto wadial
	od;
dialing:
	do
	:: h_normal?close    -> c_normal!aclose; goto rclosed
	:: h_normal?adial
	:: h_normal?talk     -> c_normal!atalk; h_envirn!htalk; goto talking
	:: h_normal?atalk
	:: h_extern?sysclose -> c_normal!close; goto lclosed
	od;
talking:
	do
	:: h_normal?close    -> c_normal!aclose; goto rclosed
	:: h_normal?adial
	:: h_normal?talk     -> c_normal!atalk
	:: h_normal?atalk
	:: h_extern?sysclose -> c_normal!close; goto lclosed
	:: h_extern?ioattn   -> c_normal!dial; goto wattn
	od;
rclosed:
	do
	:: h_normal?close    -> c_normal!aclose
	:: h_extern?sysclose -> c_normal!close; goto lclosed
	od;
watalk:
	do
	:: h_normal?close    -> c_normal!aclose
	:: h_normal?aclose
	:: h_normal?atalk    -> goto wtalk
	:: h_normal?nak
	:: h_extern?sysclose -> c_normal!close; goto lclosed
	:: timeout   -> c_normal!talk
	od;
wadial:
	do
	:: h_normal?close    -> c_normal!aclose
	:: h_normal?aclose
	:: h_normal?adial    -> goto dialing
	:: h_normal?atalk
	:: h_normal?nak
	:: h_extern?sysclose -> c_normal!close; goto lclosed
	:: timeout   -> c_normal!dial
	od;
lclosed:
	do
	:: h_normal?close    -> c_normal!aclose
	:: h_normal?aclose   -> goto closed
	:: h_normal?adial
	:: h_normal?talk     -> c_normal!atalk; c_normal!close
	:: h_normal?atalk
	:: h_normal?nak
	:: h_extern?sysclose
	:: timeout   -> c_normal!close
	od;
wtalk:
	do
	:: h_normal?close    -> c_normal!aclose; goto rclosed
	:: h_normal?talk     -> c_normal!atalk; goto talking
	:: h_normal?atalk
	:: h_normal?nak   -> goto closed
	:: h_extern?sysclose -> c_normal!close
	od;
wattn:
	do
	:: h_normal?close    -> c_normal!aclose; goto rclosed
	:: h_normal?adial    -> goto dialing
	:: h_normal?talk     -> c_normal!atalk
	:: h_normal?atalk
	:: h_extern?sysclose -> c_normal!aclose; goto lclosed
	:: timeout  -> c_normal!dial
	od;
endfail:
	do
	:: h_normal?nak
	:: h_extern?sysclose
	od
}

active proctype cont()
{
	xr c_normal;
	xr c_extern;
	xs h_normal;
	xs c_envirn;
end:
idle:
	do
	:: c_normal?close  -> h_normal!aclose
	:: c_normal?aclose
	:: c_normal?dial   -> h_normal!adial; c_envirn!trans; goto dialing
	:: c_normal?adial
	:: c_normal?talk   ->  goto wproc
	:: c_normal?atalk
	:: c_normal?nak    -> h_normal!close
	:: c_extern?call   -> c_envirn!cnak
	od;
dialing:
	do
	:: c_normal?close   -> h_normal!aclose; goto idle
	:: c_normal?dial    -> h_normal!adial
	:: c_extern?call    -> c_envirn!cnak
	:: c_extern?cnak    -> h_normal!nak; goto wclose
	:: c_extern?transok -> c_envirn!call; goto wproc
	od;
talking:
	do
	:: c_normal?close  -> h_normal!aclose; c_envirn!hangup; goto idle
	:: c_normal?dial   -> h_normal!adial; goto dialing
	:: c_normal?talk   -> h_normal!atalk
	:: c_normal?atalk
	:: c_extern?call   -> c_envirn!cnak
	:: c_extern?hangup -> h_normal!close; goto lclosed
	od;
wcall:
	do
	:: c_normal?close  -> h_normal!aclose; goto idle
	:: c_normal?talk   -> h_normal!atalk
	:: c_extern?call   -> c_envirn!numb; goto wnumb
	od;
wnumb:
	do
	:: c_normal?close  -> h_normal!aclose; c_envirn!hangup; goto idle
	:: c_normal?talk   -> h_normal!atalk
	:: c_extern?call   -> c_envirn!cnak
	:: c_extern?cnak   -> h_normal!nak; goto wclose
	:: c_extern?numbis -> h_normal!talk; c_envirn!answer; goto watalk
	od;
watalk:
	do
	:: c_normal?close  -> h_normal!aclose; c_envirn!hangup; goto idle
	:: c_normal?dial   -> h_normal!adial
	:: c_normal?talk   -> h_normal!atalk
	:: c_normal?atalk  -> goto talking
	:: c_extern?call   -> c_envirn!cnak
	:: c_extern?hangup -> h_normal!close; goto lclosed
	:: timeout -> h_normal!talk
	od;
wclose:
	do
	:: c_normal?close  -> h_normal!aclose; goto idle
	:: c_normal?dial   -> h_normal!adial
	:: c_normal?adial
	:: c_normal?talk   -> h_normal!atalk
	:: c_normal?atalk
	:: c_extern?call   -> c_envirn!cnak
	od;
lclosed:
	do
	:: c_normal?close  -> h_normal!aclose; goto idle
	:: c_normal?aclose -> goto idle
	:: c_normal?dial   -> h_normal!adial; h_normal!close
	:: c_normal?adial
	:: c_normal?talk   -> h_normal!atalk; h_normal!close
	:: c_normal?atalk
	:: c_normal?nak -> h_normal!close
	:: c_extern?call   -> c_envirn!cnak
	:: timeout -> h_normal!close
	od;
wproc:
	do
	:: c_normal?close  -> h_normal!aclose; c_envirn!hangup; goto idle
	:: c_normal?dial   -> h_normal!adial
	:: c_normal?talk   -> h_normal!atalk
	:: c_extern?call   -> c_envirn!cnak
	:: c_extern?answer -> h_normal!talk; goto watalk
	:: c_extern?cnak   -> h_normal!nak; goto wclose
	:: c_extern?numb   -> c_envirn!numbis
	od;
endfail:
	do
	:: c_normal?nak
	:: c_extern?call   -> c_envirn!cnak
	od
}

active proctype cenvir()
{
	xr c_envirn;
	xs c_extern;

end:	do
	:: c_envirn?numbis ->
			if
			:: c_extern!answer
			:: c_extern!hangup
			fi
	:: c_envirn?trans ->
			if
			:: c_extern!transok
			:: c_extern!cnak
			fi
	:: c_envirn?answer -> c_extern!hangup
	:: c_envirn?cnak
	:: c_envirn?hangup
	:: c_envirn?numb   ->
			if
			:: c_extern!numbis
			:: c_extern!hangup
			fi
	:: c_envirn?call   ->
			if
			:: c_extern!numb
			:: c_extern!cnak
			fi
	od
}

active proctype henvir()
{
	xs h_extern;
	xr h_envirn;
end:
idle:
	if
	:: h_extern!opent; goto open
	:: h_extern!opend; goto open
	fi;
open:
	if
	:: h_extern!sysclose; goto idle	
	:: h_envirn?htalk;    goto talking
	fi;
talking:
	if
	:: h_extern!sysclose
	:: h_extern!ioattn; goto open
	fi
}