Using predicates in Alloy

Question

I am trying to use two predicates (say, methodsWiThSameParameters and methodsWiThSameReturn) from another one (i.e. checkOverriding) but i receive the following error: "There are no commands to execute". Any clues? I also tried to use functions but with no success, either due to syntax or to functions do not return boolean values.

They are part of a java metamodel specified in Alloy, as i commented in some earlier questions.

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

---

Thank you for your response, mr C. M. Sperberg-McQueen, but i think i was not clear enough in my question.

My predicate, say checkOverriding, is being called from a fact like this:

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

Thus, i continue not understanding the error: "There are no commands to execute" .

Answer 1

You've defined predicates; they have a purely declarative semantics and they will be true in some subset of instances of the model and false in the complementary subset.

If you want the Analyzer to do anything, you need to give it an instruction; the instruction to search for an instance of a predicate is run. So you'll want to say something like

run methodsWithSameParameters for 3

or

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

Note that you can have more than one instruction in an Alloy model; the Analyzer lets you tell it which to execute.

---

[Addendum]

The Alloy Analyzer regards the keywords run and check (and only them) as 'commands'. From your description, it sounds very much as if you don't have any occurrences of those keywords in the model.

If all you want to do is to see some instances of the Alloy model (to verify that the model is not self-contradictory), then the simplest way is to add something like the following to the model:

pred show {}
run show for 3

Or, if you already have a named predicate, you could simply add a run command for that predicate:

run checkOverriding 

But without a clause in the model that begins with either run or check, you do not have a 'command' in the model.

You say that you have defined a predicate (checkOverriding) and then specified in a fact that that predicate is always satisfied. This amounts to saying that the predicate checkOverriding is always true (and might just as well be done by making checkOverriding a fact instead of a predicate), but it has a purely declarative meaning, and it does not count as a "command". If you want Alloy to find instances of a predicate, you must use the run command; if you want Alloy to find counter-examples for an assertion, you must use the check command.