Date: Wed, 07 Mar 2007 21:10:12 -0000
From: Pawel Sidoryk

Hello everybody,

I have a very small problem that I cannot solve with alloy. Here is
the code:

abstract sig State{}

sig State1 extends State{}

sig State2 extends State{}

pred oper(s, s': State) {
    s in State1 && s' in State2
}

pred anti_oper(s: State) {
    s in State2
}

assert anti_oper_ok{
    all s: State | not anti_oper[s] => some s': State | oper[s, s']
}

check anti_oper_ok

Alloy finds a counterexample (all State1 elements, no State2 element)
and that is how it is expected to run.

But it does not solve my problem. And my problem is to find for a
given 2-argument predicate (like oper(s, s')) a different predicate
(like anti_oper(s)) that is true only if oper(s, s') is false for all
possible s' allowed by the model.

In the above example it is plain to see that anti_oper(s) is a
solution for oper(s, s) but I do not know how to prove such a simple
fact with Alloy. assert anti_oper_ok is not proper for this purpose
because some s': State there does not cover all possible occurrences
of a State, it covers occurrences of a State for a counterexample
that has been found.

Does anybody know how to prove that anti_oper(s) is a solution for
oper(s, s) with Alloy?