0

合金で二重にリンクされたリストを逆にしようとしていたので、その署名を作成しました。これが署名です

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つの要素を実行したときに望ましい結果が得られることです。その後、1つの要素が3度以上と3度以上ある場合を示します。

4

1 に答える 1

1

私の第一印象は、このモデルはこの問題に対して非常に複雑であるということです。デバッグするのではなく、書き直すことを強くお勧めします。

ここにあなたのモデルについてのいくつかの無関係なコメントがあります

  • スコープ仕様で使用する代わりに、対応するsig宣言でexactly 1使用できます(たとえば、;の代わりに;one sigone sig firstexactly 1 first

  • スコープ仕様で使用する代わりに、対応するsig宣言でexactly 0使用できます(たとえば、;の代わりに;abstract sigabstract sig nodeexactly 0 node

  • 「最初」、「最後」、「要素」を異なるタイプのノードにする正当な理由は本当にわかりません。node代わりに単一の署名を使用したいと思います。

  • 両方head: one firstを持っており、headpoint: head -> one ele冗長に見えます。単一のヘッドノードを使用する場合は、単純に次のように言うことができますhead: one node

  • 同様に、one r: head追加されたファクトの1つで使用することも不要です。これは、正確に1つのノード(モデルでは常にの単一のアトムになる)headを指していることがわかっているため、常にそのノードになります。firstr

リストをこのようにモデル化する強い理由があるかどうかはわかりません。私の最初のアプローチは、オブジェクト指向スタイルの何かです。

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

sig DLinkedList {
    head: lone Node
}

...

二重リンクリストから独立してノードを存在させたい場合(つまり、DLinkedListsigにそれを定義する必要なすべての関係が含まれている場合、これは絶対に問題ありません)、私はまだspecialfirstlastsubsigを使用しません。多分何かのような

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 に答える