双链表合金

Question

我试图逆转合金中的双重链表，我为它创建了一个签名。这是签名

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

问题是，当我正好运行8个元素时，它给出了期望的结果。在此之后，它会显示一个元素具有超过3个indedegree和3个outdegree的实例。

Answer 1

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

这里是一些与你的模型无关的评论

• 代替在作用域规范中使用exactly 1，您可以在相应的签名声明中使用one sig(例如，用one sig first代替exactly 1 first;

• 代替在作用域规范中使用exactly 0，您可以在相应的签名声明中使用abstract sig(例如，用abstract sig node代替exactly 0 node;

• 我真的没有看到一个很好的理由使"first"， "last"one_answers"element"不同类型的节点;我宁愿使用单个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
}
...

如果您希望您的节点独立于双链表存在(即，让DLinkedList签名包含定义它的所有必要关系，这绝对没问题)，我仍然不会使用特殊的first和last子签名。比如

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
}