Linked Data Structures: Restricting a link operation

Question

I have a model (see below) with two signatures: Data and Node. I have defined some predicates which characterise inhabitants of Node, namely: Orphan, Terminal, and Isolated.

What I want to do - but have not yet achieved - is to define a predicate Link which models the linking of two Node such that one Node becomes the successor (succ) of the other. Moreover, I would like to restrict the operation such that links can only be made to Isolated Nodes. Furthermore, I would like the restriction - if it is possible - to somehow be internal to the Link predicate.

Here is my latest attempt:

sig Data {}

sig Node {
    data: Data,
    succ: lone Node
}

// Node characterisation
pred Isolated (n: Node) { Orphan[n] and Terminal[n] }

pred Orphan (n: Node) { no m: Node | m.succ = n }

pred Terminal (n: Node) { no n.succ }


/*
 * Link
 * 
 * May only Link n to an m, when:
 *  - n differs from m
 *  - m is an Isolated Node (DOES NOT WORK)
 *
 * After the operation: 
 *  - m is the succcessor of n
 */
pred Link (n,m: Node) {
    n != m
    Isolated[m] /* Not satisfiable */
    m = succ[n]
}

pred LinkFeasible { some n,m: Node | Link[n,m] }

run LinkFeasible

Including the conjunct Isolated[m] renders the model unsatisfiable. I think I understand why: there can be no Node which is both Isolated and a successor of another. I include it only in the hope that it might reveal my intentions.

My question: how do I define the Link predicate to link two Nodes such that only Isolated nodes may be linked-to?

Answer 1

The problem is that you want Link to be an operation which changes the value of succ. In order to model change in Alloy, you need to add an ordered signature which represents the distinct states of your system. So your signature would look something like this:

open util/ordering[time]

sig Time {}
sig Data {}

sig Node {
    data: Data,
    succ: Node lone -> Time
}

But this also changes all of your predicates. You can't say that a node is isolated or terminal, you can only say that a node is isolated at time T.

If you have Software Abstractions, this is all covered in section 6.1. I'm not familiar with any good guides to modeling time in Alloy outside of that book.