Search code examples
subsetmodelingalloyrequirements

Getting subsets of signatures in Alloy

I was wondering if there is a way to extract a subset of a set in a given signature in Alloy. The extracted set will then be used in the definition of some facts of the model.

Assume the following model:

abstract sig Status{}
one sig Status1 extends Status{}
one sig Status2 extends Status{}

sig A {
     status: one Status
}

sig B {
     setA: set A
}

fun SubsetOfSetAinB [b: B] : set A {
    //have some kind of operation here 
    //that returns a subset of b.setA where b.setA.status in Status1
}

Thank you for your time.

Solution

  • You should be able to get this with a set intersection, like b.setA & Status1.~status.