I was following along with the Software abstractions book and started to just try things and im wondering if anyone can tell me why its possible with my code to get an example of a name with no address? I thought the fact I put should prevent it since All names get some addr and vice versa. What am i missing? thanks for the help
sig Name, Addr { }
sig Book {
addr: Name → lone Addr
}
// to see an instance with more than 1 link of name to Addr
fact noUnmappedNameorAddr {
all a: Addr | some n: Name | n → a in Book.addr and
all n: Name | some a: Addr | n-> a in Book.addr
}
// This command generates an instance similar to Fig 2.2
run {}
I’m not sure if I understand your question, but be aware that the restriction n->a in Book.addr only forces name n to have address a in some Book, and not in all the Books. So, if you project on Book when visualising, in some of the Books name n may not have an address associated.
thank you and that does some what answer my question. I changed to the following but still get examples in which there is a lone Addr with no mappings. I am new to this so there could be something easy I am not putting together. Thanks for the help.
fact noUnmappedNameorAddr {
all a: Addr, b: Book | some Name | n → a in b.addr and
all n: Name, b: Book | some Addr | n → a in b.addr
}
im just trying to make it so that no Addr can be without a relationship to Name in all books
Now the problem is a bit more subtle - the and at the end of the first line means that the second all is inside the scope of the first all quantifier. This means that if there are no addresses the fact is trivially true and it will be possible that names without addresses exist. Either you remove the and
fact noUnmappedNameorAddr {
all a: Addr, b: Book | some n : Name | n -> a in b.addr
all n: Name, b: Book | some a : Addr | n -> a in b.addr
}
or insert parenthesis.
fact noUnmappedNameorAddr {
(all a: Addr, b: Book | some n : Name | n -> a in b.addr) and
(all n: Name, b: Book | some a : Addr | n -> a in b.addr)
}