Category Archives: Modelling

SiTra and Eclipse 3.3 or Java 1.6

Posted on by | Leave a reply

I recently installed eclipse 3.3 and Java 1.6. Today I tried to use SiTra (Simple Transformations in Java) but when I tried to compile it Java started complaining on the following methods of the SimpleTransformerImpl.java:

public Object transform(Object object) {
return transform(Rule.class, object);
}
public List<? extends Object> transformAll(List<? extends Object> sourceObjects) {
return transformAll(Rule.class, sourceObjects);
}

The error was something about java inconvertible types. I don’t know if it is the new version of eclipse or Java 1.6. Looks like for some reason the compiler doesn’t recognise that Rule.class is of type Class<? extends Rule<S, T>>, so as to call the public <S, T> T transform(Class<? extends Rule<S, T>> ruleType, S source)

A simple solution is to ct the Rule.class expression to Class (it sounds weird but it worked).

So the transform and transformAll methods become:

public Object transform(Object object) {
Class r = Rule.class;
return transform(r, object);
}
public List<? extends Object> transformAll(List<? extends Object> sourceObjects){
Class r = Rule.class;
return transformAll(r, sourceObjects);
}

Making UML2Alloy compatible with Alloy v4.0

Posted on by | Leave a reply

Alloy Analyzer v4.0 has been out for quite a while. Alloy v4.0 is an extension of the Alloy v 3.0 language (http://alloy.mit.edu/alloy4/quickguide/a4.html). More specifically parts of the concrete syntax of the language has changed (i.e. when invoking a predicate from within another predicate we now have to use brackets “pred1 [param1,param2,..]” instead of parentheses “pred 1(param1, param2,..)“. Also some of the properties of the language have changed (in MDA terms constraints on the metamodel, or well-formedness rules have changed). For example in Alloy 4 you are able to overload predicates, functions and fields. These are relatively small changes and it should be easy to accommodate them in UML2Alloy.

However, Alloy v4.0 has been developed from scratch and it is based on the kodkod model finder. The AST implementation has changed substantially and the convenience methods provided on the AST model elements are fine tuned for the Alloy compiler. For example Signature constructors are private and I couldn’t find a way to update the properties of Signatures (i.e. the Multiplicity of the Signature) after a Signature has been created.

Of course this is perfect if you have an Alloy model and you just want to parse, but not very convenient if you use an MDA approach to instantiate Alloy AST objects. For example in UML2Alloy you can change the Multiplicity of a Signature (i.e. change from set to some to enforce that some Signature instances will exist in the model). If you don’t have access to the Multiplicity attribute of the Signature class, after the object has been created, complicates the situation.

Moreover the AST class elements have been defined as final so there is no way you can override the Alloy v4.0 AST classes.

So, I spent almost 1 day evaluating the situation and trying to find a solution. One solution would be to create my own implementation of Alloy’s AST. Another would be to create wrapper classes of Alloy’s AST that will have pointers to the actual Alloy implementation.

Then I stepped back and thought about the siltation. Well, I already have a rather stable implementation that uses Alloy v3.0 AST. In Alloy v4.0 the AST has NOT changed. Just the concrete syntax. So the solution is easy.

Currently in UML2Alloy after the Alloy AST objects have been generated by SiTra, a visitor is used to create a text file that contains the Alloy model. So, all I have to do is use another visitor and override the methods that create the part of the model for which the concrete syntax has changed.

Using Alloy Analyzer to solve the first Google Davinci Code Quest puzzle!

Posted on by | 3 Replies

As I was searching for something on google, I saw an ad at the bottom of the page. The ad was about the Davinci code new movie that is coming out. I clicked and found a sudoku like puzzle, related to the movie. The puzzle is explained in the following two pictures (description can also be found on: http://student-rant.blogspot.com/2006/04/googles-da-vinci-code-quest-1.html)

Well… it is clearly a very simple problem for a constraint solver, like Alloy Analyzer! I created the following model (took me half an hour, so no comments or too much thought about it).

module testopen util/ordering[Natural] as ord

abstract sig Natural{}

one sig One extends Natural{}
one sig Two extends Natural{}
one sig Three extends Natural{}
one sig Four extends Natural{}

abstract sig Symbol{}

one sig Cross extends Symbol{}{}
one sig Fi extends Symbol{}{}
one sig Blade extends Symbol{}{}
one sig Star extends Symbol{}{}

sig Cell{
symbol: one Symbol,
rowIndex: Natural,
columnIndex: Natural,
inRange: Natural
}

fact Numbers{
ord/first() = One
ord/next(One) = Two
ord/next(Two) = Three
ord/last() = Four

}

pred defineRange(row:Natural,column:Natural,r:Natural){
all c:Cell |
c.rowIndex = row && c.columnIndex = column => c.inRange = r
}

fact DefineRange{
defineRange(One,One,Two)
defineRange(One,Two,One)
defineRange(One,Three,One)
defineRange(One,Four,One)
defineRange(Two,One,Two)
defineRange(Two,Two,Two)
defineRange(Two,Three,Three)
defineRange(Two,Four,One)
defineRange(Three,One,Four)
defineRange(Three,Two,Two)
defineRange(Three,Three,Three)
defineRange(Three,Four,Three)
defineRange(Four,One,Four)
defineRange(Four,Two,Four)
defineRange(Four,Three,Four)
defineRange(Four,Four,Three)
}

pred staticSymbols(row:Natural, column:Natural, s:Symbol){
all c:Cell |
c.rowIndex = row && c.columnIndex = column =>
c.symbol = s
}

fact{
staticSymbols(One,Four,Fi) &&
staticSymbols(Two,Two,Cross) &&
staticSymbols(Four,Two,Blade) &&
staticSymbols(Four,Three,Star)
}

// No two same symbols in the same Range
fact{
all disj c,c’:Cell |
c.inRange = c’.inRange =>
c.symbol != c’.symbol
}

// All cells have different rowIndex and columnIndex
fact{
no disj c,c’:Cell | (c.rowIndex = c’.rowIndex && c.columnIndex = c’.columnIndex)
}

//No two same symbols in the same row Column
fact{
all disj c,c’:Cell |
c.rowIndex = c’.rowIndex =>
c.symbol != c’.symbol

all disj c,c’:Cell |
c.columnIndex = c’.columnIndex =>
c.symbol != c’.symbol
}

pred solution(){
#Cell = 16
}

run solution for 16 Cell

Alloy Analyzer came up with a solution in 3 seconds, on the dual core 2GB RAM opteron server running linux!

The solution is the following one:

symbol= { (Cell_0 Blade_0) (Cell_1 Blade_0) (Cell_2 Blade_0) (Cell_3 Blade_0) (Cell_4 Fi_0) (Cell_5 Fi_0) (Cell_6 Fi_0) (Cell_7 Fi_0) (Cell_8 Cross_0) (Cell_9 Cross_0) (Cell_10 Cross_0) (Cell_11 Cross_0) (Cell_12 Star_0) (Cell_13 Star_0) (Cell_14 Star_0) (Cell_15 Star_0) }

rowIndex = { (Cell_0 One_0) (Cell_1 Two_0) (Cell_2 Three_0) (Cell_3 Four_0) (Cell_4 One_0) (Cell_5 Two_0) (Cell_6 Three_0) (Cell_7 Four_0) (Cell_8 One_0) (Cell_9 Two_0) (Cell_10 Three_0) (Cell_11 Four_0) (Cell_12 One_0) (Cell_13 Two_0) (Cell_14 Three_0) (Cell_15 Four_0) }

columnIndex = { (Cell_0 One_0) (Cell_1 Four_0) (Cell_2 Three_0) (Cell_3 Two_0) (Cell_4 Four_0) (Cell_5 Three_0) (Cell_6 Two_0) (Cell_7 One_0) (Cell_8 Three_0) (Cell_9 Two_0) (Cell_10 One_0) (Cell_11 Four_0) (Cell_12 Two_0) (Cell_13 One_0) (Cell_14 Four_0) (Cell_15 Three_0) }

It is quite straightforward! The symbol of Cell_0 is Blade, its row is One and column One. The symbol of Cell_1 is Blade again, he row is Two and Column Four etc.

The symbol names are not related to the movie or book symbol names. In my model Blade is the pyramid like shape, Fi is the Greek letter fi, Cross is the symbol that looks like a cross and Star is the symbol that looks like a star. I know that I spent half an hour to solve a problem that would have taken me around 10 minutes to solve manually, but as a proper nerd I prefer to use my (few) grey cells to think how to use a computer to solve a problem for me, instead of solving the problem myself.

Well.. that’s it! I don’t want to spend more than 1 hour on this!

There are a couple of blogs with solutions to the puzzles.
Links to solutions:
http://student-rant.blogspot.com/2006/04/warning-solution-to-google-da-vinci.html
http://googlefact.blogspot.com/

UPDATE: I used the model on my P4 running @ 2.8G with 712 MB ram and took AA 23 seconds to solve the problem. Not bad at all! But for bigger problems the state space will be increased by too much. Looks like an AI technique should be used to find a solution.