abstract sig state
{
    prev : some state,
    next : some state
}

one sig begin extends state{}
some sig end extends state{}
sig mid extends state{}

//There is no state after end state, and there is no state before begin state

pred dosomething
{
    all s : state, b : begin | b.prev = s
}

run{dosomething}