This is a model checker and visualizer for the c't race track puzzle
as published in the German computer journal c't 20015 issue 25, e.g.,

  http://ct.de/ypvd

You can compile the model checker by 

  ./configure.sh && make

For more compilation options run:

  ./configure.sh -h

In particular, there are some experimental configurations,
which for instance only allow forward model checking, for which
further static memory instead of heap memory can be used.  It
might also be necessary to adapt the number of bits for
coordinates and velocity.

By default the model checker will use the internal encoded
parcours (problem), as original given in the puzzle.  See
'./mcracetrack -h' for further options.  The source code comes
with a 'regression.sh' script and further test parcours in
the 'parcours' subdirectory.

Currently only Linux Ubuntu 14.04 is tested.  If you have 'opengl'
installed (see also './configure.sh -h') you can first compile in
the OpenGL search visualization with './configure.sh -v && make'.
The actual visualization of what the model checker is doing is
shown using the command line option '-v'.

Fri Dec  4 19:56:30 CET 2015
Armin Biere