@model<TSCS>

def main()
{
	let m= 3; 
	let n= 4; 
	
	call init_membrane_structure();
	call init_first_alphabet(m,n);
	call init_second_alphabet(m,n);
	call init_environment(m,n);
	call init_multisets();
	call init_rules(m,n);
	call define_input();
}


def define_input()
{
/* DEFINIR AQUI LA DE ENTRADA DEL SISTEMA P */
/* ESCRIBIR DIFERENTES FUNCIONES PARA DIFERENTES ENTRADAS */
@ms(3) +=nx{1,1},x{2,1},x{3,1},x{1,2},nx{2,2},nx{3,2},x{1,3},nx{2,3},x{3,3}, x{1,4},x{2,4},x{3,4};

}


def init_membrane_structure()
{
	@mu = [ [ ]'1 [ ]'2 [ ]'3 ]'0;
}


def init_first_alphabet(m,n)
{
	@ms1 += A{i},B{i} : 1<=i<=n+1;
	@ms1 += a{i},b{i},T{i},F{i},y{i},v{i},w{i} : 1<=i<=n;
	@ms1 += c{i},t{i},f{i},s{i},z{i} : 1<= i <= n-1;
	@ms1 += E{j} : 1<= j <= m+1;
	@ms1 += alpha{i} : 0<= i <= 3*n+2*m+1;
	@ms1 += beta{i} : 0<= i <= 3*n + 2*m +2;
	@ms1 += q{i,j},r{i,j},u{i,j} : 1<=i<=n-1,1<=j<=n-1;
	@ms1 += x{i,j},nx{i,j},e{i,j},ne{i,j} : 1<=i<=n,1<=j<=m;
	@ms1 += d{i,j,k},nd{i,j,k} : 1 <=i<=n,1<=j<=m,1<=k<=n;
	@ms1 += q{0},S,yes,no;

}

def init_second_alphabet(m,n)
{
	@ms2 += Ap{i},Bp{i} : 1<=i<=n+1;
	@ms2 += ap{i},bp{i},Tp{i},Fp{i} : 1<=i<=n;
}

def init_environment(m,n)
{
	@ms(0) += S;
	@ms(0) += A{i},B{i},Ap{i},Bp{i} : 2<=i<=n+1;
	@ms(0) += T{i},F{i},Fp{i},y{i},w{i} : 1<=i<=n;
	@ms(0) += a{i},ap{i},b{i},bp{i},v{i} : 2<=i<=n;
	@ms(0) += Tp{i},c{i},t{i},f{i},s{i},z{i} : 1<=i<=n-1;
	@ms(0) += E{j} : 1<=j<=m+1;
	@ms(0) += alpha{i} : 1<= i <= 3*n+2*m+1;
	@ms(0) += beta{i} : 1<=i<=3*n+2*m+2;
	@ms(0) += q{i,j},r{i,j},u{i,j} : 1<=i<=n-1,2<=j<=n-1;
	@ms(0) += r{1,1}; 
	@ms(0) += u{1,1}; 
	@ms(0) += e{i,j},ne{i,j} : 1<=i<=n,1<=j<=m;
	@ms(0) += d{i,j,k},nd{i,j,k} : 1<=i<=n,1<=k<=n,1<=j<=m;
}

def init_multisets()
{
	@ms(1) = A{1},B{1};
	@ms(2) = a{1},ap{1},b{1},bp{1},v{1},q{1,1},alpha{0},yes,no;
	@ms(3) = beta{0};
}
def init_rules(m,n)
{
	/*1*/  [A{i}]'1    <--> [a{i},ap{i}]'2 : 1<=i<=n;
	       [A{n+1}]'1  <--> [E{1}]'2;
	/*2*/  [Ap{i}]'1   <--> [a{i},ap{i}]'2 : 1<=i<=n;
	       [Ap{n+1}]'1 <--> [E{1}]'2;
	/*3*/  [B{i}]'1    <--> [b{i},bp{i}]'2 : 1<=i<=n;
	/*4*/  [Bp{i}]'1   <--> [b{i},bp{i}]'2 : 1<=i<=n;
	/*5*/  [T{i}]'1    <--> [t{i}]'2       : 1<=i<=n-1;
	/*6*/  [Tp{i}]'1   <--> [t{i}]'2       : 1<=i<=n-1;
	/*7*/  [F{i}]'1    <--> [f{i}]'2       : 1<=i<=n-1;
	/*8*/  [Fp{i}]'1   <--> [f{i}]'2       : 1<=i<=n-1;
	/*9*/  [t{i}]'1    <--> [T{i},Tp{i}]'0 : 1<=i<=n-1; 
	/*10*/ [f{i}]'1    <--> [F{i},Fp{i}]'0 : 1<=i<=n-1;
	/*11*/ [b{i}]'1    <--> [B{i+1},S]'0   : 1<=i<=n;
	       [B{n+1}]'1  <--> [#]'0;
	/*12*/ [bp{i}]'1   <--> [Bp{i+1}]'0    : 1<=i<=n;
	       [Bp{n+1}]'1 <--> [#]'0;
	/*13*/ [a{i}]'1    <--> [T{i},A{i+1}]'0 : 1<=i<=n;
	/*14*/ [ap{i}]'1   <--> [Fp{i},Ap{i+1}]'0 : 1<=i<=n;
	/*15*/ [A{i}]'2    <--> [c{i}]'0          : 1<=i<=n-1;
	       [A{i}]'2    <--> [#]'0             : n<=i<=n+1;
	/*16*/ [Ap{i}]'2   <--> [c{i}]'0          : 1<=i<=n-1;
	       [Ap{i}]'2   <--> [#]'0             : n<=i<=n+1;
	/*17*/ [B{i}]'2    <--> [c{i}]'0          : 1<=i<=n-1;
	       [B{n}]'2    <--> [#]'0;
	/*18*/ [Bp{i}]'2   <--> [c{i}]'0          : 1<=i<=n-1;
	       [Bp{n}]'2   <--> [#]'0;
	/*19*/ [c{i}]'2    <--> [b{i+1},bp{i+1}]'0 : 1<=i<=n-1;
	/*20*/ [v{i}]'2    <--> [y{i}*2]'0         : 1<=i<=n;
	/*21*/ [y{i}]'2    <--> [z{i},w{i}]'0      : 1<=i<=n-1;
	       [y{n}]'2    <--> [w{n}]'0;
	/*22*/ [z{i}]'2    <--> [v{i+1}]'0         : 1<=i<=n-1;
	/*23*/ [w{i}]'2    <--> [a{i+1},ap{i+1}]'0  : 1<=i<=n-1;
	       [w{n}]'2    <--> [E{1}]'0;
	/*24*/ [q{1,1}]'2  <--> [r{1,1}]'0;
	/*25*/ [q{i,j}]'2  <--> [r{i,j}*2]'0       : 1<=i<=n-1,2<=j<=n-1;
	/*26*/ [r{i,j}]'2  <--> [s{i},u{i,j}]'0    : 1<=i<=n-1,1<=j<=n-1;
	/*27*/ [s{i}]'2    <--> [t{i},f{i}]'0      : 1<=i<=n-1;
	/*28*/ [u{1,j}]'2  <--> [q{1,j+1},q{2,j+1}]'0 : 1<=j<=n-2;
	/*29*/ [u{i,j}]'2  <--> [q{i+1,j+1}]'0 : 2<=i<=n-2,2<=j<=n-2;
	/*30*/ [u{i,n-1}]'2 <--> [#]'0         : 1<=i<=n-1;
	/*31*/ [T{i}]'2     <--> [#]'0         : 1<=i<=n-1;
	/*32*/ [Tp{i}]'2    <--> [#]'0         : 1<=i<=n-1;
	/*33*/ [F{i}]'2     <--> [#]'0         : 1<=i<=n-1;
	/*34*/ [Fp{i}]'2    <--> [#]'0         : 1<=i<=n-1;
	/*35*/ [S]'1 --> [ ]'1 [ ]'1;
	/*36*/ [alpha{i}]'2 <--> [alpha{i+1}]'0 : 0<=i<=3*n+2*m;
	/*37*/ [beta{i}]'3  <--> [beta{i+1}]'0  : 0<=i<=3*n+2*m+1;
	/*38*/ [x{i,j}]'3   <--> [d{i,j,1}*2]'0 : 1<=i<=n,1<=j<=m;
	       [nx{i,j}]'3  <--> [nd{i,j,1}*2]'0 : 1<=i<=n,1<=j<=m;
	/*39*/ [d{i,j,k}]'3 <--> [d{i,j,k+1}*2]'0 : 1<=i<=n,1<=j<=m,1<=k<=n-1;
	       [nd{i,j,k}]'3 <--> [nd{i,j,k+1}*2]'0 : 1<=i<=n,1<=j<=m,1<=k<=n-1;
	/*40*/ [d{i,j,n}]'3 <--> [e{i,j}]'0 : 1<=i<=n,1<=j<=m;
	       [nd{i,j,n}]'3 <--> [ne{i,j}]'0 : 1<=i<=n, 1<=j<=m;
	/*41*/ [T{i},E{j}]'1 <--> [e{i,j}]'3 : 1<=i<=n,1<=j<=m;
	       [F{i},E{j}]'1 <--> [ne{i,j}]'3 : 1<=i<=n,1<=j<=m;
	       [Tp{i},E{j}]'1 <--> [e{i,j}]'3 : 1<=i<=n,1<=j<=m;
	       [Fp{i},E{j}]'1 <--> [ne{i,j}]'3 : 1<=i<=n,1<=j<=m;
	/*42*/ [e{i,j}]'1 <--> [T{i},E{j+1}]'0 : 1<=i<=n,1<=j<=m-1;
	       [ne{i,j}]'1 <--> [F{i},E{j+1}]'0 : 1<=i<=n,1<=j<=m-1;
	/*43*/ [e{i,m}]'1 <--> [E{m+1}]'0 : 1<=i<=n;
	       [ne{i,m}]'1 <--> [E{m+1}]'0 : 1<=i<=n;
	/*44*/ [T{i}]'3 <--> [#]'0 : 1<=i<=n;
	       [F{i}]'3 <--> [#]'0 : 1<=i<=n;
	       [Tp{i}]'3 <--> [#]'0 : 1<=i<=n;
	       [Fp{i}]'3 <--> [#]'0 : 1<=i<=n;
	/*45*/ [E{j}]'3 <--> [#]'0 : 1<=j<=m;
	/*46*/ [E{m+1}]'1 <--> [yes,alpha{3*n+1+2*m}]'2;
	/*47*/ [yes]'1 <--> [beta{3*n+1+2*m+1}]'3;
	/*48*/ [alpha{3*n+1+2*m}]'2 <--> [beta{3*n+1+2*m+1}]'3;
	/*49*/ [no,beta{3*n+1+2*m+1}]'2 <--> [#]'0;
	/*50*/ [yes]'3 <--> [#]'0;      
	                            
}