开发者

Problem with predicate in Alloy

开发者 https://www.devze.com 2023-02-09 23:10 出处:网络
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

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 e开发者_JAVA百科quivalent predicate

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

but the output is the same.

Am I missing something?


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
0

精彩评论

暂无评论...
验证码 换一张
取 消

关注公众号