# One Fact Or Many?

**URL:** <https://alloytools.discourse.group/t/one-fact-or-many/446>\
**Category:** Questions\
**Created:** [February 25, 2024, 2:50am UTC](https://alloytools.discourse.group/t/one-fact-or-many/446 "2024-02-25T02:50:52Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![awwaiid](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/awwaiid/32/222_2.png) [@awwaiid](https://alloytools.discourse.group/u/awwaiid)\
**Post date:** [February 25, 2024, 2:50am UTC](https://alloytools.discourse.group/t/one-fact-or-many/446/1 "2024-02-25T02:50:52Z")

</div>

I’m brushing up on Alloy after some years. Over on the [Structural Design with Alloy](https://haslab.github.io/formal-software-design/structural-design/index.html) example, there is a set of facts:

```auto
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:

```auto
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
}

```

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [February 25, 2024, 8:15pm UTC](https://alloytools.discourse.group/t/one-fact-or-many/446/2 "2024-02-25T20:15:59Z")

</div>

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.)

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [February 26, 2024, 8:03am UTC](https://alloytools.discourse.group/t/one-fact-or-many/446/3 "2024-02-26T08:03:55Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![hwayne](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/hwayne/32/67_2.png) [@hwayne](https://alloytools.discourse.group/u/hwayne)\
**Post date:** [February 26, 2024, 5:23pm UTC](https://alloytools.discourse.group/t/one-fact-or-many/446/4 "2024-02-26T17:23:21Z")

</div>

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.