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!
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:
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!
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.
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]
}