0

I was trying to reverse a doubly linked list in alloy, I created a signature for it. This is the signature

sig node{}


//define each field as disjoint subset of node
sig first extends node{}

sig last extends node{} 

sig element extends node{}


sig doublylinkedlist{
head:one first,  //define one head pointer
null:one last,  //define one null pointer
ele:set element, //elements of the linked list
links:ele->ele, //paths between elements of a linked list
headpoint:head->one ele, //head points to one element of linked list
nullpoint:ele->null //one element of linked list points to null
}{
no links & iden  // no self refrence
one nullpoint //only one element points to null
links=links + ~links    //elements can point to prev element
all e:ele | e.(^(links))=ele // elements are connected
all e:ele | one r:head, n:null | (r->e) in headpoint => (e->n) not in nullpoint     //element being pointed by head cannot point to null
all e:ele | #(e.(links))<3 and #((links).e)<3 //elements cannot have more than 3   indegree and more than 3 outdegree
all e:ele | one r:head | (r->e) in headpoint => #((links).e)=1 && #(e.(links))=1 //element being pointed by head has indegree and outdegree 1
all e:ele | one n:null | (e->n) in nullpoint => #((links).e)=1 && #(e.(links))=1 //element being pointing to null has indegree and outdegree 1
 }

pred reverse{
}

run reverse for 1 doublylinkedlist, exactly  4 element ,exactly 1 first,exactly 1 last,exactly 0 node

The problem is that it gives desired result when i run for exactly 8 elemnts. After that it shows instances where one element has more than 3 indegree and 3 outdegree.

4

1 回答 1

1

我的第一印象是这个模型对于这个问题过于复杂，我强烈建议重写而不是调试它。

以下是关于您的模型的一些不相关的评论

  • 而不是exactly 1在范围规范中使用，您可以one sig在相应的 sig 声明中使用（例如，one sig first代替exactly 1 first;

  • 而不是exactly 0在范围规范中使用，您可以abstract sig在相应的 sig 声明中使用（例如，abstract sig node代替exactly 0 node;

  • 我真的不认为有充分的理由让“第一个”、“最后一个”和“元素”不同类型的节点；我宁愿使用单个node签名；

  • 两者兼而有之head: one first，headpoint: head -> one ele似乎是多余的。如果打算有一个头节点，你可以简单地说head: one node；

  • 同样，one r: head在您附加的事实之一中使用也是不必要的，因为您知道这head将指向一个节点（在您的模型中始终是 的单个原子first），因此r始终是该节点。

我不知道您是否有充分的理由以这种方式为您的列表建模。我的第一种方法是更多面向对象的风格，例如，

sig Node {
    next: lone Node, 
    prev: lone Node
}

sig DLinkedList {
    head: lone Node
}

...

如果您希望您的节点独立于双向链表而存在（即，让DLinkedListsig 包含定义它的所有必要关系，这绝对没问题），我仍然不会使用特殊first和lastsubsigs。也许像

sig Node {}

sig DLinkedList {
    head: lone Node,
    tail: lone Node,
    nxt: Node -> lone Node,
    prv: Node -> lone Node,
    nodes: set Node
} {
    nodes = head.*nxt
    some nodes => one tail
    no ^nxt & iden // no cycles
    nxt = ~prv     // symetric   
    no prv[head]   // head has no prv
    no nxt[tail]   // tail has no nxt
    head.^nxt = Node.^nxt // all nodes in nxt are reachable from head
}

pred reverse[dl, dl': DLinkedList] {
    dl'.head = dl.tail
    dl'.tail = dl.head
    dl'.nxt = dl.prv
}

run {
    some dl, dl': DLinkedList | reverse[dl, dl']

    // don't create any other lists or nodes
    #DLinkedList = 2
    Node = DLinkedList.nodes
}
于 2013-03-28T20:29:06.330 回答