HACKING

Introduction
============

This document is intended for people writing algorithms or working on
the framework itself. The source code is currently layed out like this:

* divine/ is sources and headers of the framework and algorithms
  * divine/legacy/ contains code from original DiVinE library, among
    others the DVE state space generator and utilities it requires
* tools/ is for binaries
  * tools/divine-mc.cpp is the main user-level entrypoint of the tool

It is advisable, that you first compile the tool on the user level
(see README) and find out how the divine-mc binary works.

Using Darcs
===========

Preferably, you should use darcs 2.x (see <http://www.darcs.net>) for version
control. After installing darcs, there is a single "main" branch, which you
should use as a base for your work. Get it by issuing:

    $ darcs get http://divine.fi.muni.cz/darcs/mainline divine

Now, you should have a directory called divine, which contains a copy of the
source code. You can modify a few files in there, and issue

    $ darcs whatsnew
    $ darcs record

You will notice, that unlike CVS, darcs will ask you which changes to record
(or commit, in the CVS vocabulary). Also, darcs will ask you for a short patch
name. You are encouraged to only record small changes at once, so that you can
describe the change in a single line. Of course, for bigger changes (or those
that need more explanation), you can still include a longer description after
the short one (darcs will ask). The description should be an English sentence,
starting with a capital letter and ending with a period. It should preferably
be no longer than 80 characters.

Now, after you provide this data, darcs will run the testsuite, to ensure you
didn't break anything. However, this is most often something you do not want to
happen, and should disable in your personal repo (you can always run the suite
with `make check`). Prevent darcs from running the tests with:

    $ echo "ALL no-test" > _darcs/prefs/default

Another important command is:

    $ darcs changes -s -i

This will let you browse the recent changes, with summary of changed files in
each. You can hit `v` in the interactive prompt to inspect the change in
detail.

When you record a change you don't like, you can use `darcs unrecord` to remove
the recorded patch. Note however, that the changes will be kept in the working
copy, so you can `darcs record` them again, or `darcs revert` them, if you
don't like them, after all.

If you have changes, that you would like to have included within the main
divine branch, it is probably best to send those changes by mail. They will be
reviewed and if suitable, added to the repository.

    $ darcs send

Alternatively, you can publish your darcs repository at a place the maintainer
can reach it (eg. public http service or otherwise). Then contact the
maintainer and ask them to merge your changes into mainline.

Over time, the mainline will accumulate some changes, and you will probably
want to stay in sync with those. It is advisable, that before merging from
mainline, you record all your unrecorded changes. Then, you may issue:

    $ darcs pull

Which will ask you which changes would you like to bring into your branch. Most
of the time, you should not see any conflicts, as darcs handles merging
automatically (unless there are real conflicts).

If you get spurious conflicts when pulling, it is advisable that you `darcs
get` a new copy of the mainline repository and use `darcs pull` to move your
local changes from your previous copy. This means that some patches have been
removed from the mainline, although this happens only very rarely.

Compiling from Darcs
====================

The configure script contained in the source tree is intended for distribution
tarballs only. When you are using development version, it is recommended that
you create a build directory and run cmake manually:

    $ mkdir _build
    $ cd _build
    $ cmake ..
    $ make

The binaries etc. are in the same places, as they would be when using
./configure (see README for details on usage).

Source Code Overview
====================

There is a number of toplevel source directories in the repository. The most
interesting ones are `divine`, `tools` and `gui`.

Moreover, there is a toplevel directory named `wibble`, which is a
general-purpose utility library for C++. DiVinE uses the Thread abstraction
provided in this library, as well as the commandline parser, and the unit
testing framework.

The directory `divine` contains the divine library: (1) a parallel programming
toolkit (`parallel.h`, `barrier.h`, `fifo.h`, `hashmap.h`, `blob.h`, `pool.h`,
`mpi.h`), parallel graph traversal utilities (`visitor.h`, `datastruct.h`), an
LTL to Büchi conversion algorithm (the `ltl2ba` directory), a DVE language
interpreter (the `divine/legacy/system` subdirectory) and the model-checking
algorithms (`metrics.h`, `reachability.h`, `ndfs.h`, `owcty.h`, `map.h`) and a
few other utility units. (The `.test.h` files contain unit tests for the
respective unit defined in the corresponding `.h` file.)

The directory `tools` contains the commandline interface of the tool --
`divine.cpp`, a ProMeLa/NIPS compiler (`compile-pml.pl`, `packjars.pl`), a
standalone probabilistic model checker (`probabilistic.cpp`) and a legacy DVE
simulator (`simulator.cpp`). It also contains the code for the `divine combine`
command, in `combine.h`.

Finally, the `gui` directory contains the sources of a graphical user interface
for the DiVinE tool, based on Qt 4.x.

Debugging
=========

When debugging DiVinE with gdb, no special precautions are usually needed. You
however probably want a build with debugging enabled and optimisations
disabled: pass -DCMAKE_BUILD_TYPE=Debug to obtain such a build. This also
enables assertion checking, which is definitely useful for debugging.

Moreover, when using valgrind to hunt down leaks and/or memory corruption, it
is often desirable do disable custom memory management: pass -DHOARD=OFF and
-DPOOLS=OFF (in addition to the above) at configure time to achieve this.