Building the Collatz Graph in Henshin

The other day I saw an online video about a number-theoretical problem called the Collatz conjecture. The video included some visualizations of the problem which were based on force-directed graph drawing. It was immediately clear to me that such visualizations could be also easily done in Henshin. So I built a minimalistic EMF model and sketched two simple rules:

The first one multiplies x by 2, the second one is the inverse of the 3x+1 rule. Technically, it is not exactly the inverse of the Collatz function, but the conjecture is still true if and only if these two rules can generate every natural number (if we ignore the upper bound in the first rule).

Finally I created an instance model for the initial state and set up a state space. In the following video you can see how to use Henshin's state space explorer to generate the Collatz graph. Have fun. 

Parallel State Space Exploration in Henshin

Back from the summer break, I read an interesting article on combining OCL expressions with CTL formulas. Apart from the modeling approach itself, it was interesting to me that the authors used Henshin to generate their state spaces and also compared their modeling and the performance of Henshin's state space generator with GROOVE.

While the GROOVE tool does not really provide an API for its simulator and state space generator, it is fairly easy to do this programmatically in Henshin:

// Set-up:
StateSpace stateSpace = new StateSpaceImpl();
stateSpace.getRules().addAll(rules);
StateSpaceManager manager = 
   new ParallelStateSpaceManager(stateSpace, 4);
manager.createInitialState(new ModelImpl(resource));

// Exploration:
StateSpaceExplorationHelper helper = 
   new StateSpaceExplorationHelper(manager);
helper.doExploration(-1, monitor);

That's it. After you have generated the state space, you can either save it or use a validator to check invariants or to do model checking etc.

The authors of the OCL-meets-CTL paper mention that there is room for improving the performance of Henshin's state space generator, which I fully agree to. Nevertheless, I want to show here that we have put a lot of effort to make Henshin's state space generator as fast as possible. A key difference to GROOVE is that state space generation in Henshin can be parallelized. Let me show you some numbers.

The chart shows the time needed to generate the state space of the dining philosophers example for 10 philosophers. What you can see is that by using multi-threaded state space generation, we obtain a speed-up of factor 3. In absolute numbers, the generator explores around 2000 states per second. That is just half a millisecond to find all rule matches for a state graph, make a copy and transform it for every match, and look up states and update the state space. If you compare it with the performance of the Henshin interpreter itself (see e.g. here), these numbers are top notch. Note also that the speed can be greatly improved simply by increasing the cache sizes of the state space generator (which requires more main memory though).

That being said, there is still of course room for improvement. For example, the scale-up for a high number of processors and threads is not as good as we have hoped. The required locking of the state space seems to be the main bottleneck. The performance can be probably tweaked but it will of course never be as fast as model checkers that work on vector-based data (as opposed to graphs).

Henshin 0.9.10 on its way. We are working on the new version of Henshin which we hope to release in November 2013. It will target and require Eclipse Kepler. The most exciting new feature will be a new execution platform for Henshin transformations. More on this later.