Generating a set through fact restrictions

[Paulo J. Matos]

Hello,

I'm trying to generate a specific integer set through a fact restriction.

For example, the set of all integers between 5 and 10:
module intsset

open util/integer as integer

sig I {
        i : Int
}

fact Irange {
        all n : Int | (n >= 5 && n =< 10) => (n in I.i)
}

pred show {}

run show for 8 int, exactly 1 I

However, this returns inconsistent. I would assume the SAT solver
would be able to find a model to this given that it just needs to find
a set within the integers from -128 to 127 where integers between 5
and 10 belong to the set.

What is the problem with this?

--
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK
Sponsor ECS runners - Action against Hunger:
http://www.justgiving.com/ecsrunslikethewind

[Felix Chang-2]

On Mon, 24 Mar 2008, Paulo J. Matos wrote:

> Hello,
>
> I'm trying to generate a specific integer set through a fact restriction.
>
> For example, the set of all integers between 5 and 10:
> module intsset
>
> open util/integer as integer
>
> sig I {
> i : Int
> }
>
> fact Irange {
> all n : Int | (n >= 5 && n =< 10) => (n in I.i)
> }
>
> What is the problem with this?

sig I { i: Int }  says each I is associated with *exactly* one Int.
So your fact "I.i = {5,6,7,8,9,10}" is impossible to satisfy.

Try this instead:

one sig I { i: set Int }
fact { I.i = {n:Int | 5 <= n && n <= 10} }
run { } for 8 int

Sincerely,
Felix Chang
Alloy4 Developer

[Paulo J. Matos]

On Mon, Mar 24, 2008 at 12:51 PM, Felix Chang <fschang@...> wrote:

>
> On Mon, 24 Mar 2008, Paulo J. Matos wrote:
>  > Hello,
>  >
>  > I'm trying to generate a specific integer set through a fact restriction.
>  >
>  > For example, the set of all integers between 5 and 10:
>  > module intsset
>  >
>  > open util/integer as integer
>  >
>  > sig I {
>  > i : Int
>  > }
>  >
>  > fact Irange {
>  > all n : Int | (n >= 5 && n =< 10) => (n in I.i)
>  > }
>  >
>  > What is the problem with this?
>
>  sig I { i: Int } says each I is associated with *exactly* one Int.
>  So your fact "I.i = {5,6,7,8,9,10}" is impossible to satisfy.
>

Argh, I missed that. Thanks!

>  Try this instead:
>
>  one sig I { i: set Int }
>  fact { I.i = {n:Int | 5 <= n && n <= 10} }
>  run { } for 8 int
>
>  Sincerely,
>  Felix Chang
>  Alloy4 Developer
>
>  

--
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK
Sponsor ECS runners - Action against Hunger:
http://www.justgiving.com/ecsrunslikethewind