Commit 01237811 authored by Elwin Pater's avatar Elwin Pater
Browse files

Divine 2.2 import

parents
DiVinE (2003-2009), by members of the ParaDiSe Laboratory:
Jiri Barnat
Petr Bauch
Lubos Brim
Jakub Chaloupka
Tomas Janousek
Jitka Kudrnacova
Pavel Moravec
Martin Moracek
Petr Rockai
Pavel Simecek
Portions of the code have been written by:
Michael Weber
HOARD (1998-2007) by Emery Berger <emery@cs.umass.edu>.
LPSOLVE by Michel Berkelaar, Kjell Eikland, Peter Notebaert.
dlfcn-win32 by Ramiro Polla
See COPYING for authoritative copyright and licence information.
cmake_minimum_required(VERSION 2.4.7)
project( divine )
if(COMMAND cmake_policy)
cmake_policy(SET CMP0002 OLD) # FIXME
cmake_policy(SET CMP0003 NEW)
endif(COMMAND cmake_policy)
if( NOT CMAKE_BUILD_TYPE )
set( CMAKE_BUILD_TYPE "Release" )
endif( NOT CMAKE_BUILD_TYPE )
macro(appendFlag flags value)
foreach( F ${flags} )
set( CMAKE_${F}_FLAGS_${CMAKE_BUILD_TYPE}
"${CMAKE_${F}_FLAGS_${CMAKE_BUILD_TYPE}} ${value}" )
endforeach( F )
endmacro(appendFlag)
option( PROFILE "generate profiling information for lcov coverage" OFF )
option( HOARD "use HOARD SMP memory allocator" ON )
option( POOLS "use pool allocation for graph vertices" ON )
option( USE64 "pass -m64 to gcc to force 64b on multiarch" OFF )
option( USE32 "pass -m32 to gcc to force 32b on multiarch" OFF )
option( MPI "compile DiVinE with MPI for clustering support" ON )
option( GUI "compile the Qt GUI" ON )
if( NOT WIN32 )
add_definitions( -DPOSIX )
endif( NOT WIN32 )
if( PROFILE )
appendFlag( "CXX;C" "-fprofile-arcs -ftest-coverage" )
link_libraries( "gcov" )
endif( PROFILE )
if( USE64 )
appendFlag( "CXX;C;EXE_LINKER;SHARED_LINKER" "-m64" )
endif( USE64 )
if( USE32 )
appendFlag( "CXX;C;EXE_LINKER;SHARED_LINKER" "-m32" )
endif( USE32 )
if( NOT POOLS )
add_definitions( "-DDISABLE_POOLS" )
endif( NOT POOLS )
if( GUI )
find_package( Qt4 4.5.0 )
endif( GUI )
# on some mingw32, regex.h is not on the default include path
find_path( RX_PATH regex.h )
include_directories( ${RX_PATH} )
link_directories( ${RX_PATH} )
if( MPI AND NOT WIN32 )
include( FindMPI )
endif( MPI AND NOT WIN32 )
if( MPI AND MPI_FOUND )
add_definitions( "-DHAVE_MPI" )
else( MPI AND MPI_FOUND )
set( MPI_INCLUDE_PATH "" )
set( MPI_LIBRARIES "" )
set( MPI_LIBRARY "" )
if( MPI )
message( "-- WARNING: Could not find MPI. Disabling cluster support." )
endif( MPI )
set( MPI OFF )
set( MPIEXEC "" )
endif( MPI AND MPI_FOUND )
set( DIVINE_INCLUDES
${divine_SOURCE_DIR}
${divine_BINARY_DIR}
${MPI_INCLUDE_PATH}
${divine_SOURCE_DIR}/divine/legacy )
include( CheckCXXSourceCompiles )
check_cxx_source_compiles(
"template< typename T > struct A {
static const int x = sizeof( T );
};
struct B {
A< B > a;
};
int main() { return 0; }" TMPL_SIZEOF_WORKS )
if( NOT TMPL_SIZEOF_WORKS )
message( FATAL_ERROR "Your C++ compiler apparently does not support language features required by DiVinE. It is recommended that you compile with G++ 4.1 or 4.2." )
endif( NOT TMPL_SIZEOF_WORKS )
find_program( SHA1SUM sha1sum )
if( NOT SHA1SUM )
message( "I could use a working sha1sum program for the build. Please install one or supply me with a path if you already have it. Thank you." )
endif( NOT SHA1SUM )
add_custom_target( check )
add_custom_target( unit )
add_custom_target( lcovd-unit )
if( PROFILE )
find_program( LCOV lcov )
find_program( LCOV_GENHTML genhtml )
if( NOT LCOV )
message( "-- WARNING: Could not find LCOV, disabling coverage report generation." )
endif( NOT LCOV )
endif( PROFILE )
if( LCOV )
set( LCOV_RDIR "${divine_BINARY_DIR}/lcov-report" )
add_custom_target( lcov-clean
COMMAND mkdir -p ${LCOV_RDIR}
COMMAND ${LCOV} -d ${divine_SOURCE_DIR} -z
COMMAND ${LCOV} -c -i -d ${divine_SOURCE_DIR} -o ${LCOV_RDIR}/base.info
)
macro( lcov_collect id )
add_custom_target( lcov-collect-${id}
COMMAND mkdir -p ${LCOV_RDIR}
COMMAND ${LCOV} --quiet -b ${divine_SOURCE_DIR} -d ${divine_SOURCE_DIR} -c
-o ${LCOV_RDIR}/collect-${id}.info || true
COMMAND ${LCOV} -d ${divine_SOURCE_DIR} --zerocounters || true
)
endmacro( lcov_collect )
add_custom_target( lcov-report
COMMAND mkdir -p ${LCOV_RDIR}
COMMAND ${LCOV} --quiet -b ${divine_SOURCE_DIR} -d ${divine_SOURCE_DIR}
-a ${LCOV_RDIR}/base.info
-a ${LCOV_RDIR}/collect-1.info
-a ${LCOV_RDIR}/collect-2.info
-o ${LCOV_RDIR}/overall.info
COMMAND ${LCOV_GENHTML} -o lcov-report -p `pwd` -p ${divine_SOURCE_DIR}
${LCOV_RDIR}/overall.info
)
add_dependencies( check lcov-clean )
endif( LCOV )
add_subdirectory( wibble )
if( HOARD )
add_subdirectory( hoard )
endif( HOARD )
add_subdirectory( lpsolve )
add_subdirectory( divine )
add_subdirectory( tools )
add_subdirectory( examples )
if( GUI )
if( QT4_FOUND AND QT_VERSION_MINOR GREATER 4 )
add_subdirectory( gui )
else()
message( "-- WARNING: Could not find Qt4 >= 4.5. Disabling GUI." )
endif()
endif( GUI )
add_dependencies( lcovd-unit unit )
if( LCOV )
lcov_collect( "1" )
add_dependencies( lcovd-unit lcov-collect-1 )
add_dependencies( lcov-collect-1 unit )
endif( LCOV )
add_dependencies( check lcovd-unit )
add_dependencies( check functional )
add_subdirectory( test )
# FIXME: better dependency detection
if( WIN32 )
find_file( REGEX_LIB libgnurx-0.dll )
find_file( GCC_SJL_LIB libgcc_s_sjlj-1.dll )
install(FILES ${REGEX_LIB} DESTINATION ./ COMPONENT sys)
install(FILES ${GCC_SJL_LIB} DESTINATION ./ COMPONENT qt)
endif( WIN32 )
install(FILES README RENAME README.txt DESTINATION ./ COMPONENT sys)
install(FILES COPYING RENAME COPYING.txt DESTINATION ./ COMPONENT sys)
install(FILES AUTHORS RENAME AUTHORS.txt DESTINATION ./ COMPONENT sys)
install(FILES WHATS_NEW RENAME WHATS_NEW.txt DESTINATION ./ COMPONENT sys)
set( CPACK_PACKAGE_DESCRIPTION_SUMMARY "DiViNE Distributed and Parallel Verification Environment" )
set( CPACK_PACKAGE_VENDOR "ParaDiSe Laboratory" )
set( CPACK_PACKAGE_DESCRIPTION_FILE "${CMAKE_CURRENT_SOURCE_DIR}/README" )
set( CPACK_RESOURCE_FILE_LICENSE "${CMAKE_CURRENT_SOURCE_DIR}/COPYING" )
set( CPACK_PACKAGE_VERSION_MAJOR "2" )
set( CPACK_PACKAGE_VERSION_MINOR "1" )
set( CPACK_PACKAGE_VERSION_PATCH "0" )
set( CPACK_PACKAGE_INSTALL_DIRECTORY "divine-2.1" )
set( CPACK_COMPONENTS_ALL console_tools gui_tools divine_dev wibble_dev qt sys examples help)
if(WIN32)
set(CPACK_NSIS_MENU_LINKS "./divine.ide.exe" "DiViNE IDE"
"./README.txt" "README"
"./COPYING.txt" "COPYING"
"./AUTHORS.txt" "AUTHORS"
"./WHATS_NEW.txt" "WHATS_NEW")
set(CPACK_PACKAGE_EXECUTABLES "" "")
set(CPACK_NSIS_MODIFY_PATH ON)
endif(WIN32)
include( CPack )
if(CMAKE_MINOR_VERSION EQUAL 6 AND CMAKE_PATCH_VERSION GREATER 0)
set(HAVE_CMAKE_261 1)
endif()
if(CMAKE_MAJOR_VERSION GREATER 2 OR CMAKE_MINOR_VERSION GREATER 6 OR HAVE_CMAKE_261)
cpack_add_component_group( tools DISPLAY_NAME "Tools"
DESCRIPTION "Installs the basic tools"
EXPANDED )
cpack_add_component_group( devel DISPLAY_NAME "Development"
DESCRIPTION "Installs header and library files"
EXPANDED )
cpack_add_component( console_tools DISPLAY_NAME "Console Tools"
DESCRIPTION "Console tools"
GROUP tools )
cpack_add_component( gui_tools DISPLAY_NAME "IDE"
DESCRIPTION "Graphical environment"
GROUP tools )
cpack_add_component( wibble_dev DISPLAY_NAME "Wibble"
DESCRIPTION "Wibble library"
GROUP devel )
cpack_add_component( divine_dev DISPLAY_NAME "Divine"
DESCRIPTION "Divine development files"
DEPENDS wibble_dev
GROUP devel )
cpack_add_component( help HIDDEN DEPENDS gui_tools )
cpack_add_component( qt HIDDEN DEPENDS gui_tools )
cpack_add_component( sys HIDDEN )
cpack_add_component( examples DISPLAY_NAME "Examples"
DESCRIPTION "Sample models" )
endif()
This diff is collapsed.
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.
all check divine-mc clean lcov-report install:
$(MAKE) -C _build $(@)
distclean:
rm -rf _build
DiVinE 2.0
==========
Introduction
------------
DiVinE 2.0 exploits full power of modern x86 hardware and reduces unnecessary
delays in workflow. Employing state-of-the-art parallel liveness checking
algorithm, DiVinE 2.0 offers unmatched scalability on both shared memory and
distributed memory platforms in the range of 2- to 16-core machines and
clusters thereof. Moreover, the tool supports 64-bit platforms out of the box,
allowing it to leverage all the memory available in contemporary systems (and
systems of the upcoming years).
In the current DiVinE release, input is provided in DVE format -- an
industry-strength specification language, as used in original DiVinE Cluster
0.7 and DiVinE Multi-Core 1.x, with plenty of diverse example models, ranging
from simple toys to complex real-world models. There is an extensive model
resource available, [The Beem Database] [1], with large amount of downloadable
models and properties.
[1]: http://anna.fi.muni.cz/models.
Build Instructions
------------------
This package requires pthreads and a recent g++ (4.1 or later, tested under
4.3.4). You will also need cmake (www.cmake.org, tested with 2.6 -- however,
the configure script could download and compile it for you, just run configure
and answer the question(s)).
After unpacking the tarball, compile the source (the build system
should give you fairly clear indication what's wrong in case of
failure).
$ ./configure
$ make
Assuming, that build finishes successfully, you can try to run the binary:
$ ./_build/tools/divine help
$ ./_build/tools/divine reachability examples/shuffle.dve
$ ./_build/tools/divine owcty examples/peterson-liveness.dve
$ ./_build/tools/divine owcty examples/peterson-naive.dve
There is no need to install the binaries, as they are mostly
self-contained. However, to make the tool more readily available, you can
install using:
# make install
Further usage instructions
--------------------------
Reference of commandline options is available with `divine help`, as detailed
above. The most useful invocations are these:
* run reachability on 8 cores:
`./_build/tools/divine reachability -w 8 input.dve`
* run model checking on 4 cores:
`./_build/tools/divine owcty -w 4 input-with-property.dve`
There are several example inputs, mostly coming from [The BEEM Database] [1],
distributed with the tool under the `examples/` directory. These are the files
prefixed `beem-`. Many more models are available for download in the BEEM
repository.
[1]: http://anna.fi.muni.cz/models
Graphical User Interface
------------------------
If Qt4 development files are available on your machine, a graphical user
interface for the DiVinE Tool will be compiled as part of the build process.
You can run the interface with:
$ PATH=./_build/tools:$PATH ./_build/gui/divine.ide
Please see online help for further information about using the interface. If
you have chosen to install the tool, you should put it on your PATH, and then
issue `divine.ide`.
Known Issues
------------
Scalability on 64-bit platforms is inferior to scalability on 32-bit
platforms. If you are running on x86_64 or other similar architecture
which can run 32-bit binaries natively, you can compile DiVinE in
32-bit mode:
$ CXXFLAGS=-m32 ./configure
$ make
If you have previously run configure, you may need to delete or move
the _build directory out of way. However, using 32-bit mode limits the
size of verifiable models to roughly 3GB.
Reporting Problems
------------------
The DiVinE project uses Trac for managing problem reports. If you encounter a
behaviour you believe is a bug in DiVinE, please [file a new ticket] [1] in
[DiVinE Trac] [2]. However, before reporting issues, please consider checking
if there is a more recent version available and if the issue has been reported
already (in the latter case, please add a comment to the existing ticket, that
you have encountered the issue, and if possible, any further details you may
know about the problem). Thanks in advance.
[1]: http://divine.fi.muni.cz/trac/newticket?version=2.0
[2]: http://divine.fi.muni.cz/trac/
Obtaining New Versions
----------------------
The latest release is always available through [project pages] [1], section
Download. You could also obtain the latest development snapshot through darcs
(you need version 2.0 or later), which is used for version control:
$ darcs get http://divine.fi.muni.cz/darcs/mainline divine
When you already have a darcs repository of the project, you can get
the latest changes by issuing:
$ darcs pull
in the repository directory. For further details on using darcs, please consult
the file "HACKING" in the source tree and [darcs homepage] [2].
[1]: http://divine.fi.muni.cz/
[2]: http://www.darcs.net/
Licence
-------
The source code comes with NO WARRANTY, as detailed in the licence texts, which
may be found in the file "COPYING" in the distribution tarball. The tool is a
product of The ParaDiSe Laboratory, Faculty of Informatics of Masaryk
University.
This distribution includes freely redistributable third-party
code. Please refer to AUTHORS and COPYING included in the distribution
for copyright and licensing details.
<h1>DiVinE 2.0</h1>
<h2>Introduction</h2>
<p>DiVinE 2.0 exploits full power of modern x86 hardware and reduces unnecessary
delays in workflow. Employing state-of-the-art parallel liveness checking
algorithm, DiVinE 2.0 offers unmatched scalability on both shared memory and
distributed memory platforms in the range of 2- to 16-core machines and
clusters thereof. Moreover, the tool supports 64-bit platforms out of the box,
allowing it to leverage all the memory available in contemporary systems (and
systems of the upcoming years).</p>
<p>In the current DiVinE release, input is provided in DVE format -- an
industry-strength specification language, as used in original DiVinE Cluster
0.7 and DiVinE Multi-Core 1.x, with plenty of diverse example models, ranging
from simple toys to complex real-world models. There is an extensive model
resource available, <a href="http://divine.fi.muni.cz/">The Beem Database</a>, with large amount of downloadable
models and properties.</p>
<h2>Build Instructions</h2>
<p>This package requires pthreads and a recent g++ (4.1 or later, tested under
4.3.4). You will also need cmake (www.cmake.org, tested with 2.6 -- however,
the configure script could download and compile it for you, just run configure
and answer the question(s)).</p>
<p>After unpacking the tarball, compile the source (the build system
should give you fairly clear indication what's wrong in case of
failure).</p>
<pre><code>$ ./configure
$ make
</code></pre>
<p>Assuming, that build finishes successfully, you can try to run the binary:</p>
<pre><code>$ ./_build/tools/divine help
$ ./_build/tools/divine reachability examples/shuffle.dve
$ ./_build/tools/divine owcty examples/peterson-liveness.dve
$ ./_build/tools/divine owcty examples/peterson-naive.dve
</code></pre>
<p>There is no need to install the binaries, as they are mostly
self-contained. However, to make the tool more readily available, you can
install using:</p>
<pre><code># make install
</code></pre>
<h2>Further usage instructions</h2>
<p>Reference of commandline options is available with <code>divine help</code>, as detailed
above. The most useful invocations are these:</p>
<ul>
<li>run reachability on 8 cores:
<code>./_build/tools/divine reachability -w 8 input.dve</code></li>
<li>run model checking on 4 cores:
<code>./_build/tools/divine owcty -w 4 input-with-property.dve</code></li>
</ul>
<p>There are several example inputs, mostly coming from <a href="http://divine.fi.muni.cz/">The BEEM Database</a>,
distributed with the tool under the <code>examples/</code> directory. These are the files
prefixed <code>beem-</code>. Many more models are available for download in the BEEM
repository.</p>
<h2>Graphical User Interface</h2>
<p>If Qt4 development files are available on your machine, a graphical user
interface for the DiVinE Tool will be compiled as part of the build process.
You can run the interface with:</p>
<pre><code>$ PATH=./_build/tools:$PATH ./_build/gui/divine.ide
</code></pre>
<p>Please see online help for further information about using the interface. If
you have chosen to install the tool, you should put it on your PATH, and then
issue <code>divine.ide</code>.</p>
<h2>Known Issues</h2>
<p>Scalability on 64-bit platforms is inferior to scalability on 32-bit
platforms. If you are running on x86_64 or other similar architecture
which can run 32-bit binaries natively, you can compile DiVinE in
32-bit mode:</p>
<pre><code>$ CXXFLAGS=-m32 ./configure
$ make
</code></pre>