首页 文章

找不到简单List示例的实例

提问于
浏览 次
0

我正在研究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说：找不到实例 . 加上我的不一致 . 但是当我运行check listSize时，它没有找到任何反例，表明listSize是有效的 . 有人知道为什么Alloy Analyzer找不到一个添加实例？我尝试更改元素的数量，但不起作用 . 我认为这个模块非常简单，但我真的不知道为什么我会遇到这个问题 .

alloy

1 回答

  • 0

    这是我注意到的一件事 . 你内容的decl

    content: Int ->one A,

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

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

    这是不一致的 .

    更一般的观点：只要有可能，使用关系（即图形）的结构不使用整数作为索引 . 因为Alloy是有界的，整数是非常微妙的 .

    回复于

相关问题