@model<tissue_psystems>

def main()
{
/* Yes en 63 pasos */

call sat_tissue(4,7);
@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{4,3},
          s{2,4},sp{3,4},s{4,4},
          sp{1,5},s{2,5},s{4,5},
          s{1,6},s{4,6},
          sp{1,7},s{2,7},s{3,7},s{4,7};
}

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) = q,b{1},c{1},d{1},e{1},yes,no;
  @ms(2) += a{i} : 1<=i<=n;
  @ms(2) += f;
}

def init_environment(n,m)
{
  
  @ms(0) += s{i,j},sp{i,j} : 1<=i<=n,1<=j<=m;
  @ms(0) += a{i},t{i},f{i},T{i},F{i} : 1<=i<=n;
  @ms(0) += r{i} : 1<=i<=m;
  @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;
  @ms(0) += f,q;
}

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+2;

  [b{n+1},c{n+1},d{n+1}]'1 <--> [f]'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<=3*n+m;

  {
    [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;
  
  [yes]'2 <--> [#]'0;

	/*
  
  [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;
  
  */

  [e{3*n+n*m+2*m+3},q,no]'1 <--> [#]'2;

  [no]'2 <--> [#]'0;
}