abstract sig Ser { onde : one Margem } fun Come : Ser -> Ser { Homem->Ser + Lobo->(Ovelha+Homem) + Ovelha->Couve } one sig Homem, Lobo, Ovelha, Couve extends Ser {} abstract sig Margem {} one sig Esq, Dir extends Margem {} pred inv { all m : Margem | Homem in onde.m or no (Come.(onde.m) & onde.m) } run inv