dehnert
9 years ago
2741 changed files with 445862 additions and 8784 deletions
-
494CMakeLists.txt
-
1README.md
-
23doc/build.md
-
41doc/dependencies.md
-
1doc/getting-started.md
-
4examples/dft/and.dft
-
5examples/dft/and_param.dft
-
4examples/dft/be_nonfail.dft
-
21examples/dft/cardiac.dft
-
24examples/dft/cas.dft
-
22examples/dft/cm2.dft
-
41examples/dft/cm4.dft
-
26examples/dft/cps.dft
-
16examples/dft/deathegg.dft
-
8examples/dft/fdep.dft
-
5examples/dft/fdep2.dft
-
5examples/dft/fdep3.dft
-
129examples/dft/ftpp_complex.dft
-
63examples/dft/ftpp_large.dft
-
53examples/dft/ftpp_standard.dft
-
22examples/dft/mcs.dft
-
26examples/dft/mdcs.dft
-
19examples/dft/mdcs2.dft
-
7examples/dft/mp.dft
-
8examples/dft/nonmonoton_param.dft
-
4examples/dft/or.dft
-
4examples/dft/pand.dft
-
6examples/dft/pand_param.dft
-
12examples/dft/pdep.dft
-
9examples/dft/pdep2.dft
-
5examples/dft/pdep3.dft
-
7examples/dft/pdep4.dft
-
11examples/dft/pdep_symmetry.dft
-
5examples/dft/por.dft
-
5examples/dft/seq.dft
-
6examples/dft/seq2.dft
-
6examples/dft/seq3.dft
-
7examples/dft/seq4.dft
-
9examples/dft/seq5.dft
-
5examples/dft/spare.dft
-
8examples/dft/spare2.dft
-
10examples/dft/spare3.dft
-
9examples/dft/spare4.dft
-
9examples/dft/spare5.dft
-
7examples/dft/spare6.dft
-
5examples/dft/spare7.dft
-
7examples/dft/spare8.dft
-
5examples/dft/spare_cold.dft
-
9examples/dft/spare_param.dft
-
9examples/dft/spare_symmetry.dft
-
8examples/dft/symmetry.dft
-
8examples/dft/symmetry2.dft
-
12examples/dft/symmetry3.dft
-
12examples/dft/symmetry4.dft
-
21examples/dft/symmetry5.dft
-
10examples/dft/symmetry_param.dft
-
7examples/dft/symmetry_shared.dft
-
8examples/dft/tripple_and1.dft
-
8examples/dft/tripple_and2.dft
-
6examples/dft/tripple_and2_c.dft
-
7examples/dft/tripple_and_c.dft
-
9examples/dft/tripple_or.dft
-
8examples/dft/tripple_or2.dft
-
6examples/dft/tripple_or2_c.dft
-
7examples/dft/tripple_or_c.dft
-
9examples/dft/tripple_pand.dft
-
8examples/dft/tripple_pand2.dft
-
6examples/dft/tripple_pand2_c.dft
-
7examples/dft/tripple_pand_c.dft
-
5examples/dft/voting.dft
-
5examples/dft/voting2.dft
-
10examples/dtmc/crowds/crowds10_5.pm
-
8examples/dtmc/crowds/crowds15_5.pm
-
8examples/dtmc/crowds/crowds20_5.pm
-
8examples/dtmc/crowds/crowds5_5.pm
-
2604examples/jani-examples/beb.jani
-
27examples/jani-examples/beb.jani.txt
-
64examples/jani-examples/beb.modest
-
27examples/jani-examples/beb.modest.txt
-
2092examples/jani-examples/brp.jani
-
63examples/jani-examples/brp.jani.txt
-
213examples/jani-examples/brp.modest
-
63examples/jani-examples/brp.modest.txt
-
2129examples/jani-examples/consensus-6.jani
-
27examples/jani-examples/consensus-6.jani.txt
-
157examples/jani-examples/consensus-6.modest
-
27examples/jani-examples/consensus-6.modest.txt
-
354examples/jani-examples/dice.jani
-
29examples/jani-examples/dice.jani.txt
-
2install.sh
-
575resources/3rdparty/CMakeLists.txt
-
1resources/3rdparty/carl
-
0resources/3rdparty/cpplint/cpplint.py
-
1resources/3rdparty/cudd-3.0.0/configure
-
3resources/3rdparty/cudd-3.0.0/configure.ac
-
4resources/3rdparty/eigen-3.3-beta1/.hg_archival.txt
-
11resources/3rdparty/eigen-3.3-beta1/.hgeol
-
34resources/3rdparty/eigen-3.3-beta1/.hgignore
-
25resources/3rdparty/eigen-3.3-beta1/.hgtags
-
491resources/3rdparty/eigen-3.3-beta1/CMakeLists.txt
@ -0,0 +1 @@ |
|||||
|
For more instructions, check out the documentation found in [Getting Started](doc/getting-started.md) |
||||
@ -0,0 +1,23 @@ |
|||||
|
CMake >= 2.8.11 |
||||
|
CMake is required as it is used to generate the Makefiles or Projects/Solutions required to build StoRM. |
||||
|
|
||||
|
Compiler: |
||||
|
A C++11 compliant compiler is required to build StoRM. It is tested and known to work with the following compilers: |
||||
|
- GCC 5.0 |
||||
|
- Clang 3.5.0 |
||||
|
|
||||
|
Other versions or compilers might work, but are not tested. |
||||
|
|
||||
|
The following Compilers are known NOT to work: Microsoft Visual Studio versions older than 2013, GCC versions 4.7 and older. |
||||
|
|
||||
|
Prerequisites: |
||||
|
Boost >= 1.60 |
||||
|
Build using the Boost Build system, for x64 use "bjam address-model=64" or "bjam.exe address-model=64 --build-type=complete" |
||||
|
|
||||
|
|
||||
|
It is recommended to make an out-of-source build, meaning that the folder in which CMake generates its Cache, Makefiles and output files should not be the Project Root nor its Source Directory. |
||||
|
A typical build layout is to create a folder "build" in the project root alongside the CMakeLists.txt file, change into this folder and execute "cmake .." as this will leave all source files untouched |
||||
|
and makes cleaning up the build tree very easy. |
||||
|
There are several options available for the CMake Script as to control behaviour and included components. |
||||
|
If no error occured during the last CMake Configure round, press Generate. |
||||
|
Now you can build StoRM using the generated project/makefiles in the Build folder you selected. |
||||
@ -0,0 +1,41 @@ |
|||||
|
|
||||
|
|
||||
|
|
||||
|
Included Dependencies: |
||||
|
Carl 1.0 |
||||
|
|
||||
|
CUDD 3.0.0 |
||||
|
CUDD is included in the StoRM Sources under /resources/3rdparty/cudd-2.5.0 and builds automatically alongside StoRM. |
||||
|
Its Sourced where heavily modified as to incorporate newer Versions of Boost, changes in C++ (TR1 to C++11) and |
||||
|
to remove components only available under UNIX. |
||||
|
|
||||
|
Eigen 3.3 beta1 |
||||
|
Eigen is included in the StoRM Sources under /resources/3rdparty/eigen and builds automatically alongside StoRM. |
||||
|
|
||||
|
|
||||
|
GTest 1.7.0 |
||||
|
GTest is included in the StoRM Sources under /resources/3rdparty/gtest-1.7.0 and builds automatically alongside StoRM |
||||
|
GMM >= 4.2 |
||||
|
GMM is included in the StoRM Sources under /resources/3rdparty/gmm-4.2 and builds automatically alongside StoRM. |
||||
|
|
||||
|
|
||||
|
Optional: |
||||
|
Gurobi >= 5.6.2 |
||||
|
Specify the path to the gurobi root dir using -DGUROBI_ROOT=/your/path/to/gurobi |
||||
|
Z3 >= 4.3.2 |
||||
|
Specify the path to the z3 root dir using -DZ3_ROOT=/your/path/to/z3 |
||||
|
MathSAT >= 5.2.11 |
||||
|
Specify the path to the mathsat root dir using -DMSAT_ROOT=/your/path/to/mathsat |
||||
|
MPIR >= 2.7.0 |
||||
|
MSVC only and only if linked with MathSAT |
||||
|
Specify the path to the gmp-include directory -DGMP_INCLUDE_DIR=/your/path/to/mathsat |
||||
|
Specify the path to the mpir.lib directory -DGMP_MPIR_LIBRARY=/your/path/to/mpir.lib |
||||
|
Specify the path to the mpirxx.lib directory -DGMP_MPIRXX_LIBRARY=/your/path/to/mpirxx.lib |
||||
|
GMP |
||||
|
clang and gcc only |
||||
|
CUDA Toolkit >= 6.5 |
||||
|
Specify the path to the cuda toolkit root dir using -DCUDA_ROOT=/your/path/to/cuda |
||||
|
CUSP >= 0.4.0 |
||||
|
Only of built with CUDA Toolkit |
||||
|
CUSP is included in the StoRM Sources as a git-submodule unter /resources/3rdparty/cusplibrary |
||||
|
|
||||
@ -0,0 +1 @@ |
|||||
|
|
||||
@ -0,0 +1,4 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,5 @@ |
|||||
|
param x; |
||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=x dorm=0.3; |
||||
@ -0,0 +1,4 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" lambda=0 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,21 @@ |
|||||
|
toplevel "SYSTEM"; |
||||
|
"SYSTEM" or "FDEP" "CPU" "MOTOR" "PUMPS"; |
||||
|
"FDEP" fdep "TRIGGER" "P" "B"; |
||||
|
"TRIGGER" or "CS" "SS"; |
||||
|
"CPU" wsp "P" "B"; |
||||
|
"MOTOR" or "SWITCH" "MOTORS"; |
||||
|
"SWITCH" pand "MS" "MA"; |
||||
|
"MOTORS" csp "MA" "MB"; |
||||
|
"PUMPS" and "PUMP1" "PUMP2"; |
||||
|
"PUMP1" csp "PA" "PS"; |
||||
|
"PUMP2" csp "PB" "PS"; |
||||
|
"P" lambda=5.0e-5 dorm=0; |
||||
|
"B" lambda=5.0e-5 dorm=0.5; |
||||
|
"CS" lambda=2.0e-5 dorm=0; |
||||
|
"SS" lambda=2.0e-5 dorm=0; |
||||
|
"MS" lambda=1.0e-6 dorm=0; |
||||
|
"MA" lambda=1.0e-4 dorm=0; |
||||
|
"MB" lambda=1.0e-4 dorm=0; |
||||
|
"PA" lambda=1.0e-4 dorm=0; |
||||
|
"PB" lambda=1.0e-4 dorm=0; |
||||
|
"PS" lambda=1.0e-4 dorm=0; |
||||
@ -0,0 +1,24 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "CPUfdep" "CPUunit" "Motorunit" "Pumpunit"; |
||||
|
|
||||
|
"CPUfdep" fdep "trigger" "P" "B"; |
||||
|
"trigger" or "CS" "SS"; |
||||
|
"CS" lambda=0.2 dorm=0; |
||||
|
"SS" lambda=0.2 dorm=0; |
||||
|
"CPUunit" wsp "P" "B"; |
||||
|
"P" lambda=0.5 dorm=0; |
||||
|
"B" lambda=0.5 dorm=0.5; |
||||
|
|
||||
|
"Motorunit" or "MP" "Motors"; |
||||
|
"MP" pand "MS" "MA"; |
||||
|
"Motors" csp "MA" "MB"; |
||||
|
"MS" lambda=0.01 dorm=0; |
||||
|
"MA" lambda=1 dorm=0; |
||||
|
"MB" lambda=1 dorm=0; |
||||
|
|
||||
|
"Pumpunit" and "PumpA" "PumpB"; |
||||
|
"PumpA" csp "PA" "PS"; |
||||
|
"PumpB" csp "PB" "PS"; |
||||
|
"PA" lambda=1 dorm=0; |
||||
|
"PB" lambda=1 dorm=0; |
||||
|
"PS" lambda=1 dorm=0; |
||||
@ -0,0 +1,22 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "BUS" "CM"; |
||||
|
"CM" and "CM1" "CM2"; |
||||
|
"CM1" or "DISK1" "POWER1" "MEMORY1"; |
||||
|
"CM2" or "DISK2" "POWER2" "MEMORY2"; |
||||
|
"DISK1" wsp "D11" "D12"; |
||||
|
"DISK2" wsp "D21" "D22"; |
||||
|
"POWER1" or "P1" "PS"; |
||||
|
"POWER2" or "P2" "PS"; |
||||
|
"MEMORY1" wsp "M1" "M3"; |
||||
|
"MEMORY2" wsp "M2" "M3"; |
||||
|
"BUS" lambda=0.0002 dorm=0; |
||||
|
"P1" lambda=0.05 dorm=0; |
||||
|
"P2" lambda=0.05 dorm=0; |
||||
|
"PS" lambda=0.6 dorm=0; |
||||
|
"D11" lambda=8.0 dorm=0; |
||||
|
"D12" lambda=8.0 dorm=0.5; |
||||
|
"D21" lambda=8.0 dorm=0; |
||||
|
"D22" lambda=8.0 dorm=0.5; |
||||
|
"M1" lambda=0.003 dorm=0; |
||||
|
"M2" lambda=0.003 dorm=0; |
||||
|
"M3" lambda=0.003 dorm=0.5; |
||||
@ -0,0 +1,41 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "BUS" "CM"; |
||||
|
"CM" and "CM1" "CM2" "CM3" "CM4"; |
||||
|
"CM1" or "DISK1" "POWER1" "MEMORY1"; |
||||
|
"CM2" or "DISK2" "POWER2" "MEMORY2"; |
||||
|
"CM3" or "DISK3" "POWER3" "MEMORY3"; |
||||
|
"CM4" or "DISK4" "POWER4" "MEMORY4"; |
||||
|
"DISK1" wsp "D11" "D12"; |
||||
|
"DISK2" wsp "D21" "D22"; |
||||
|
"DISK3" wsp "D31" "D32"; |
||||
|
"DISK4" wsp "D41" "D42"; |
||||
|
"POWER1" or "P1" "PS"; |
||||
|
"POWER2" or "P2" "PS"; |
||||
|
"POWER3" or "P3" "PS2"; |
||||
|
"POWER4" or "P4" "PS2"; |
||||
|
"MEMORY1" wsp "M1" "M3" "M4"; |
||||
|
"MEMORY2" wsp "M2" "M3" "M4"; |
||||
|
"MEMORY3" wsp "M31" "M3"; |
||||
|
"MEMORY4" wsp "M41" "M4"; |
||||
|
"BUS" lambda=0.0002 dorm=0; |
||||
|
"P1" lambda=0.05 dorm=0; |
||||
|
"P2" lambda=0.05 dorm=0; |
||||
|
"P3" lambda=0.05 dorm=0; |
||||
|
"P4" lambda=0.05 dorm=0; |
||||
|
"PS" lambda=0.6 dorm=0; |
||||
|
"PS2" lambda=0.6 dorm=0; |
||||
|
"D11" lambda=8.0 dorm=0; |
||||
|
"D12" lambda=8.0 dorm=0.5; |
||||
|
"D21" lambda=8.0 dorm=0; |
||||
|
"D22" lambda=8.0 dorm=0.5; |
||||
|
"D31" lambda=8.0 dorm=0; |
||||
|
"D32" lambda=8.0 dorm=0.5; |
||||
|
"D41" lambda=8.0 dorm=0; |
||||
|
"D42" lambda=8.0 dorm=0.5; |
||||
|
"M1" lambda=0.003 dorm=0; |
||||
|
"M2" lambda=0.003 dorm=0; |
||||
|
"M31" lambda=0.003 dorm=0; |
||||
|
"M41" lambda=0.003 dorm=0; |
||||
|
"M3" lambda=0.003 dorm=0.5; |
||||
|
"M4" lambda=0.003 dorm=0.5; |
||||
|
|
||||
@ -0,0 +1,26 @@ |
|||||
|
toplevel "System"; |
||||
|
|
||||
|
"System" pand "A" "B"; |
||||
|
|
||||
|
"A" and "AA" "AB" "AC" "AD"; |
||||
|
|
||||
|
"B" pand "C" "D"; |
||||
|
|
||||
|
"C" and "CA" "CB" "CC" "CD"; |
||||
|
|
||||
|
"D" and "DA" "DB" "DC" "DD"; |
||||
|
|
||||
|
"AA" lambda=1 dorm=0; |
||||
|
"AB" lambda=1 dorm=0; |
||||
|
"AC" lambda=1 dorm=0; |
||||
|
"AD" lambda=1 dorm=0; |
||||
|
|
||||
|
"CA" lambda=1 dorm=0; |
||||
|
"CB" lambda=1 dorm=0; |
||||
|
"CC" lambda=1 dorm=0; |
||||
|
"CD" lambda=1 dorm=0; |
||||
|
|
||||
|
"DA" lambda=1 dorm=0; |
||||
|
"DB" lambda=1 dorm=0; |
||||
|
"DC" lambda=1 dorm=0; |
||||
|
"DD" lambda=1 dorm=0; |
||||
@ -0,0 +1,16 @@ |
|||||
|
toplevel "DeathEgg"; |
||||
|
"DeathEgg" or "DeathEggProxy" "DeathEggServer" "CampusPowerDependency" "ProxyPowerDependency"; |
||||
|
"DeathEggServer" or "CampusNET" "DES_Disks"; |
||||
|
"DES_Disks" and "DES_Disks_RAID1" "DES_Disks_RAID2"; |
||||
|
"DES_Disks_RAID1" and "DES_Disk_1" "DES_Disk_2"; |
||||
|
"DES_Disks_RAID2" and "DES_Disk_3" "DES_Disk_4"; |
||||
|
"DeathEggProxy" lambda=0.01 dorm=0; |
||||
|
"DES_Disk_1" lambda=0.01 dorm=0; |
||||
|
"DES_Disk_2" lambda=0.01 dorm=0; |
||||
|
"DES_Disk_3" lambda=0.01 dorm=0; |
||||
|
"DES_Disk_4" lambda=0.01 dorm=0; |
||||
|
"CampusPowerDependency" fdep "CampusPower" "DeathEggServer"; |
||||
|
"ProxyPowerDependency" fdep "ProxyPower" "DeathEggProxy"; |
||||
|
"CampusPower" lambda=0.01 dorm=0; |
||||
|
"CampusNET" lambda=0.01 dorm=0; |
||||
|
"ProxyPower" lambda=0.01 dorm=0; |
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "Power" "Machine"; |
||||
|
"Power" fdep "B_Power" "P" "B"; |
||||
|
"Machine" or "P" "B"; |
||||
|
|
||||
|
"B_Power" lambda=0.5 dorm=0; |
||||
|
"P" lambda=0.5 dorm=0; |
||||
|
"B" lambda=0.5 dorm=0.5; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"F" fdep "B" "C"; |
||||
|
"B" lambda=0.5 dorm=0; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C" "F"; |
||||
|
"F" fdep "B" "C"; |
||||
|
"B" lambda=0.4 dorm=0; |
||||
|
"C" lambda=0.8 dorm=0; |
||||
@ -0,0 +1,129 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD"; |
||||
|
|
||||
|
"triadA" 2of3 "aA" "bA" "cA"; |
||||
|
"aA" csp "TAA" "TAS"; |
||||
|
"bA" csp "TAB" "TAS"; |
||||
|
"cA" csp "TAC" "TAS"; |
||||
|
|
||||
|
"triadB" 2of3 "aB" "bB" "cB"; |
||||
|
"aB" csp "TBA" "TBS"; |
||||
|
"bB" csp "TBB" "TBS"; |
||||
|
"cB" csp "TBC" "TBS"; |
||||
|
|
||||
|
"triadC" 2of3 "aC" "bC" "cC"; |
||||
|
"aC" csp "TCA" "TCS"; |
||||
|
"bC" csp "TCB" "TCS"; |
||||
|
"cC" csp "TCC" "TCS"; |
||||
|
|
||||
|
"triadD" 2of3 "aD" "bD" "cD"; |
||||
|
"aD" csp "TDA" "TDS"; |
||||
|
"bD" csp "TDB" "TDS"; |
||||
|
"cD" csp "TDC" "TDS"; |
||||
|
|
||||
|
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; |
||||
|
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; |
||||
|
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; |
||||
|
"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS"; |
||||
|
|
||||
|
|
||||
|
"NEA" lambda=0.017 dorm=1; |
||||
|
"NEB" lambda=0.017 dorm=1; |
||||
|
"NEC" lambda=0.017 dorm=1; |
||||
|
"NED" lambda=0.017 dorm=1; |
||||
|
|
||||
|
"TAA" or "cpuAA" "memAA"; |
||||
|
"memAA" csp "memAA1" "memAA2"; |
||||
|
"cpuAA" lambda=0.11 dorm=0; |
||||
|
"memAA1" lambda=0.11 dorm=0; |
||||
|
"memAA2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TAB" or "cpuAB" "memAB"; |
||||
|
"memAB" csp "memAB1" "memAB2"; |
||||
|
"cpuAB" lambda=0.11 dorm=0; |
||||
|
"memAB1" lambda=0.11 dorm=0; |
||||
|
"memAB2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TAC" or "cpuAC" "memAC"; |
||||
|
"memAC" csp "memAC1" "memAC2"; |
||||
|
"cpuAC" lambda=0.11 dorm=0; |
||||
|
"memAC1" lambda=0.11 dorm=0; |
||||
|
"memAC2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TAS" or "cpuAS" "memAS"; |
||||
|
"memAS" csp "memAS1" "memAS2"; |
||||
|
"cpuAS" lambda=0.11 dorm=0; |
||||
|
"memAS1" lambda=0.11 dorm=0; |
||||
|
"memAS2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBA" or "cpuBA" "memBA"; |
||||
|
"memBA" csp "memBA1" "memBA2"; |
||||
|
"cpuBA" lambda=0.11 dorm=0; |
||||
|
"memBA1" lambda=0.11 dorm=0; |
||||
|
"memBA2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBB" or "cpuBB" "memBB"; |
||||
|
"memBB" csp "memBB1" "memBB2"; |
||||
|
"cpuBB" lambda=0.11 dorm=0; |
||||
|
"memBB1" lambda=0.11 dorm=0; |
||||
|
"memBB2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBC" or "cpuBC" "memBC"; |
||||
|
"memBC" csp "memBC1" "memBC2"; |
||||
|
"cpuBC" lambda=0.11 dorm=0; |
||||
|
"memBC1" lambda=0.11 dorm=0; |
||||
|
"memBC2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBS" or "cpuBS" "memBS"; |
||||
|
"memBS" csp "memBS1" "memBS2"; |
||||
|
"cpuBS" lambda=0.11 dorm=0; |
||||
|
"memBS1" lambda=0.11 dorm=0; |
||||
|
"memBS2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCA" or "cpuCA" "memCA"; |
||||
|
"memCA" csp "memCA1" "memCA2"; |
||||
|
"cpuCA" lambda=0.11 dorm=0; |
||||
|
"memCA1" lambda=0.11 dorm=0; |
||||
|
"memCA2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCB" or "cpuCB" "memCB"; |
||||
|
"memCB" csp "memCB1" "memCB2"; |
||||
|
"cpuCB" lambda=0.11 dorm=0; |
||||
|
"memCB1" lambda=0.11 dorm=0; |
||||
|
"memCB2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCC" or "cpuCC" "memCC"; |
||||
|
"memCC" csp "memCC1" "memCC2"; |
||||
|
"cpuCC" lambda=0.11 dorm=0; |
||||
|
"memCC1" lambda=0.11 dorm=0; |
||||
|
"memCC2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCS" or "cpuCS" "memCS"; |
||||
|
"memCS" csp "memCS1" "memCS2"; |
||||
|
"cpuCS" lambda=0.11 dorm=0; |
||||
|
"memCS1" lambda=0.11 dorm=0; |
||||
|
"memCS2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDA" or "cpuDA" "memDA"; |
||||
|
"memDA" csp "memDA1" "memDA2"; |
||||
|
"cpuDA" lambda=0.11 dorm=0; |
||||
|
"memDA1" lambda=0.11 dorm=0; |
||||
|
"memDA2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDB" or "cpuDB" "memDB"; |
||||
|
"memDB" csp "memDB1" "memDB2"; |
||||
|
"cpuDB" lambda=0.11 dorm=0; |
||||
|
"memDB1" lambda=0.11 dorm=0; |
||||
|
"memDB2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDC" or "cpuDC" "memDC"; |
||||
|
"memDC" csp "memDC1" "memDC2"; |
||||
|
"cpuDC" lambda=0.11 dorm=0; |
||||
|
"memDC1" lambda=0.11 dorm=0; |
||||
|
"memDC2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDS" or "cpuDS" "memDS"; |
||||
|
"memDS" csp "memDS1" "memDS2"; |
||||
|
"cpuDS" lambda=0.11 dorm=0; |
||||
|
"memDS1" lambda=0.11 dorm=0; |
||||
|
"memDS2" lambda=0.11 dorm=0; |
||||
@ -0,0 +1,63 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD" "fE"; |
||||
|
|
||||
|
"triadA" 3of4 "aA" "bA" "cA" "dA"; |
||||
|
"aA" csp "TAA" "TAS"; |
||||
|
"bA" csp "TAB" "TAS"; |
||||
|
"cA" csp "TAC" "TAS"; |
||||
|
"dA" csp "TAD" "TAS"; |
||||
|
|
||||
|
"triadB" 3of4 "aB" "bB" "cB" "dB"; |
||||
|
"aB" csp "TBA" "TBS"; |
||||
|
"bB" csp "TBB" "TBS"; |
||||
|
"cB" csp "TBC" "TBS"; |
||||
|
"dB" csp "TBD" "TBS"; |
||||
|
|
||||
|
"triadC" 3of4 "aC" "bC" "cC" "dC"; |
||||
|
"aC" csp "TCA" "TCS"; |
||||
|
"bC" csp "TCB" "TCS"; |
||||
|
"cC" csp "TCC" "TCS"; |
||||
|
"dC" csp "TCD" "TCS"; |
||||
|
|
||||
|
"triadD" 3of4 "aD" "bD" "cD" "dD"; |
||||
|
"aD" csp "TDA" "TDS"; |
||||
|
"bD" csp "TDB" "TDS"; |
||||
|
"cD" csp "TDC" "TDS"; |
||||
|
"dD" csp "TDD" "TDS"; |
||||
|
|
||||
|
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; |
||||
|
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; |
||||
|
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; |
||||
|
"fD" fdep "NED" "TAD" "TBD" "TCD" "TDD"; |
||||
|
"fE" fdep "NEE" "TAS" "TBS" "TCS" "TDS"; |
||||
|
|
||||
|
|
||||
|
"NEA" lambda=0.017 dorm=1; |
||||
|
"NEB" lambda=0.017 dorm=1; |
||||
|
"NEC" lambda=0.017 dorm=1; |
||||
|
"NED" lambda=0.017 dorm=1; |
||||
|
"NEE" lambda=0.017 dorm=1; |
||||
|
|
||||
|
"TAA" lambda=0.11 dorm=0; |
||||
|
"TAB" lambda=0.11 dorm=0; |
||||
|
"TAC" lambda=0.11 dorm=0; |
||||
|
"TAD" lambda=0.11 dorm=0; |
||||
|
"TAS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBA" lambda=0.11 dorm=0; |
||||
|
"TBB" lambda=0.11 dorm=0; |
||||
|
"TBC" lambda=0.11 dorm=0; |
||||
|
"TBD" lambda=0.11 dorm=0; |
||||
|
"TBS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCA" lambda=0.11 dorm=0; |
||||
|
"TCB" lambda=0.11 dorm=0; |
||||
|
"TCC" lambda=0.11 dorm=0; |
||||
|
"TCD" lambda=0.11 dorm=0; |
||||
|
"TCS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDA" lambda=0.11 dorm=0; |
||||
|
"TDB" lambda=0.11 dorm=0; |
||||
|
"TDC" lambda=0.11 dorm=0; |
||||
|
"TDD" lambda=0.11 dorm=0; |
||||
|
"TDS" lambda=0.11 dorm=0; |
||||
@ -0,0 +1,53 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD"; |
||||
|
|
||||
|
"triadA" 2of3 "aA" "bA" "cA"; |
||||
|
"aA" csp "TAA" "TAS"; |
||||
|
"bA" csp "TAB" "TAS"; |
||||
|
"cA" csp "TAC" "TAS"; |
||||
|
|
||||
|
"triadB" 2of3 "aB" "bB" "cB"; |
||||
|
"aB" csp "TBA" "TBS"; |
||||
|
"bB" csp "TBB" "TBS"; |
||||
|
"cB" csp "TBC" "TBS"; |
||||
|
|
||||
|
"triadC" 2of3 "aC" "bC" "cC"; |
||||
|
"aC" csp "TCA" "TCS"; |
||||
|
"bC" csp "TCB" "TCS"; |
||||
|
"cC" csp "TCC" "TCS"; |
||||
|
|
||||
|
"triadD" 2of3 "aD" "bD" "cD"; |
||||
|
"aD" csp "TDA" "TDS"; |
||||
|
"bD" csp "TDB" "TDS"; |
||||
|
"cD" csp "TDC" "TDS"; |
||||
|
|
||||
|
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; |
||||
|
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; |
||||
|
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; |
||||
|
"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS"; |
||||
|
|
||||
|
|
||||
|
"NEA" lambda=0.017 dorm=1; |
||||
|
"NEB" lambda=0.017 dorm=1; |
||||
|
"NEC" lambda=0.017 dorm=1; |
||||
|
"NED" lambda=0.017 dorm=1; |
||||
|
|
||||
|
"TAA" lambda=0.11 dorm=0; |
||||
|
"TAB" lambda=0.11 dorm=0; |
||||
|
"TAC" lambda=0.11 dorm=0; |
||||
|
"TAS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBA" lambda=0.11 dorm=0; |
||||
|
"TBB" lambda=0.11 dorm=0; |
||||
|
"TBC" lambda=0.11 dorm=0; |
||||
|
"TBS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCA" lambda=0.11 dorm=0; |
||||
|
"TCB" lambda=0.11 dorm=0; |
||||
|
"TCC" lambda=0.11 dorm=0; |
||||
|
"TCS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDA" lambda=0.11 dorm=0; |
||||
|
"TDB" lambda=0.11 dorm=0; |
||||
|
"TDC" lambda=0.11 dorm=0; |
||||
|
"TDS" lambda=0.11 dorm=0; |
||||
@ -0,0 +1,22 @@ |
|||||
|
toplevel "n12"; |
||||
|
"n12" or "n1" "n103" "n7"; |
||||
|
"n103" wsp "n106" "n14"; |
||||
|
"n7" and "n18" "n26"; |
||||
|
"n26" or "n28" "n19" "n23"; |
||||
|
"n19" wsp "n16" "n13"; |
||||
|
"n23" wsp "n0" "n17"; |
||||
|
"n18" or "n15" "n9" "n3"; |
||||
|
"n3" wsp "n2" "n17"; |
||||
|
"n9" wsp "n8" "n27"; |
||||
|
"n16" lambda=8.0 dorm=0.0; |
||||
|
"n0" lambda=0.003 dorm=0.0; |
||||
|
"n13" lambda=8.0 dorm=0.5; |
||||
|
"n2" lambda=0.003 dorm=0.0; |
||||
|
"n17" lambda=0.003 dorm=0.5; |
||||
|
"n15" lambda=0.05 dorm=0.0; |
||||
|
"n106" lambda=1.2 dorm=0.0; |
||||
|
"n14" lambda=0.6 dorm=0.0; |
||||
|
"n1" lambda=2.0E-4 dorm=0.0; |
||||
|
"n27" lambda=8.0 dorm=0.5; |
||||
|
"n8" lambda=8.0 dorm=0.0; |
||||
|
"n28" lambda=0.05 dorm=0.0; |
||||
@ -0,0 +1,26 @@ |
|||||
|
toplevel "System"; |
||||
|
|
||||
|
"System" or "S" "N"; |
||||
|
|
||||
|
"N" lambda=2e-5 dorm=0; |
||||
|
|
||||
|
"S" and "CMA" "CMB"; |
||||
|
|
||||
|
"CMA" or "DiskA" "PA" "MemA"; |
||||
|
"DiskA" wsp "DAA" "DAB"; |
||||
|
"PA" lambda=500e-5 dorm=0; |
||||
|
"MemA" wsp "MA" "MC"; |
||||
|
"DAA" lambda=80000e-5 dorm=0.5; |
||||
|
"DAB" lambda=80000e-5 dorm=0.5; |
||||
|
"MA" lambda=30e-5 dorm=0; |
||||
|
|
||||
|
"CMB" or "DiskB" "PB" "MemB"; |
||||
|
"DiskB" wsp "DBA" "DBB"; |
||||
|
"PB" lambda=500e-5 dorm=0; |
||||
|
"MemB" wsp "MB" "MC"; |
||||
|
"DBA" lambda=80000e-5 dorm=0.5; |
||||
|
"DBB" lambda=80000e-5 dorm=0.5; |
||||
|
"MB" lambda=30e-5 dorm=0; |
||||
|
|
||||
|
"MC" lambda=30e-5 dorm=0.5; |
||||
|
|
||||
@ -0,0 +1,19 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "S" "N"; |
||||
|
"N" lambda=0.0000200000 dorm=0.0000000000; |
||||
|
"S" and "CMA" "CMB"; |
||||
|
"CMA" or "DiskA" "PA" "MemA"; |
||||
|
"DiskA" wsp "DAA" "DAB"; |
||||
|
"PA" lambda=0.0049999999 dorm=0.0000000000; |
||||
|
"MemA" wsp "MA" "MC"; |
||||
|
"DAA" lambda=0.8000000119 dorm=0.5000000000; |
||||
|
"DAB" lambda=0.8000000119 dorm=0.5000000000; |
||||
|
"MA" lambda=0.0003000000 dorm=0.0000000000; |
||||
|
"CMB" or "DiskB" "PB" "MemB"; |
||||
|
"DiskB" wsp "DBA" "DBB"; |
||||
|
"PB" lambda=0.0049999999 dorm=0.0000000000; |
||||
|
"MemB" wsp "MB" "MC"; |
||||
|
"DBA" lambda=0.8000000119 dorm=0.5000000000; |
||||
|
"DBB" lambda=0.8000000119 dorm=0.5000000000; |
||||
|
"MB" lambda=0.0003000000 dorm=0.0000000000; |
||||
|
"MC" lambda=0.0003000000 dorm=0.5000000000; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" or "D" "E"; |
||||
|
"C" or "F" "E"; |
||||
|
"D" lambda=0.1 dorm=0; |
||||
|
"E" lambda=0.2 dorm=0; |
||||
|
"F" lambda=0.3 dorm=0; |
||||
@ -0,0 +1,8 @@ |
|||||
|
param x; |
||||
|
param y; |
||||
|
toplevel "A"; |
||||
|
"A" or "B" "Z"; |
||||
|
"B" pand "D" "S"; |
||||
|
"Z" lambda=y dorm=0; |
||||
|
"D" lambda=100 dorm=0; |
||||
|
"S" lambda=100*x dorm=0; |
||||
@ -0,0 +1,4 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,4 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "B" "C"; |
||||
|
"B" lambda=0.4 dorm=0.3; |
||||
|
"C" lambda=0.2 dorm=0.3; |
||||
@ -0,0 +1,6 @@ |
|||||
|
param x; |
||||
|
param y; |
||||
|
toplevel "A"; |
||||
|
"A" pand "B" "C"; |
||||
|
"B" lambda=x dorm=0.3; |
||||
|
"C" lambda=y dorm=0.3; |
||||
@ -0,0 +1,12 @@ |
|||||
|
// From Junges2015 |
||||
|
// Example 3.19 |
||||
|
|
||||
|
toplevel "SF"; |
||||
|
"SF" or "A" "B" "PDEP"; |
||||
|
"A" pand "S" "MA"; |
||||
|
"B" and "MA" "MB"; |
||||
|
"PDEP" pdep=0.2 "MA" "S"; |
||||
|
|
||||
|
"S" lambda=0.5 dorm=0; |
||||
|
"MA" lambda=0.5 dorm=0; |
||||
|
"MB" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "SF"; |
||||
|
"SF" or "A" "B" "PDEP"; |
||||
|
"A" pand "S" "MA"; |
||||
|
"B" and "MA" "MB"; |
||||
|
"PDEP" pdep=0.2 "MA" "S" "MB"; |
||||
|
|
||||
|
"S" lambda=0.5 dorm=0; |
||||
|
"MA" lambda=0.5 dorm=0; |
||||
|
"MB" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C" "F"; |
||||
|
"F" pdep=0.3 "B" "C"; |
||||
|
"B" lambda=0.4 dorm=0; |
||||
|
"C" lambda=0.8 dorm=0; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "SF"; |
||||
|
"SF" pand "S" "A" "B"; |
||||
|
"PDEP" pdep=0.2 "S" "A" "B"; |
||||
|
|
||||
|
"S" lambda=0.5 dorm=0; |
||||
|
"A" lambda=0.5 dorm=0; |
||||
|
"B" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,11 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" and "C" "D" "PDEP"; |
||||
|
"B'" and "C'" "D'" "PDEP'"; |
||||
|
"PDEP" pdep=0.6 "C" "D"; |
||||
|
"PDEP'" pdep=0.6 "C'" "D'"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=0.5 dorm=0; |
||||
|
|
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" por "B" "C" "D"; |
||||
|
"B" lambda=0.4 dorm=0.0; |
||||
|
"C" lambda=0.2 dorm=0.0; |
||||
|
"D" lambda=0.2 dorm=0.0; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"X" seq "B" "C" |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C" "D"; |
||||
|
"X" seq "B" "C" "D"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
|
"D" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "C" "D"; |
||||
|
"X" seq "B" "C" "D"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
|
"D" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "T1" "B3"; |
||||
|
"T1" or "B1" "B2"; |
||||
|
"X" seq "B1" "B2" "B3"; |
||||
|
"B1" lambda=0.5 dorm=0.3; |
||||
|
"B2" lambda=0.5 dorm=0.3; |
||||
|
"B3" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "T1" "T2"; |
||||
|
"T1" pand "B1" "B2"; |
||||
|
"T2" pand "B3" "B4"; |
||||
|
"X" seq "B4" "B3"; |
||||
|
"B1" lambda=0.7 dorm=0.3; |
||||
|
"B2" lambda=0.5 dorm=0.3; |
||||
|
"B3" lambda=0.5 dorm=0.3; |
||||
|
"B4" lambda=0.7 dorm=0.3; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "I" "M"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"M" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" wsp "I" "J"; |
||||
|
"C" wsp "M" "J"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"M" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,10 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C" "D"; |
||||
|
"B" wsp "I" "M"; |
||||
|
"C" wsp "J" "M"; |
||||
|
"D" wsp "K" "M"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"K" lambda=0.5 dorm=0.3; |
||||
|
"M" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" wsp "I" "J" "K"; |
||||
|
"C" wsp "M" "J"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"K" lambda=0.5 dorm=0.3; |
||||
|
"M" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "I" "B"; |
||||
|
"B" or "C" "J"; |
||||
|
"C" or "K" "L"; |
||||
|
"I" lambda=0.5 dorm=0; |
||||
|
"J" lambda=0.5 dorm=0; |
||||
|
"K" lambda=0.5 dorm=0; |
||||
|
"L" lambda=0.5 dorm=0; |
||||
|
|
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "I" "B"; |
||||
|
"B" wsp "J" "M"; |
||||
|
"I" lambda=0.5 dorm=0.5; |
||||
|
"J" lambda=0.5 dorm=0.5; |
||||
|
"M" lambda=0.5 dorm=0.5; |
||||
|
|
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "K" "J" "I"; |
||||
|
"I" lambda=0.5 dorm=0.5; |
||||
|
"J" lambda=1 dorm=0.5; |
||||
|
"K" lambda=0.5 dorm=0.5; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "I" "B"; |
||||
|
"B" wsp "J" "K"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"K" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "I" "M"; |
||||
|
"I" lambda=0.5 dorm=0.0; |
||||
|
"M" lambda=0.5 dorm=0.0; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
param x; |
||||
|
param y; |
||||
|
toplevel "SF"; |
||||
|
"SF" or "FW" "BW"; |
||||
|
"FW" wsp "W1" "WS"; |
||||
|
"BW" wsp "W2" "WS"; |
||||
|
"W1" lambda=x dorm=0; |
||||
|
"W2" lambda=1 dorm=0; |
||||
|
"WS" lambda=y dorm=0; |
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" wsp "I" "J"; |
||||
|
"C" wsp "K" "L"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"K" lambda=0.5 dorm=0.3; |
||||
|
"L" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" and "C" "D"; |
||||
|
"B'" and "C'" "D'"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" and "C" "D"; |
||||
|
"B'" and "C'" "D'"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=2 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=2 dorm=0; |
||||
@ -0,0 +1,12 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'" "B''"; |
||||
|
"B" and "C" "D"; |
||||
|
"B'" and "C'" "D'"; |
||||
|
"B''" and "C''" "D''"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=0.5 dorm=0; |
||||
|
"C''" lambda=0.5 dorm=0; |
||||
|
"D''" lambda=0.5 dorm=0; |
||||
|
|
||||
@ -0,0 +1,12 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'" "C" "C'"; |
||||
|
"B" and "D" "E"; |
||||
|
"B'" and "D'" "E'"; |
||||
|
"C" or "F"; |
||||
|
"C'" or "F'"; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"E" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=0.5 dorm=0; |
||||
|
"E'" lambda=0.5 dorm=0; |
||||
|
"F" lambda=0.5 dorm=0; |
||||
|
"F'" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,21 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "BA" "BB" "BC" "BD" "BE" "BF"; |
||||
|
"BA" and "CA" "DA"; |
||||
|
"BB" and "CB" "DB"; |
||||
|
"BC" and "CC" "DC"; |
||||
|
"BD" and "CD" "DD"; |
||||
|
"BE" and "CE" "DE"; |
||||
|
"BF" and "CF" "DF"; |
||||
|
"CA" lambda=0.5 dorm=0; |
||||
|
"DA" lambda=0.5 dorm=0; |
||||
|
"CB" lambda=0.5 dorm=0; |
||||
|
"DB" lambda=0.5 dorm=0; |
||||
|
"CC" lambda=0.5 dorm=0; |
||||
|
"DC" lambda=0.5 dorm=0; |
||||
|
"CD" lambda=0.5 dorm=0; |
||||
|
"DD" lambda=0.5 dorm=0; |
||||
|
"CE" lambda=0.5 dorm=0; |
||||
|
"DE" lambda=0.5 dorm=0; |
||||
|
"CF" lambda=0.5 dorm=0; |
||||
|
"DF" lambda=0.5 dorm=0; |
||||
|
|
||||
@ -0,0 +1,10 @@ |
|||||
|
param x; |
||||
|
param y; |
||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" and "C" "D"; |
||||
|
"B'" and "C'" "D'"; |
||||
|
"C" lambda=x dorm=0; |
||||
|
"D" lambda=y dorm=0; |
||||
|
"C'" lambda=x dorm=0; |
||||
|
"D'" lambda=y dorm=0; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" wsp "C" "D"; |
||||
|
"B'" wsp "C'" "D"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" and "BE1" "BE2"; |
||||
|
"C" and "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=0.3; |
||||
|
"BE2" lambda=0.5 dorm=0.3; |
||||
|
"BE3" lambda=0.5 dorm=0.3; |
||||
|
"BE4" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" and "BE1" "BE2"; |
||||
|
"C" and "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=0.3; |
||||
|
"BE2" lambda=0.5 dorm=0.3; |
||||
|
"BE3" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "BE1" "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "BE1" "BE2" "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" or "BE1" "BE2"; |
||||
|
"C" or "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" or "BE1" "BE2"; |
||||
|
"C" or "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "BE1" "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "BE1" "BE2" "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "B" "BE4"; |
||||
|
"B" pand "C" "BE3"; |
||||
|
"C" pand "BE1" "BE2"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "B" "C"; |
||||
|
"B" pand "BE1" "BE2"; |
||||
|
"C" pand "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "BE1" "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "BE1" "BE2" "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" 1of3 "B" "C" "D"; |
||||
|
"B" lambda=0.1 dorm=0; |
||||
|
"C" lambda=0.2 dorm=0; |
||||
|
"D" lambda=0.3 dorm=0; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" 1of3 "B" "C" "D"; |
||||
|
"B" lambda=0.3 dorm=0; |
||||
|
"C" lambda=0.4 dorm=0; |
||||
|
"D" lambda=1 dorm=0; |
||||
2604
examples/jani-examples/beb.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,27 @@ |
|||||
|
Peak memory usage: 38 MB |
||||
|
Analysis results for beb.jani |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 4528 |
||||
|
Transitions: 4874 |
||||
|
Branches: 6899 |
||||
|
Time: 0.0 s |
||||
|
Rate: 92408 states/s |
||||
|
|
||||
|
+ LineSeized |
||||
|
Probability: 0.9166259765625 |
||||
|
Time: 0.1 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 8 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ GaveUp |
||||
|
Probability: 0.0833740234375 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 9 |
||||
|
Time: 0.0 s |
||||
@ -0,0 +1,64 @@ |
|||||
|
// Modest MDP model of the bounded exponential backoff procedure (BEB) |
||||
|
// [BFHH11] |
||||
|
action tick, tack, tock; |
||||
|
|
||||
|
const int K = 4; // maximum value for backoff |
||||
|
const int N = 3; // number of tries before giving up |
||||
|
const int H = 3; // number of hosts (must correspond to the number of Host() instantiations in the global composition) |
||||
|
|
||||
|
int(0..2) cr; // count how many hosts attempt to seize the line in a slot (zero, one, many) |
||||
|
bool line_seized; |
||||
|
bool gave_up; |
||||
|
|
||||
|
property LineSeized = Pmax(<> line_seized); // some host managed to seize the line before any other gave up |
||||
|
property GaveUp = Pmax(<> gave_up); // some host gave up before any other managed to seize the line (does not work with POR) |
||||
|
|
||||
|
process Clock() |
||||
|
{ |
||||
|
tick; tack; tau {= cr = 0 =}; tock; Clock() |
||||
|
} |
||||
|
|
||||
|
process Host() |
||||
|
{ |
||||
|
int(0..N) na; // nr_attempts 0..N |
||||
|
int(0..K) ev = 2; // exp_val 0..K |
||||
|
int(0..K) wt; // slots_to_wait 0..K |
||||
|
|
||||
|
do |
||||
|
{ |
||||
|
if(wt > 0) |
||||
|
{ |
||||
|
// wait this slot |
||||
|
tick {= wt-- =} |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
tau {= cr = min(2, cr + 1) =}; // attempt to seize the line |
||||
|
tick; |
||||
|
if(cr == 1) |
||||
|
{ |
||||
|
// someone managed to seize the line |
||||
|
tau {= line_seized = true =}; stop |
||||
|
} |
||||
|
else if(na >= N) |
||||
|
{ |
||||
|
// maximum number of attempts exceeded |
||||
|
tau {= gave_up = true =}; stop |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
// backoff |
||||
|
tau {= na++, wt = DiscreteUniform(0, max(0, ev - 1)), ev = min(2 * ev, K) =} |
||||
|
} |
||||
|
}; |
||||
|
tack; tock |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
par |
||||
|
{ |
||||
|
:: Clock() |
||||
|
:: Host() |
||||
|
:: Host() |
||||
|
:: Host() |
||||
|
} |
||||
@ -0,0 +1,27 @@ |
|||||
|
Peak memory usage: 39 MB |
||||
|
Analysis results for beb.modest |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 4528 |
||||
|
Transitions: 4874 |
||||
|
Branches: 6899 |
||||
|
Time: 0.0 s |
||||
|
Rate: 94333 states/s |
||||
|
|
||||
|
+ LineSeized |
||||
|
Probability: 0.9166259765625 |
||||
|
Time: 0.1 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 8 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ GaveUp |
||||
|
Probability: 0.0833740234375 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 9 |
||||
|
Time: 0.0 s |
||||
2092
examples/jani-examples/brp.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,63 @@ |
|||||
|
Peak memory usage: 39 MB |
||||
|
Analysis results for brp.jani |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 3959 |
||||
|
Transitions: 4244 |
||||
|
Branches: 4593 |
||||
|
Time: 0.1 s |
||||
|
Rate: 74698 states/s |
||||
|
|
||||
|
+ P_A |
||||
|
Probability: 0 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 1 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_B |
||||
|
Probability: 0 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 1 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_1 |
||||
|
Probability: 0.000423333443357766 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 2.35005704803786E-07 |
||||
|
Iterations: 13 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_2 |
||||
|
Probability: 2.64530890961023E-05 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 2.05561452068843E-07 |
||||
|
Iterations: 14 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_3 |
||||
|
Probability: 0.000185191226393368 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 3.32462409056221E-07 |
||||
|
Iterations: 13 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_4 |
||||
|
Probability: 8E-06 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 2 |
||||
|
Time: 0.0 s |
||||
@ -0,0 +1,213 @@ |
|||||
|
// Modest PTA model of the bounded retransmission protocol (BRP) |
||||
|
// [HH09], http://www.modestchecker.net/CaseStudies/BRP/ |
||||
|
action put, get, put_k, get_k, put_l, get_l; |
||||
|
action new_file; |
||||
|
action s_ok, s_dk, s_nok, s_restart; |
||||
|
action r_ok, r_inc, r_fst, r_nok, r_timeout; |
||||
|
exception error; |
||||
|
|
||||
|
const int N = 16; // number of frames per file |
||||
|
const int MAX = 2; // maximum number of retransmissions per frame |
||||
|
const int TD = 1; // transmission delay |
||||
|
const int TS = 2 * TD + 1; // sender timeout |
||||
|
const int TR = 2 * MAX * TS + 3 * TD; // receiver timeout |
||||
|
const int SYNC = TR; |
||||
|
|
||||
|
bool ff, lf, ab; // channel data: first/last frame, alternating bit |
||||
|
int(0..N) i; // sender chunk counter |
||||
|
bool inTransitK = false; |
||||
|
bool inTransitL = false; |
||||
|
|
||||
|
bool first_file_done = false; |
||||
|
bool get_k_seen, s_ok_seen, s_nok_seen, s_dk_seen, s_restart_seen, r_ok_seen, r_timeout_seen; |
||||
|
|
||||
|
// Invariant (timed) properties (from [BrpOnTime], the TA model) |
||||
|
bool premature_timeout, channel_k_overflow, channel_l_overflow; |
||||
|
// "there is at most one message in transit for each channel" |
||||
|
property T_1 = A[] (!(channel_k_overflow || channel_l_overflow)); |
||||
|
// "there is at most one message in transit in total" |
||||
|
property T_2 = A[] (!(inTransitK && inTransitL)); |
||||
|
// Assumption (A1): "no premature timeouts" |
||||
|
property T_A1 = A[] (!premature_timeout); |
||||
|
// Assumption (A2): "sender starts new file only after receiver reacted to failure" |
||||
|
// Note that receiver can only notice failure if it received at least one chunk, i.e. get_k_seen |
||||
|
property T_A2 = A[] (!s_restart_seen || !get_k_seen || r_timeout_seen); |
||||
|
|
||||
|
// Probabilistic reachability properties (from [D'AJJL01], the RAPTURE/PRISM model) |
||||
|
// property A of [D'AJJL01]: "the maximum probability that eventually the sender reports |
||||
|
// a certain unsuccessful transmission but the receiver got the complete file" |
||||
|
property P_A = Pmax(<>(s_nok_seen && r_ok_seen)); |
||||
|
// property B of [D'AJJL01]: "the maximum probability that eventually the sender reports |
||||
|
// a certain successful transmission but the receiver did not get the complete file" |
||||
|
property P_B = Pmax(<>(s_ok_seen && !r_ok_seen)); |
||||
|
// property 1 of [D'AJJL01]: "the maximum probability that eventually the sender |
||||
|
// does not report a successful transmission" |
||||
|
property P_1 = Pmax(<>(s_nok_seen || s_dk_seen)); |
||||
|
// property 2 of [D'AJJL01]: "the maximum probability that eventually the sender |
||||
|
// reports an uncertainty on the success of the transmission" |
||||
|
property P_2 = Pmax(<>(s_dk_seen)); |
||||
|
// property 3 of [D'AJJL01]: "the maximum probability that eventually the sender |
||||
|
// reports an unsuccessful transmission after more than 8 chunks have been sent successfully" |
||||
|
property P_3 = Pmax(<>(s_nok_seen && i > 8)); |
||||
|
// property 4 of [D'AJJL01]: "the maximum probability that eventually the receiver |
||||
|
// does not receive any chunk and the sender tried to send a chunk" |
||||
|
property P_4 = Pmax(<>((s_ok_seen || s_nok_seen || s_dk_seen) && !get_k_seen)); |
||||
|
|
||||
|
|
||||
|
process Sender() |
||||
|
{ |
||||
|
bool bit; |
||||
|
int(0..MAX) rc; |
||||
|
clock c; |
||||
|
|
||||
|
try |
||||
|
{ |
||||
|
do { |
||||
|
:: when urgent(i < N) {= i++ =}; |
||||
|
do |
||||
|
{ |
||||
|
// send frame |
||||
|
invariant(c <= 0) put_k {= ff = (i == 1), lf = (i == N), ab = bit, c = 0 =}; |
||||
|
invariant(c <= TS) alt { |
||||
|
:: // receive ack |
||||
|
get_l {= bit = !bit, rc = 0, c = 0 =}; |
||||
|
urgent break |
||||
|
:: // timeout |
||||
|
when(c >= TS) |
||||
|
if(rc < MAX) |
||||
|
{ |
||||
|
// retry |
||||
|
{= rc++, c = 0 =} |
||||
|
} |
||||
|
else if(i < N) |
||||
|
{ |
||||
|
// no retries left |
||||
|
s_nok {= rc = 0, c = 0 =}; |
||||
|
urgent throw(error) |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
// no retries left |
||||
|
s_dk {= rc = 0, c = 0 =}; |
||||
|
urgent throw(error) |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
:: when(i == N) |
||||
|
// file transmission successfully completed |
||||
|
invariant(c <= 0) s_ok {= first_file_done = true =}; |
||||
|
urgent break |
||||
|
} |
||||
|
} |
||||
|
catch error |
||||
|
{ |
||||
|
// File transfer did not succeed: wait, then restart with next file |
||||
|
invariant(c <= SYNC) when(c >= SYNC) |
||||
|
s_restart {= bit = false, first_file_done = true =} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
process Receiver() |
||||
|
{ |
||||
|
bool r_ff, r_lf, r_ab; |
||||
|
bool bit; |
||||
|
clock c; |
||||
|
|
||||
|
// receive first frame |
||||
|
if(ff) { get_k {= c = 0, bit = ab, r_ff = ff, r_lf = lf, r_ab = ab =} } |
||||
|
else { get_k {= c = 0, premature_timeout = true =}; stop }; |
||||
|
do |
||||
|
{ |
||||
|
invariant(c <= 0) |
||||
|
{ |
||||
|
if(r_ab != bit) |
||||
|
{ |
||||
|
// repetition, re-ack |
||||
|
put_l |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
// report frame |
||||
|
if(r_lf) { r_ok } |
||||
|
else if(r_ff) { r_fst } |
||||
|
else { r_inc }; |
||||
|
put_l {= bit = !bit =} |
||||
|
} |
||||
|
}; |
||||
|
invariant(c <= TR) |
||||
|
{ |
||||
|
alt { |
||||
|
:: // receive next frame |
||||
|
get_k {= c = 0, r_ff = ff, r_lf = lf, r_ab = ab =} |
||||
|
:: // timeout |
||||
|
when(c == TR) |
||||
|
if(r_lf) |
||||
|
{ |
||||
|
// we just got the last frame, though |
||||
|
r_timeout; break |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
r_nok; |
||||
|
// abort transfer |
||||
|
r_timeout; break |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
}; |
||||
|
Receiver() |
||||
|
} |
||||
|
|
||||
|
process ChannelK() |
||||
|
{ |
||||
|
clock c; |
||||
|
|
||||
|
put_k palt |
||||
|
{ |
||||
|
:98: {= c = 0, inTransitK = true =}; |
||||
|
invariant(c <= TD) alt { |
||||
|
:: get_k {= inTransitK = false =} |
||||
|
:: put_k {= channel_k_overflow = true =}; stop |
||||
|
} |
||||
|
: 2: {==} |
||||
|
}; |
||||
|
ChannelK() |
||||
|
} |
||||
|
|
||||
|
process ChannelL() |
||||
|
{ |
||||
|
clock c; |
||||
|
|
||||
|
put_l palt |
||||
|
{ |
||||
|
:99: {= c = 0, inTransitL = true =}; |
||||
|
invariant(c <= TD) alt { |
||||
|
:: get_l {= inTransitL = false =} |
||||
|
:: put_l {= channel_l_overflow = true =}; stop |
||||
|
} |
||||
|
: 1: {==} |
||||
|
}; |
||||
|
ChannelL() |
||||
|
} |
||||
|
|
||||
|
process Observer() |
||||
|
{ |
||||
|
alt { |
||||
|
:: get_k {= get_k_seen = true =} |
||||
|
:: s_ok {= s_ok_seen = true =} |
||||
|
:: s_nok {= s_nok_seen = true =} |
||||
|
:: s_dk {= s_dk_seen = true =} |
||||
|
:: s_restart {= s_restart_seen = true =} |
||||
|
:: r_ok {= r_ok_seen = true =} |
||||
|
:: r_timeout {= r_timeout_seen = true =} |
||||
|
}; |
||||
|
Observer() |
||||
|
} |
||||
|
|
||||
|
par { |
||||
|
:: Sender() |
||||
|
:: Receiver() |
||||
|
:: ChannelK() |
||||
|
:: ChannelL() |
||||
|
:: Observer() |
||||
|
} |
||||
@ -0,0 +1,63 @@ |
|||||
|
Peak memory usage: 40 MB |
||||
|
Analysis results for brp.modest |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 3959 |
||||
|
Transitions: 4244 |
||||
|
Branches: 4593 |
||||
|
Time: 0.1 s |
||||
|
Rate: 73315 states/s |
||||
|
|
||||
|
+ P_A |
||||
|
Probability: 0 |
||||
|
Time: 0.1 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 1 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_B |
||||
|
Probability: 0 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 1 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_1 |
||||
|
Probability: 0.000423333443357766 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 2.35005704803786E-07 |
||||
|
Iterations: 13 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_2 |
||||
|
Probability: 2.64530890961023E-05 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 2.05561452068843E-07 |
||||
|
Iterations: 14 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_3 |
||||
|
Probability: 0.000185191226393368 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 3.32462409056221E-07 |
||||
|
Iterations: 13 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_4 |
||||
|
Probability: 8E-06 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 2 |
||||
|
Time: 0.0 s |
||||
2129
examples/jani-examples/consensus-6.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,27 @@ |
|||||
|
Peak memory usage: 530 MB |
||||
|
Analysis results for consensus-6.jani |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 2345194 |
||||
|
Transitions: 9418584 |
||||
|
Branches: 13891248 |
||||
|
Time: 8.7 s |
||||
|
Rate: 270964 states/s |
||||
|
|
||||
|
+ C1 |
||||
|
Result: True |
||||
|
Time for min. prob. 0 states: 1.6 s |
||||
|
Time for min. prob. 1 states: 0.1 s |
||||
|
Time: 1.7 s |
||||
|
Min. probability: 1 |
||||
|
|
||||
|
+ C2 |
||||
|
Probability: 0.395776147642961 |
||||
|
Time for min. prob. 0 states: 2.0 s |
||||
|
Time for min. prob. 1 states: 0.1 s |
||||
|
Time: 125.8 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 9.96634356860147E-07 |
||||
|
Iterations: 2137 |
||||
|
Time: 123.8 s |
||||
@ -0,0 +1,157 @@ |
|||||
|
// Modest version of http://www.prismmodelchecker.org/casestudies/consensus_prism.php |
||||
|
// Command line: mcsta.exe consensus-6.modest -S Memory --nochainopt --bounded-alg StateElimination -E "K=2" |
||||
|
|
||||
|
action done; |
||||
|
|
||||
|
// constants |
||||
|
const int N = 6; |
||||
|
const int K = 4; |
||||
|
const int range = 2 * (K + 1) * N; |
||||
|
const int counter_init = (K + 1) * N; |
||||
|
const int left = N; |
||||
|
const int right = 2 * (K + 1) * N - N; |
||||
|
|
||||
|
// shared coin |
||||
|
int(0..range) counter = counter_init; |
||||
|
reward coin_flips; |
||||
|
|
||||
|
property C1 = P(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1)) >= 1; |
||||
|
property C2 = Pmin(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1 && coin1 == 1 && coin2 == 1 && coin3 == 1 && coin4 == 1 && coin5 == 1 && coin6 == 1)); |
||||
|
|
||||
|
int(0..1) fin1, fin2, fin3, fin4, fin5, fin6; |
||||
|
int(0..1) coin1, coin2, coin3, coin4, coin5, coin6; |
||||
|
|
||||
|
process Tourist1() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin1 = 0, coin_flips++ =} :1: {= coin1 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin1 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin1 == 1 && counter < range) {= counter++, coin1 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin1 = 0, fin1 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin1 = 1, fin1 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist1() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist2() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin2 = 0, coin_flips++ =} :1: {= coin2 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin2 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin2 == 1 && counter < range) {= counter++, coin2 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin2 = 0, fin2 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin2 = 1, fin2 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist2() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist3() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin3 = 0, coin_flips++ =} :1: {= coin3 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin3 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin3 == 1 && counter < range) {= counter++, coin3 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin3 = 0, fin3 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin3 = 1, fin3 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist3() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist4() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin4 = 0, coin_flips++ =} :1: {= coin4 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin4 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin4 == 1 && counter < range) {= counter++, coin4 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin4 = 0, fin4 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin4 = 1, fin4 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist4() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist5() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin5 = 0, coin_flips++ =} :1: {= coin5 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin5 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin5 == 1 && counter < range) {= counter++, coin5 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin5 = 0, fin5 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin5 = 1, fin5 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist5() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist6() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin6 = 0, coin_flips++ =} :1: {= coin6 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin6 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin6 == 1 && counter < range) {= counter++, coin6 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin6 = 0, fin6 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin6 = 1, fin6 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist6() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
par { |
||||
|
:: Tourist1() |
||||
|
:: Tourist2() |
||||
|
:: Tourist3() |
||||
|
:: Tourist4() |
||||
|
:: Tourist5() |
||||
|
:: Tourist6() |
||||
|
} |
||||
@ -0,0 +1,27 @@ |
|||||
|
Peak memory usage: 531 MB |
||||
|
Analysis results for consensus-6.modest |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 2345194 |
||||
|
Transitions: 9418584 |
||||
|
Branches: 13891248 |
||||
|
Time: 8.2 s |
||||
|
Rate: 287507 states/s |
||||
|
|
||||
|
+ C1 |
||||
|
Result: True |
||||
|
Time for min. prob. 0 states: 1.5 s |
||||
|
Time for min. prob. 1 states: 0.2 s |
||||
|
Time: 1.7 s |
||||
|
Min. probability: 1 |
||||
|
|
||||
|
+ C2 |
||||
|
Probability: 0.395776147642961 |
||||
|
Time for min. prob. 0 states: 2.0 s |
||||
|
Time for min. prob. 1 states: 0.1 s |
||||
|
Time: 126.8 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 9.96634356860147E-07 |
||||
|
Iterations: 2137 |
||||
|
Time: 124.7 s |
||||
@ -0,0 +1,354 @@ |
|||||
|
{ |
||||
|
"jani-version": 1, |
||||
|
"name": "dice", |
||||
|
"type" : "mdp", |
||||
|
"actions" : [], |
||||
|
"variables" : [ |
||||
|
{ |
||||
|
"name": "thrownSix", |
||||
|
"type": "bool", |
||||
|
"initial-value": false |
||||
|
}, |
||||
|
{ |
||||
|
"name": "terminated", |
||||
|
"type": "bool", |
||||
|
"initial-value": false |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"name" : "step" |
||||
|
} |
||||
|
], |
||||
|
"properties" : [ |
||||
|
{ |
||||
|
"name" : "ProbThrowSix", |
||||
|
"reach" : "thrownSix", |
||||
|
"type": "probability-max-query" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "StepsUntilReach", |
||||
|
"reach" : "terminated", |
||||
|
"reward": "step", |
||||
|
"type": "expected-reachability-reward-max-query" |
||||
|
} |
||||
|
], |
||||
|
"automata" : [ |
||||
|
{ |
||||
|
"name" : "dice", |
||||
|
"variables" : [ |
||||
|
{ |
||||
|
"name" : "d", |
||||
|
"type" : { |
||||
|
"kind": "bounded", |
||||
|
"base": "int", |
||||
|
"lower-bound" : 0, |
||||
|
"upper-bound" : 6 |
||||
|
}, |
||||
|
"initial-value" : 0 |
||||
|
} |
||||
|
], |
||||
|
"locations" : [ |
||||
|
{ |
||||
|
"name" : "s0" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s1" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s2" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s3" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s4" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s5" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s6" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s7" |
||||
|
} |
||||
|
], |
||||
|
"initial-location" : "s0", |
||||
|
"edges" : [ |
||||
|
{ |
||||
|
"location" : "s0", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s1", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s2", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s1", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s3", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s4", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s2", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s5", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s6", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s3", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s1", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 1 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s4", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 2 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 3 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s5", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 4 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 5 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s6", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s2", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 6 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "thrownSix", |
||||
|
"value" : true |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s7", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 1, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
], |
||||
|
"system" : "dice" |
||||
|
} |
||||
@ -0,0 +1,29 @@ |
|||||
|
Peak memory usage: 36 MB |
||||
|
Analysis results for dice.jani |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 8 |
||||
|
Transitions: 8 |
||||
|
Branches: 14 |
||||
|
Time: 0.0 s |
||||
|
Rate: 190 states/s |
||||
|
|
||||
|
+ ProbThrowSix |
||||
|
Probability: 0.166666626930237 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 7.15255907834985E-07 |
||||
|
Iterations: 11 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ StepsUntilReach |
||||
|
Value: 3.66666650772095 |
||||
|
Time for min. prob. 0 states: 0.0 s |
||||
|
Time for min. prob. 1 states: 0.0 s |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 4.08717619857464E-07 |
||||
|
Iterations: 12 |
||||
|
Time: 0.0 s |
||||
@ -0,0 +1,2 @@ |
|||||
|
#!/bin/bash |
||||
|
pip install -ve . --install-option="--cmake=" --install-option="--make=" |
||||
@ -1,82 +1,555 @@ |
|||||
add_custom_target(resources) |
add_custom_target(resources) |
||||
add_custom_target(test-resources) |
add_custom_target(test-resources) |
||||
|
|
||||
ExternalProject_Add( |
|
||||
xercesc |
|
||||
SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/xercesc-3.1.2 |
|
||||
CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/xercesc-3.1.2/configure --prefix=${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2 --libdir=${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} CFLAGS=-O3 CXXFLAGS=-O3 |
|
||||
PREFIX ${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2 |
|
||||
BUILD_COMMAND make |
|
||||
BUILD_IN_SOURCE 0 |
|
||||
LOG_CONFIGURE ON |
|
||||
LOG_BUILD ON |
|
||||
LOG_INSTALL ON |
|
||||
) |
|
||||
|
set(STORM_3RDPARTY_SOURCE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty) |
||||
|
set(STORM_3RDPARTY_BINARY_DIR ${PROJECT_BINARY_DIR}/resources/3rdparty) |
||||
|
|
||||
|
#### |
||||
|
#### Find autoreconf for cudd update step |
||||
|
find_program(AUTORECONF autoreconf) |
||||
|
mark_as_advanced(AUTORECONF) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## l3pp |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
|
||||
ExternalProject_Add( |
|
||||
glpk |
|
||||
DOWNLOAD_COMMAND "" |
|
||||
PREFIX ${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57 |
|
||||
SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/glpk-4.57 |
|
||||
CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/glpk-4.57/configure --prefix=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57 --libdir=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57/lib CC=${CMAKE_C_COMPILER} |
|
||||
BUILD_COMMAND make "CFLAGS=-O2 -w" |
|
||||
INSTALL_COMMAND make install |
|
||||
BUILD_IN_SOURCE 0 |
|
||||
LOG_CONFIGURE ON |
|
||||
LOG_BUILD ON |
|
||||
LOG_INSTALL ON |
|
||||
) |
|
||||
|
|
||||
ExternalProject_Add( |
ExternalProject_Add( |
||||
cudd3 |
|
||||
DOWNLOAD_COMMAND "" |
|
||||
SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0 |
|
||||
PREFIX ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0 |
|
||||
CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --prefix=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0 --libdir=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} |
|
||||
BUILD_COMMAND make "CFLAGS=-O2 -w" |
|
||||
INSTALL_COMMAND make install |
|
||||
BUILD_IN_SOURCE 0 |
|
||||
LOG_CONFIGURE ON |
|
||||
LOG_BUILD ON |
|
||||
LOG_INSTALL ON |
|
||||
|
l3pp |
||||
|
GIT_REPOSITORY https://github.com/hbruintjes/l3pp.git |
||||
|
GIT_TAG master |
||||
|
SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/l3pp |
||||
|
CONFIGURE_COMMAND "" |
||||
|
BUILD_COMMAND "" |
||||
|
INSTALL_COMMAND "" |
||||
|
LOG_INSTALL ON |
||||
) |
) |
||||
|
ExternalProject_Get_Property(l3pp source_dir) |
||||
|
set(l3pp_INCLUDE "${source_dir}/") |
||||
|
include_directories(${l3pp_INCLUDE}) |
||||
|
add_dependencies(resources l3pp) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## gmm |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
# Add the shipped version of GMM to the include pathes |
||||
|
set(GMMXX_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-5.0/include") |
||||
|
include_directories(${GMMXX_INCLUDE_DIR}) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Eigen |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
# Add the shipped version of Eigen to the include pathes |
||||
|
set(EIGEN_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/eigen-3.3-beta1") |
||||
|
include_directories(${EIGEN_INCLUDE_DIR}) |
||||
|
|
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Boost |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
# Boost Option variables |
||||
|
set(Boost_USE_STATIC_LIBS ${USE_BOOST_STATIC_LIBRARIES}) |
||||
|
set(Boost_USE_MULTITHREADED ON) |
||||
|
set(Boost_USE_STATIC_RUNTIME OFF) |
||||
|
|
||||
|
find_package(Boost 1.57.0 QUIET REQUIRED) |
||||
|
|
||||
|
if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL "")) |
||||
|
set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib") |
||||
|
endif () |
||||
|
link_directories(${Boost_LIBRARY_DIRS}) |
||||
|
|
||||
|
include_directories(${Boost_INCLUDE_DIRS}) |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${Boost_LIBRARIES}) |
||||
|
message(STATUS "StoRM - Using Boost ${Boost_VERSION} (lib ${Boost_LIB_VERSION})") |
||||
|
#message(STATUS "StoRM - BOOST_INCLUDE_DIRS is ${Boost_INCLUDE_DIRS}") |
||||
|
#message(STATUS "StoRM - BOOST_LIBRARY_DIRS is ${Boost_LIBRARY_DIRS}") |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## ExprTk |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
# Use the shipped version of ExprTK |
||||
|
message (STATUS "StoRM - Including ExprTk") |
||||
|
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk") |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## ModernJSON |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
#use the shipped version of modernjson |
||||
|
message (STATUS "StoRM - Including ModernJSON") |
||||
|
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/modernjson/src/") |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Z3 (optional) |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
find_package(Z3 QUIET) |
||||
|
|
||||
|
# Z3 Defines |
||||
|
set(STORM_HAVE_Z3 ${Z3_FOUND}) |
||||
|
|
||||
|
if(Z3_FOUND) |
||||
|
message (STATUS "StoRM - Linking with Z3") |
||||
|
include_directories(${Z3_INCLUDE_DIRS}) |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${Z3_LIBRARIES}) |
||||
|
endif(Z3_FOUND) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## glpk |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
include(${STORM_3RDPARTY_SOURCE_DIR}/include_glpk.cmake) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Gurobi (optional) |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
if (STORM_USE_GUROBI) |
||||
|
find_package(Gurobi QUIET REQUIRED) |
||||
|
set(STORM_HAVE_GUROBI ${GUROBI_FOUND}) |
||||
|
if (GUROBI_FOUND) |
||||
|
message (STATUS "StoRM - Linking with Gurobi") |
||||
|
include_directories(${GUROBI_INCLUDE_DIRS}) |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${GUROBI_LIBRARY}) |
||||
|
#link_directories("${GUROBI_ROOT}/lib") |
||||
|
else() |
||||
|
#message(FATAL_ERROR "StoRM - Gurobi was requested, but not found!") |
||||
|
endif() |
||||
|
else() |
||||
|
set(STORM_HAVE_GUROBI OFF) |
||||
|
endif() |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## CUDD |
||||
|
## |
||||
|
############################################################# |
||||
|
include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## CLN |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
find_package(CLN QUIET) |
||||
|
|
||||
|
if(CLN_FOUND) |
||||
|
set(STORM_HAVE_CLN ON) |
||||
|
message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}") |
||||
|
include_directories("${CLN_INCLUDE_DIR}") |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES}) |
||||
|
else() |
||||
|
set(STORM_HAVE_CLN OFF) |
||||
|
if(NOT GMP_FOUND) |
||||
|
message(FATAL_ERROR "StoRM - Neither CLN nor GMP found") |
||||
|
endif() |
||||
|
endif() |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## carl |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
set(STORM_HAVE_CARL OFF) |
||||
|
if(USE_CARL) |
||||
|
find_package(carl QUIET) |
||||
|
if(carl_FOUND) |
||||
|
set(STORM_HAVE_CARL ON) |
||||
|
message(STATUS "StoRM - Use system version of carl") |
||||
|
message(STATUS "StoRM - Linking with carl ${carl_VERSION_STRING}") |
||||
|
include_directories("${carl_INCLUDE_DIR}") |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES}) |
||||
|
else() |
||||
|
message(STATUS "StoRM - Using shipped version of carl") |
||||
|
# |
||||
|
ExternalProject_Add( |
||||
|
carl |
||||
|
GIT_REPOSITORY https://github.com/smtrat/carl |
||||
|
GIT_TAG master |
||||
|
INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl |
||||
|
SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/carl |
||||
|
CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl |
||||
|
BUILD_IN_SOURCE 0 |
||||
|
BUILD_COMMAND make lib_carl |
||||
|
INSTALL_COMMAND make install |
||||
|
LOG_UPDATE ON |
||||
|
LOG_CONFIGURE ON |
||||
|
LOG_BUILD ON |
||||
|
LOG_INSTALL ON |
||||
|
) |
||||
|
|
||||
|
add_dependencies(resources xercesc) |
||||
|
include_directories(${STORM_3RDPARTY_BINARY_DIR}/carl/include) |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}) |
||||
|
set(STORM_HAVE_CARL ON) |
||||
|
endif() |
||||
|
endif() |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## SMT-RAT |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
# No find routine yet |
||||
|
#find_package(smtrat QUIET) |
||||
|
# Not yet supported |
||||
|
set(smtrat_FOUND OFF) |
||||
|
set(STORM_HAVE_SMTRAT OFF) |
||||
|
if(smtrat_FOUND) |
||||
|
set(STORM_HAVE_SMTRAT ON) |
||||
|
message(STATUS "StoRM - Linking with smtrat.") |
||||
|
include_directories("${smtrat_INCLUDE_DIR}") |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${smtrat_LIBRARIES}) |
||||
|
endif() |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## GiNaC |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
find_package(GiNaC QUIET) |
||||
|
|
||||
|
if(GINAC_FOUND) |
||||
|
set(STORM_HAVE_GINAC ON) |
||||
|
message(STATUS "StoRM - Linking with GiNaC ${GINAC_VERSION_STRING}") |
||||
|
# Right now only link with GiNaC for carl |
||||
|
#include_directories("${GINAC_INCLUDE_DIR}") |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${GINAC_LIBRARIES}) |
||||
|
else() |
||||
|
set(STORM_HAVE_GINAC OFF) |
||||
|
#TODO: Check if CARL actually requires the use of GiNaC |
||||
|
endif() |
||||
|
|
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## gmp |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
# GMP is optional (unless MathSAT is used, see below) |
||||
|
find_package(GMP QUIET) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## MathSAT (optional) |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
if ("${MSAT_ROOT}" STREQUAL "") |
||||
|
set(ENABLE_MSAT OFF) |
||||
|
else() |
||||
|
set(ENABLE_MSAT ON) |
||||
|
endif() |
||||
|
|
||||
|
# MathSAT Defines |
||||
|
set(STORM_HAVE_MSAT ${ENABLE_MSAT}) |
||||
|
if (ENABLE_MSAT) |
||||
|
message (STATUS "StoRM - Linking with MathSAT") |
||||
|
link_directories("${MSAT_ROOT}/lib") |
||||
|
include_directories("${MSAT_ROOT}/include") |
||||
|
list(APPEND STORM_LINK_LIBRARIES "mathsat") |
||||
|
if(GMP_FOUND) |
||||
|
include_directories("${GMP_INCLUDE_DIR}") |
||||
|
list(APPEND STORM_LINK_LIBRARIES "gmp") |
||||
|
elseif(MPIR_FOUND) |
||||
|
include_directories("${GMP_INCLUDE_DIR}") |
||||
|
list(APPEND STORM_LINK_LIBRARIES "mpir" "mpirxx") |
||||
|
else(GMP_FOUND) |
||||
|
message(FATAL_ERROR "GMP is required for MathSAT, but was not found!") |
||||
|
endif(GMP_FOUND) |
||||
|
endif(ENABLE_MSAT) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Xerces |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
include(${STORM_3RDPARTY_SOURCE_DIR}/include_xerces.cmake) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Sylvan |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
ExternalProject_Add( |
ExternalProject_Add( |
||||
sylvan |
|
||||
DOWNLOAD_COMMAND "" |
|
||||
PREFIX "sylvan" |
|
||||
SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/sylvan |
|
||||
CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release |
|
||||
BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan" |
|
||||
INSTALL_COMMAND "" |
|
||||
INSTALL_DIR "${PROJECT_BINARY_DIR}/sylvan" |
|
||||
|
sylvan |
||||
|
DOWNLOAD_COMMAND "" |
||||
|
PREFIX "sylvan" |
||||
|
SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan |
||||
|
CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release |
||||
|
BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan" |
||||
|
BUILD_IN_SOURCE 0 |
||||
|
INSTALL_COMMAND "" |
||||
|
INSTALL_DIR "${STORM_3RDPARTY_BINARY_DIR}/sylvan" |
||||
|
LOG_CONFIGURE ON |
||||
|
LOG_BUILD ON |
||||
) |
) |
||||
ExternalProject_Get_Property(sylvan source_dir) |
ExternalProject_Get_Property(sylvan source_dir) |
||||
ExternalProject_Get_Property(sylvan binary_dir) |
ExternalProject_Get_Property(sylvan binary_dir) |
||||
set(Sylvan_INCLUDE_DIR "${source_dir}/src" PARENT_SCOPE) |
|
||||
set(Sylvan_LIBRARY "${binary_dir}/src/libsylvan.a" PARENT_SCOPE) |
|
||||
|
set(Sylvan_INCLUDE_DIR "${source_dir}/src") |
||||
|
set(Sylvan_LIBRARY "${binary_dir}/src/libsylvan.a") |
||||
|
|
||||
|
|
||||
|
|
||||
|
message(STATUS "StoRM - Using shipped version of sylvan") |
||||
|
message(STATUS "StoRM - Linking with sylvan") |
||||
|
include_directories("${Sylvan_INCLUDE_DIR}") |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${Sylvan_LIBRARY}) |
||||
|
add_dependencies(resources sylvan) |
||||
|
|
||||
|
if(${OPERATING_SYSTEM} MATCHES "Linux") |
||||
|
find_package(Hwloc QUIET REQUIRED) |
||||
|
if(Hwloc_FOUND) |
||||
|
message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}") |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) |
||||
|
else() |
||||
|
message(FATAL_ERROR "HWLOC is required but was not found.") |
||||
|
endif() |
||||
|
endif() |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Google Test gtest |
||||
|
## |
||||
|
############################################################# |
||||
ExternalProject_Add( |
ExternalProject_Add( |
||||
googletest |
googletest |
||||
#For downloads (may be useful later!) |
#For downloads (may be useful later!) |
||||
#SVN_REPOSITORY http://googletest.googlecode.com/svn/trunk/ |
#SVN_REPOSITORY http://googletest.googlecode.com/svn/trunk/ |
||||
#TIMEOUT 10 |
#TIMEOUT 10 |
||||
DOWNLOAD_COMMAND "" |
DOWNLOAD_COMMAND "" |
||||
SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/gtest-1.7.0" |
|
||||
|
SOURCE_DIR "${STORM_3RDPARTY_SOURCE_DIR}/gtest-1.7.0" |
||||
# Force the same output paths for debug and release builds so that |
# Force the same output paths for debug and release builds so that |
||||
# we know in which place the binaries end up when using the Xcode generator |
# we know in which place the binaries end up when using the Xcode generator |
||||
CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 |
|
||||
|
CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 |
||||
# Disable install step |
# Disable install step |
||||
INSTALL_COMMAND "" |
INSTALL_COMMAND "" |
||||
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0" |
|
||||
INSTALL_DIR "${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0" |
|
||||
|
BINARY_DIR "${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0" |
||||
|
INSTALL_DIR "${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0" |
||||
# Wrap download, configure and build steps in a script to log output |
# Wrap download, configure and build steps in a script to log output |
||||
LOG_CONFIGURE ON |
LOG_CONFIGURE ON |
||||
LOG_BUILD ON) |
LOG_BUILD ON) |
||||
|
|
||||
# Specify include dir |
# Specify include dir |
||||
ExternalProject_Get_Property(googletest source_dir) |
ExternalProject_Get_Property(googletest source_dir) |
||||
set(GTEST_INCLUDE_DIR ${source_dir}/include PARENT_SCOPE) |
|
||||
|
set(GTEST_INCLUDE_DIR ${source_dir}/include) |
||||
# Specify MainTest's link libraries |
# Specify MainTest's link libraries |
||||
ExternalProject_Get_Property(googletest binary_dir) |
ExternalProject_Get_Property(googletest binary_dir) |
||||
set(GTEST_LIBRARIES ${binary_dir}/libgtest.a ${binary_dir}/libgtest_main.a PARENT_SCOPE) |
|
||||
|
set(GTEST_LIBRARIES ${binary_dir}/libgtest.a ${binary_dir}/libgtest_main.a) |
||||
|
|
||||
|
add_dependencies(test-resources googletest) |
||||
|
list(APPEND STORM_TEST_LINK_LIBRARIES ${GTEST_LIBRARIES}) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Intel Threading Building Blocks (optional) |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
set(STORM_HAVE_INTELTBB OFF) |
||||
|
if (STORM_USE_INTELTBB) |
||||
|
# Point to shipped TBB directory |
||||
|
set(TBB_INSTALL_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/tbb42_20140122_merged-win-lin-mac") |
||||
|
find_package(TBB QUIET REQUIRED) |
||||
|
|
||||
|
if (TBB_FOUND) |
||||
|
message(STATUS "StoRM - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.") |
||||
|
message(STATUS "StoRM - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.") |
||||
|
set(STORM_HAVE_INTELTBB ON) |
||||
|
link_directories(${TBB_LIBRARY_DIRS}) |
||||
|
include_directories(${TBB_INCLUDE_DIRS}) |
||||
|
list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc) |
||||
|
else(TBB_FOUND) |
||||
|
message(FATAL_ERROR "StoRM - TBB was requested, but not found!") |
||||
|
endif(TBB_FOUND) |
||||
|
endif(STORM_USE_INTELTBB) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Threads |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
find_package(Threads QUIET REQUIRED) |
||||
|
if (NOT Threads_FOUND) |
||||
|
message(FATAL_ERROR "StoRM - Threads was requested, but not found!") |
||||
|
endif() |
||||
|
include_directories(${THREADS_INCLUDE_DIRS}) |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${CMAKE_THREAD_LIBS_INIT}) |
||||
|
if (STORM_USE_COTIRE) |
||||
|
target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT}) |
||||
|
endif(STORM_USE_COTIRE) |
||||
|
|
||||
|
if (MSVC) |
||||
|
# Add the DebugHelper DLL |
||||
|
set(CMAKE_CXX_STANDARD_LIBRARIES "${CMAKE_CXX_STANDARD_LIBRARIES} Dbghelp.lib") |
||||
|
target_link_libraries(storm "Dbghelp.lib") |
||||
|
endif(MSVC) |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## CUDA Library generation |
||||
|
## |
||||
|
############################################################# |
||||
|
|
||||
|
|
||||
|
if ("${CUDA_ROOT}" STREQUAL "") |
||||
|
set(ENABLE_CUDA OFF) |
||||
|
else() |
||||
|
set(ENABLE_CUDA ON) |
||||
|
endif() |
||||
|
|
||||
|
# CUDA Defines |
||||
|
if (ENABLE_CUDA) |
||||
|
set(STORM_CPP_CUDA_DEF "define") |
||||
|
else() |
||||
|
set(STORM_CPP_CUDA_DEF "undef") |
||||
|
endif() |
||||
|
|
||||
|
|
||||
|
# CUDA Defines |
||||
|
set(STORM_CPP_CUDAFORSTORM_DEF "undef") |
||||
|
|
||||
|
|
||||
|
if(ENABLE_CUDA) |
||||
|
|
||||
|
# Test for type alignment |
||||
|
try_run(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT |
||||
|
${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp" |
||||
|
COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR |
||||
|
) |
||||
|
if(NOT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT) |
||||
|
message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") |
||||
|
elseif(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT EQUAL 0) |
||||
|
message(STATUS "StoRM (CudaPlugin) - Result of Type Alignment Check: OK.") |
||||
|
else() |
||||
|
message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})") |
||||
|
endif() |
||||
|
|
||||
|
# Test for Float 64bit Alignment |
||||
|
try_run(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT |
||||
|
${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp" |
||||
|
COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR |
||||
|
) |
||||
|
if(NOT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT) |
||||
|
message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test float type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") |
||||
|
elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 2) |
||||
|
message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment active.") |
||||
|
set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "define") |
||||
|
elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 3) |
||||
|
message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment disabled.") |
||||
|
set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "undef") |
||||
|
else() |
||||
|
message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Float Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_FLOATALIGNMENT})") |
||||
|
endif() |
||||
|
# |
||||
|
# Make a version file containing the current version from git. |
||||
|
# |
||||
|
include(GetGitRevisionDescription) |
||||
|
git_describe_checkout(STORM_GIT_VERSION_STRING) |
||||
|
# Parse the git Tag into variables |
||||
|
string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CUDAPLUGIN_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}") |
||||
|
string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_MINOR "${STORM_GIT_VERSION_STRING}") |
||||
|
string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_PATCH "${STORM_GIT_VERSION_STRING}") |
||||
|
string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}") |
||||
|
string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_HASH "${STORM_GIT_VERSION_STRING}") |
||||
|
string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_CUDAPLUGIN_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}") |
||||
|
if ("${STORM_CUDAPLUGIN_VERSION_APPENDIX}" MATCHES "^.*dirty.*$") |
||||
|
set(STORM_CUDAPLUGIN_VERSION_DIRTY 1) |
||||
|
else() |
||||
|
set(STORM_CUDAPLUGIN_VERSION_DIRTY 0) |
||||
|
endif() |
||||
|
message(STATUS "StoRM (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})") |
||||
|
|
||||
|
|
||||
|
# Configure a header file to pass some of the CMake settings to the source code |
||||
|
configure_file ( |
||||
|
"${PROJECT_SOURCE_DIR}/cuda/storm-cudaplugin-config.h.in" |
||||
|
"${PROJECT_BINARY_DIR}/include/storm-cudaplugin-config.h" |
||||
|
) |
||||
|
|
||||
|
#create library |
||||
|
find_package(CUDA REQUIRED) |
||||
|
set(CUSP_INCLUDE_DIRS "${PROJECT_SOURCE_DIR}/resources/3rdparty/cusplibrary") |
||||
|
find_package(Cusp REQUIRED) |
||||
|
find_package(Thrust REQUIRED) |
||||
|
|
||||
|
set(STORM_CUDA_LIB_NAME "storm-cuda") |
||||
|
|
||||
|
file(GLOB_RECURSE STORM_CUDA_KERNEL_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.cu) |
||||
|
file(GLOB_RECURSE STORM_CUDA_HEADER_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.h) |
||||
|
|
||||
|
source_group(kernels FILES ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES}) |
||||
|
include_directories(${PROJECT_SOURCE_DIR}/cuda/kernels/) |
||||
|
|
||||
|
#set(CUDA_PROPAGATE_HOST_FLAGS OFF) |
||||
|
set(CUDA_NVCC_FLAGS "-arch=sm_30") |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## CUSP |
||||
|
## |
||||
|
############################################################# |
||||
|
if(CUSP_FOUND) |
||||
|
include_directories(${CUSP_INCLUDE_DIR}) |
||||
|
cuda_include_directories(${CUSP_INCLUDE_DIR}) |
||||
|
message(STATUS "StoRM (CudaPlugin) - Found CUSP Version ${CUSP_VERSION} in location ${CUSP_INCLUDE_DIR}") |
||||
|
else() |
||||
|
message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find CUSP!") |
||||
|
endif() |
||||
|
|
||||
|
############################################################# |
||||
|
## |
||||
|
## Thrust |
||||
|
## |
||||
|
############################################################# |
||||
|
if(THRUST_FOUND) |
||||
|
include_directories(${THRUST_INCLUDE_DIR}) |
||||
|
cuda_include_directories(${THRUST_INCLUDE_DIR}) |
||||
|
message(STATUS "StoRM (CudaPlugin) - Found Thrust Version ${THRUST_VERSION} in location ${THRUST_INCLUDE_DIR}") |
||||
|
else() |
||||
|
message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find Thrust! Check your CUDA installation.") |
||||
|
endif() |
||||
|
|
||||
|
include_directories(${CUDA_INCLUDE_DIRS}) |
||||
|
include_directories(${ADDITIONAL_INCLUDE_DIRS}) |
||||
|
|
||||
|
cuda_add_library(${STORM_CUDA_LIB_NAME} |
||||
|
${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES} |
||||
|
) |
||||
|
|
||||
|
message (STATUS "StoRM - Linking with CUDA") |
||||
|
list(APPEND STORM_LINK_LIBRARIES ${STORM_CUDA_LIB_NAME}) |
||||
|
include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") |
||||
|
endif() |
||||
@ -0,0 +1,4 @@ |
|||||
|
repo: 8a21fd850624c931e448cbcfb38168cb2717c790 |
||||
|
node: ce5a455b34c0a0ac3545a1497cb4a16c38ed90e8 |
||||
|
branch: default |
||||
|
tag: 3.3-beta1 |
||||
@ -0,0 +1,11 @@ |
|||||
|
[patterns] |
||||
|
*.sh = LF |
||||
|
*.MINPACK = CRLF |
||||
|
scripts/*.in = LF |
||||
|
debug/msvc/*.dat = CRLF |
||||
|
debug/msvc/*.natvis = CRLF |
||||
|
unsupported/test/mpreal/*.* = CRLF |
||||
|
** = native |
||||
|
|
||||
|
[repository] |
||||
|
native = LF |
||||
@ -0,0 +1,34 @@ |
|||||
|
syntax: glob |
||||
|
qrc_*cxx |
||||
|
*.orig |
||||
|
*.pyc |
||||
|
*.diff |
||||
|
diff |
||||
|
*.save |
||||
|
save |
||||
|
*.old |
||||
|
*.gmo |
||||
|
*.qm |
||||
|
core |
||||
|
core.* |
||||
|
*.bak |
||||
|
*~ |
||||
|
build* |
||||
|
*.moc.* |
||||
|
*.moc |
||||
|
ui_* |
||||
|
CMakeCache.txt |
||||
|
tags |
||||
|
.*.swp |
||||
|
activity.png |
||||
|
*.out |
||||
|
*.php* |
||||
|
*.log |
||||
|
*.orig |
||||
|
*.rej |
||||
|
log |
||||
|
patch |
||||
|
a |
||||
|
a.* |
||||
|
lapack/testing |
||||
|
lapack/reference |
||||
@ -0,0 +1,25 @@ |
|||||
|
2db9468678c6480c9633b6272ff0e3599d1e11a3 2.0-beta3 |
||||
|
375224817dce669b6fa31d920d4c895a63fabf32 2.0-beta1 |
||||
|
3b8120f077865e2a072e10f5be33e1d942b83a06 2.0-rc1 |
||||
|
19dfc0e7666bcee26f7a49eb42f39a0280a3485e 2.0-beta5 |
||||
|
7a7d8a9526f003ffa2430dfb0c2c535b5add3023 2.0-beta4 |
||||
|
7d14ad088ac23769c349518762704f0257f6a39b 2.0.1 |
||||
|
b9d48561579fd7d4c05b2aa42235dc9de6484bf2 2.0-beta6 |
||||
|
e17630a40408243cb1a51ad0fe3a99beb75b7450 before-hg-migration |
||||
|
eda654d4cda2210ce80719addcf854773e6dec5a 2.0.0 |
||||
|
ee9a7c468a9e73fab12f38f02bac24b07f29ed71 2.0-beta2 |
||||
|
d49097c25d8049e730c254a2fed725a240ce4858 after-hg-migration |
||||
|
655348878731bcb5d9bbe0854077b052e75e5237 actual-start-from-scratch |
||||
|
12a658962d4e6dfdc9a1c350fe7b69e36e70675c 3.0-beta1 |
||||
|
5c4180ad827b3f869b13b1d82f5a6ce617d6fcee 3.0-beta2 |
||||
|
7ae24ca6f3891d5ac58ddc7db60ad413c8d6ec35 3.0-beta3 |
||||
|
c40708b9088d622567fecc9208ad4a426621d364 3.0-beta4 |
||||
|
b6456624eae74f49ae8683d8e7b2882a2ca0342a 3.0-rc1 |
||||
|
a810d5dbab47acfe65b3350236efdd98f67d4d8a 3.1.0-alpha1 |
||||
|
304c88ca3affc16dd0b008b1104873986edd77af 3.1.0-alpha2 |
||||
|
920fc730b5930daae0a6dbe296d60ce2e3808215 3.1.0-beta1 |
||||
|
8383e883ebcc6f14695ff0b5e20bb631abab43fb 3.1.0-rc1 |
||||
|
bf4cb8c934fa3a79f45f1e629610f0225e93e493 3.1.0-rc2 |
||||
|
da195914abcc1d739027cbee7c52077aab30b336 3.2-beta1 |
||||
|
a8e0d153fc5e239ef8b06e3665f1f9e8cb8d49c8 before-evaluators |
||||
|
09a8e21866106b49c5dec1d6d543e5794e82efa0 3.3-alpha1 |
||||
@ -0,0 +1,491 @@ |
|||||
|
project(Eigen) |
||||
|
|
||||
|
cmake_minimum_required(VERSION 2.8.5) |
||||
|
|
||||
|
# guard against in-source builds |
||||
|
|
||||
|
if(${CMAKE_SOURCE_DIR} STREQUAL ${CMAKE_BINARY_DIR}) |
||||
|
message(FATAL_ERROR "In-source builds not allowed. Please make a new directory (called a build directory) and run CMake from there. You may need to remove CMakeCache.txt. ") |
||||
|
endif() |
||||
|
|
||||
|
# guard against bad build-type strings |
||||
|
|
||||
|
if (NOT CMAKE_BUILD_TYPE) |
||||
|
set(CMAKE_BUILD_TYPE "Release") |
||||
|
endif() |
||||
|
|
||||
|
string(TOLOWER "${CMAKE_BUILD_TYPE}" cmake_build_type_tolower) |
||||
|
if( NOT cmake_build_type_tolower STREQUAL "debug" |
||||
|
AND NOT cmake_build_type_tolower STREQUAL "release" |
||||
|
AND NOT cmake_build_type_tolower STREQUAL "relwithdebinfo") |
||||
|
message(FATAL_ERROR "Unknown build type \"${CMAKE_BUILD_TYPE}\". Allowed values are Debug, Release, RelWithDebInfo (case-insensitive).") |
||||
|
endif() |
||||
|
|
||||
|
|
||||
|
############################################################################# |
||||
|
# retrieve version infomation # |
||||
|
############################################################################# |
||||
|
|
||||
|
# automatically parse the version number |
||||
|
file(READ "${PROJECT_SOURCE_DIR}/Eigen/src/Core/util/Macros.h" _eigen_version_header) |
||||
|
string(REGEX MATCH "define[ \t]+EIGEN_WORLD_VERSION[ \t]+([0-9]+)" _eigen_world_version_match "${_eigen_version_header}") |
||||
|
set(EIGEN_WORLD_VERSION "${CMAKE_MATCH_1}") |
||||
|
string(REGEX MATCH "define[ \t]+EIGEN_MAJOR_VERSION[ \t]+([0-9]+)" _eigen_major_version_match "${_eigen_version_header}") |
||||
|
set(EIGEN_MAJOR_VERSION "${CMAKE_MATCH_1}") |
||||
|
string(REGEX MATCH "define[ \t]+EIGEN_MINOR_VERSION[ \t]+([0-9]+)" _eigen_minor_version_match "${_eigen_version_header}") |
||||
|
set(EIGEN_MINOR_VERSION "${CMAKE_MATCH_1}") |
||||
|
set(EIGEN_VERSION_NUMBER ${EIGEN_WORLD_VERSION}.${EIGEN_MAJOR_VERSION}.${EIGEN_MINOR_VERSION}) |
||||
|
|
||||
|
# if the mercurial program is absent, this will leave the EIGEN_HG_CHANGESET string empty, |
||||
|
# but won't stop CMake. |
||||
|
execute_process(COMMAND hg tip -R ${CMAKE_SOURCE_DIR} OUTPUT_VARIABLE EIGEN_HGTIP_OUTPUT) |
||||
|
execute_process(COMMAND hg branch -R ${CMAKE_SOURCE_DIR} OUTPUT_VARIABLE EIGEN_BRANCH_OUTPUT) |
||||
|
|
||||
|
# if this is the default (aka development) branch, extract the mercurial changeset number from the hg tip output... |
||||
|
if(EIGEN_BRANCH_OUTPUT MATCHES "default") |
||||
|
string(REGEX MATCH "^changeset: *[0-9]*:([0-9;a-f]+).*" EIGEN_HG_CHANGESET_MATCH "${EIGEN_HGTIP_OUTPUT}") |
||||
|
set(EIGEN_HG_CHANGESET "${CMAKE_MATCH_1}") |
||||
|
endif(EIGEN_BRANCH_OUTPUT MATCHES "default") |
||||
|
#...and show it next to the version number |
||||
|
if(EIGEN_HG_CHANGESET) |
||||
|
set(EIGEN_VERSION "${EIGEN_VERSION_NUMBER} (mercurial changeset ${EIGEN_HG_CHANGESET})") |
||||
|
else(EIGEN_HG_CHANGESET) |
||||
|
set(EIGEN_VERSION "${EIGEN_VERSION_NUMBER}") |
||||
|
endif(EIGEN_HG_CHANGESET) |
||||
|
|
||||
|
|
||||
|
include(CheckCXXCompilerFlag) |
||||
|
include(GNUInstallDirs) |
||||
|
|
||||
|
set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) |
||||
|
|
||||
|
############################################################################# |
||||
|
# find how to link to the standard libraries # |
||||
|
############################################################################# |
||||
|
|
||||
|
find_package(StandardMathLibrary) |
||||
|
|
||||
|
|
||||
|
set(EIGEN_TEST_CUSTOM_LINKER_FLAGS "" CACHE STRING "Additional linker flags when linking unit tests.") |
||||
|
set(EIGEN_TEST_CUSTOM_CXX_FLAGS "" CACHE STRING "Additional compiler flags when compiling unit tests.") |
||||
|
|
||||
|
set(EIGEN_STANDARD_LIBRARIES_TO_LINK_TO "") |
||||
|
|
||||
|
if(NOT STANDARD_MATH_LIBRARY_FOUND) |
||||
|
|
||||
|
message(FATAL_ERROR |
||||
|
"Can't link to the standard math library. Please report to the Eigen developers, telling them about your platform.") |
||||
|
|
||||
|
else() |
||||
|
|
||||
|
if(EIGEN_STANDARD_LIBRARIES_TO_LINK_TO) |
||||
|
set(EIGEN_STANDARD_LIBRARIES_TO_LINK_TO "${EIGEN_STANDARD_LIBRARIES_TO_LINK_TO} ${STANDARD_MATH_LIBRARY}") |
||||
|
else() |
||||
|
set(EIGEN_STANDARD_LIBRARIES_TO_LINK_TO "${STANDARD_MATH_LIBRARY}") |
||||
|
endif() |
||||
|
|
||||
|
endif() |
||||
|
|
||||
|
if(EIGEN_STANDARD_LIBRARIES_TO_LINK_TO) |
||||
|
message(STATUS "Standard libraries to link to explicitly: ${EIGEN_STANDARD_LIBRARIES_TO_LINK_TO}") |
||||
|
else() |
||||
|
message(STATUS "Standard libraries to link to explicitly: none") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_BUILD_BTL "Build benchmark suite" OFF) |
||||
|
if(NOT WIN32) |
||||
|
option(EIGEN_BUILD_PKGCONFIG "Build pkg-config .pc file for Eigen" ON) |
||||
|
endif(NOT WIN32) |
||||
|
|
||||
|
set(CMAKE_INCLUDE_CURRENT_DIR ON) |
||||
|
|
||||
|
option(EIGEN_SPLIT_LARGE_TESTS "Split large tests into smaller executables" ON) |
||||
|
|
||||
|
option(EIGEN_DEFAULT_TO_ROW_MAJOR "Use row-major as default matrix storage order" OFF) |
||||
|
if(EIGEN_DEFAULT_TO_ROW_MAJOR) |
||||
|
add_definitions("-DEIGEN_DEFAULT_TO_ROW_MAJOR") |
||||
|
endif() |
||||
|
|
||||
|
set(EIGEN_TEST_MAX_SIZE "320" CACHE STRING "Maximal matrix/vector size, default is 320") |
||||
|
|
||||
|
macro(ei_add_cxx_compiler_flag FLAG) |
||||
|
string(REGEX REPLACE "-" "" SFLAG1 ${FLAG}) |
||||
|
string(REGEX REPLACE "\\+" "p" SFLAG ${SFLAG1}) |
||||
|
check_cxx_compiler_flag(${FLAG} COMPILER_SUPPORT_${SFLAG}) |
||||
|
if(COMPILER_SUPPORT_${SFLAG}) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${FLAG}") |
||||
|
endif() |
||||
|
endmacro(ei_add_cxx_compiler_flag) |
||||
|
|
||||
|
if(NOT MSVC) |
||||
|
# We assume that other compilers are partly compatible with GNUCC |
||||
|
|
||||
|
# clang outputs some warnings for unknwon flags that are not caught by check_cxx_compiler_flag |
||||
|
# adding -Werror turns such warnings into errors |
||||
|
check_cxx_compiler_flag("-Werror" COMPILER_SUPPORT_WERROR) |
||||
|
if(COMPILER_SUPPORT_WERROR) |
||||
|
set(CMAKE_REQUIRED_FLAGS "-Werror") |
||||
|
endif() |
||||
|
|
||||
|
ei_add_cxx_compiler_flag("-pedantic") |
||||
|
ei_add_cxx_compiler_flag("-Wall") |
||||
|
ei_add_cxx_compiler_flag("-Wextra") |
||||
|
#ei_add_cxx_compiler_flag("-Weverything") # clang |
||||
|
|
||||
|
ei_add_cxx_compiler_flag("-Wundef") |
||||
|
ei_add_cxx_compiler_flag("-Wcast-align") |
||||
|
ei_add_cxx_compiler_flag("-Wchar-subscripts") |
||||
|
ei_add_cxx_compiler_flag("-Wnon-virtual-dtor") |
||||
|
ei_add_cxx_compiler_flag("-Wunused-local-typedefs") |
||||
|
ei_add_cxx_compiler_flag("-Wpointer-arith") |
||||
|
ei_add_cxx_compiler_flag("-Wwrite-strings") |
||||
|
ei_add_cxx_compiler_flag("-Wformat-security") |
||||
|
ei_add_cxx_compiler_flag("-Wshorten-64-to-32") |
||||
|
ei_add_cxx_compiler_flag("-Wenum-conversion") |
||||
|
ei_add_cxx_compiler_flag("-Wc++11-extensions") |
||||
|
|
||||
|
# -Wshadow is insanely too strict with gcc, hopefully it will become usable with gcc 6 |
||||
|
# if(NOT CMAKE_COMPILER_IS_GNUCXX OR (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER "5.0.0")) |
||||
|
if(NOT CMAKE_COMPILER_IS_GNUCXX) |
||||
|
ei_add_cxx_compiler_flag("-Wshadow") |
||||
|
endif() |
||||
|
|
||||
|
ei_add_cxx_compiler_flag("-Wno-psabi") |
||||
|
ei_add_cxx_compiler_flag("-Wno-variadic-macros") |
||||
|
ei_add_cxx_compiler_flag("-Wno-long-long") |
||||
|
|
||||
|
ei_add_cxx_compiler_flag("-fno-check-new") |
||||
|
ei_add_cxx_compiler_flag("-fno-common") |
||||
|
ei_add_cxx_compiler_flag("-fstrict-aliasing") |
||||
|
ei_add_cxx_compiler_flag("-wd981") # disable ICC's "operands are evaluated in unspecified order" remark |
||||
|
ei_add_cxx_compiler_flag("-wd2304") # disbale ICC's "warning #2304: non-explicit constructor with single argument may cause implicit type conversion" produced by -Wnon-virtual-dtor |
||||
|
|
||||
|
|
||||
|
# The -ansi flag must be added last, otherwise it is also used as a linker flag by check_cxx_compiler_flag making it fails |
||||
|
# Moreover we should not set both -strict-ansi and -ansi |
||||
|
check_cxx_compiler_flag("-strict-ansi" COMPILER_SUPPORT_STRICTANSI) |
||||
|
ei_add_cxx_compiler_flag("-Qunused-arguments") # disable clang warning: argument unused during compilation: '-ansi' |
||||
|
|
||||
|
if(COMPILER_SUPPORT_STRICTANSI) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -strict-ansi") |
||||
|
else() |
||||
|
ei_add_cxx_compiler_flag("-ansi") |
||||
|
endif() |
||||
|
|
||||
|
if(ANDROID_NDK) |
||||
|
ei_add_cxx_compiler_flag("-pie") |
||||
|
ei_add_cxx_compiler_flag("-fPIE") |
||||
|
endif() |
||||
|
|
||||
|
set(CMAKE_REQUIRED_FLAGS "") |
||||
|
|
||||
|
option(EIGEN_TEST_SSE2 "Enable/Disable SSE2 in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_SSE2) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -msse2") |
||||
|
message(STATUS "Enabling SSE2 in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_SSE3 "Enable/Disable SSE3 in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_SSE3) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -msse3") |
||||
|
message(STATUS "Enabling SSE3 in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_SSSE3 "Enable/Disable SSSE3 in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_SSSE3) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mssse3") |
||||
|
message(STATUS "Enabling SSSE3 in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_SSE4_1 "Enable/Disable SSE4.1 in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_SSE4_1) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -msse4.1") |
||||
|
message(STATUS "Enabling SSE4.1 in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_SSE4_2 "Enable/Disable SSE4.2 in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_SSE4_2) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -msse4.2") |
||||
|
message(STATUS "Enabling SSE4.2 in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_AVX "Enable/Disable AVX in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_AVX) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mavx") |
||||
|
message(STATUS "Enabling AVX in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_FMA "Enable/Disable FMA in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_FMA AND NOT EIGEN_TEST_NEON) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mfma") |
||||
|
message(STATUS "Enabling FMA in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_ALTIVEC "Enable/Disable AltiVec in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_ALTIVEC) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -maltivec -mabi=altivec") |
||||
|
message(STATUS "Enabling AltiVec in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_VSX "Enable/Disable VSX in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_VSX) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -m64 -mvsx") |
||||
|
message(STATUS "Enabling VSX in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_NEON "Enable/Disable Neon in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_NEON) |
||||
|
if(EIGEN_TEST_FMA) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mfpu=neon-vfpv4") |
||||
|
else() |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mfpu=neon") |
||||
|
endif() |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mfloat-abi=softfp") |
||||
|
message(STATUS "Enabling NEON in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_NEON64 "Enable/Disable Neon in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_NEON64) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS}") |
||||
|
message(STATUS "Enabling NEON in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
|
||||
|
|
||||
|
check_cxx_compiler_flag("-fopenmp" COMPILER_SUPPORT_OPENMP) |
||||
|
if(COMPILER_SUPPORT_OPENMP) |
||||
|
option(EIGEN_TEST_OPENMP "Enable/Disable OpenMP in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_OPENMP) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fopenmp") |
||||
|
message(STATUS "Enabling OpenMP in tests/examples") |
||||
|
endif() |
||||
|
endif() |
||||
|
|
||||
|
else(NOT MSVC) |
||||
|
|
||||
|
# C4127 - conditional expression is constant |
||||
|
# C4714 - marked as __forceinline not inlined (I failed to deactivate it selectively) |
||||
|
# We can disable this warning in the unit tests since it is clear that it occurs |
||||
|
# because we are oftentimes returning objects that have a destructor or may |
||||
|
# throw exceptions - in particular in the unit tests we are throwing extra many |
||||
|
# exceptions to cover indexing errors. |
||||
|
# C4505 - unreferenced local function has been removed (impossible to deactive selectively) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} /EHsc /wd4127 /wd4505 /wd4714") |
||||
|
|
||||
|
# replace all /Wx by /W4 |
||||
|
string(REGEX REPLACE "/W[0-9]" "/W4" CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS}") |
||||
|
|
||||
|
check_cxx_compiler_flag("/openmp" COMPILER_SUPPORT_OPENMP) |
||||
|
if(COMPILER_SUPPORT_OPENMP) |
||||
|
option(EIGEN_TEST_OPENMP "Enable/Disable OpenMP in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_OPENMP) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} /openmp") |
||||
|
message(STATUS "Enabling OpenMP in tests/examples") |
||||
|
endif() |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_SSE2 "Enable/Disable SSE2 in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_SSE2) |
||||
|
if(NOT CMAKE_CL_64) |
||||
|
# arch is not supported on 64 bit systems, SSE is enabled automatically. |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} /arch:SSE2") |
||||
|
endif(NOT CMAKE_CL_64) |
||||
|
message(STATUS "Enabling SSE2 in tests/examples") |
||||
|
endif(EIGEN_TEST_SSE2) |
||||
|
endif(NOT MSVC) |
||||
|
|
||||
|
option(EIGEN_TEST_NO_EXPLICIT_VECTORIZATION "Disable explicit vectorization in tests/examples" OFF) |
||||
|
option(EIGEN_TEST_X87 "Force using X87 instructions. Implies no vectorization." OFF) |
||||
|
option(EIGEN_TEST_32BIT "Force generating 32bit code." OFF) |
||||
|
|
||||
|
if(EIGEN_TEST_X87) |
||||
|
set(EIGEN_TEST_NO_EXPLICIT_VECTORIZATION ON) |
||||
|
if(CMAKE_COMPILER_IS_GNUCXX) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mfpmath=387") |
||||
|
message(STATUS "Forcing use of x87 instructions in tests/examples") |
||||
|
else() |
||||
|
message(STATUS "EIGEN_TEST_X87 ignored on your compiler") |
||||
|
endif() |
||||
|
endif() |
||||
|
|
||||
|
if(EIGEN_TEST_32BIT) |
||||
|
if(CMAKE_COMPILER_IS_GNUCXX) |
||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -m32") |
||||
|
message(STATUS "Forcing generation of 32-bit code in tests/examples") |
||||
|
else() |
||||
|
message(STATUS "EIGEN_TEST_32BIT ignored on your compiler") |
||||
|
endif() |
||||
|
endif() |
||||
|
|
||||
|
if(EIGEN_TEST_NO_EXPLICIT_VECTORIZATION) |
||||
|
add_definitions(-DEIGEN_DONT_VECTORIZE=1) |
||||
|
message(STATUS "Disabling vectorization in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_NO_EXPLICIT_ALIGNMENT "Disable explicit alignment (hence vectorization) in tests/examples" OFF) |
||||
|
if(EIGEN_TEST_NO_EXPLICIT_ALIGNMENT) |
||||
|
add_definitions(-DEIGEN_DONT_ALIGN=1) |
||||
|
message(STATUS "Disabling alignment in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_NO_EXCEPTIONS "Disables C++ exceptions" OFF) |
||||
|
if(EIGEN_TEST_NO_EXCEPTIONS) |
||||
|
ei_add_cxx_compiler_flag("-fno-exceptions") |
||||
|
message(STATUS "Disabling exceptions in tests/examples") |
||||
|
endif() |
||||
|
|
||||
|
option(EIGEN_TEST_CXX11 "Enable testing with C++11 and C++11 features (e.g. Tensor module)." OFF) |
||||
|
|
||||
|
include_directories(${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_BINARY_DIR}) |
||||
|
|
||||
|
# Backward compatibility support for EIGEN_INCLUDE_INSTALL_DIR |
||||
|
if(EIGEN_INCLUDE_INSTALL_DIR) |
||||
|
message(WARNING "EIGEN_INCLUDE_INSTALL_DIR is deprecated. Use INCLUDE_INSTALL_DIR instead.") |
||||
|
endif() |
||||
|
|
||||
|
if(EIGEN_INCLUDE_INSTALL_DIR AND NOT INCLUDE_INSTALL_DIR) |
||||
|
set(INCLUDE_INSTALL_DIR ${EIGEN_INCLUDE_INSTALL_DIR} |
||||
|
CACHE PATH "The directory relative to CMAKE_PREFIX_PATH where Eigen header files are installed") |
||||
|
else() |
||||
|
set(INCLUDE_INSTALL_DIR |
||||
|
"${CMAKE_INSTALL_INCLUDEDIR}/eigen3" |
||||
|
CACHE PATH "The directory relative to CMAKE_PREFIX_PATH where Eigen header files are installed" |
||||
|
) |
||||
|
endif() |
||||
|
set(CMAKEPACKAGE_INSTALL_DIR |
||||
|
"${CMAKE_INSTALL_LIBDIR}/cmake/eigen3" |
||||
|
CACHE PATH "The directory relative to CMAKE_PREFIX_PATH where Eigen3Config.cmake is installed" |
||||
|
) |
||||
|
set(PKGCONFIG_INSTALL_DIR |
||||
|
"${CMAKE_INSTALL_DATADIR}/pkgconfig" |
||||
|
CACHE PATH "The directory relative to CMAKE_PREFIX_PATH where eigen3.pc is installed" |
||||
|
) |
||||
|
|
||||
|
|
||||
|
# similar to set_target_properties but append the property instead of overwriting it |
||||
|
macro(ei_add_target_property target prop value) |
||||
|
|
||||
|
get_target_property(previous ${target} ${prop}) |
||||
|
# if the property wasn't previously set, ${previous} is now "previous-NOTFOUND" which cmake allows catching with plain if() |
||||
|
if(NOT previous) |
||||
|
set(previous "") |
||||
|
endif(NOT previous) |
||||
|
set_target_properties(${target} PROPERTIES ${prop} "${previous} ${value}") |
||||
|
endmacro(ei_add_target_property) |
||||
|
|
||||
|
install(FILES |
||||
|
signature_of_eigen3_matrix_library |
||||
|
DESTINATION ${INCLUDE_INSTALL_DIR} COMPONENT Devel |
||||
|
) |
||||
|
|
||||
|
if(EIGEN_BUILD_PKGCONFIG) |
||||
|
configure_file(eigen3.pc.in eigen3.pc @ONLY) |
||||
|
install(FILES ${CMAKE_CURRENT_BINARY_DIR}/eigen3.pc |
||||
|
DESTINATION ${PKGCONFIG_INSTALL_DIR} |
||||
|
) |
||||
|
endif(EIGEN_BUILD_PKGCONFIG) |
||||
|
|
||||
|
add_subdirectory(Eigen) |
||||
|
|
||||
|
add_subdirectory(doc EXCLUDE_FROM_ALL) |
||||
|
|
||||
|
include(EigenConfigureTesting) |
||||
|
|
||||
|
# fixme, not sure this line is still needed: |
||||
|
enable_testing() # must be called from the root CMakeLists, see man page |
||||
|
|
||||
|
|
||||
|
if(EIGEN_LEAVE_TEST_IN_ALL_TARGET) |
||||
|
add_subdirectory(test) # can't do EXCLUDE_FROM_ALL here, breaks CTest |
||||
|
else() |
||||
|
add_subdirectory(test EXCLUDE_FROM_ALL) |
||||
|
endif() |
||||
|
|
||||
|
if(EIGEN_LEAVE_TEST_IN_ALL_TARGET) |
||||
|
add_subdirectory(blas) |
||||
|
add_subdirectory(lapack) |
||||
|
else() |
||||
|
add_subdirectory(blas EXCLUDE_FROM_ALL) |
||||
|
add_subdirectory(lapack EXCLUDE_FROM_ALL) |
||||
|
endif() |
||||
|
|
||||
|
add_subdirectory(unsupported) |
||||
|
|
||||
|
add_subdirectory(demos EXCLUDE_FROM_ALL) |
||||
|
|
||||
|
# must be after test and unsupported, for configuring buildtests.in |
||||
|
add_subdirectory(scripts EXCLUDE_FROM_ALL) |
||||
|
|
||||
|
# TODO: consider also replacing EIGEN_BUILD_BTL by a custom target "make btl"? |
||||
|
if(EIGEN_BUILD_BTL) |
||||
|
add_subdirectory(bench/btl EXCLUDE_FROM_ALL) |
||||
|
endif(EIGEN_BUILD_BTL) |
||||
|
|
||||
|
if(NOT WIN32) |
||||
|
add_subdirectory(bench/spbench EXCLUDE_FROM_ALL) |
||||
|
endif(NOT WIN32) |
||||
|
|
||||
|
configure_file(scripts/cdashtesting.cmake.in cdashtesting.cmake @ONLY) |
||||
|
|
||||
|
ei_testing_print_summary() |
||||
|
|
||||
|
message(STATUS "") |
||||
|
message(STATUS "Configured Eigen ${EIGEN_VERSION_NUMBER}") |
||||
|
message(STATUS "") |
||||
|
|
||||
|
option(EIGEN_FAILTEST "Enable failtests." OFF) |
||||
|
if(EIGEN_FAILTEST) |
||||
|
add_subdirectory(failtest) |
||||
|
endif() |
||||
|
|
||||
|
string(TOLOWER "${CMAKE_GENERATOR}" cmake_generator_tolower) |
||||
|
if(cmake_generator_tolower MATCHES "makefile") |
||||
|
message(STATUS "Some things you can do now:") |
||||
|
message(STATUS "--------------+--------------------------------------------------------------") |
||||
|
message(STATUS "Command | Description") |
||||
|
message(STATUS "--------------+--------------------------------------------------------------") |
||||
|
message(STATUS "make install | Install Eigen. Headers will be installed to:") |
||||
|
message(STATUS " | <CMAKE_INSTALL_PREFIX>/<INCLUDE_INSTALL_DIR>") |
||||
|
message(STATUS " | Using the following values:") |
||||
|
message(STATUS " | CMAKE_INSTALL_PREFIX: ${CMAKE_INSTALL_PREFIX}") |
||||
|
message(STATUS " | INCLUDE_INSTALL_DIR: ${INCLUDE_INSTALL_DIR}") |
||||
|
message(STATUS " | Change the install location of Eigen headers using:") |
||||
|
message(STATUS " | cmake . -DCMAKE_INSTALL_PREFIX=yourprefix") |
||||
|
message(STATUS " | Or:") |
||||
|
message(STATUS " | cmake . -DINCLUDE_INSTALL_DIR=yourdir") |
||||
|
message(STATUS "make doc | Generate the API documentation, requires Doxygen & LaTeX") |
||||
|
message(STATUS "make check | Build and run the unit-tests. Read this page:") |
||||
|
message(STATUS " | http://eigen.tuxfamily.org/index.php?title=Tests") |
||||
|
message(STATUS "make blas | Build BLAS library (not the same thing as Eigen)") |
||||
|
message(STATUS "make uninstall| Removes files installed by make install") |
||||
|
message(STATUS "--------------+--------------------------------------------------------------") |
||||
|
else() |
||||
|
message(STATUS "To build/run the unit tests, read this page:") |
||||
|
message(STATUS " http://eigen.tuxfamily.org/index.php?title=Tests") |
||||
|
endif() |
||||
|
|
||||
|
message(STATUS "") |
||||
|
|
||||
|
|
||||
|
set ( EIGEN_VERSION_STRING ${EIGEN_VERSION_NUMBER} ) |
||||
|
set ( EIGEN_VERSION_MAJOR ${EIGEN_WORLD_VERSION} ) |
||||
|
set ( EIGEN_VERSION_MINOR ${EIGEN_MAJOR_VERSION} ) |
||||
|
set ( EIGEN_VERSION_PATCH ${EIGEN_MINOR_VERSION} ) |
||||
|
set ( EIGEN_DEFINITIONS "") |
||||
|
set ( EIGEN_INCLUDE_DIR "${CMAKE_INSTALL_PREFIX}/${INCLUDE_INSTALL_DIR}" ) |
||||
|
set ( EIGEN_INCLUDE_DIRS ${EIGEN_INCLUDE_DIR} ) |
||||
|
set ( EIGEN_ROOT_DIR ${CMAKE_INSTALL_PREFIX} ) |
||||
|
|
||||
|
configure_file ( ${CMAKE_CURRENT_SOURCE_DIR}/cmake/Eigen3Config.cmake.in |
||||
|
${CMAKE_CURRENT_BINARY_DIR}/Eigen3Config.cmake |
||||
|
@ONLY ESCAPE_QUOTES |
||||
|
) |
||||
|
|
||||
|
install ( FILES ${CMAKE_CURRENT_SOURCE_DIR}/cmake/UseEigen3.cmake |
||||
|
${CMAKE_CURRENT_BINARY_DIR}/Eigen3Config.cmake |
||||
|
DESTINATION ${CMAKEPACKAGE_INSTALL_DIR} |
||||
|
) |
||||
|
|
||||
|
# Add uninstall target |
||||
|
add_custom_target ( uninstall |
||||
|
COMMAND ${CMAKE_COMMAND} -P ${CMAKE_CURRENT_SOURCE_DIR}/cmake/EigenUninstall.cmake) |
||||
Some files were not shown because too many files changed in this diff
Write
Preview
Loading…
Cancel
Save
Reference in new issue