colpn  [garden_multigates_fixedGateNumber_test]
{
constants:
all:
  int LOOP = 10;
  int N = 2;
  int TOTAL = N*LOOP;
  int bbb = 1;
  int bba = bbb;
  int g2 = 5;
  int gg = g2*4;

colorsets:
  Dot = {dot};
  Loop = {0..LOOP};
  Count = {0..TOTAL};
  Gates = {1..N};
  Loops = PROD(Gates,Loop);
  Counts = PROD(Gates,Count);

variables:
  Count : x;
  Loop : i;
  Count : y;
  Gates : g;
  Count : a;

places:
discrete:
  Dot begin = 1`dot;
  Dot cobegin_p = 0`dot;
  Gates process_begin = 0`all;
  Gates process_end = 0`all;
  Dot write = 0`dot;
  Dot end = 0`dot;
  Gates T_loop = 0`all;
  Gates T_in_loop = 0`all;
  Count count = 1`0;
  Counts T_set = 0`all;
  Loops loop = 1`(all,LOOP);
  Gates reset = 0`all;
  Gates loop_set = 0`all;

transitions:
  cobegin
    : 
    : [process_begin + {all}] & [cobegin_p - {1`dot}]
    ;
  coend
    : 
    : [write + {1`dot}] & [process_end - {all}]
    ;
  do_write
    : 
    : [end + {1`dot}] & [write - {1`dot}]
    ;
  T_turnstile
    : 
    : [T_loop + {g}] & [process_begin - {g}]
    ;
  T_end_for
    : 
    : [process_end + {g}] & [loop + {(g,0)}] & [T_loop - {g}] & [loop - {(g,0)}]
    ;
  T_begin_for
 {[i!=0]}
    : 
    : [T_in_loop + {g}] & [loop + {(g,i-1)}] & [T_loop - {g}] & [loop - {(g,i)}]
    ;
  T_read
    : 
    : [count + {x}] & [T_set + {(g,x)}] & [count - {x}] & [T_in_loop - {g}]
    ;
  T_incr
    : 
    : [count + {x+1}] & [T_loop + {g}] & [count - {y}] & [T_set - {(g,x)}]
    ;
  set_0
    : 
    : [count + {0}] & [cobegin_p + {1`dot}] & [count - {x}] & [begin - {1`dot}]
    ;
  next_run1
    : 
    : [reset + {all}] & [end - {1`dot}]
    ;
  next_run2
    : 
    : [begin + {1`dot}] & [loop_set - {all}]
    ;
  reset_loop
    : 
    : [loop_set + {g}] & [loop + {(g,LOOP)}] & [reset - {g}] & [loop - {(g,i)}]
    ;

}