1

Linked ListからElementを削除してStackにプッシュしたいのですが、こんなコードを書いてみました。要素をスタックにプッシュするコードを書いていましたが、エラーが発生しています。そのコードはコメントにあります。

//双方向リンクリスト

sig node{}
sig list
{
    elts: set node,
    next: elts lone->lone elts,
    prev: elts lone->lone elts,
    first: one node,
    last: one node
} 
{
    all x:elts | x not in x.^next
    all x:elts | x not in x.^prev
    no first.prev
    no last.next

    first.^next=elts-first
    last.^prev=elts-last
    all x,x1:elts | (x.next=x1) =>(x1.prev=x)
}

//スタック

one sig Null extends node{}

sig stack
{
    elts: set node,
    top: one elts,
    next: elts lone ->lone elts
} 
{
    all e:elts | all l:list | all l1:l.elts | l1 not in e
    all e:elts | e not in e.^next
    no Null.next
    top.^next=elts-top
    Null in elts
} 
pred undo(beforelist,afterlist:list,beforestack,afterstack:stack)
{

要素をスタックに挿入するために、このコード(コメント内)を試しました。しかし、これによりインスタンスが見つかりませんというエラーが発生します。

/*
    afterstack.elts=beforestack.elts+(beforelist.last)
    beforelist.last=afterstack.top
    afterstack.next=beforestack.next+(beforelist.last->beforestack.top)
*/  

    //afterstack.elts=(beforestack.elts)+(beforelist.last)

        afterlist.elts=beforelist.elts-beforelist.last
        afterlist.last=beforelist.last.(beforelist.prev)
    }
run undo for 2 list,2 stack, 5 node
4

1 に答える 1

0

「インスタンスが見つかりません」はエラーではなく、分析の結果です。

あなたの場合、これらの2つの競合する制約のためにインスタンスを見つけることができません

// inside appended facts for sig stack
all e:elts | all l:list | all l1:l.elts | l1 not in e

と

afterstack.elts=beforestack.elts+(beforelist.last)

最初のものは、どのスタックもどのリストともノードを共有できないことを示しています。afterstack2 番目のものは、 の要素がの最後のノードを含まなければならないことを明示的に示していますbeforelist。

node最初の事実を削除して、特定の ( , list) ペア (またはペアのセット) でアサートできる述語として記述する必要があると思います。 「後」の状態と同様に、制約が保たれている状態。

于 2013-04-23T14:05:11.927 に答える