没有找到简单列表示例的实例答案

【问题标题】：No instance found for simple List example没有找到简单列表示例的实例
【发布时间】：2017-03-03 19:24:28
【问题描述】：

我正在研究 Alloy，我正在尝试指定一个通用的简单数组列表。我的规范基于 Alloy 的书籍和在线教程的第一个示例。我只是通过尝试测试其基本功能来探索该语言，而我想做的事情非常简单，但不起作用，我不知道为什么，因为它与示例非常相似。这是我的规范：

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

当我执行 run add 时，Alloy Analyzer 显示：未找到实例。添加我的不一致。但是当我运行检查 listSize 时，它没有找到任何反例，表明 listSize 是有效的。有人知道为什么合金分析仪找不到要添加的实例吗？我尝试更改元素的数量，但没有奏效。我认为这个模块真的很简单，但我真的不知道为什么我会遇到这个问题。

【问题讨论】：

P.S.：我知道存在 seq 类型，但我正在尝试指定我自己的序列。

标签： alloy

【解决方案1】：

这是我注意到的一件事。您的内容声明

content: Int ->one A,

说每个 int 都被映射，然后你添加一个约束，说只有一些 int 被映射

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

这是一个不一致的地方。

更一般的一点：尽可能使用不使用整数作为索引的关系（即图形）结构。因为合金是有界的，所以整数非常微妙。

【讨论】：