|
MinCoverPetri Developer Documentation
|
|
MinCoverPetri Developer Documentation
|
Welcome to the developer documentation of MinCoverPetri, a command-line application for the fast computation of the minimal coverability set of place/transition Petri nets.
This site provides the build and test information below as well as the reference documentation for the code through the tabs on top of the page.
MinCoverPetri uses the monotone pruning algorithm proposed in [Reynier].
MinCoverPetri is free software released under the terms of the GNU General Public License version 3 or later (GPLv3+).
The development of MinCoverPetri is done in its GitLab project, which provides the Git repository managing the source code and where issues can be reported.
This GitLab Project also provides a Docker registry where a fully preconfigured Docker image usable to build and test the application and generate its documentation is available (see the section Continuous integration for more details).
The development is done using GNU/Linux and the instructions given below apply for this operating system. The same instructions should apply with no or little modification for other operating systems of the UNIX family, including macOS.
Compilation under Windows has not been tested but should be possible as the project uses standard C++ and multi-platform tools. Nevertheless the process would probably require some adaptation. Refer to the documentation of CMake, the cross-platform build system used by the project, if you want to manage to compile under Windows. Note also that instructions for cross-compilation in GNU/Linux targeting Windows are given in the section Cross-compiled build targeting Windows.
The code of MinCoverPetri uses the following lightweight third party libraries:
The source code of both libraries is directly included in the code of MinCoverPetri, in the directory third_party. So no special download or configuration is needed regarding theses libraries when compiling the code.
The code of the tests uses the Catch framework released under the Boost Software License 1.0.
The source code of this framework is also directly included in the code of MinCoverPetri, in the directory third_party. So no special download or configuration is needed regarding this framework when compiling the tests.
The documentation of these third party libraries is available from their respective websites. An automatically generated documentation using Doxygen is also available here.
CMake is required to build and test the code.
Optionally, gcovr is needed if you want to produce reports of the code coverage of the tests and Valgrind is needed if you want to check the correct use of memory by the application during the tests.
The developer documentation can be automatically generated from the source code using Doxygen.
To get the source code of MinCoverPetri, clone the Git repository of the project:
git clone https://gitlab.lis-lab.fr/dev/mincoverpetri.git
Alternatively, a compressed archive of the latest version of the code can be directly downloaded using this link.
CMake is needed to build the code. It can be downloaded from its website or installed using the package manager of the system (package named cmake on Debian and its derivatives).
In the following we suppose that the code has been downloaded in the directory /path/to/source/ which contains the file CMakeLists.txt and that we want to make the out-of-source build in the directory /path/to/build/.
As a first step, use CMake to generate the makefiles for the project in /path/to/build/ by running:
cd /path/to/build/ cmake /path/to/source/
Now the following steps of the compilation are handled using make.
To build the application, simply build the default target with:
make
This creates the executable named mincoverpetri in /path/to/build/.
To build the executable running the tests, build the target build_tests with:
make build_tests
This creates the executable named mincoverpetri_tests in /path/to/build/.
Note that in the first step above CMake used the default build type to generate the makefiles, which generally implies that the generated executable are built without compiler optimization flags.
To turn on the compilation optimization, specify the Release build type when running CMake in the first step with:
cmake -D CMAKE_BUILD_TYPE=Release /path/to/source/
The following steps to build the executables using make are unchanged.
This results in an executable running significantly faster when processing Petri nets, so pay attention to specify the Release build type when planning some real world use of the generated executable.
If needed, you can also specify the Debug build type when running CMake in the first step to add the compilation flags for generation of the debug symbols, with:
cmake -D CMAKE_BUILD_TYPE=Debug /path/to/source/
The following steps to build the executables using make are unchanged.
By default, the compilation uses the default linking options which generally results in dynamic linking to the C++ Standard Library.
An option has been added to enable static linking when building the executables. This can be useful when you want to create a self-contained executable to simplify the distribution and the use of the file on a system which is different from the compilation system.
To enable static linking during build, pass the following option to CMake in the first step:
cmake -D STATIC_LINK=ON /path/to/source/
The following steps to build the executables using make are unchanged.
An option to cross-compile the code in order to generate a Windows executable has been added. This cross-compilation requires the development environment MinGW-w64 (package named mingw-w64 on Debian and its derivatives).
To build an executable for Windows 32 bits, pass the following option to CMake in the first step:
cmake -D CROSS_COMPILE_WIN32=ON /path/to/source/
To build an executable for Windows 64 bits, pass the following option to CMake in the first step:
cmake -D CROSS_COMPILE_WIN64=ON /path/to/source/
The following steps to build the executables using make are unchanged.
The different options described above can be combined when calling CMake.
For example, when cross-compiling for Windows 64 bits, you probably also want to use static linking to build a self-contained executable and to choose the Release build type to build the most efficient executable. To do this, pass the following options to CMake in the first step:
cmake -D CROSS_COMPILE_WIN64=ON -D STATIC_LINK=ON -D CMAKE_BUILD_TYPE=Release /path/to/source/
The following steps to build the executables using make are unchanged.
The code of the tests is stored in the directory tests and the corresponding reference documentation generated using Doxygen is available here.
If the tests executable mincoverpetri_tests has been previously built as described above using the command:
make build_tests
the tests can be run using one of the following commands:
ctest
or equivalently:
make test
or by directly running the generated executable:
./mincoverpetri_tests
This last option provides more control as it gives the possibility to run the test cases individually by passing a name or a tag to the executable. For example, to run only the tests related to omega-markings, run the command with the tag [marking]:
./mincoverpetri_tests [marking]
The help of the executable lists the available options, see:
./mincoverpetri_tests -h
If the tests executable has not yet been built, it is possible to build and run the tests with a single command using the target build_and_test:
make build_and_test
If you have installed gcovr (package named gcovr in Debian and its derivatives), you can generate a code coverage report of the tests with the command:
make coverage
This outputs both a text report in the terminal and an HTML report in the directory /path/to/build/coverage/.
The test coverage report for the current version of MinCoverPetri is available here.
If you have installed Valgrind (package valgrind in Debian and its derivatives), you can check that no memory leak is detected when running the tests with the command:
make memcheck
The developer documentation is automatically generated using Doxygen (package named doxygen in Debian and its derivatives).
The documentation for the code of the application can be generated in /path/to/source/doc/src/ using the target doc_src:
make doc_src
The documentation for the code of the tests can be generated in /path/to/source/doc/tests/ using the target doc_tests:
make doc_tests
The documentation for the code of the third party libraries can be generated in /path/to/source/doc/third_party/ using the target doc_tests:
make doc_third_party
The full documentation can be generated in /path/to/source/doc/ using the target doc that builds the three targets above:
make doc
The continuous integration features provided by GitLab are used by the MinCoverPetri project to:
The continuous integration tasks are configured in the file .gitlab-ci.yml.
A Docker image is used to run the continuous integration tasks.
This image is publicly accessible and can be used as a preconfigured development environment if wanted. For example, to run the image in an interactive session, run:
docker run -it registry.gitlab.lis-lab.fr:5005/dev/mincoverpetri/mincoverpetri
Some instructions about this Docker image are available in this page.
The Dockerfile used to generate the Docker image is available in the directory docker.
1.8.11
