シンプルリストのインスタンスが見つかりません

Question

私は合金を研究していて、一般的な単純な配列リストを指定しようとしています。私の仕様は、Alloy's Book and Online Tutorialの最初の例に基づいています。私はその基本的な機能をテストしようとしていますが、実際には単純なものですが、動作していないため、その理由が分かりません。これは私の仕様です：

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 

私は実行し、追加を実行し、合金Analyzerは言う：インスタンスが見つかりませんでした。私の矛盾を追加してください。しかし、私がcheckSizeを実行すると、どのcounterexampleも見つからず、listSizeが有効であることが示唆されます。 Alloy Analyzerがaddのインスタンスを1つ見つけることができない理由を知っていますか？私は要素の数を変更しようとしますが、うまくいきません。私はこのモジュールが本当にシンプルだと思っていますが、私はなぜこの問題を抱えているのか分かりません。

Answer 1

ここに私が気づいたことがあります。コンテンツ

content: Int ->one A, 

のためのあなたの供述は、すべてのint型がマッピングされ、その後、あなただけのいくつかのint型が矛盾である

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

をマッピングされていると言って制約を追加されると言います。

もっと一般的な点：可能な限り、いつでも整数をインデックスとして使用しないで、リレーションを持つ構造体（つまりグラフ）を作成します。合金は境界があるので、整数は非常に微妙です。