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

print("*** The Dining Philosophers Problem ***\n");
print("This example illustrates the effect of different partition\n");
print("strategies on the time requirements to generate the state space\n");
print("using MDDs (set the Verbose option to true to display runtimes).\n\n");

spn phils(int N, int P) := { 
  for (int i in {0..N-1}) {
    place Idle[i], WaitL[i], WaitR[i], HasL[i], HasR[i], Fork[i];
    partition(1+div(i,P):Idle[i]:WaitL[i]:WaitR[i]:HasL[i]:HasR[i]:Fork[i]);
    trans GoEat[i], GetL[i], GetR[i], Release[i]; 
    firing(GoEat[i]:expo(1),GetL[i]:expo(1),GetR[i]:expo(1),Release[i]:expo(1));
    init(Idle[i]:1, Fork[i]:1);       
  }
  for (int i in {0..N-1}) {
    arcs(Idle[i]:GoEat[i], GoEat[i]:WaitL[i], GoEat[i]:WaitR[i],
	 WaitL[i]:GetL[i], Fork[i]:GetL[i], GetL[i]:HasL[i],
	 WaitR[i]:GetR[i], Fork[mod(i+1, N)]:GetR[i], GetR[i]:HasR[i],
	 HasL[i]:Release[i], HasR[i]:Release[i], Release[i]:Idle[i], 
	 Release[i]:Fork[i], Release[i]:Fork[mod(i+1, N)]);
  } 
  bigint count := num_states(false);
};

# Verbose true 
# StateStorage MDD_SATURATION
# GarbageCollection LAZY

int P := read_int("maximum number of philosophers per level");
int N := read_int("number of philosophers");
for (int i in {1..P}) {
  print(N," philosophers, ",i," per level.\n");
//# Verbose true
  phils(N,i).count;
}