Вставка и удаление в связанных списках в сплаве

Ваш подход немного сбивает с толку, он мог бы быть намного проще. я бы сделал вот так

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. Динамический подход к связному списку будет слишком сложным для понимания на данном этапе, вам следует выполнить более простое упражнение.

Основная идея состояний (упражнение, основанное на примере адресной книги в книга):

статический пример:

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 {}

динамический пример, в идиоме локального состояния (= способ выразить состояния, есть также идиома глобального состояния и идиома события). Взгляните на предикаты

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

Вы также можете просмотреть следующие слайды.

Вам не нужно делать модель «динамической», чтобы моделировать такие операции, как вставка и удаление. Посмотрите на эту тему (double-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
  ...
}