sjunges
9 years ago
2546 changed files with 431264 additions and 7858 deletions
-
527CMakeLists.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
-
576resources/3rdparty/CMakeLists.txt
-
1resources/3rdparty/carl
-
0resources/3rdparty/cpplint/cpplint.py
-
1resources/3rdparty/cudd-3.0.0/configure
-
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
-
26resources/3rdparty/eigen-3.3-beta1/COPYING.BSD
-
674resources/3rdparty/eigen-3.3-beta1/COPYING.GPL
@ -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 |
|||
@ -1,83 +1,555 @@ |
|||
add_custom_target(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( |
|||
cudd3 |
|||
DOWNLOAD_COMMAND "" |
|||
SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0 |
|||
PREFIX ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0 |
|||
UPDATE_COMMAND autoreconf |
|||
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( |
|||
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 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( |
|||
googletest |
|||
#For downloads (may be useful later!) |
|||
#SVN_REPOSITORY http://googletest.googlecode.com/svn/trunk/ |
|||
#TIMEOUT 10 |
|||
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 |
|||
# 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 |
|||
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 |
|||
LOG_CONFIGURE ON |
|||
LOG_BUILD ON) |
|||
|
|||
# Specify include 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 |
|||
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) |
|||
@ -0,0 +1,26 @@ |
|||
/* |
|||
Copyright (c) 2011, Intel Corporation. All rights reserved. |
|||
|
|||
Redistribution and use in source and binary forms, with or without modification, |
|||
are permitted provided that the following conditions are met: |
|||
|
|||
* Redistributions of source code must retain the above copyright notice, this |
|||
list of conditions and the following disclaimer. |
|||
* Redistributions in binary form must reproduce the above copyright notice, |
|||
this list of conditions and the following disclaimer in the documentation |
|||
and/or other materials provided with the distribution. |
|||
* Neither the name of Intel Corporation nor the names of its contributors may |
|||
be used to endorse or promote products derived from this software without |
|||
specific prior written permission. |
|||
|
|||
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND |
|||
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED |
|||
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE |
|||
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR |
|||
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES |
|||
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
|||
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON |
|||
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT |
|||
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS |
|||
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
|||
*/ |
|||
@ -0,0 +1,674 @@ |
|||
GNU GENERAL PUBLIC LICENSE |
|||
Version 3, 29 June 2007 |
|||
|
|||
Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/> |
|||
Everyone is permitted to copy and distribute verbatim copies |
|||
of this license document, but changing it is not allowed. |
|||
|
|||
Preamble |
|||
|
|||
The GNU General Public License is a free, copyleft license for |
|||
software and other kinds of works. |
|||
|
|||
The licenses for most software and other practical works are designed |
|||
to take away your freedom to share and change the works. By contrast, |
|||
the GNU General Public License is intended to guarantee your freedom to |
|||
share and change all versions of a program--to make sure it remains free |
|||
software for all its users. We, the Free Software Foundation, use the |
|||
GNU General Public License for most of our software; it applies also to |
|||
any other work released this way by its authors. You can apply it to |
|||
your programs, too. |
|||
|
|||
When we speak of free software, we are referring to freedom, not |
|||
price. Our General Public Licenses are designed to make sure that you |
|||
have the freedom to distribute copies of free software (and charge for |
|||
them if you wish), that you receive source code or can get it if you |
|||
want it, that you can change the software or use pieces of it in new |
|||
free programs, and that you know you can do these things. |
|||
|
|||
To protect your rights, we need to prevent others from denying you |
|||
these rights or asking you to surrender the rights. Therefore, you have |
|||
certain responsibilities if you distribute copies of the software, or if |
|||
you modify it: responsibilities to respect the freedom of others. |
|||
|
|||
For example, if you distribute copies of such a program, whether |
|||
gratis or for a fee, you must pass on to the recipients the same |
|||
freedoms that you received. You must make sure that they, too, receive |
|||
or can get the source code. And you must show them these terms so they |
|||
know their rights. |
|||
|
|||
Developers that use the GNU GPL protect your rights with two steps: |
|||
(1) assert copyright on the software, and (2) offer you this License |
|||
giving you legal permission to copy, distribute and/or modify it. |
|||
|
|||
For the developers' and authors' protection, the GPL clearly explains |
|||
that there is no warranty for this free software. For both users' and |
|||
authors' sake, the GPL requires that modified versions be marked as |
|||
changed, so that their problems will not be attributed erroneously to |
|||
authors of previous versions. |
|||
|
|||
Some devices are designed to deny users access to install or run |
|||
modified versions of the software inside them, although the manufacturer |
|||
can do so. This is fundamentally incompatible with the aim of |
|||
protecting users' freedom to change the software. The systematic |
|||
pattern of such abuse occurs in the area of products for individuals to |
|||
use, which is precisely where it is most unacceptable. Therefore, we |
|||
have designed this version of the GPL to prohibit the practice for those |
|||
products. If such problems arise substantially in other domains, we |
|||
stand ready to extend this provision to those domains in future versions |
|||
of the GPL, as needed to protect the freedom of users. |
|||
|
|||
Finally, every program is threatened constantly by software patents. |
|||
States should not allow patents to restrict development and use of |
|||
software on general-purpose computers, but in those that do, we wish to |
|||
avoid the special danger that patents applied to a free program could |
|||
make it effectively proprietary. To prevent this, the GPL assures that |
|||
patents cannot be used to render the program non-free. |
|||
|
|||
The precise terms and conditions for copying, distribution and |
|||
modification follow. |
|||
|
|||
TERMS AND CONDITIONS |
|||
|
|||
0. Definitions. |
|||
|
|||
"This License" refers to version 3 of the GNU General Public License. |
|||
|
|||
"Copyright" also means copyright-like laws that apply to other kinds of |
|||
works, such as semiconductor masks. |
|||
|
|||
"The Program" refers to any copyrightable work licensed under this |
|||
License. Each licensee is addressed as "you". "Licensees" and |
|||
"recipients" may be individuals or organizations. |
|||
|
|||
To "modify" a work means to copy from or adapt all or part of the work |
|||
in a fashion requiring copyright permission, other than the making of an |
|||
exact copy. The resulting work is called a "modified version" of the |
|||
earlier work or a work "based on" the earlier work. |
|||
|
|||
A "covered work" means either the unmodified Program or a work based |
|||
on the Program. |
|||
|
|||
To "propagate" a work means to do anything with it that, without |
|||
permission, would make you directly or secondarily liable for |
|||
infringement under applicable copyright law, except executing it on a |
|||
computer or modifying a private copy. Propagation includes copying, |
|||
distribution (with or without modification), making available to the |
|||
public, and in some countries other activities as well. |
|||
|
|||
To "convey" a work means any kind of propagation that enables other |
|||
parties to make or receive copies. Mere interaction with a user through |
|||
a computer network, with no transfer of a copy, is not conveying. |
|||
|
|||
An interactive user interface displays "Appropriate Legal Notices" |
|||
to the extent that it includes a convenient and prominently visible |
|||
feature that (1) displays an appropriate copyright notice, and (2) |
|||
tells the user that there is no warranty for the work (except to the |
|||
extent that warranties are provided), that licensees may convey the |
|||
work under this License, and how to view a copy of this License. If |
|||
the interface presents a list of user commands or options, such as a |
|||
menu, a prominent item in the list meets this criterion. |
|||
|
|||
1. Source Code. |
|||
|
|||
The "source code" for a work means the preferred form of the work |
|||
for making modifications to it. "Object code" means any non-source |
|||
form of a work. |
|||
|
|||
A "Standard Interface" means an interface that either is an official |
|||
standard defined by a recognized standards body, or, in the case of |
|||
interfaces specified for a particular programming language, one that |
|||
is widely used among developers working in that language. |
|||
|
|||
The "System Libraries" of an executable work include anything, other |
|||
than the work as a whole, that (a) is included in the normal form of |
|||
packaging a Major Component, but which is not part of that Major |
|||
Component, and (b) serves only to enable use of the work with that |
|||
Major Component, or to implement a Standard Interface for which an |
|||
implementation is available to the public in source code form. A |
|||
"Major Component", in this context, means a major essential component |
|||
(kernel, window system, and so on) of the specific operating system |
|||
(if any) on which the executable work runs, or a compiler used to |
|||
produce the work, or an object code interpreter used to run it. |
|||
|
|||
The "Corresponding Source" for a work in object code form means all |
|||
the source code needed to generate, install, and (for an executable |
|||
work) run the object code and to modify the work, including scripts to |
|||
control those activities. However, it does not include the work's |
|||
System Libraries, or general-purpose tools or generally available free |
|||
programs which are used unmodified in performing those activities but |
|||
which are not part of the work. For example, Corresponding Source |
|||
includes interface definition files associated with source files for |
|||
the work, and the source code for shared libraries and dynamically |
|||
linked subprograms that the work is specifically designed to require, |
|||
such as by intimate data communication or control flow between those |
|||
subprograms and other parts of the work. |
|||
|
|||
The Corresponding Source need not include anything that users |
|||
can regenerate automatically from other parts of the Corresponding |
|||
Source. |
|||
|
|||
The Corresponding Source for a work in source code form is that |
|||
same work. |
|||
|
|||
2. Basic Permissions. |
|||
|
|||
All rights granted under this License are granted for the term of |
|||
copyright on the Program, and are irrevocable provided the stated |
|||
conditions are met. This License explicitly affirms your unlimited |
|||
permission to run the unmodified Program. The output from running a |
|||
covered work is covered by this License only if the output, given its |
|||
content, constitutes a covered work. This License acknowledges your |
|||
rights of fair use or other equivalent, as provided by copyright law. |
|||
|
|||
You may make, run and propagate covered works that you do not |
|||
convey, without conditions so long as your license otherwise remains |
|||
in force. You may convey covered works to others for the sole purpose |
|||
of having them make modifications exclusively for you, or provide you |
|||
with facilities for running those works, provided that you comply with |
|||
the terms of this License in conveying all material for which you do |
|||
not control copyright. Those thus making or running the covered works |
|||
for you must do so exclusively on your behalf, under your direction |
|||
and control, on terms that prohibit them from making any copies of |
|||
your copyrighted material outside their relationship with you. |
|||
|
|||
Conveying under any other circumstances is permitted solely under |
|||
the conditions stated below. Sublicensing is not allowed; section 10 |
|||
makes it unnecessary. |
|||
|
|||
3. Protecting Users' Legal Rights From Anti-Circumvention Law. |
|||
|
|||
No covered work shall be deemed part of an effective technological |
|||
measure under any applicable law fulfilling obligations under article |
|||
11 of the WIPO copyright treaty adopted on 20 December 1996, or |
|||
similar laws prohibiting or restricting circumvention of such |
|||
measures. |
|||
|
|||
When you convey a covered work, you waive any legal power to forbid |
|||
circumvention of technological measures to the extent such circumvention |
|||
is effected by exercising rights under this License with respect to |
|||
the covered work, and you disclaim any intention to limit operation or |
|||
modification of the work as a means of enforcing, against the work's |
|||
users, your or third parties' legal rights to forbid circumvention of |
|||
technological measures. |
|||
|
|||
4. Conveying Verbatim Copies. |
|||
|
|||
You may convey verbatim copies of the Program's source code as you |
|||
receive it, in any medium, provided that you conspicuously and |
|||
appropriately publish on each copy an appropriate copyright notice; |
|||
keep intact all notices stating that this License and any |
|||
non-permissive terms added in accord with section 7 apply to the code; |
|||
keep intact all notices of the absence of any warranty; and give all |
|||
recipients a copy of this License along with the Program. |
|||
|
|||
You may charge any price or no price for each copy that you convey, |
|||
and you may offer support or warranty protection for a fee. |
|||
|
|||
5. Conveying Modified Source Versions. |
|||
|
|||
You may convey a work based on the Program, or the modifications to |
|||
produce it from the Program, in the form of source code under the |
|||
terms of section 4, provided that you also meet all of these conditions: |
|||
|
|||
a) The work must carry prominent notices stating that you modified |
|||
it, and giving a relevant date. |
|||
|
|||
b) The work must carry prominent notices stating that it is |
|||
released under this License and any conditions added under section |
|||
7. This requirement modifies the requirement in section 4 to |
|||
"keep intact all notices". |
|||
|
|||
c) You must license the entire work, as a whole, under this |
|||
License to anyone who comes into possession of a copy. This |
|||
License will therefore apply, along with any applicable section 7 |
|||
additional terms, to the whole of the work, and all its parts, |
|||
regardless of how they are packaged. This License gives no |
|||
permission to license the work in any other way, but it does not |
|||
invalidate such permission if you have separately received it. |
|||
|
|||
d) If the work has interactive user interfaces, each must display |
|||
Appropriate Legal Notices; however, if the Program has interactive |
|||
interfaces that do not display Appropriate Legal Notices, your |
|||
work need not make them do so. |
|||
|
|||
A compilation of a covered work with other separate and independent |
|||
works, which are not by their nature extensions of the covered work, |
|||
and which are not combined with it such as to form a larger program, |
|||
in or on a volume of a storage or distribution medium, is called an |
|||
"aggregate" if the compilation and its resulting copyright are not |
|||
used to limit the access or legal rights of the compilation's users |
|||
beyond what the individual works permit. Inclusion of a covered work |
|||
in an aggregate does not cause this License to apply to the other |
|||
parts of the aggregate. |
|||
|
|||
6. Conveying Non-Source Forms. |
|||
|
|||
You may convey a covered work in object code form under the terms |
|||
of sections 4 and 5, provided that you also convey the |
|||
machine-readable Corresponding Source under the terms of this License, |
|||
in one of these ways: |
|||
|
|||
a) Convey the object code in, or embodied in, a physical product |
|||
(including a physical distribution medium), accompanied by the |
|||
Corresponding Source fixed on a durable physical medium |
|||
customarily used for software interchange. |
|||
|
|||
b) Convey the object code in, or embodied in, a physical product |
|||
(including a physical distribution medium), accompanied by a |
|||
written offer, valid for at least three years and valid for as |
|||
long as you offer spare parts or customer support for that product |
|||
model, to give anyone who possesses the object code either (1) a |
|||
copy of the Corresponding Source for all the software in the |
|||
product that is covered by this License, on a durable physical |
|||
medium customarily used for software interchange, for a price no |
|||
more than your reasonable cost of physically performing this |
|||
conveying of source, or (2) access to copy the |
|||
Corresponding Source from a network server at no charge. |
|||
|
|||
c) Convey individual copies of the object code with a copy of the |
|||
written offer to provide the Corresponding Source. This |
|||
alternative is allowed only occasionally and noncommercially, and |
|||
only if you received the object code with such an offer, in accord |
|||
with subsection 6b. |
|||
|
|||
d) Convey the object code by offering access from a designated |
|||
place (gratis or for a charge), and offer equivalent access to the |
|||
Corresponding Source in the same way through the same place at no |
|||
further charge. You need not require recipients to copy the |
|||
Corresponding Source along with the object code. If the place to |
|||
copy the object code is a network server, the Corresponding Source |
|||
may be on a different server (operated by you or a third party) |
|||
that supports equivalent copying facilities, provided you maintain |
|||
clear directions next to the object code saying where to find the |
|||
Corresponding Source. Regardless of what server hosts the |
|||
Corresponding Source, you remain obligated to ensure that it is |
|||
available for as long as needed to satisfy these requirements. |
|||
|
|||
e) Convey the object code using peer-to-peer transmission, provided |
|||
you inform other peers where the object code and Corresponding |
|||
Source of the work are being offered to the general public at no |
|||
charge under subsection 6d. |
|||
|
|||
A separable portion of the object code, whose source code is excluded |
|||
from the Corresponding Source as a System Library, need not be |
|||
included in conveying the object code work. |
|||
|
|||
A "User Product" is either (1) a "consumer product", which means any |
|||
tangible personal property which is normally used for personal, family, |
|||
or household purposes, or (2) anything designed or sold for incorporation |
|||
into a dwelling. In determining whether a product is a consumer product, |
|||
doubtful cases shall be resolved in favor of coverage. For a particular |
|||
product received by a particular user, "normally used" refers to a |
|||
typical or common use of that class of product, regardless of the status |
|||
of the particular user or of the way in which the particular user |
|||
actually uses, or expects or is expected to use, the product. A product |
|||
is a consumer product regardless of whether the product has substantial |
|||
commercial, industrial or non-consumer uses, unless such uses represent |
|||
the only significant mode of use of the product. |
|||
|
|||
"Installation Information" for a User Product means any methods, |
|||
procedures, authorization keys, or other information required to install |
|||
and execute modified versions of a covered work in that User Product from |
|||
a modified version of its Corresponding Source. The information must |
|||
suffice to ensure that the continued functioning of the modified object |
|||
code is in no case prevented or interfered with solely because |
|||
modification has been made. |
|||
|
|||
If you convey an object code work under this section in, or with, or |
|||
specifically for use in, a User Product, and the conveying occurs as |
|||
part of a transaction in which the right of possession and use of the |
|||
User Product is transferred to the recipient in perpetuity or for a |
|||
fixed term (regardless of how the transaction is characterized), the |
|||
Corresponding Source conveyed under this section must be accompanied |
|||
by the Installation Information. But this requirement does not apply |
|||
if neither you nor any third party retains the ability to install |
|||
modified object code on the User Product (for example, the work has |
|||
been installed in ROM). |
|||
|
|||
The requirement to provide Installation Information does not include a |
|||
requirement to continue to provide support service, warranty, or updates |
|||
for a work that has been modified or installed by the recipient, or for |
|||
the User Product in which it has been modified or installed. Access to a |
|||
network may be denied when the modification itself materially and |
|||
adversely affects the operation of the network or violates the rules and |
|||
protocols for communication across the network. |
|||
|
|||
Corresponding Source conveyed, and Installation Information provided, |
|||
in accord with this section must be in a format that is publicly |
|||
documented (and with an implementation available to the public in |
|||
source code form), and must require no special password or key for |
|||
unpacking, reading or copying. |
|||
|
|||
7. Additional Terms. |
|||
|
|||
"Additional permissions" are terms that supplement the terms of this |
|||
License by making exceptions from one or more of its conditions. |
|||
Additional permissions that are applicable to the entire Program shall |
|||
be treated as though they were included in this License, to the extent |
|||
that they are valid under applicable law. If additional permissions |
|||
apply only to part of the Program, that part may be used separately |
|||
under those permissions, but the entire Program remains governed by |
|||
this License without regard to the additional permissions. |
|||
|
|||
When you convey a copy of a covered work, you may at your option |
|||
remove any additional permissions from that copy, or from any part of |
|||
it. (Additional permissions may be written to require their own |
|||
removal in certain cases when you modify the work.) You may place |
|||
additional permissions on material, added by you to a covered work, |
|||
for which you have or can give appropriate copyright permission. |
|||
|
|||
Notwithstanding any other provision of this License, for material you |
|||
add to a covered work, you may (if authorized by the copyright holders of |
|||
that material) supplement the terms of this License with terms: |
|||
|
|||
a) Disclaiming warranty or limiting liability differently from the |
|||
terms of sections 15 and 16 of this License; or |
|||
|
|||
b) Requiring preservation of specified reasonable legal notices or |
|||
author attributions in that material or in the Appropriate Legal |
|||
Notices displayed by works containing it; or |
|||
|
|||
c) Prohibiting misrepresentation of the origin of that material, or |
|||
requiring that modified versions of such material be marked in |
|||
reasonable ways as different from the original version; or |
|||
|
|||
d) Limiting the use for publicity purposes of names of licensors or |
|||
authors of the material; or |
|||
|
|||
e) Declining to grant rights under trademark law for use of some |
|||
trade names, trademarks, or service marks; or |
|||
|
|||
f) Requiring indemnification of licensors and authors of that |
|||
material by anyone who conveys the material (or modified versions of |
|||
it) with contractual assumptions of liability to the recipient, for |
|||
any liability that these contractual assumptions directly impose on |
|||
those licensors and authors. |
|||
|
|||
All other non-permissive additional terms are considered "further |
|||
restrictions" within the meaning of section 10. If the Program as you |
|||
received it, or any part of it, contains a notice stating that it is |
|||
governed by this License along with a term that is a further |
|||
restriction, you may remove that term. If a license document contains |
|||
a further restriction but permits relicensing or conveying under this |
|||
License, you may add to a covered work material governed by the terms |
|||
of that license document, provided that the further restriction does |
|||
not survive such relicensing or conveying. |
|||
|
|||
If you add terms to a covered work in accord with this section, you |
|||
must place, in the relevant source files, a statement of the |
|||
additional terms that apply to those files, or a notice indicating |
|||
where to find the applicable terms. |
|||
|
|||
Additional terms, permissive or non-permissive, may be stated in the |
|||
form of a separately written license, or stated as exceptions; |
|||
the above requirements apply either way. |
|||
|
|||
8. Termination. |
|||
|
|||
You may not propagate or modify a covered work except as expressly |
|||
provided under this License. Any attempt otherwise to propagate or |
|||
modify it is void, and will automatically terminate your rights under |
|||
this License (including any patent licenses granted under the third |
|||
paragraph of section 11). |
|||
|
|||
However, if you cease all violation of this License, then your |
|||
license from a particular copyright holder is reinstated (a) |
|||
provisionally, unless and until the copyright holder explicitly and |
|||
finally terminates your license, and (b) permanently, if the copyright |
|||
holder fails to notify you of the violation by some reasonable means |
|||
prior to 60 days after the cessation. |
|||
|
|||
Moreover, your license from a particular copyright holder is |
|||
reinstated permanently if the copyright holder notifies you of the |
|||
violation by some reasonable means, this is the first time you have |
|||
received notice of violation of this License (for any work) from that |
|||
copyright holder, and you cure the violation prior to 30 days after |
|||
your receipt of the notice. |
|||
|
|||
Termination of your rights under this section does not terminate the |
|||
licenses of parties who have received copies or rights from you under |
|||
this License. If your rights have been terminated and not permanently |
|||
reinstated, you do not qualify to receive new licenses for the same |
|||
material under section 10. |
|||
|
|||
9. Acceptance Not Required for Having Copies. |
|||
|
|||
You are not required to accept this License in order to receive or |
|||
run a copy of the Program. Ancillary propagation of a covered work |
|||
occurring solely as a consequence of using peer-to-peer transmission |
|||
to receive a copy likewise does not require acceptance. However, |
|||
nothing other than this License grants you permission to propagate or |
|||
modify any covered work. These actions infringe copyright if you do |
|||
not accept this License. Therefore, by modifying or propagating a |
|||
covered work, you indicate your acceptance of this License to do so. |
|||
|
|||
10. Automatic Licensing of Downstream Recipients. |
|||
|
|||
Each time you convey a covered work, the recipient automatically |
|||
receives a license from the original licensors, to run, modify and |
|||
propagate that work, subject to this License. You are not responsible |
|||
for enforcing compliance by third parties with this License. |
|||
|
|||
An "entity transaction" is a transaction transferring control of an |
|||
organization, or substantially all assets of one, or subdividing an |
|||
organization, or merging organizations. If propagation of a covered |
|||
work results from an entity transaction, each party to that |
|||
transaction who receives a copy of the work also receives whatever |
|||
licenses to the work the party's predecessor in interest had or could |
|||
give under the previous paragraph, plus a right to possession of the |
|||
Corresponding Source of the work from the predecessor in interest, if |
|||
the predecessor has it or can get it with reasonable efforts. |
|||
|
|||
You may not impose any further restrictions on the exercise of the |
|||
rights granted or affirmed under this License. For example, you may |
|||
not impose a license fee, royalty, or other charge for exercise of |
|||
rights granted under this License, and you may not initiate litigation |
|||
(including a cross-claim or counterclaim in a lawsuit) alleging that |
|||
any patent claim is infringed by making, using, selling, offering for |
|||
sale, or importing the Program or any portion of it. |
|||
|
|||
11. Patents. |
|||
|
|||
A "contributor" is a copyright holder who authorizes use under this |
|||
License of the Program or a work on which the Program is based. The |
|||
work thus licensed is called the contributor's "contributor version". |
|||
|
|||
A contributor's "essential patent claims" are all patent claims |
|||
owned or controlled by the contributor, whether already acquired or |
|||
hereafter acquired, that would be infringed by some manner, permitted |
|||
by this License, of making, using, or selling its contributor version, |
|||
but do not include claims that would be infringed only as a |
|||
consequence of further modification of the contributor version. For |
|||
purposes of this definition, "control" includes the right to grant |
|||
patent sublicenses in a manner consistent with the requirements of |
|||
this License. |
|||
|
|||
Each contributor grants you a non-exclusive, worldwide, royalty-free |
|||
patent license under the contributor's essential patent claims, to |
|||
make, use, sell, offer for sale, import and otherwise run, modify and |
|||
propagate the contents of its contributor version. |
|||
|
|||
In the following three paragraphs, a "patent license" is any express |
|||
agreement or commitment, however denominated, not to enforce a patent |
|||
(such as an express permission to practice a patent or covenant not to |
|||
sue for patent infringement). To "grant" such a patent license to a |
|||
party means to make such an agreement or commitment not to enforce a |
|||
patent against the party. |
|||
|
|||
If you convey a covered work, knowingly relying on a patent license, |
|||
and the Corresponding Source of the work is not available for anyone |
|||
to copy, free of charge and under the terms of this License, through a |
|||
publicly available network server or other readily accessible means, |
|||
then you must either (1) cause the Corresponding Source to be so |
|||
available, or (2) arrange to deprive yourself of the benefit of the |
|||
patent license for this particular work, or (3) arrange, in a manner |
|||
consistent with the requirements of this License, to extend the patent |
|||
license to downstream recipients. "Knowingly relying" means you have |
|||
actual knowledge that, but for the patent license, your conveying the |
|||
covered work in a country, or your recipient's use of the covered work |
|||
in a country, would infringe one or more identifiable patents in that |
|||
country that you have reason to believe are valid. |
|||
|
|||
If, pursuant to or in connection with a single transaction or |
|||
arrangement, you convey, or propagate by procuring conveyance of, a |
|||
covered work, and grant a patent license to some of the parties |
|||
receiving the covered work authorizing them to use, propagate, modify |
|||
or convey a specific copy of the covered work, then the patent license |
|||
you grant is automatically extended to all recipients of the covered |
|||
work and works based on it. |
|||
|
|||
A patent license is "discriminatory" if it does not include within |
|||
the scope of its coverage, prohibits the exercise of, or is |
|||
conditioned on the non-exercise of one or more of the rights that are |
|||
specifically granted under this License. You may not convey a covered |
|||
work if you are a party to an arrangement with a third party that is |
|||
in the business of distributing software, under which you make payment |
|||
to the third party based on the extent of your activity of conveying |
|||
the work, and under which the third party grants, to any of the |
|||
parties who would receive the covered work from you, a discriminatory |
|||
patent license (a) in connection with copies of the covered work |
|||
conveyed by you (or copies made from those copies), or (b) primarily |
|||
for and in connection with specific products or compilations that |
|||
contain the covered work, unless you entered into that arrangement, |
|||
or that patent license was granted, prior to 28 March 2007. |
|||
|
|||
Nothing in this License shall be construed as excluding or limiting |
|||
any implied license or other defenses to infringement that may |
|||
otherwise be available to you under applicable patent law. |
|||
|
|||
12. No Surrender of Others' Freedom. |
|||
|
|||
If conditions are imposed on you (whether by court order, agreement or |
|||
otherwise) that contradict the conditions of this License, they do not |
|||
excuse you from the conditions of this License. If you cannot convey a |
|||
covered work so as to satisfy simultaneously your obligations under this |
|||
License and any other pertinent obligations, then as a consequence you may |
|||
not convey it at all. For example, if you agree to terms that obligate you |
|||
to collect a royalty for further conveying from those to whom you convey |
|||
the Program, the only way you could satisfy both those terms and this |
|||
License would be to refrain entirely from conveying the Program. |
|||
|
|||
13. Use with the GNU Affero General Public License. |
|||
|
|||
Notwithstanding any other provision of this License, you have |
|||
permission to link or combine any covered work with a work licensed |
|||
under version 3 of the GNU Affero General Public License into a single |
|||
combined work, and to convey the resulting work. The terms of this |
|||
License will continue to apply to the part which is the covered work, |
|||
but the special requirements of the GNU Affero General Public License, |
|||
section 13, concerning interaction through a network will apply to the |
|||
combination as such. |
|||
|
|||
14. Revised Versions of this License. |
|||
|
|||
The Free Software Foundation may publish revised and/or new versions of |
|||
the GNU General Public License from time to time. Such new versions will |
|||
be similar in spirit to the present version, but may differ in detail to |
|||
address new problems or concerns. |
|||
|
|||
Each version is given a distinguishing version number. If the |
|||
Program specifies that a certain numbered version of the GNU General |
|||
Public License "or any later version" applies to it, you have the |
|||
option of following the terms and conditions either of that numbered |
|||
version or of any later version published by the Free Software |
|||
Foundation. If the Program does not specify a version number of the |
|||
GNU General Public License, you may choose any version ever published |
|||
by the Free Software Foundation. |
|||
|
|||
If the Program specifies that a proxy can decide which future |
|||
versions of the GNU General Public License can be used, that proxy's |
|||
public statement of acceptance of a version permanently authorizes you |
|||
to choose that version for the Program. |
|||
|
|||
Later license versions may give you additional or different |
|||
permissions. However, no additional obligations are imposed on any |
|||
author or copyright holder as a result of your choosing to follow a |
|||
later version. |
|||
|
|||
15. Disclaimer of Warranty. |
|||
|
|||
THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY |
|||
APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT |
|||
HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY |
|||
OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, |
|||
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR |
|||
PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM |
|||
IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF |
|||
ALL NECESSARY SERVICING, REPAIR OR CORRECTION. |
|||
|
|||
16. Limitation of Liability. |
|||
|
|||
IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING |
|||
WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS |
|||
THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY |
|||
GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE |
|||
USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF |
|||
DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD |
|||
PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), |
|||
EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF |
|||
SUCH DAMAGES. |
|||
|
|||
17. Interpretation of Sections 15 and 16. |
|||
|
|||
If the disclaimer of warranty and limitation of liability provided |
|||
above cannot be given local legal effect according to their terms, |
|||
reviewing courts shall apply local law that most closely approximates |
|||
an absolute waiver of all civil liability in connection with the |
|||
Program, unless a warranty or assumption of liability accompanies a |
|||
copy of the Program in return for a fee. |
|||
|
|||
END OF TERMS AND CONDITIONS |
|||
|
|||
How to Apply These Terms to Your New Programs |
|||
|
|||
If you develop a new program, and you want it to be of the greatest |
|||
possible use to the public, the best way to achieve this is to make it |
|||
free software which everyone can redistribute and change under these terms. |
|||
|
|||
To do so, attach the following notices to the program. It is safest |
|||
to attach them to the start of each source file to most effectively |
|||
state the exclusion of warranty; and each file should have at least |
|||
the "copyright" line and a pointer to where the full notice is found. |
|||
|
|||
<one line to give the program's name and a brief idea of what it does.> |
|||
Copyright (C) <year> <name of author> |
|||
|
|||
This program is free software: you can redistribute it and/or modify |
|||
it under the terms of the GNU General Public License as published by |
|||
the Free Software Foundation, either version 3 of the License, or |
|||
(at your option) any later version. |
|||
|
|||
This program is distributed in the hope that it will be useful, |
|||
but WITHOUT ANY WARRANTY; without even the implied warranty of |
|||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|||
GNU General Public License for more details. |
|||
|
|||
You should have received a copy of the GNU General Public License |
|||
along with this program. If not, see <http://www.gnu.org/licenses/>. |
|||
|
|||
Also add information on how to contact you by electronic and paper mail. |
|||
|
|||
If the program does terminal interaction, make it output a short |
|||
notice like this when it starts in an interactive mode: |
|||
|
|||
<program> Copyright (C) <year> <name of author> |
|||
This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. |
|||
This is free software, and you are welcome to redistribute it |
|||
under certain conditions; type `show c' for details. |
|||
|
|||
The hypothetical commands `show w' and `show c' should show the appropriate |
|||
parts of the General Public License. Of course, your program's commands |
|||
might be different; for a GUI interface, you would use an "about box". |
|||
|
|||
You should also get your employer (if you work as a programmer) or school, |
|||
if any, to sign a "copyright disclaimer" for the program, if necessary. |
|||
For more information on this, and how to apply and follow the GNU GPL, see |
|||
<http://www.gnu.org/licenses/>. |
|||
|
|||
The GNU General Public License does not permit incorporating your program |
|||
into proprietary programs. If your program is a subroutine library, you |
|||
may consider it more useful to permit linking proprietary applications with |
|||
the library. If this is what you want to do, use the GNU Lesser General |
|||
Public License instead of this License. But first, please read |
|||
<http://www.gnu.org/philosophy/why-not-lgpl.html>. |
|||
Some files were not shown because too many files changed in this diff
Write
Preview
Loading…
Cancel
Save
Reference in new issue