No Instance Found When Using "always"

Question

I'm trying to visualise a spec for a Payment object where it moves from "queued" to "processing" to "complete". I have come up with the following:

enum State {Queued, Processing, Complete}

sig Payment {
    var state: State
}

pred processPayment[p: Payment] {
    p.state = Queued // guard
    p.state' = Processing // action
}

pred completePayment[p: Payment] {
    p.state = Processing // guard
    p.state' = Complete // action
}

fact init {
    Payment.state = Queued
}

fact next {
    always (some p : Payment | processPayment[p] or completePayment[p])
}

run {} for 1 Payment

Unfortunately, I get no instances found for this spec. From my understanding, a Payment with state "Queued" initially and a next state where it's in "Processing" should be allowed with the always (some p : Payment | processPayment[p] or completePayment[p])" formula according to the tutorial at https://haslab.github.io/formal-software-design/overview/index.html. Am I missing something?

Answer 1

The issue turned out to be a missing terminating predicate, adding the below(or a stutter) fixes it.

pred afterComplete[p: Payment] {
    p.state = Complete // guard
    p.state' = Complete // action
}