1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
VerifyPN
========
VerifyPN is based on [PeTe](https://github.com/jopsen/PeTe) and aims to provide
a fast untimed engine for TAPAAL.
Building VerifyPN
-----------------
VerifyPN is build using a simple makefile, depending on you platform and
configuration of it, you might need to modify the makefile in order link
correctly against following dependencies:
* GNU Bison (>= 2.4)
* flex (>= 2.5)
* lp_solve (>= 5.5)
For simplicity, compiled output form GNU Bison, flex and binaries of lpsolve
are included in the source tree.
To cross compile for Windows on linux install `g++-mingw-w64` and run
`make -f makefile.win32` for 32 bit version, and `make -f makefile.win64` for
64 bit version.
**Warning** both `verifypn-win32` and `verifypn-win64` are accompanied by a dll
called `lpsolve55.dll`, however, this is **not** the same dll for both 32 and 64
bit versions. Unfortunately, we cannot rename the dll either, so either we need
to build with MSVC or accept this pain, and distribute Windows 32 and 64 bit
versions in different folders, and watch out of this during deployment.
To cross compile for 32 bit linux you need to run install `gcc-multilib`,
`g++-multilib` and probably a few others.
To build on OS X run `make -f makefile.osx32` or `make -f makefile.osx64`,
as cross compilers for OS X are not readily available (e.g. in package manager)
cross compilation for OS X is not supported.
Testing
-------
VerifyPN builds can be validated with `make check` (for the respective makefiles).
This executes a simple script that iterates over the files in the Tests/ folder,
the tested Petri net is <test-name>-<exit-code>-<strategy>.xml and queries for
this network is in <test-name>-<exit-code>-<strategy>.xml.q, here <test-name> is
an identifier for the test, <exit-code> is the exit code expected by VerifyPN when
given the Petri net and query. <strategy> is the search strategy used for the
verification, `All` if all strategies should be tested.
License
-------
VerifyPN is available under the terms of the GNU GPL versoin 3 or
(at your option) any later version.
If this license doesn't suit you're welcome to contact us, and purpose an
alternative license.
Authors
-------
* Jonas Finnemann Jensen
* Thomas Søndersø Nielsen
* Lars Kærlund Østergaard
* Jiri Srba
|