One Fact Or Many?

Questions
1

I’m brushing up on Alloy after some years. Over on the Structural Design with Alloy example, there is a set of facts:

fact {
  // Different entries in the same directory must have different names
  all d : Dir, n : Name | lone n.(d.contents)
}

fact {
  // A directory cannot be contained in more than one directory
  all o : Dir | lone contents.o
}

fact {
  // Directories cannot contain themselves directly or indirectly
  all d : Dir | d not in d.^{ d : Dir, o : Object | some d.contents.o }
}

fact {
  // Every object except the root is contained somewhere
  Name.(Object.contents) = Object - Root
}

Is separate fact blocks preferred over a single one, and if so why? Is it about readability and maintenance, or is there a difference in execution? Here they are all crammed together in one block:

fact {
  // Different entries in the same directory must have different names
  all d : Dir, n : Name | lone n.(d.contents)

  // A directory cannot be contained in more than one directory
  all o : Dir | lone contents.o

  // Directories cannot contain themselves directly or indirectly
  all d : Dir | d not in d.^{ d : Dir, o : Object | some d.contents.o }

  // Every object except the root is contained somewhere
  Name.(Object.contents) = Object - Root
}
2

AFAIK there’s no difference in execution. My suggestion is to group related assumptions in a given fact but to separate facts that talk about different concerns. It’s both for readability and maintenance (you may sometimes comment out a fact, or make it into a pred to perform some verifications.)

3

A tip I learned.

I find expressing facts in predicates far superior. Facts are like static global variables with a single letter name. They tend to bite you when you least expect.

I tend to use pred for the facts and then in the run or check block activate the predicates that I need. This makes the specification much more modular, flexible, and readable. Especially in test cases it is very handy that you can invoke only the needed predicates.

1 Like
4

Facts are good for some specific things:

  1. Making sure there’s no “free-floating” atoms in your model. fact "all pets have owners" {Person.pet = Pet}
  2. Reducing a module to a single instance of something. fact "only one graph" {util/graph/weaklyConnected[edge]}
  3. Adding extra definitions to fields that you can’t do by definition. fact "Person.parents matches Person.children" {~parents = children}.*
  4. If you have a temporal spec spec.als and a lot of properties of the form spec => always prop, you can make a separate properties.als file, add open spec, and then add fact {spec}. Then you can define the properties as just always prop.

Otherwise I agree with @peter.kriens you want to use the predicates.

*Yeah this could be a function but there are complex cases where adding an extra field model-checks faster than defining a function.