sig Estado {} abstract sig Ser { onde : Margem -> Estado, ser : set Estado } 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 [e : Estado] { all m : Margem | Homem in (onde.e).m or no (Come.((onde.e).m) & (onde.e).m) onde.e in ser.e -> one Margem } run inv for 1 Estado pred sozinho[e, e' : Estado] { -- pre conditions Homem in ser.e let m = Homem.(onde.e), sozinhos = (onde.e).m - Homem | no (Come.sozinhos & sozinhos) -- post conditions Homem.(onde.e') = Margem - Homem.(onde.e) -- frame conditions all s : Ser - Homem | s.(onde.e') = s.(onde.e) ser.e' = ser.e } check sozinho_preserva_invariante { all e, e' : Estado | inv[e] and sozinho[e,e'] implies inv[e'] } for 3 but 2 Estado run sozinho_consistente { some e, e' : Estado | inv[e] and sozinho[e,e'] } for 3 but 2 Estado pred acompanhado[s : Ser, e, e' : Estado] { -- pre conditions Homem in ser.e s in ser.e s.(onde.e) = Homem.(onde.e) s != Homem let m = Homem.(onde.e), sozinhos = (onde.e).m - Homem - s | no (Come.sozinhos & sozinhos) -- post conditions Homem.(onde.e') = Margem - Homem.(onde.e) s.(onde.e') = Homem.(onde.e') -- frame conditions all x : Ser - Homem - s | x.(onde.e') = x.(onde.e) ser.e' = ser.e } check acompanhado_preserva_invariante { all e, e' : Estado, s : Ser | inv[e] and acompanhado[s,e,e'] implies inv[e'] } for 3 but 2 Estado run acompanhado_consistente { some e, e' : Estado, s : Ser | inv[e] and acompanhado[s,e,e'] } for 3 but 2 Estado pred come[x, y : Ser, e, e' : Estado] { -- pre conditions x in ser.e y in ser.e y in x.Come x.(onde.e) = y.(onde.e) // O Homem pode comer sempre, mas outro Ser só come se o Homem não estiver a controlar x = Homem or x.(onde.e) != y.(onde.e) -- post conditions ser.e' = ser.e - y -- frame conditions onde.e' = onde.e - y->Margem } // A auto-fagia é tramada... check come_preserva_invariante { all e, e' : Estado, x,y : Ser | inv[e] and come[x,y,e,e'] implies inv[e'] } for 3 but 2 Estado run come_consistente { some e,e' : Estado, x,y : Ser | inv[e] and come[x,y,e,e'] } for 3 but 2 Estado check so_o_homem_e_que_consegue_comer { all e,e' : Estado, x, y : Ser | inv[e] and come[x,y,e,e'] implies x = Homem } for 3 but 2 Estado