Modeling from A to Z/Modeling principles/A is for Alloy analyzer
What is the Alloy analyzer?
editAlloy is a formal language deeply rooted in Z[1]. It was developed by Daniel Jackson, currently at MIT. Daniel is the son of Michael Jackson who is well-known for his contributions to computing.
The Alloy analyzer is a constraint analyzer developed by Felix Chang[2], currently at MIT.
Simple model of the address book
editLet us take the classic example of the address book[3] and convert it into a formal equivalent model of a digital art gallery catalog. Here we are thinking of the names of paintings[4]. A physical painting is located in exactly one place. But the digital form of that painting, which we will call digital image, may be located in many different places. Such digital images are to be subject to control, for quality purposes, for copyright purpose, and so on. To motivate the work we will concentrate on a real-world example: the digital art exhibition.
But first let us start with the address book. In today's world we might be thinking of names and web addresses, or names and e-mail adresses, or ... There is so much potential. Let us be conservative and have some fun? Here is a simple old-fashioned address book:
| Name | Address |
|---|---|
| Harry Knooall | Black Rock, Big Peak county |
| Martha Underwude | Black Rock, Big Peak county |
| Charlie Bigfoot | on the road |
| Mary Wethervain | White Rock, Big Peak county |
To build a model requires investment of time and energy. To develop a meaningful model of one's own helps to understand the process of model building. This gives one a sense of ownership in the model. One might experiment with the simple model above. For example, if interested in the prison system, one might change „Black Rock“ to „Black Rock penitentiary“ or „Black Rock jail“ and maybe change „on the road“ to „on the run“.
Let us take the first first example used by Jackson in his book[5]:
module addressbook
sig Name, Addr {}
sig Book {
addr: Name -> lone Addr
}
The special keyword lone needs explanation. It indicates that each name is mapped to at most one address. It is possible for someone to have no address. In our little model „Charlie Bigfoot“ has no address in the usual sense. So, just for fun, we have given him[6] a special sort of address "on the road".
We can get a picture of our simple model.
|
|
| The structure of the simple model of the addressBook | The structure of the simple model of the addressBook using Magic Layout |
The image on the left is the default layout in the Alloy analyzer; that on the right uses the „Magic Layout“.
Our next step is to produce some typical address books. In particular we are interested to see if we can produce an example that corresponds to the old-fashioned address book with which we began.
pred show () {}
run show for 4 but 1 Book
Following the pattern of Jackson's development closely, one adds the predicate show to get at most 4 objects in each signature: Name and Addr but only 1 object Book.
So! We can think of „Harry Knooall“ having Name1, „Martha Underwude“ having Name0, „Black Rock, Big Peak county“ being represented by Addr2, and so on. In other words, we do have a good working model for the kind of address book we have in mind. Now what shall we do?
Digital Art Exhibition
editLet us begin with a simple correspondence. An address book associates names with addresses. The exhibition catalog associates names of digital images (of paintings or whatever) with web addresses.
We jump in straight away with the name of the module:
module exhibitionCatalog
The next step is the introduction of an abstract signature which we will call Xpoint[7]. The idea behind Xpoint is to indicate some end point in an XML namespace.
abstract sig Xpoint {}
Now we can define exactly what we mean by the web address of the digital image (of the painting or whatever).
sig WebAddr extends Xpoint {}
We also consider the possibility of groups of names. The purpose of the group is to cover the concept of artistic theme, such as Impressionism, Cubism, and so on. Let us try out the use of ArtTheme for such a group?
Similarly, an alias is a name for another name. It is frequently the case, that an artwork will have some name, such as Mother with Child. It is also possible that a caloguer will use an alias such as the Chicago Madonna for exactly the same artwork. It might seem convenient to use Alias for this purpose. However, in order to avoid confusion between this new (isomorphic) model and the original Jackson model we will use OtherName. Both ArtTheme and OtherName are sorts of Names, words which identify. But Name is used in the original Jackson model. Let us use instead the word Identity. And just as the Xpoint is in an XML space, then why not consider the Identity to be a kind of Xpoint?
abstract sig Identity extends Xpoint {}
Now we can define ArtTheme and OtherName as extensions of Identity:
sig ArtTheme extends Identity {}
sig OtherName extends Identity {}
For convenience, one might like to wrap up the previous two defintion in one line:
sig ArtTheme, OtherName extends Identity {}
Finally the ArtExhibitionCatalog is determined by setting up a relationship between the Identity (of the ArtWork) and the Xpoint (where it is located).
sig ArtExhibitionCatalog {webAddr: Identity —> Xpoint}
Encoding the model
editNow we put everything together
module exhibitionCatalog
abstract sig Xpoint {}
sig WebAddr extends Xpoint {}
abstract sig Identity extends Xpoint {}
sig ArtTheme, OtherName extends Identity {}
sig ArtExhibitionCatalog {webAddr: Identity -> Xpoint}
The first thing to do is show a picture of the structure of the metamodel:
It might be a good idea to make a printout or a sketch of this picture while studying the rest of the model.
Exercising the model
editNow we are ready to play with our little model. Before we do, it is really worthwhile to listen to what Daniel Jackson has to say on the subject:
«Building a model incrementally with an analyzer, simulating and checking as you go along, is a very different experience from using pencil and paper alone. The first reaction tends to be amazement: modeling is much more fun when you get instant, visual feedback, When you simulate a partial model, you see examples immediately that suggest new constraints to be added.»[8]
The most basic way to show what is going on is to use the predicate show. Here we want to show some of the possible webAddresses associated with our ArtExhibitionCatalog:
pred show (aec: ArtExhibitionCatalog) {some aec.webAddr}
and we want to limit our exploration of the model to at most 3 objects in each signature, except for the ArtExhibitionCatalog which is limited to 1 object:
run show for 3 but 1 ArtExhibitionCatalog
Finally, to get a picture of what is happening with respect to the ArtExhibitionCatalog, we project over it. That is to say, we know there is just one. Let us put it in the background and see what the rest of the picture looks like. Here is one such result.
Elimination of identity cycling
editWe must go back and fix the model. Specifically, one might add the fact that for any ArtExhibitionCatalog there is no Identity that is in a set of Xpoints which can be reached from that Identity. In other words, cycling (i.e. going round in circles) is out!
We state this as
fact {
all aec: ArtExhibitionCatalog | no id: Identity | id in id.^(aec.webAddr)
}
From OtherNames to Xpoints
editNow let us consider the following result:
pred show (ace: ArtExhibitionCatalog) some OtherName.(ace.webaddress)}
From addressBook to vCard
editStarting again from the simple address book we can move in the direction of the vCard. The task is to find a simple way of building up the model of the vCard, step by step. Why not begin with the example given in the Wikipedia article?
BEGIN:VCARD VERSION:2.1 N:Gump;Forrest FN:Forrest Gump ORG:Bubba Gump Shrimp Co. TITLE:Shrimp Man TEL;WORK;VOICE:(111) 555-1212 TEL;HOME;VOICE:(404) 555-1212 ADR;WORK:;;100 Waters Edge;Baytown;LA;30314;United States of America LABEL;WORK;ENCODING=QUOTED-PRINTABLE:100 Waters Edge=0D=0ABaytown, LA 30314=0D=0AUnited States of America ADR;HOME:;;42 Plantation St.;Baytown;LA;30314;United States of America LABEL;HOME;ENCODING=QUOTED-PRINTABLE:42 Plantation St.=0D=0ABaytown, LA 30314=0D=0AUnited States of America EMAIL;PREF;INTERNET:forrestgump@walladalla.com REV:20080424T195243Z END:VCARD
Our first task is to identify the meaning of the "key" words which are apparently given in uppercase. We recognize TITLE, WORK, VOICE, HOME and so on. But what exactly is N, FN, REV? These "key" words are called properties. The basic list of properties is FN, N, NICKNAME, PHOTO, BDAY, ADR, LABEL, TEL, EMAIL, MAILER, TZ, GEO, TITLE, ROLE, LOGO, AGENT, ORG, CATEGORIES, NOTE, PRODID, REV, SORT-STRING, SOUND, URL, UID, VERSION, CLASS, KEY. Let us begin by organizing these in a nice table. We will not fill in all the details right now.
| key | meaning | example | comment |
|---|---|---|---|
| FN | formatted name | Mr. Harry Knooall jnr | "This is the way that the name is to be displayed"[9] |
| N | name | KNOOALL;Harry;Mr.;Jnr | "a structured representation of the name of the person, place or thing"[10] |
| PHOTO | photograph | • | "This property specifies an image or photograph of the individual associated with the vCard." [11] |
| JPEG | photo format type | • | "This property parameter is provided to specify the graphics format for the Photo property value. The property parameter includes..."[12] |
| BDAY | |||
| ADR | |||
| LABEL | |||
| TEL | |||
| ADR |
Notes
edit- ↑ "Like Z, it describes all structures (in space and time) with a minimal toolkit of mathematical notions," Jackson 2006, p.xii
- ↑ Some brief information on Felix Chang is given in the e-Links.
- ↑ We use addressBook2 as the key example taken from Daniel Jackson's book Software Abstractions, p.17
- ↑ In practical work we will use digital photographs as digital images in our exhibition. Such digital photographs will be freely available under the usual Creative Commons license.
- ↑ We have simplified Jackson's model a little bit. His module, page 6, has the longer title „tour/addressBook1“
- ↑ It is important to be open about possible meanings of names. I say him. I could say her. If we want to be specific about gender, then we have to model it: female, male, other, for example.
- ↑ Jackson uses the name Target, p.17. It is very hard to imagine how one might come up with this particular way of doing things. In other words, to start with such an abstract signature seems to require prior knowledge. Such prior knowledge seems to require a great deal of sophistication or intuition.
- ↑ Jackson 2006, p.xiii
- ↑ vCard version 2.1 Specification
- ↑ vCard version 2.1 Specification
- ↑ vCard version 2.1 Specification
- ↑ vCard version 2.1 Specification
Reading links
edit- Jackson, Daniel (2006). Software abstractions : logic, language and analysis. Cambridge, Massachusetts: The MIT Press. ISBN 978-0262101149.
{{cite book}}: Check|isbn=value: checksum (help); Cite has empty unknown parameter:|coauthors=(help)
e-Links
edit- Felix Chang last access {2008-08-15}
vCard
edit- Representing vCard Objects in RDF/XML
- vCard, The Electronic Business Card, Version 2.1. A versit Consortium Specification, September 18, 1996