// Define a type for the black token // An empty struct type has only one possible value, so it can be used. // One could also use any type with only one possible value, e.g. unsigned(1) typedef struct {} token; place cabbage1 token : {}; place goat1 token : {}; place wolf1 token : {}; place boat1 token : {}; place cabbage2 token; place goat2 token; place wolf2 token; place boat2 token; trans c1 in { place cabbage1 : {}; place boat1 : {}; } out { place cabbage2 : {}; place boat2 : {}; }; trans c2 in { place cabbage2 : {}; place boat2 : {}; } out { place cabbage1 : {}; place boat1 : {}; }; trans g1 in { place goat1 : {}; place boat1 : {}; } out { place goat2 : {}; place boat2 : {}; }; trans g2 in { place goat2 : {}; place boat2 : {}; } out { place goat1 : {}; place boat1 : {}; }; trans w1 in { place wolf1 : {}; place boat1 : {}; } out { place wolf2 : {}; place boat2 : {}; }; trans w2 in { place wolf2 : {}; place boat2 : {}; } out { place wolf1 : {}; place boat1 : {}; }; trans b in { place boat2 : {}; } out { place boat1 : {}; }; //reject (place goat1 equals is token {}) && (place cabbage1 equals is token {}) && (place boat2 equals is token {}); //reject (place goat1 equals is token {}) && (place wolf1 equals is token {}) && (place boat2 equals is token {}); //reject (place goat2 equals is token {}) && (place cabbage2 equals is token {}) && (place boat1 equals is token {}); //reject (place goat2 equals is token {}) && (place wolf2 equals is token {}) && (place boat1 equals is token {});