Contents

(*
*  Tag owner address coherence: address on all tags with the same ower are equal
*  
*)

CoherentOwnerAddress == \A tag \in v_tags: \A tag2 \in v_tags: tag.owner.name = tag2.owner.name => tag.owner.address = tag2.owner.address

Version data entries

7 entries across 7 versions & 1 rubygems

Version	Path
tla-sbuilder-0.3.9	src/pet/correctness_coherent_owner_address.tla
tla-sbuilder-0.3.8	src/pet/correctness_coherent_owner_address.tla
tla-sbuilder-0.3.7	src/pet/correctness_coherent_owner_address.tla
tla-sbuilder-0.3.4	src/pet/correctness_coherent_owner_address.tla
tla-sbuilder-0.2.2	src/pet/correctness_coherent_owner_address.tla
tla-sbuilder-0.2.1	src/pet/correctness_coherent_owner_address.tla
tla-sbuilder-0.1.0	src/pet/correctness_coherent_owner_address.tla