Usando predicados na Liga

Question

Estou tentando usar dois predicados (digamos, methodsWiThSameParameters e methodsWiThSameReturn) a partir de outra (por exemplo,checkOverriding), mas eu receber o seguinte erro:"Não existem comandos a executar".Algum palpite?Eu também tentei usar funções, mas sem sucesso, devido ao sintaxe ou funções não retornam valores booleanos.

Eles são parte de um java metamodelo especificado na Liga, como eu comentei em algumas questões anteriores.

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) 
}

---

Obrigado pela sua resposta, C.M.Sperberg-McQueen, mas eu acho que não fui suficientemente claro na minha pergunta.

Meu predicado, dizer checkOverriding, está sendo chamado a partir de um fato como este:

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

Assim, eu continuo não entendendo o erro:"Não existem comandos a executar" .

Answer 1

Você definiu predicados;eles têm um sentimento puramente declarativa semântica e eles vão ser verdadeiro em alguns subconjunto de instâncias do modelo e falso na complementares subconjunto.

Se você deseja que o Analisador de fazer qualquer coisa, você precisa dar uma instrução;a instrução de busca para uma instância de um predicado é run.Portanto, você vai querer dizer algo como

run methodsWithSameParameters for 3

ou

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

Observe que você pode ter mais de uma instrução em uma Liga de modelo;o Analisador permite que você diga a ele o que executar.

---

[Adendo]

O Alloy Analyzer relação a palavras-chave run e check (e só eles) como 'comandos'.A partir de sua descrição, ele soa muito como se você não tiver quaisquer ocorrências dessas palavras-chave no modelo.

Se tudo o que você quer fazer é ver algumas instâncias da Liga de modelo (para verificar que o modelo não é auto-contraditório) e, em seguida, a maneira mais simples é adicionar algo como o seguinte modelo:

pred show {}
run show for 3

Ou, se você já tiver um nome de predicado, você pode simplesmente adicionar um run comando para esse predicado:

run checkOverriding 

Mas sem uma cláusula no modelo que começa com run ou check, você não tem um 'comando' no modelo.

Você diz que você tenha definido um predicado (checkOverriding) e, em seguida, especificado no fato de que o predicado é sempre satisfeito.Isso equivale a dizer que o predicado checkOverriding é sempre verdadeira (e pode muito bem ser feito por meio da checkOverriding um fato, em vez de um predicado), mas tem um puramente declarativa significado, e não conta como um "comando".Se você deseja Liga para encontrar instâncias de um predicado, você deve usar o run de comando;se você deseja Liga para encontrar contra-exemplos de uma afirmação, você deve usar o check de comando.