No instance found for simple List example

Question

I'm studying Alloy and I'm trying to specify a general simple array list. My specification is based on the first examples of Alloy's Book and Online Tutorial. I'm just exploring the language by trying to test its basic features and what I want to do is really simple, but isn't working and I don't know why because it is very similar to the examples. This is my specification:

module FileSystem/Lists[A]
open util/ordering[List]

sig List {
    content: Int ->one A,
    size: Int
}{
    size = #content
    all i : Int, e : A | i -> e in content => i >= 0
    all i : Int | i in content.univ =>  i >= 0 and i < size
}

pred init [l: List]  { (no l.content) && l.size = 0}

fact traces {
    init[first]
    all l: List-last |
      let l' = l.next |
        some e: A |
          add [l, l', e]
}

pred add [l, l': List, e: A] {
    l'.content = l.content + (l.size -> e)      
    l'.size = l.size + 1
}
run add for 3 but 2 List

assert listSize {
    all l: List - last, l': l.next, e: A |
        add[l,l',e] => l'.size = (l.size + 1) and
        e in univ.(l'.content)
}
check listSize for 10

When I execute run add, the Alloy Analyzer says: No instance found. add my be inconsistent. But when I run check listSize it don't found any counterexample, suggesting that listSize is valid. Someone knows why the Alloy Analyzer can't found one instance for add? I try to change the number of elements, but don't worked. I think that this module is really simple, but I really don't know why I'm having this problems.

P.S.: I know that exists the seq type, but I'm trying to specify my own sequence. — user3537142

Daniel Jackson Daniel Jackson · Accepted Answer · 2017-03-07T19:11:55

Here's one thing I noticed. Your decl for content

content: Int ->one A,

says every int is mapped, and then you add a constraint saying only some ints are mapped

all i : Int, e : A | i -> e in content => i >= 0

which is an inconsistency.

A more general point: make structures with relations (that is, as graphs) not using using integers as indexes, whenever you can. Because Alloy is bounded, integers are quite subtle.

No instance found for simple List example

1 Answers