CODEWITHSUNDEEP
alloy
FormalizeMe
FormalizeMe

Reputation: 66

No Instance Found When Using "always"

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?

Upvotes: 0

Views: 83

Answers (2)

FormalizeMe
FormalizeMe

Reputation: 66

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
}

Upvotes: 1

gordonc
gordonc

Reputation: 532

I am not an expert but I believe that it is impossible for either of your predicates to be true at t0. I think you need a holdPayment predicate like this:

pred holdPayment[p:Payment] {
  p.state = p.state'
}

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

run {} for 1 Payment

Upvotes: 0

Related Questions