// FILE: kanban.sm
// An example of state-space generation.

print(" *** The kanban manufacturing system example            *** \n");
print("*** (set Verbose to true to obtain the exact runtimes). ***\n\n");


spn kanban(int n, bool rough) := { 
  place pm1, pback1, pkan1, pout1, pm2, pback2, pkan2, pout2,
        pm3, pback3, pkan3, pout3, pm4, pback4, pkan4, pout4; 
  trans tin1, tredo1, tok1, tback1, tin2, tredo2, tok2, tback2, tout2,
        tredo3, tok3, tback3, tredo4, tok4, tback4, tout4; 
  cond(rough,
  partition(pm1:pback1:pkan1:pout1,   pm2:pback2:pkan2:pout2,
            pm3:pback3:pkan3:pout3,   pm4:pback4:pkan4:pout4),
  partition(pm1, pback1, pkan1, pout1, pm2, pback2, pkan2, pout2,
            pm3, pback3, pkan3, pout3, pm4, pback4, pkan4, pout4));
  firing(tin1:expo(1.0), tredo1:expo(0.36), tok1:expo(0.84), 
	 tback1:expo(0.3), tin2: expo(0.4), tredo2:expo(0.42), 
	 tok2: expo(0.98), tback2:expo(0.3), tout2: expo(0.5), 
	 tredo3:expo(0.39), tok3:expo(0.91), tback3:expo(0.3), 
	 tredo4:expo(0.33), tok4:expo(0.77), 
	 tback4:expo(0.3), tout4:expo(0.9)); 
  arcs(pkan1:tin1, tin1:pm1, pm1:tredo1, pm1:tok1, tredo1:pback1,
       tok1:pout1, pback1:tback1, tback1:pm1, pout1:tin2, tin2:pkan1, 
       pkan2:tin2, tin2:pm2, pm2:tredo2, pm2:tok2, tredo2:pback2,
       tok2:pout2, pback2:tback2, tback2:pm2, pout2:tout2, tout2:pkan2, 
       pkan3:tin2, tin2:pm3, pm3:tredo3, pm3:tok3, tredo3:pback3,
       tok3:pout3, pback3:tback3, tback3:pm3, pout3:tout2, tout2:pkan3, 
       pkan4:tout2, tout2:pm4, pm4:tredo4, pm4:tok4, tredo4:pback4,
       tok4:pout4, pback4:tback4, tback4:pm4, pout4:tout4, tout4:pkan4); 
  init(pkan1:n, pkan2:n, pkan3:n, pkan4:n); 
  bigint m := num_states(false);
};

# Verbose true
# Report true
# StateStorage MDD_SATURATION
# GarbageCollection LAZY

int N := read_int("Number of tokens");
print("Kanban model with a partition into K=4  levels, N=", N, "\n");
print("   number of states : ", kanban(N,true).m, "\n"); 
print("Kanban model with a partition into K=16 levels, N=", N, "\n");
print("   number of states : ", kanban(N,false).m, "\n");