1

我使用合金创建了一个简单版本的链表。现在我想创建一个可以在其中执行插入和删除的链表。我刚开始用合金编码。现在我在使用函数和实用程序等复杂操作时遇到了麻烦。如果我能得到一些关于如何使用实用程序和函数以及如何在合金中实际执行插入和删除的示例。我会很感激你的帮助。

sig node{}

sig linked
{
  ele:set node,
  link:ele->lone ele,   
  head:lone ele
}{
  node = ele
  all x:ele | x in head.*link && head not in x.link && #x.link <=1 
}

fact{
  all  l:linked| all  e:l.ele| e->e not  in l.link //no self loop
}

fact
{
  all  l:linked|no e : l.ele | (e  in e.^(l.link )) //acyclic
}

pred a (l:linked,x:node)
{
  x in l.ele    
}

run a for 6 node,1 linked
4

2 回答 2

2

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

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

该模型是静态的，为了使模型动态，您需要了解状态的概念。我建议您阅读由 Alloy 的作者撰写的Software Abstractions 。链表的动态方法对您来说太复杂了，此时您无法理解，您应该做一些更简单的练习。

状态的基本思想是（根据书中的通讯录例子练习）：

静态示例：

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

您还可以查看以下幻灯片。

于 2013-04-21T13:43:05.993 回答
1

您不需要使模型“动态”来模拟插入和删除等操作。查看这个主题（双向链表在合金中），我在其中给出了如何为双向链表建模反向操作的答案，然后让我们知道这是否不够有用。您将看到的基本思想是创建一个谓词，该谓词接受前状态和后状态的参数，并断言两者之间的关系。例如，您的插入谓词可能看起来像

// 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
  ...
}
于 2013-04-21T15:11:09.930 回答