#no update  variables
{
init
	node s0; true
	[ 
	snd_req21||tran  s1; true; z1=0,z2=0; 1
      ]
      [
	snd_ack21||tran  s3; true; z1=0,z2=0 ; 1
      ]
      [
	snd_idle21||tran  s5; true; z1=0,z2=0 ; 1
	 ] 
}
{
	node s1;  z2<=360
	[ 
	snd_req21||tran  s1; true; null; 1
      ]
      [
	rec_req21||tran  s0; true; z1=0,z2=0 ; 1
      ]
      [
	snd_ack21||tran  s2; true; z2=0 ; 1
      ]
      [
	snd_idle21||tran  s8; true; z2=0 ; 1
	 ] 
}
{
	node s2; z1<=360
	[ 
	snd_ack21||tran  s2; true; null; 1
      ]
      [
	rec_req21||tran  s3; true; null ; 1
	 ] 
}
{
	node s3;  z2<=360
	[ 
	snd_ack21||tran  s3; true; null; 1
      ]
      [
	rec_ack21||tran  s0; true; z1=0,z2=0 ; 1
      ]
      [
	snd_idle21||tran  s4; true; z2=0 ; 1
      ]
      [
	snd_req21||tran  s7; true; z2=0 ; 1
	 ] 
}
{
	node s4; z1<=360
	[ 
	snd_idle21||tran  s4; true; null; 1
      ]
      [
	rec_ack21||tran  s5; true; null ; 1
	 ] 
}
{
	node s5;  z2<=360
	[ 
	snd_idle21||tran  s5; true; null; 1
      ]
      [
	rec_idle21||tran  s0; true; z1=0,z2=0 ; 1
      ]
      [
	snd_req21||tran  s6; true; z2=0 ; 1
      ]
      [
	snd_ack21||tran  s9; true; z2=0 ; 1
	 ] 
}
{
	node s6; z1<=360
	[ 
	snd_req21||tran  s6; true; null; 1
	]
	[
	rec_idle21||tran  s1; true; null ; 1
	 ] 
}
{
	node s7; z1<=360
	[ 
	snd_req21||tran  s7; true; null; 1
      ]
      [
	rec_ack21||tran  s1; true; null ; 1
	 ] 
}
{
	node s8; z1<=360
	[ 
	snd_idle21||tran  s8; true; null; 1
      ]
      [
	rec_req21||tran  s5; true; null ; 1
	 ] 
}
{
	node s9; z1<=360
	[ 
	snd_ack21||tran  s9; true; null; 1
      ]
      [
	rec_idle21||tran  s3; true; null ; 1
	 ] 
*