@model<tissue_psystems>

def main()
{
  /* YES EN 27 PASOS */
  /* call sat_tissue(4,2);
  @ms(2) += s{1,1},sp{2,1},s{3,1},sp{1,2},s{4,2}; */
  
  /* YES EN 33 PASOS */
  /* call sat_tissue(4,3);
  @ms(2) += s{1,1},sp{2,1},s{3,1},sp{1,2},s{4,2},s{2,2},s{2,3},sp{3,3},s{4,3};*/

 /* YES en 39 pasos */
/*	call sat_tissue(4,4);
  @ms(2) += s{1,1},sp{2,1},s{3,1},sp{1,2},s{4,2},s{2,2},s{2,3},sp{3,3},s{4,3},sp{4,4};*/

/* yes en 45 pasos */
/*	call sat_tissue(4,5);
  @ms(2) += s{1,1},sp{2,1},s{3,1},sp{1,2},s{4,2},s{2,2},s{2,3},sp{3,3},s{4,3},sp{4,4},sp{2,5};*/

/* NO en 52 pasos */
/*call sat_tissue(4,6);
  @ms(2) += s{1,1},sp{2,1},s{3,1},sp{1,2},s{4,2},s{2,2},s{2,3},sp{3,3},s{4,3},sp{4,4},sp{2,5},s{1,6};
*/

/* NO en 22 pasos*/
/*call sat_tissue(2,3);
@ms(2) += s{1,1},sp{2,1},s{2,2};
*/

/* YES en 27 pasos */
/*call sat_tissue(3,3);
@ms(2) += s{1,1},sp{2,1},s{2,2},s{3,3};
*/

/* Yes en 32 pasos */
/*
call sat_tissue(3,4);
@ms(2) += s{1,1},sp{2,1},sp{1,2},sp{2,3},s{3,4};
*/

/* Yes en 63 pasos */
/*call sat_tissue(4,8);
@ms(2) += s{1,1},s{2,1},sp{3,1},s{4,1},
          sp{1,2},s{2,2},
          s{1,3},sp{2,3},sp{3,3},s{1,3},
          s{2,4},sp{3,4},s{4,4},
          sp{1,5},s{2,5},s{4,5},
          s{2,6},sp{3,6},s{4,6},
          s{1,7},s{4,7},
          sp{1,8},s{2,8},s{3,8},s{4,8};
*/

/* yes en 69 pasos */
/*call sat_tissue(4,9);
@ms(2) += s{1,1},s{2,1},sp{3,1},s{4,1},
          sp{1,2},s{2,2},
          s{1,3},sp{2,3},sp{3,3},s{1,3},
          s{2,4},sp{3,4},s{4,4},
          sp{1,5},s{2,5},s{4,5},
          s{2,6},sp{3,6},s{4,6},
          s{1,7},s{4,7},
          sp{1,8},s{2,8},s{3,8},s{4,8},
          s{2,9},sp{3,9};*/
/* yes en 75 pasos */
/*
call sat_tissue(4,10);
@ms(2) += s{1,1},s{2,1},sp{3,1},s{4,1},
          sp{1,2},s{2,2},
          s{1,3},sp{2,3},sp{3,3},s{1,3},
          s{2,4},sp{3,4},s{4,4},
          sp{1,5},s{2,5},s{4,5},
          s{2,6},sp{3,6},s{4,6},
          s{1,7},s{4,7},
          sp{1,8},s{2,8},s{3,8},s{4,8},
          s{2,9},sp{3,9},
          s{1,10};
*/

call sat_tissue(4,11);
@ms(2) += s{1,1},s{2,1},sp{3,1},s{4,1},
          sp{1,2},s{2,2},
          s{1,3},sp{2,3},sp{3,3},s{1,3},
          s{2,4},sp{3,4},s{4,4},
          sp{1,5},s{2,5},s{4,5},
          s{2,6},sp{3,6},s{4,6},
          s{1,7},s{4,7},
          sp{1,8},s{2,8},s{3,8},s{4,8},
          s{2,9},sp{3,9},
          s{1,10},
          sp{2,11};
}

def sat_tissue(n,m)
{
  call init_cells();
  call init_multisets(n);
  call init_environment(n,m);
  call rules(n,m); 
}

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

def init_multisets(n)
{
  @ms(1) = yes,no,b{1},c{1},d{1},e{1};
  @ms(2) = f,g;
  @ms(2) += a{i} : 1<=i<=n;
}

def init_environment(n,m)
{
  @ms(0) = f,q;
  @ms(0) += s{i,j},sp{i,j} : 1<=i<=n,1<=j<=m;
  @ms(0) += a{i},t{i},f{i} : 1<=i<=n;
  @ms(0) += r{i} : 1<=i<=m;
  @ms(0) += T{i},F{i} : 1<=i<=n;
  @ms(0) += T{i,j},F{i,j} : 1<=i<=n,1<=j<=m+1;
  @ms(0) += b{i} : 1<=i<=3*n+m+1;
  @ms(0) += c{i} : 1<=i<=n+1;
  @ms(0) += d{i} : 1<=i<=3*n+n*m+2*m+1;
  @ms(0) += e{i} : 1<=i<=3*n+n*m+2*m+3;
}

def rules(n,m)
{
  [a{i}]'2 --> [T{i}]'2 [F{i}]'2 : 1<=i<=n;
 
  {
    [b{i}]'1 <--> [b{i+1}*2]'0; 
    [c{i}]'1 <--> [c{i+1}*2]'0; 
    [d{i}]'1 <--> [d{i+1}*2]'0;
  } : 1<=i<=n;
  
  [e{i}]'1 <--> [e{i+1}]'0   : 1<=i<=3*n+n*m+2*m;
  
 
  
  [b{n+1},c{n+1},d{n+1}]'1 <--> [f]'2;
  /*[d{n+1}]'1        <--> [g]'2;*/
 
  {
    [c{n+1},T{i}]'2 <--> [c{n+1},T{i,1}]'0;
    [c{n+1},F{i}]'2 <--> [c{n+1},F{i,1}]'0; 
  } : 1<=i<=n;
  {
    [T{i,j}]'2 <--> [t{i},T{i,j+1}]'0;
    [F{i,j}]'2 <--> [f{i},F{i,j+1}]'0;
  } : 1<=i<=n,1<=j<=m;
 
  {
    [b{i}]'2 <--> [b{i+1}]'0;
    [d{i}]'2 <--> [d{i+1}]'0;
  } : n+1<=i<=(n+1)+(2*n+m)-1;
 
  {
    [b{3*n+m+1},t{i},s{i,j}]'2 <--> [b{3*n+m+1},r{j}]'0;
    [b{3*n+m+1},f{i},sp{i,j}]'2 <--> [b{3*n+m+1},r{j}]'0;
  } : 1<=i<=n,1<=j<=m;
  
  [d{i}]'2 <--> [d{i+1}]'0 : 3*n+m+1<=i<=3*n+n*m+m;
  
  [d{3*n+n*m+m+i},r{i}]'2 <--> [d{3*n+n*m+m+i+1}]'0 : 1<=i<=m;
  
  [d{3*n+n*m+2*m+1}]'2 <--> [yes,q]'1;
  
  [e{3*n+n*m+2*m+1}]'1 <--> [e{3*n+n*m+2*m+2},q]'0;
 
  [e{3*n+n*m+2*m+2}]'1 <--> [e{3*n+n*m+2*m+3}]'0;
  
  [yes]'2 <--> [#]'0;
  
  [e{3*n+n*m+2*m+3},no,q]'1 <--> [#]'2;
  [no]'2 <--> [#]'0;
}