Usando predicados en Alloy

Question

Estoy tratando de usar dos predicados (por ejemplo, métodos con los mismos parámetros y métodos con el mismo retorno) de otro (es decir,checkOverriding) pero recibo el siguiente error:"No hay comandos para ejecutar".¿Alguna pista?También intenté usar funciones pero sin éxito, ya sea por la sintaxis o porque las funciones no devuelven valores booleanos.

Son parte de un metamodelo de Java especificado en Alloy, como comenté en algunas preguntas 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) 
}

---

Gracias por su respuesta, señor C.METRO.Sperberg-McQueen, pero creo que no fui lo suficientemente claro en mi pregunta.

Mi predicado, digamos checkOverriding, se llama a partir de un hecho como este:

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

Por lo tanto, sigo sin entender el error:"No hay comandos para ejecutar".

Answer 1

Ha definido predicados;tienen una semántica puramente declarativa y serán verdaderas en algún subconjunto de instancias del modelo y falsas en el subconjunto complementario.

Si desea que el analizador haga algo, debe darle una instrucción;la instrucción para buscar una instancia de un predicado es run.Entonces querrás decir algo como

run methodsWithSameParameters for 3

o

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

Tenga en cuenta que puede tener más de una instrucción en un modelo Alloy;el analizador le permite indicarle cuál ejecutar.

---

[Apéndice]

El Alloy Analyzer considera las palabras clave run y check (y sólo ellos) como 'comandos'.Según su descripción, parece como si no tuviera ninguna aparición de esas palabras clave en el modelo.

Si todo lo que desea hacer es ver algunas instancias del modelo Alloy (para verificar que el modelo no sea contradictorio), entonces la forma más sencilla es agregar algo como lo siguiente al modelo:

pred show {}
run show for 3

O, si ya tiene un predicado con nombre, simplemente puede agregar un run comando para ese predicado:

run checkOverriding 

Pero sin una cláusula en el modelo que comience con run o check, no tienes un 'comando' en el modelo.

Dices que has definido un predicado (checkOverriding) y luego se especifica en un hecho que ese predicado siempre se cumple.Esto equivale a decir que el predicado checkOverriding siempre es cierto (y bien podría hacerse haciendo checkOverriding un hecho en lugar de un predicado), pero tiene un significado puramente declarativo y no cuenta como una "orden".Si desea que Alloy encuentre instancias de un predicado, debe utilizar el run dominio;Si desea que Alloy encuentre contraejemplos para una afirmación, debe utilizar el check dominio.