Alloy6 allowing invalid state transitions

Question

This is my spec, it tries to model a Sale with multiple Orders:

abstract sig Sale {
    var status: one Status,
    orders: some Order,
    amount: Int
}

enum Status { Pending, Ok, Err }

sig SingleSale extends Sale {}

sig MultiSale extends Sale {}

sig Order {
    var status: one Status,
    symbol: one Sym,
    amount: Int
}

sig Sym {}

fact "amounts are positive" {
    all s: Sale | s.amount > 0
    all o: Order | o.amount > 0
}

fact "single sales have a single order" {
    all ss : SingleSale | one ss.orders
}

fact "multi sales have multiple orders" {
    all ms: MultiSale | #(ms.orders) > 1
}

fact "orders are not shared by sales" {
    orders in Sale one -> some Order
}

fact "orders amount sums up to sale amount" {
    all s: Sale | s.amount = (sum o: s.orders | o.amount)
}

fact "all sale orders have the same symbol" {
    all s: Sale, o, p: s.orders | o.symbol = p.symbol
}

fact "multi sales can be at most of two different amounts, the even split and reminder" {
    all ms: MultiSale | #(ms.orders.amount) <= 2
}

pred pending_orders[s: Sale] {
    some o: s.orders | o.status = Pending
}

fact "successful sales mean all orders are successful" {
    all s: Sale | s.status = Ok implies (all o: s.orders | o.status = Ok) and not pending_orders[s]
}

fact "err sales mean at least one order is err" {
    all s: Sale | s.status = Err implies (some o: s.orders | o.status = Err) and not pending_orders[s]
}

fact "pending sales have pending orders" {
    all s: Sale | s.status = Pending implies pending_orders[s]
}

pred order_success[o: Order] {
    o.status = Pending
    o.status' = Ok
    all p: (Order - o) | p.status' = p.status
    all s: Sale | s.status' = s.status
}

pred stutter {
    all o: Order | o.status' = o.status
    all s: Sale | s.status' = s.status
}

fact transitions { 
    always stutter or (some o: Order | order_success[o]) 
}

check {
    all o: Order | o.status = Ok implies always o.status = Ok
}

The problem lies with the state transitions, the check should disallow order transitions from Ok to other states but in fact this fails, allowing any kind of state transitions for orders (back to Pending or even to Err).

Why does this happen? Any additional comments and improvements are welcome 🤗

Answer 1

In Alloy, all unary operators bind stronger than binary ones. Hence your transitions fact actually reads (always stutter) or (some o: Order | order_success[o]), rather than the expected always (stutter or (some o: Order | order_success[o])).