在合金的链表中插入和删除

2 回答

• 1

  你的方法有点令人困惑，它可能会简单得多 . 我会这样做的

  sig Node{
      next : lone Node
  }
  
  one sig Head in Node {}                     -- head node is still a node
  
  fact{
      all n : Node | n not in n.^next         -- no cycles
      no next.Head                            -- no node points to Head
      all n : Node - Head | some next.n       -- for all other nodes, there has to be someone pointing to them
  }
  
  run {} for 10
  

  这个模型是静态的，为了使模型动态化，你需要了解de的概念 . 我建议你阅读Software Abstractions，由Alloy的作者撰写 . 链接列表的动态方法太复杂了，你现在无法理解，你应该做一些简单的练习 .

  国家的基本思想是（根据书中的例子进行练习）：

  静态示例：

  sig State {}
  
  abstract sig Target {}
  
  sig Email extends Target {}
  
  abstract sig Name extends Email {
      name : set State,
      addr : Target some -> State
  }
  
  sig Group, Alias extends Name {}
  
  fact {
      all a : Alias | lone a.addr
      no n : Name | n in n.^addr
  }
  
  run {}
  

  动态的例子，在本地状态习语中（=一种表达状态的方式，还有一个全局状态习语和一个事件习语） . 看一下谓词

  open util/ordering[State]
  sig State {}
  
  abstract sig Target {}
  
  sig Email extends Target {}
  
  abstract sig Name extends Email {
      name : set State,
      addr : Target -> State
  }
  
  sig Group, Alias extends Name {}
  
  fact {
      all s : State {
          all a : Alias & name.s | lone a.addr.s
          no n : name.s | n in n.^(addr.s)
          addr.s in name.s -> Target
          addr.s :> Name in Name -> name.s
      }
  }
  
  run {} for 3 but exactly 1 State
  
  -- adding a name n, for a given pre state s and post state s'
  pred addName [n : Name, s,s' : State] {
  
      -- the name must not exist in the pre state
      n not in name.s    
  
      -- the relation names in the post state is what is was
      -- in the pre state in addition to the new name
      name.s' = name.s + n  
  
      -- the address relation stays the same    
      addr.s' = addr.s
  }
  
  run addName for 3 but 2 State
  
  pred addTarget [n : Name, t : Target, s,s' : State] {
      t not in n.addr.s
      name.s' = name.s
      addr.s' = addr.s + n->t
  }
  
  run addTarget for 3 but 2 State
  

  您还可以查看以下slides .

  回复于 2024-04-26T12:44:54+08:00
• 2

  您不需要创建模型"dynamic"来模拟插入和删除等操作 . 看看这个主题（doubly-linked-list-in-alloy），在那里我给出了如何为双向链表建模反向操作的答案，然后让我们知道是否't helpful enough. The basic idea you' ll看到要创建一个谓词，它接受两个前面的参数州和后州，并断言两者是如何相关的 . 例如，您的插入谓词可能看起来像

  // l - list in the pre-state
  // x - node to be inserted
  // l' - list in the post-state
  pred insert (l: linked, x: node, l': linked) {
    l'.ele = l.ele + x
    ...
  }
  

  回复于 2024-04-26T12:44:54+08:00