how to run predicates and assertions in alloy

Question

I come from a C/C++ background and am trying to understand how are predicates/assertions run/checked in Alloy. (a) If I have more than one predicates and I want to run both of them, when I run the first predicate how do I ensure that the conditions related to constraint in my other predicate remain static? I am simply puzzled on how do you run multiple predicates. (b) Same for assertions. Do I have to run check of each assertion?

Thanks for any feedback on this.

Answer 1

You can have an arbitrary formula in your "run" commands, so in there you can conjoin as many predicates as you want. Here is an example:

one sig S {
  x: Int
}

pred gt[n: Int] { S.x > n }
pred lt[n: Int] { S.x < n }

run { gt[2] and lt[4] }

With assertions, I think you have to check them one by one, e.g.,

one sig S {
  x: Int
}

assert plus_1  { plus[S.x, 1] > S.x }
assert minus_1 { minus[S.x, 1] < S.x }

check plus_1
check minus_1
// doesn't compile: check { plus_1 and minus_1 } 

However, you can turn your assertions into predicates, and then you can form arbitrary formulas from them in the body of a "check" command, e.g.,

one sig S {
  x: Int
}

pred plus_1[]  { plus[S.x, 1] > S.x }
pred minus_1[] { minus[S.x, 1] < S.x }

check { plus_1 and minus_1 }