Search code examples
alloy

Does Alloy accept free variable?

In the book, Software Abstractions, chapter 5.2.2 Skolemization, it mentions, enter image description here

where sx is a new free variable and F[sx/x] is the constraint F, with sx substituted for x.

However when I present the free variable in Alloy, it says Syntax Error. Does Alloy accept free variable?

sig A {
  relation:  A
}
fact {
 some A
}
check{
  //correct expression
  //some a : A | one a.relation

  //Skolemization
  (a: A) and (one a.relation)
}
Solution

  • First, Skolemization is a classic logical operation and, if you don't already know it, it's perhaps a good idea to study it using a book on logic.

    That being said, the constraint mentioned in the book is not valid Alloy code, it's rather an explanation of what happens at the solver level (what Jackson calls "the analysis constraint"). So, no, written as such, the model is not valid Alloy due to the presence of this free variable.

    But, you don't have to perform Skolemization yourself as Alloy does it for you (depending on a configuration in the Options menu).

    Still, if you want to, you can. The way to do it is to add a new object a of type A for the existential variable as follows:

    sig A {
  relation:  A
}
fact {
  some A
}
one sig a in A {}
check{ one a.relation }