// Lautturin ongelma
// Verkon graafinen kuvaus löytyy laskuharjoituksen 3 vastauksista

typedef enum {kaali,vuohi,susi} k_t;
typedef unsigned(1..2) r_t;
typedef struct {
  k_t k;
  r_t r;
} kulj_t;

// Kaikki kuljetettavat ovat aluksi rannalla 1
// Lauseke k_t k : {k,1} määrittää paikan alkumerkinnän. Muuttuja k
// saa yksi kerrallaan kaikki tyypin k_t arvot ja jokaista k:n arvoa 
// vastaava token {k,1} lisätään paikan alkumerkintään.
// Alkumerkinnäksi tulee siis {kaali,1},{vuohi,1},{susi,1}
place kulj (#k_t) kulj_t : k_t k : {k,1};
place vene (1) r_t : 1;

trans t12
in {
  place kulj : {k,1};
  place vene : 1;
}
out {
  place kulj : {k,2};
  place vene : 2;
};

trans t21
in {
  place kulj : {k,2};
  place vene : 2;
}
out {
  place kulj : {k,1};
  place vene : 1;
};
trans vene21
in {
  place vene : 2;
}
out {
  place vene : 1;
};

trans virhe
in {
  place kulj : {vuohi,x},{y,x};
  place vene : +x;
}
gate undefined;