CODEWITHSUNDEEP
linked-listdoubly-linked-listalloy
leo
leo

Reputation: 3

doubly linked list in alloy

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.

Upvotes: 0

Views: 1061

Answers (1)

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3857

My first impression is that this model is overly complex for this problem, and I'd strongly suggest rewriting instead of debugging it.

Here are some unrelated comments about your model

  • instead of using exactly 1 in a scope specification, you can use one sig in the corresponding sig declaration (e.g., one sig first instead of exactly 1 first;

  • instead of using exactly 0 in a scope specification, you can use abstract sig in the corresponding sig declaration (e.g., abstract sig node instead of exactly 0 node;

  • I really don't see a good reason to make "first", "last", and "element" different types of nodes; I would rather use a single node signature instead;

  • having both head: one first and headpoint: head -> one ele seems redundant. If the intention is to have a single head node, you can simply say head: one node;

  • similarly, using one r: head in one of your appended facts is also unnecessary, because you know that head is going to point to exactly one node (which in your model is always going to be the single atom of first), so r is always going to be that node.

I don't know if you have a strong reason to model your list this way. My first approach would be something more in the object-oriented style, e.g., 

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

sig DLinkedList {
    head: lone Node
}

...

If you want your nodes to exist independently of the doubly-linked list (i.e., have the DLinkedList sig contain all necessary relations defining it, which is btw absolutely fine), I would still not use special first and last subsigs. Maybe something like

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
}

Upvotes: 1

Related Questions