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

Question

Я пытаюсь использовать два предиката (скажем, methodsWiThSameParameters и methodsWiThSameReturn) из другого (т. Е.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) 
}

---

Благодарю вас за ваш ответ, мистер К.M.Сперберг-Маккуин, но я думаю, что я недостаточно ясно выразился в своем вопросе.

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

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

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

Answer 1

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

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

run methodsWithSameParameters for 3

или

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

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

---

[Добавление]

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

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

pred show {}
run show for 3

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

run checkOverriding 

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

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