Problemas da especificação anterior

Há um erro na especificação anterior (sistema_policial_v2) na operação REGISTRATION. Esta operação não verifica se o elemento que está sendo cadastrado já está cadastrado. O problema do elemento já estar cadastrado é que, foreign? pode pertencer ao conjunto offenders e a operação REGISTRATION o adicionará ao conjunto innocents. Esta operação pode, portanto, produzir um estado inválido para o sistema, onde innocents e offenders não são disjuntos. Para solucionar este problema, foi adicionado mais um predicado à parte predicativa de REGISTRATION. O predicado adicionado é: foreign? \notin population.