Modeling from A to Z/Modeling principles/A is for Alloy analyzer

From Wikibooks, open books for an open world
Jump to navigation Jump to search

What is the Alloy analyzer?[edit | edit source]

Alloy 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[edit | edit source]

Let 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:

simple 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.

The structure of the simple model of the addressBook

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[edit | edit source]

Let 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[edit | edit source]

Now 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:

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[edit | edit source]

Now 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.

An illustration of a problem in the design of our model.

Elimination of identity cycling[edit | edit source]

We 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)
    }

Problem of cycling identities solved.

From OtherNames to Xpoints[edit | edit source]

Now let us consider the following result:

An ArtTheme which has two webAddresses.

pred show (ace: ArtExhibitionCatalog) some OtherName.(ace.webaddress)}

From addressBook to vCard[edit | edit source]

Starting 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.

simple vCard
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
EMAIL
ADR

http://www.imc.org/pdi/pdiproddev.html

Notes[edit | edit source]

  1. "Like Z, it describes all structures (in space and time) with a minimal toolkit of mathematical notions," Jackson 2006, p.xii
  2. Some brief information on Felix Chang is given in the e-Links.
  3. We use addressBook2 as the key example taken from Daniel Jackson's book Software Abstractions, p.17
  4. 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.
  5. We have simplified Jackson's model a little bit. His module, page 6, has the longer title „tour/addressBook1“
  6. 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.
  7. 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.
  8. Jackson 2006, p.xiii
  9. vCard version 2.1 Specification
  10. vCard version 2.1 Specification
  11. vCard version 2.1 Specification
  12. vCard version 2.1 Specification

Reading links[edit | edit source]

  1. 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 | edit source]

vCard[edit | edit source]