двойно свързан списък в сплав

Опитвах се да обърна двойно свързан списък в сплав, създадох подпис за него. Това е подписът

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 indegree и 3 outdegree.


linked-list doubly-linked-list alloy
person leo    schedule 27.03.2013    source източник

Отговори (1)


arrow_upward
1
arrow_downward

Първото ми впечатление е, че този модел е прекалено сложен за този проблем и силно препоръчвам пренаписване, вместо отстраняване на грешки.

Ето някои несвързани коментари за вашия модел

  • вместо да използвате 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
}

...

Ако искате вашите възли да съществуват независимо от двойно свързания списък (т.е. DLinkedList sig да съдържа всички необходими релации, които го дефинират, което между другото е абсолютно добре), все още не бих използвал специални first и last subsigs. Може би нещо подобно

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
}
person Aleksandar Milicevic    schedule 28.03.2013
comment
Аз съм начинаещ в сплавта и не се занимавам с нищо друго освен предикати. Пуснах вашата програма и тя показва, че главата и опашката са един и същ възел. Валиден екземпляр на DLL ли е?. Също така бих искал да напиша модел за реверс, но не знам откъде да започна. Как да покажа, че показаният екземпляр е обърнат LL. Ще изглежда по същия начин като екземпляр на нормален LL в сплав. Ще съм много благодарен, ако можете да посочите правилната посока откъде да започна. - person leo; 29.03.2013
comment
Ако размерът на списъка е 1, тогава е валиден екземпляр, ако и главата, и опашката сочат към един и същ възел. - person Aleksandar Milicevic; 31.03.2013
comment
Току-що редактирах отговора си, за да включа предиката reverse. За да напишете такъв предикат, обикновено предавате два аргумента, един за вход или предварително състояние (dl в моя код по-горе) и един за изход или след състояние (dl'). Тялото в този случай е доста просто, просто казва, че всичко в dl' е обратно на `dl'. - person Aleksandar Milicevic; 31.03.2013