Alloy语言链表定义及Create/Put/Find谓词实现求助

原链表实现代码 #

module List

// The List signature
lone sig List { rootElement: lone Element } 

// A list element signature
sig Element { nextElement: lone Element }


// Prevents an Element from referencing itself
fact preventElementLooping {
    no ele: Element | ele = ele.nextElement
}

// Zero Element outliers
fact allElementsBelongToOneList {
    all ele: Element | one list: List | ele in list.rootElement.*nextElement
}

// Prevents Elements from referencing a Element before it in the List
fact preventCycle {
    no ele: Element | ele in ele.^nextElement
}

原谓词实现代码 #

pred create(list, list":List) {
    list".rootElement = none    
}

pred put(list, list":List, ele: Element) {
    list".rootElement = ele
}

pred find [list:List, ele: Element] {
    ele = list.rootElement or ele in list.rootElement.^nextElement
}

疑问解答 #

1. 使用链表是否过于复杂？普通List该如何实现？ #

Alloy中实现List不一定非要用链表，内置的序列（sequence）类型是更简单的选择，它天然支持元素顺序、索引访问，无需手动维护指针关系，代码更简洁：

module List

sig List {
  elements: seq Element // 直接用序列存储元素，自带顺序和索引
}

这种实现适合绝大多数场景，只有当需要模拟底层链表的指针结构时，才需要用你当前的链表实现。

2. Put谓词仅首次添加有效，重复添加会替换根元素，如何修正？ #

原Put谓词的问题是直接覆盖了根元素，没有连接原有链表。修正后的谓词需要区分原列表为空/非空两种情况，同时保证新元素未被其他列表引用：

pred put(list, list': List, ele: Element) {
  // 新元素不属于任何现有列表，避免重复或循环
  ele not in Element
  // 处理空列表和非空列表的情况
  (list.rootElement = none => list'.rootElement = ele) else {
    list'.rootElement = list.rootElement
    // 找到原列表的最后一个元素（无nextElement的元素）
    let last = { e: list.rootElement.*nextElement | no e.nextElement } |
      last.nextElement = ele
  }
  // 保持其他元素的next关系与原列表一致
  all e: Element - ele - last | e.nextElement = list.rootElement.*nextElement[e]
}

3. Find谓词需返回匹配元素的所有索引，Alloy对数字支持有限，是否需要定义Index签名？ #

Alloy的整数支持确实有限，但无需额外定义Index签名，可通过**函数（function）**返回索引集合（谓词只能返回布尔值，不适合返回结果）：

链表实现下的索引计算函数

// 返回元素在列表中的所有索引（索引从0开始）
fun find(list: List, ele: Element): set Int {
  { i: Int | 
    // 先判断元素是否在列表中
    ele in list.rootElement.*nextElement or ele = list.rootElement
    // 计算从根到当前元素的前驱节点数量，作为索引
    and i = #(list.rootElement.*nextElement & ele.^~nextElement)
  }
}

序列实现下的索引获取（更简单）

如果用序列实现List，直接调用内置的idxOf方法即可：

fun find(list: List, ele: Element): set Int {
  list.elements.idxOf(ele)
}

内容的提问来源于stack exchange，提问作者Cyberboy1551