MIT Alloy: Predicate in Receiver Notation

Question

I have a simple model of a bank with two account types A and B

abstract sig Account {}
sig A extends Account {}
sig B extends Account {}

sig Customer {
    hasAccount: some Account
}

sig Bank {
    hasCustomer: some Customer
}

I want to express that all customers must have at least one account of type B if they have an account of type A. My predicate:

pred Customer::BifA(){
    some a:A,b:B | a in this.hasAccount => b in this.hasAccount
}

However, this does not yield the desired result. Many of the instances the Analyser gives me contain customers who have account of type A, but then not of type B.

Where is the mistake in my predicate?

How did you generate the instances? Did you use the predicate when generating them? — dejvuth

dejvuth dejvuth · Accepted Answer · 2016-03-15T10:12:36

You shouldn't use the existential quantification for A. Imagine a customer does not have an account of type A. With that account the implication is trivially true.

Changing it to the universal quantification should work. Something like:

all a:A | a in this.hasAccount => some b:B | b in this.hasAccount

MIT Alloy: Predicate in Receiver Notation

1 Answers