DiPro – Directed Probabilistic Counterexample Generation Tool Released

After many months of implementation and testing we finally released the DiPro tool for probabilistic counterexample generation tool.
I will give a talk on DiPro’s features on the SPIN 2011 Workshop (July 14-15), co-located with CAV 2011 in Snowbird Utah.

What is DiPro?

Current stochastic model checkers do not make counterexamples for property violations readily available. DiPro is a tool, that applies directed explicit state space search to discrete- and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties.

Directed explicit state space search algorithms explore the state space on-the-fly which makes DiPro very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method.

Counterexamples provided by DiPro have two important properties. First, they include those traces which contribute the most amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes.

DiPro allows for the computation of counterexamples for the stochastic model checkers PRISM or MRMC.

Download DiPro here.

Mac OSX Text Editor: TextWrangler

On my Windows computers I use Notepad++ for editing text files like html, css, php and other script files. Now, that I’m using a MacBook Pro as work computer, I searched for an equivalent text editor.

The features I need are:

  • Freeware
  • Syntax Highlighting
  • Comparing Files
  • Good Search / Replace capabilities

After I tested a few editors, I stuck with TextWrangler which also offers nice features like editing files on a SSH / FTP server.

Tool List

Yesterday I received my new quad core PC and I want to present a list of software tools that I don’t want to miss:

Google Browser Sync

Wer häufig an mehreren Rechnern arbeiten kennt das folgende Problem sicher: Man weiß das man einen Link in seinen Favoriten hat und braucht diesen genau jetzt, sitzt aber am falschen Rechner. Hier mit ist jetzt Schluss! Mit der Firefox Erweiterung Google Browser Sync kann man seine Favoriten auf allen Rechnern synchronisieren und als kleiner Bonus hat man auch immer noch ein Backup von diesen. Wenn man möchte, kann man mit dieser Erweiterung sogar ganze Firefox Sessions, die History und gespeicherte Passwörter synchronisieren. 

Papier ist böse!

  “Papier ist böse und gefährlich den es hat scharfe Kannten“ um Rodney an dieser Stelle mal zu zitieren.

Bei Coding 4 Fun habe ich nun ein interessantes Projekt gefunden, welches endlich im Kampf gegen das böse Papier helfen kann ;).
Mittels Scanner lassen sich Dokumente erfassen, welche man dann zusammen mit Meta-Daten speichern kann. Man kann (muss) zwar noch ein paar Sachen an dem Tool Verbessern um es zu einer richtigen Dokumenten Verwaltung zu machen aber auf jeden Fall ist der erste Schritt getan.

Vista Battery Saver

Mit der Installation von Windows Vista vor über 8 Monaten, wurde die “Lebensdauer” meines Notebooks Akkus in etwa halbiert.

das lag vor allem daran, dass ich auch im Akku betrieb, Aero aktiviert hatte, weil ich nicht immer wenn ich das Notebook vom Netz genommen habe umschalten wollte.

Eine Lösung für dieses Problem ist der Vista Battery Saver, der Aero automatisch beim Wechsel in den Akku Betrieb ausschaltet und beim einstecken des Netzkabels wieder anschaltet.

Windows Live Writer 1.0 hat Probleme mit Umlauten

Bei meinem letzten Post ist mir aufgefallen, das der Windows Live Writer Version 1.0 Beta Deutsch, noch Probleme mit deutschen Umlauten hat.

Dies liegt daran, das der Live Writer die Umlaute nicht HTML-Escape Tags umbaut. Sprich ein ä bleibt auch im HTML Code ein ä und wird nicht zu ä. Deswegen wird der Post dann nach dem ersten ä, ö oder ü abgeschnitten.

Beheben lässt sich dies im Moment nur durch ein umschalten in die HTML-Ansicht und ein händisches ersetzen von ä durch ä, ö durch ö und ü durch ü.