CODEWITHSUNDEEP
alloy
Roger Costello
Roger Costello

Reputation: 3209

Why does a cardinality constraint work in a run command but not in a fact?

Below is an Alloy representation of two desktops. In the fact I specify that the first desktop contains two icons, A and B, and the second desktop contains one icon, A. I'd like to specify that there are exactly two Desktops, so I put this in the fact: 

#Desktop = 2

When I did the run command, I got this message: No instance found. When I omitted that from the fact and instead specified the number of Desktops in the run command: 

run {} but 2 Desktop

then the desired instance was generated. Why? Why doesn't it work when I constrain the number of Desktops in the fact, but does work when I constrain the number of Desktops in the run command?

open util/ordering[Desktop]

sig Desktop {
     icons: set Icon
} 

abstract sig Icon {}
one sig A extends Icon {}
one sig B extends Icon {}

fact {
    first.icons = A + B
    first.next.icons = A
}

Upvotes: 2

Views: 90

Answers (1)

Hovercouch
Hovercouch

Reputation: 2314

According to page 283 of the Alloy Reference, if no explicit bound is specified for a signature and no implicit bound can be found, that signature defaults to at most 3 elements. run {#Desktop = 3} works by default.

You also have open util/ordering[Desktop]. That module starts with module util/ordering[exactly elem], which adds the exactly constraint to the scope. This means that the implicit bound is exactly 3 elements, so run {#Desktop = 2} fails. Adding run {#Desktop = 2} for 2 changes the implicit bound to 2 elements per signature, so it succeeds.

Upvotes: 5

Related Questions