двусвязный список в сплаве

Я пытался перевернуть двусвязный список в сплаве, я создал для него подпись. это подпись

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 степеней входа и 3 степени исхода.


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 содержала все необходимые отношения, определяющие его, что абсолютно нормально), я бы все равно не использовал специальные сабсиги 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
}
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