Seq num

include order

module sequence_numbers = {

    type t
    instance props : totally_ordered(t)

    action next(seq:t) returns (res:t)

    object spec = {
    after next {
        assume exists X. seq < X;
        assert seq < res & (X < res -> X <= seq)
    }
    }

    object impl = {
    interpret t->bv[16]
    implement next {
        res := seq + 1
    }
    }

    isolate iso_props = props with impl
}