Dienstag, 22. September 2009

Subethaedit Promela Mode

I have revised and fixed the Promela mode from the Subethaedit website (written by Ingmar J. Stein) a while back. Somehow my submission to the website probably got lost and i didn't follow up on it. Anyway, i revised it once again and you can download it directly from here. In a nutshell, this is what happened to the mode since i started changing the mode from the website:
  • Updated keywords.
  • Fixed a bug the prevent the keywords from being colored correctly.
  • Integrated Applescripts for syntax check and startup of a modified Xspin version.
  • Code folding.
The bundled Xspin version is a modified version of the latest Xspin 5.2 version. In a nutshell, the xspin version disables any kind of file operation (since you should do that with Subethaedit) and reloads the promela file on any operation. That way, you can use Xspin as a frontend for Spin without fear to break anything and Subethaedit for editing.

Preliminaries:
  • The promela binary must be placed in /usr/local/bin, i.e., /usr/local/bin/spin. Otherwise, it won't work. See an earlier blog post with a few comments how to compile Spin on MacOS.
  • For Xspin to work, you need Tcl/TK. The versions i use are Tl 8.4.19 and Tk 8.4.19. I can't say whether it will work for different versions. I know i had trouble with more recent versions once.
The whole thing hasn't been tested extensively, but it works for me and at least for me it works better than the mode on the Subethaedit website. Enjoy!

Freitag, 18. September 2009

Integer Programming for Finding Good Groups in Teaching

So, in a few weeks we are offering the Extreme Programming Lab again. This time we have 20 participants. Last year, we had a few (though not huge) problems, because the groups weren't assigned very evenly. We typically work with two groups who each realize a project in XP style. I got to admit, this uneven assignment was my fault. Back then, I assigned the persons randomly and shifted them them a little according to what i thought i knew about their capabilities.

This year, i decided to go a different route. For the lab application, i specifically asked for specific capabilities and what the participants thought how good they were at them. According to their statements, i classified each statement to points between 0 and 2. With 0 meaning "little knowledge", 1 meaning "normal knowledge" and 2 meaning "good knowledge". I collected a total of 10 different capabilities. So the question now is, how do i find good groups. My optimal groups would be where every capability is covered by the same degree of points. Moving the participants around in Excel to find a good solution is obviously pretty tedious. After all there are quite a lot of different combinations for those two groups.

A few years back, i heard a lecture about traffic planning and learnt about integer programming. After some thinking, i came to the conclusion that this is pretty much the same stuff and that integer programming would be the right tool to solve this problem. Therefore, i downloaded the student version of Xpress-IVT as i remembered that i liked Mosel a lot back then. I wasn't wrong. A few hours later (geeeze, you can't write your phd thesis all the time!), i had a working Mosel integer program that in fact solved my little problem for finding optimal groups with evenly distributed knowledge. Maybe someone enjoys this as much as i did. So here it is (Names have been anonymized of course):


model "Participants Assignment to Groups"
uses "mmxprs","mmquad","mmive";

declarations
PERSONS = 1..20
GROUPS = 1..2
SKILL_DIMENSIONS = 1..10
SKILLS: ARRAY(SKILL_DIMENSIONS,PERSONS) of integer
SKILL_SUMS: ARRAY(SKILL_DIMENSIONS) of integer
PERSON_NAMES: ARRAY(PERSONS) of string
SKILL_NAMES: ARRAY(SKILL_DIMENSIONS) of string
allowed_deviation = 1

assign: ARRAY(PERSONS,GROUPS) of mpvar
end-declarations

initializations from "initdata.dat"
SKILL_NAMES
PERSON_NAMES
SKILLS
end-initializations

groupCount := getsize(GROUPS);
personCount := getsize(PERSONS);

writeln("Number of groups: ", groupCount);
writeln;

forall(d in SKILL_DIMENSIONS) do
SKILL_SUMS(d) := 0;
forall(p in PERSONS) do
SKILL_SUMS(d) += SKILLS(d,p);
end-do
end-do

forall(d in SKILL_DIMENSIONS) do
writeln("Skill sum for ", SKILL_NAMES(d),": ",SKILL_SUMS(d), " - average per group: ", SKILL_SUMS(d)/groupCount)
end-do

GoodGroups := sum(d in SKILL_DIMENSIONS, p in PERSONS, g in GROUPS) SKILLS(d,p)*assign(p,g)

forall(p in PERSONS) sum(g in GROUPS) assign(p,g) = 1 ! every person is in one group only

forall(g in GROUPS) sum(p in PERSONS) assign(p,g) = personCount / groupCount !groupCount ! every group has a maximum of groupCount persons

forall(d in SKILL_DIMENSIONS) forall(g in GROUPS) sum(p in PERSONS) SKILLS(d,p)*assign(p,g) >= SKILL_SUMS(d)/groupCount - allowed_deviation

forall(d in SKILL_DIMENSIONS) forall(g in GROUPS) sum(p in PERSONS) SKILLS(d,p)*assign(p,g) <= SKILL_SUMS(d)/g


The data file looks something like this:


PERSON_NAMES: ["Person 1",
...
"Person 20"]

SKILL_NAMES: ["Eclipse",
"DB/SQL",
"SVN",
"UML",
"Design Patterns",
"Refactoring",
"Testing",
"GUI",
"Web",
"Java"]

SKILLS: [1,0,0,1,2,2,2,2,2,2,2,0,0,0,0,0,2,2,2,2,
2,2,2,0,1,2,2,2,2,2,2,2,2,2,2,1,1,2,2,2,
...
0,1,2,1,1,2,2,2,1,1,2,1,1,1,1,1,1,1,1,2]


I hope there is nothing wrong with this little Mosel program. I have to say that i really enjoy optimization every time there is reason to use it. You don't understand what i'm doing here? Just learn a little about linear optimization and integer programming. This is great fun!

Freitag, 11. September 2009

ANTLR 3 Java Promela Parser

I just made a first version of my Java Promela parser (the input language of the Spin model checker) available. Grab it while its hot ;-) Hopefully, it will be integrated into the Spin Eclipse Plugin for on-the-fly syntax checking.

Next step would be to transfer this stuff to Xtext and design a proper Promela metamodel and somehow implement a pretty printer for Promela which is needed badly. I'm not sure when i have time to do that though. Does anyone have clever ideas how to pretty print a C preprocessed language? You would have to preprocess the Promela files, pretty print them and then reverse the preprocessing somehow. This sounds kind of tricky to me...

Donnerstag, 10. September 2009

O2 UMTS Prepaid Surfstick (ICON 210) und Snow Leopard - Beim Kauf schon veraltet!

Am 31.8. bin ich in den O2 Laden gelaufen, um mir ein Backup-Internet für meine Geschäftsreisen zu besorgen. 60 EUR später festgestellt, das dieser mit Snow Leopard, am 28.8. veröffentlicht inkompatibel ist. Nagut, nicht so schlimm - ich habe ja noch einen Ersatzstick von Novatel MC950D, der nach einem Treiberupdate von einer versteckten MacOS Website von Novatel auch einwandfrei seinen Dienst verrichtete.

Heute habe ich dann mal bei O2 angerufen und nachgefragt, was denn mit einem Treiberupdate für den ICON 210 UMTS Stick sei. Sie hätten ja jetzt genügend Zeit gehabt einen neuen Treiber zu beschaffen. Antwort: für den ICON 210 wird es leider kein Update mehr geben. Es wird bald einen neuen Stick geben. Den kriege ich natürlich dann nicht für Lau. Ich habe den netten Herren darauf hingewiesen, dass Snow Leopard schon raus war als ich mir das Prepaid Angebot geholt habe und nicht darauf hingewiesen wurde, dass der Stick mit aktuellen Betriebssystemen nicht funktionieren wird.

Nunja, das gibt eine schriftliche Beschwerde. Ich weiss echt nicht was das Problem mit den UMTS Sticks und dem Support dafür ist - man hat damit fast immer nur Ärger. Da lobe ich mir ja fast meine versteckte Novatel Treiberseite (die man allerdings auch erst nach stundenlanger Netzrecherche findet). Und O2? Was für ein Saftladen! Servicewüste Deutschland halt - in anderen Ländern hätten die sich jetzt den Kopf darüber zerbrochen wie sie mir helfen können. Darauf wartet man hier lange...

Mittwoch, 9. September 2009

Compiling Spin on the Mac

This is primarily a reminder for myself :-) Edit the makefile, add to the CFLAGS "-DMAC". Then, edit main.c. Find the line:

#define CPP "/lib/cpp" /* classic Unix systems */

change it to

#define CPP "/usr/bin/cpp" /* classic Unix systems */

This is supposed to work via -DCPP=/usr/bin/cpp, but somehow it doesn't.