CODEWITHSUNDEEP
alloy
Marcel
Marcel

Reputation: 335

MIT Alloy: Predicate in Receiver Notation

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?

Upvotes: 2

Views: 92

Answers (1)

dejvuth
dejvuth

Reputation: 7136

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

Upvotes: 2

Related Questions