formal-methodsmodel-driven-developmentalloy

Problem with predicate in Alloy


So I have the following bit of code in Alloy:

sig Node { }
sig Queue { root : Node }

pred SomePred {
    no q, q' : Queue | q.root = q'.root
}

run SomePred for 3

but this won't yield any instance containing a Queue, I wonder why. It only shows up instances with Nodes. I've tried the equivalent predicate

pred SomePred' {
    all q, q' : Queue | q.root != q'.root
}

but the output is the same.

Am I missing something?


Solution

  • There's a logic flaw in there:

    fact SomeFact {
        no q, q' : Queue | q.root = q'.root
    }
    

    Assume there is an instance with a single queue Q that has a given root R. When running SomeFact, it'd test the only queue available, Q, and it'd find it that Q.root = Q.root, thus, excluding the given instance from coming to life.

    The same reasoning can be made for instances with an arbitrary number of queues.

    Here is a working version:

    sig Node {
    }
    
    sig Queue {
        root : Node
    }
    
    fact sss {
        all disj q, q' : Queue | q.root != q'.root
    }
    
    pred abc() {
    }
    
    run abc for 3