5.0.0 Change List

BETA 5.0.0 Change List

Known Issues

• Crashes when not in debug mode. Start alloy like:

   $ jar -Ddebug=yes -jar alloy.jar
  

  Will fix this asap

• Too much output of stack traces when compiling for tooltips or navigation

Markdown Syntax

The Alloy parser and editor have been adapted to support Markdown syntax. As inspiration (and motivation) the Github format is followed.

Therefore first, such a file is a markdown file and should therefore have an extension of .md.

A Markdown Alloy file is recognized if the the first line consists of 3 dashes, then a number of headers, and another 3 dashes. This is the so called YAML header.

---
title: Dining Philosophers
---

After the YAML header, the parser interprets all text as markdown. The editor will highlight some of the markdown instructions. For example, headers (#), bold (*), and italic (_) are supported. To start an Alloy section, it is necessary to have an line with the alloy code separator. This is a line that starts with 3 backticks and then the word alloy. To end the Alloy section, make a line with three backticks. For example:

# Literate Programming 

Let us change our traditional attitude to the construction of programs: Instead 
of imagining that our main task is to instruct a computer what to do, let us 
concentrate rather on explaining to human beings **what** we want a computer to do.

```alloy
sig Foo {} // this is Alloy syntax
```

If you find that you're spending almost _all_ your time on theory, start turning 
_some_ attention to practical things; it will improve your theories. If you find 
that you're spending almost all your time on practice, start turning some attention 
to theoretical things; it will improve your practice.

You can store such documents on Github. Since the syntax is aligned with Github's mechanism to associate syntax coloring. You can find the Dining Philosophers formatted and displayed this way. Github will also recognize the YAML header and format it nicely.

The YAML header can be used in conjunction with Github pages. Github Pages allow you to maintain a website via Github, the YAML header is then used to private the required meta-data like title, layout, etc. The website shows the Dining Philosophers also.

There are no open issues but I could be convinced to support more markdown formatting in the editor.

Evaluator Tables

The evaluator normally shows the output of the toString method of a TupleSet. This output is quite unreadable since it does not contain any newlines so all columns and rows are messed up. Also, each atom in the table is formatted as Signame$3. For even small tables, this quickly becomes hard to read.

For example, take the following model as an example. The evaluator would then show:

{Foo$1->A$0->-1, Foo$1->A$0->-2, Foo$1->A$0->-3, Foo$1->A$0->-4, Foo$1->A$0->0, Foo$1->A$0->1, Foo$1->A$0->2, Foo$1->A$0->3, Foo$1->B$0->-2, Foo$1->B$0->-3, Foo$1->B$0->-4, Foo$1->B$0->2, Foo$2->B$0->-1, Foo$2->B$0->0, Foo$2->B$0->1}

This is of course not easy to read for humans. For this reason, the output has been replaced with:

You'll probably notice that the output of the cells has been changed from the $ separating the atom type name and the index, it uses superscripts instead. This is slightly shorter and makes the tables look less dense. The index is suppressed when there is only a single atom in the table and it has an index of 0.

Note: Please provide feedback. I see the superscripts are a bit small. We could change the $ to a less dense character that might also help to reduce the clutter. I kind of like them but I do understand they're a bit small. You can of course always increase the font size.

In the table, the first column will not repeat the atom name when it is the same, leaving the cell blank.

You can copy the cells and paste them in the evaluator. This will change the superscripted atom names back into the $ form. I.e. Foo² then becomes Foo$2 again.

Table View

The Viz Gui has been extended with a table pane. You can select this pane in the Viz view. Select the Table icon. (Hope someone will provide a better icon before the beta is released.)

This pane shows the atoms in tables where each atom is shown in relation with its fields. For example, the following image shows some table output for well known Alloy examples:

The tables are constructed from an atom and its fields. This construction goes as follows:

1. Create a set result with the atoms of one sig.
2. for each field f
3. Set temp to f.values
4. if temp is empty, then temp is a relation with the same arity but a filled with a special atom called ∅
5. create the product of result and temp selecting on the first column of both while removing the first column of temp

Note: Can anyone put this, or similar, algorithm in in Alloy? Not sure this algorithm is actually correct.

For example. The previous model in the Evaluator section would be displayed as:

Notice how Foo² has no members for the bar relation, shown as ∅, but does have a value for the n relation.

Selecting Text

You can now double click on a word and only that word is selected. Before release 5, everything between whitespaces was annoyingly selected. This generally tended to be too long.

Shifting a block of text

A selected block of text in the Alloy editor can be indented or outdented. Select the text and hit TAB will indent the text with one tab. SHIFT-TAB will outdent the text where a line in the selected block starts with a tab.

Commenting out a block of text

Select a block of text and type COMMAND-/. If a line in the selected block starts with two slashes ('/' or pedantically called a solidus) then these slashes are removed. Otherwise, the two slashes are inserted.

This is a very convenient way to comment out a part of the model. Extremely useful when you're figuring out why a model does provide an instance.

Navigation

The F3 key is a navigation key. If a clause in a model is referencing some other part of the model then clicking on it and pressing F3 will the referenced clause become selected. For example, if in a model the cursor is on the name of a sig (i.e. it references that sig) then pressing F3 will select the clause that defines the sig. This will open another module if that sig is defined in another module.

This (should) work for:

• Sigs
• Functions
• Predicates
• Fields

For navigation to work the model must compile correctly. This is necessary because many references require disambiguation. For example, a predicate called foo could occur multiple times in a model. It is therefore not possible to just look for the same string. Also, some references can occur in another file. The navigation therefore compiles the model and uses the actual expression on which the cursor rests to find out what the reference is.

Tooltips

All references to sigs, variables, fields, and predicates now have a tooltip. The tooltip shows the type information. Just hover over an expressions and after a few seconds the tooltip will appear.