удалить узел из связанного списка и вставить в стек с помощью анализатора сплавов

Question

Я хочу удалить элемент из связанного списка и нажать его на Stack.I попытался написать этот код. Я писал код, чтобы вставить элемент в стек, но он дает ошибку. Этот код находится в комментарии.

// двусвязному список

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 

Answer 1

«Ни один случай не найден» не является ошибкой, это просто результат анализа.

В вашем случае это не может найти экземпляр из-за этих двух конкурирующих ограничений

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

Я думаю, что вы должны удалить первый факт и написать его как предикат, который вы можете затем утверждать на данной() паре (или наборе пар), поскольку, я полагаю, ваша цель - сказать что в состоянии «до» это ограничение ограничивается, а также в состоянии «после».