Alloy Community

User login

Select in Alloy

 
Posted on: Thu, 07/23/2009 - 08:40
Joined: 2009-07-23
Points: 7
User is offline
Select in Alloy
Hello,

Could you please write the shortest way of doing select in Alloy, e.g. I have

sig Address {}
sig Name {}

sig Person {
    address: Address,
    name: Name
}

somewhere I have, e.g. in predicate
a: Address
n: Name

persons: seq Person

I would like to get a subsequence of persons whose address is equal to 'a' and name is equal to 'n'. E.g. in OCL it would be

persons->select(address = a and name = n)

Thank you.
 
Posted on: Thu, 07/23/2009 - 09:06    #1
Joined: 2008-05-15
Points: 334
User is offline
Sequence is ordered. Sets are unordered.

You can write a function that
returns the set of people with that given address and name.

fun getPeople [a: Address, n: Name] : set Person {
  { p: Person | p.address = a and p.name = n }
}

But you can't write a function that returns
the sequence of people with that address and name,
because there are many different legal sequences
(eg. if Alex and Bob both have that name and address,
then the sequence 0->Alex+1->Bob is a legal return value,,
and the sequence 0->Bob+1->Alex is also legal,
thus there are multiple possible return values,
thus it is not a function!
 
Posted on: Thu, 07/23/2009 - 09:46    #2
Joined: 2009-07-23
Points: 7
User is offline
Thank you for reply. And what about if I have

sig AddressBook {
    persons: seq Person
}

I would like to only get the people meeting the condition in the same order as they are in the book, e.g.

0. John - meets
1. Paul - does not
2. Joan - meets
3. Charles - meets
4. Jim - does not
5. Mary - meets

Result

0. John - meets
1. Joan - meets
2. Charles - meets
3. Mary - meets

Is it possible to define a function that achieves that?

fun getPeople [p: seq Person, a: Address, n: Name] : seq Person {

....

}

Thank you.
 
Posted on: Thu, 07/23/2009 - 11:28    #3
Joined: 2008-05-15
Points: 334
User is offline
Not easily (especially as we don't currently support recursion).
 
Posted on: Sat, 07/25/2009 - 10:04    #4
Joined: 2009-07-23
Points: 7
User is offline
OK thank you. Alloy is very powerful for working with sets. However, during software specification I often meet a pattern that there is a sequence of items and it is necessary to take the first item that meets some conditions and drop the following items. E.g. take the first rule, first address, first subscriber etc. meeting the conditions. I was not sure it is possible to achieve this with Alloy. It seems it is:

sig Person {
    address: Address,
    name: Name
}

sig Name {}
sig Address {}

fun getFirst [p: seq Person, n: Name, a: Address] :Person {
    let selectedPersons = p.name.n<:p.address.a<:p,
        minIndex = selectedPersons.univ - (selectedPersons.univ).^next | selectedPersons[minIndex]
}

Syndicate content  

The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.

Theme originally designed by Chris Herberte