Tip: Name facts with strings

models
1

If I wanted to model DAGs, I’d write

sig Node {
  , edges: set Node
}

fact is_a_dag {
  no iden & ^edges
}

But I don’t need a regular identifier for the fact, since it’s not referred to anywhere. It’s part of the spec that you can write

fact { -- is a dag
  no iden & ^edges
}

Less well known is that we can put a string there, too!

fact "Only generate acyclic graphs" {
  no iden & ^edges
}

I believe this isn’t intended by the spec, but it’s useful enough that I take advantage of it whenever I have to write facts.

1 Like
2

really like this.

Incidentally, might be worth mentioning that there’s a dag predicate in the graph module.

3

BTW, you can do the same thing with your run and check commands. This means you won’t have to tell the difference between run$8 and run$17 from the menu. E.g.,

check { Node = Node }

becomes

check name { Node = Node }

Cheers,
– T

4

You can also do

name: check {Node = Node}