general_1_s:PlaceState {
  numTokens = 1;
}

general_2_s:PlaceState {
  numTokens = 1;
}

critical_1_s:PlaceState {
  numTokens = 0;
}

critical_2_s:PlaceState {
  numTokens = 0;
}

semaphore_s:PlaceState {
  numTokens = 1;
}

:of (general_1_s -> general_1)
:of (general_2_s -> general_2)
:of (critical_1_s -> critical_1)
:of (critical_2_s -> critical_2)
:of (semaphore_s -> semaphore)