Does multirelations in signatures has implicit facts?

Questions
1

I’m still learning English, please excuse my poor English.

I wrote two codes, one is

sig Key {}
sig Value {}

one sig Map {
  entries: Key -> Value
}
fact {
  all k: Key | one Map.entries[k]
}

run { some v: Value | v not in Map.entries[Key] }

another one is

sig Key {}
sig Value {}

one sig Map {
  entries: Key one -> Value
}

run { some v: Value | v not in Map.entries[Key] }

These codes have different results.
First one has instance, but second one has no instance.
I expected instance for both codes.
What is the difference?

2

r: A -> one B
says that each A is mapped to one B

and

r: A one -> B
says that there is one A that maps to each B.

3

Thanks for responding.
Yes, I know. But that is not a point in my question.

entries: Key one -> Value

says that there is one Key that maps to each Value, and don’t say Value instance can appear only in “entries” (in my understanding).

But alloy analyzer cannot find Value atom not in “entries”. This is my question.

4

In the second example, the declaration constraint says that each value is mapped to my exactly one key. So there are no values that are not mapped to by any key. The run constraint asks for a value that is not mapped to by any key. So the two constraints are inconsistent and there is no instance.

5

Thank you, my question has been resolved.

I reread the book, it said:

r: A m -> n B

It can be rewritten as follows

all a: A | n a.r
all b: B | m r.b

I forgot this.

1 Like