1

我想从链接列表中删除一个元素并将其推送到堆栈上。我试图编写这段代码。我正在编写将元素推入堆栈的代码，但它给出了错误。该代码在注释中。

//双向链表

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

“未找到实例”不是错误，它只是分析的结果。

在您的情况下，由于这两个相互竞争的约束，它无法找到实例

// 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)

第一个说没有堆栈可以与任何列表共享一个节点。第二个明确表示 的元素afterstack必须包括 的最后一个节点beforelist。

我认为您应该删除第一个事实并将其写为谓词，然后您可以在给定的 ( node, list) 对（或一组对）上断言，因为我假设您的目标是在“之前”声明约束 hods 以及“之后”状态。

于 2013-04-23T14:05:11.927 回答