합금의 링크 된 목록에 삽입 및 삭제

Question

합금을 사용하여 링크 된 목록의 간단한 버전을 만들었습니다. 이제 삽입 및 삭제를 수행 할 수있는 링크 된 목록을 만들고 싶습니다. 나는 방금 합금으로 코딩을 시작했다. 지금은 함수 및 유틸리티 사용과 같은 복잡한 작업을 수행하는 데 문제가 있습니다. 유틸리티와 함수를 사용할 수있는 방법과 합금에서 실제로 삽입과 삭제를 수행 할 수있는 방법에 대한 몇 가지 예를 얻을 수 있다면. 도와 주셔서 감사합니다.

sig node{} 

sig linked 
{ 
    ele:set node, 
    link:ele->lone ele, 
    head:lone ele 
}{ 
    node = ele 
    all x:ele | x in head.*link && head not in x.link && #x.link <=1 
} 

fact{ 
    all l:linked| all e:l.ele| e->e not in l.link //no self loop 
} 

fact 
{ 
    all l:linked|no e : l.ele | (e in e.^(l.link)) //acyclic 
} 

pred a (l:linked,x:node) 
{ 
    x in l.ele  
} 

run a for 6 node,1 linked 

Answer 1

귀하의 접근 방법은 다소 혼란 스럽지만 훨씬 간단 할 수 있습니다. 나는 이것을 좋아할 것입니다

sig Node{ 
    next : lone Node 
} 

one sig Head in Node {}      -- head node is still a node 

fact{ 
    all n : Node | n not in n.^next   -- no cycles 
    no next.Head       -- no node points to Head 
    all n : Node - Head | some next.n  -- for all other nodes, there has to be someone pointing to them 
} 

run {} for 10 

이 모델은 동적입니다. 모델을 동적으로 만들려면 상태 개념을 이해해야합니다. Alloy의 저자가 작성한 Software Abstractions을 읽어 보시기 바랍니다. 연결된 목록을 동적으로 접근하는 것은 너무 복잡하여이 시점에서 이해할 수 없으므로 간단한 연습을해야합니다.

정적 예 :

sig State {} 

abstract sig Target {} 

sig Email extends Target {} 

abstract sig Name extends Email { 
    name : set State, 
    addr : Target some -> State 
} 

sig Group, Alias extends Name {} 

fact { 
    all a : Alias | lone a.addr 
    no n : Name | n in n.^addr 
} 

run {} 

동적 예를 들어, 로컬 상태 관용구 (= 표현하는 방법으로

국가의 기본 아이디어는 (책에 address book 예에 따라 운동)입니다 각주의 관용구와 사건 관용어도있다). 당신은 또한 다음과 같은 slides 좀 걸릴 수 있습니다 술어

open util/ordering[State] 
sig State {} 

abstract sig Target {} 

sig Email extends Target {} 

abstract sig Name extends Email { 
    name : set State, 
    addr : Target -> State 
} 

sig Group, Alias extends Name {} 

fact { 
    all s : State { 
     all a : Alias & name.s | lone a.addr.s 
     no n : name.s | n in n.^(addr.s) 
     addr.s in name.s -> Target 
     addr.s :> Name in Name -> name.s 
    } 
} 

run {} for 3 but exactly 1 State 

-- adding a name n, for a given pre state s and post state s' 
pred addName [n : Name, s,s' : State] { 

    -- the name must not exist in the pre state 
    n not in name.s  

    -- the relation names in the post state is what is was 
    -- in the pre state in addition to the new name 
    name.s' = name.s + n 

    -- the address relation stays the same  
    addr.s' = addr.s 
} 

run addName for 3 but 2 State 

pred addTarget [n : Name, t : Target, s,s' : State] { 
    t not in n.addr.s 
    name.s' = name.s 
    addr.s' = addr.s + n->t 
} 

run addTarget for 3 but 2 State 

를 살펴 보자.

Answer 2

삽입 및 삭제와 같은 작업을 모델링하기 위해 모델을 "동적"으로 만들 필요가 없습니다. 이 주제 (doubly-linked-list-in-alloy)에서 이중 연결 목록의 역 연산을 모델링하는 방법에 대한 대답을 한 다음 충분히 도움이되지 않았다면 알려주십시오. 프리 - 스테이트와 포스트 - 스테이트 모두에 대해 인수를 취하는 술어를 생성하고 둘이 어떻게 관련되는지를 주장하는 것이 기본 아이디어입니다. 예를 들어 삽입 조건부는 다음과 같습니다.

// l - list in the pre-state 
// x - node to be inserted 
// l' - list in the post-state 
pred insert (l: linked, x: node, l': linked) { 
    l'.ele = l.ele + x 
    ... 
}