// kaalinpää, vuohi ja susi

typedef enum { kaali, vuohi, susi } otus_t;

/** lippu: onko kulkine alkupaikassa */
place alussa (1) bool: true;

/** kulkuvälineen sisältö */
place kuorma (0..2) otus_t;

/** alkupaikan otukset */
place alku (0..3) otus_t: kaali, vuohi, susi;
/** alkupaikan otusten määrä */
place kuormaa (1) unsigned: cardinality place alku;

/** loppupaikan otukset */
place loppu (0..3) otus_t;

/** siirrä 0 otusta lopusta alkuun */
trans alkuun
in { place alussa: false; place kuormaa: k; }
out { place alussa: true; place kuormaa: k; }
gate k > 0;

/** siirrä 1 otus alusta loppuun */
trans loppuun1
in { place alussa: true; place alku: otus; place kuormaa: k; }
out { place alussa: false; place loppu: otus; place kuormaa: |k; };

/** siirrä 1 otus lopusta alkuun */
trans alkuun1
in { place alussa: false; place loppu: otus; place kuormaa: k; }
out { place alussa: true; place alku: otus; place kuormaa: +k; }
gate k > 0;

#ifdef KAKSI
/** siirrä 2 otusta lopusta alkuun */
trans alkuun2
in { place alussa: false; place loppu: otus1, otus2; place kuormaa: k; }
out { place alussa: true; place alku: otus1, otus2; place kuormaa: ++k; }
gate k > 0;

/** siirrä 2 otusta alusta loppuun */
trans loppuun2
in { place alussa: true; place alku: otus1, otus2; place kuormaa: k; }
out { place alussa: false; place loppu: otus1, otus2; place kuormaa: | |k; };
#endif // KAKSI

reject (true subset place alussa)
  ? (is otus_t (kaali, vuohi) subset place loppu ||
     is otus_t (vuohi, susi) subset place loppu)
  : (is otus_t (kaali, vuohi) subset place alku ||
     is otus_t (vuohi, susi) subset place alku);

deadlock true;