Почему оператор Plus не работает с целыми числами в Alloy?

приведенный ниже код сплава предназначен для проблемы с 8 ферзями
Я не знаю, почему оператор плюс и минус не работают правильно
поэтому после выполнения есть ферзи на той же диагонали
Более того, я сталкиваюсь с этой ошибкой при использовании плюс и минус оператор между 2 #
например:
#q1.row+#q2.col-#q1.col != #q2.row

спасибо за любой ответ
с наилучшими пожеланиями


вот это код 8Queens:

sig Queens{
row:Int,
col:Int
}
{row>=0 and row <#Queens and col>=0 and col<#Queens}

pred nothreat(q1,q2 : Queens) {
   q1.row != q2.row 
   and q1.col != q2.col 
   and q1.row+q2.col-q1.col != q2.row
   and q1.row-q2.col+q1.col != q2.row
}

pred valid { 
all q1,q2 : Queens |   q1 != q2 => nothreat[q1, q2]
 }
fact card {#Queens =8}
run valid for 8 Queens, 8 Int

person user3531170    schedule 18.05.2014    source источник


Ответы (1)


Вместо этого используйте функции plus и minus (например, q1.row.plus[q2.col].minus[q1.col]), поскольку + всегда рассматривается как объединение множеств, а - — как разность множеств.

person Aleksandar Milicevic    schedule 18.05.2014