Использование предикатов в Alloy

Question

Я пытаюсь использовать два предиката (скажем, methodWiThSameParameters и methodWiThSameReturn) из другого (то есть checkOverriding), но я получаю следующую ошибку: "Нет команд для выполнения". Есть какие-нибудь подсказки? Я также пытался использовать функции, но безуспешно, либо из-за синтаксиса, либо из-за того, что функции не возвращают логические значения.

Они являются частью java метамодели, указанной в Alloy, как я прокомментировал в некоторых предыдущих вопросах.

pred checkOverriding[]{
//check accessibility of methods involved in overriding
  no c1, c2: Class {
    c1=c2.^extend
    some m1, m2:Method |
          m1 in c1.methods && m2 in c2.methods && m1.id = m2.id 
          && methodsWiThSameParameters[m1, m2] && methodsWiThSameReturn[m1, m2] && 
               ( (m1.acc = protected && (m2.acc = private_ || #(m2.acc) = 0 )) ||
                 (m1.acc = public && (m2.acc != public || #(m2.acc) = 0 )) ||
                 (#(m1.acc) = 0 && m2.acc != private_ )
               )
      }
    }

pred methodsWiThSameParameters [first,second:Method]{
    m1.param=m2.param || (#(m1.param)=0 && #(m2.param)=0)  
}
pred methodsWiThSameReturn [first, second:Method]{
    m1.return=m2.return || (#(m1.return)=0 && #(m2.return)=0) 
}

---

Спасибо за ваш ответ, г-н CM Sperberg-McQueen, но я думаю, что я не был достаточно ясен в своем вопросе.

Мой предикат, скажем, checkOverriding, вызывается из факта, подобного этому:

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

Таким образом, я продолжаю не понимать ошибку: "Нет команд для выполнения".

Answer 1

Вы определили предикаты; у них чисто декларативная семантика, и они будут истинными в некотором подмножестве экземпляров модели и ложными в дополнительном подмножестве.

Если вы хотите, чтобы Анализатор что-то делал, вам нужно дать ему инструкцию; инструкция для поиска экземпляра предиката run, Так что вы хотите сказать что-то вроде

run methodsWithSameParameters for 3

или же

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

Обратите внимание, что вы можете иметь более одной инструкции в модели Alloy; Анализатор позволяет вам сказать, что выполнить.

---

[Приложение]

Alloy Analyzer рассматривает ключевые слова run а также check (и только их) как "команды". Из вашего описания, это звучит очень похоже на то, что у вас нет каких-либо вхождений этих ключевых слов в модель.

Если все, что вы хотите сделать, это просмотреть некоторые экземпляры модели Alloy (чтобы убедиться, что модель не является самопротиворечивой), то самый простой способ - добавить в модель что-то вроде следующего:

pred show {}
run show for 3

Или, если у вас уже есть именованный предикат, вы можете просто добавить run команда для этого предиката:

run checkOverriding 

Но без оговорки в модели, которая начинается с run или же check, у вас нет "команды" в модели.

Вы говорите, что вы определили предикат (checkOverriding) и затем указывает на то, что этот предикат всегда выполняется. Это означает, что предикат checkOverriding всегда верно (и может быть сделано с помощью checkOverriding факт вместо предиката), но он имеет чисто декларативное значение и не считается "командой". Если вы хотите, чтобы Alloy находил экземпляры предиката, вы должны использовать run команда; если вы хотите, чтобы Alloy нашел контрпримеры для утверждения, вы должны использовать check команда.