Я работаю на C/C++ и пытаюсь понять, как выполняются/проверяются предикаты/утверждения в Alloy. (a) Если у меня есть более одного предиката и я хочу запустить их оба, то как при запуске первого предиката убедиться, что условия, связанные с ограничением в моем другом предикате, остаются статическими? Я просто озадачен тем, как вы запускаете несколько предикатов. (b) То же самое для утверждений. Должен ли я запускать проверку каждого утверждения?
Спасибо за любой отзыв по этому поводу.
У вас может быть произвольная формула в ваших командах «выполнить», поэтому вы можете соединить столько предикатов, сколько хотите. Вот пример:
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] }
Я думаю, что с утверждениями вы должны проверять их одно за другим, например,
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 }
Однако вы можете превратить свои утверждения в предикаты, а затем формировать из них произвольные формулы в теле команды «проверить», например,
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 }
pred plus_1 ... pred minus_1 ... assert plus_minus {plus_1 and minus_1} ... check plus_minus.
- person C. M. Sperberg-McQueen; 03.12.2013
