Browse Source
Merge branch 'gspn' of https://sselab.de/lab9/private/git/storm into gspn
Merge branch 'gspn' of https://sselab.de/lab9/private/git/storm into gspn
Former-commit-id: aee7afa309
main
ThomasH
9 years ago
6439 changed files with 702189 additions and 734669 deletions
-
4.gitignore
-
638CMakeLists.txt
-
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
-
4examples/mdp/csma/csma3_4.nm
-
4examples/mdp/csma/csma4_4.nm
-
4examples/mdp/csma/csma4_6.nm
-
16examples/pdtmc/tiny/tiny.pm
-
2install.sh
-
92resources/3rdparty/CMakeLists.txt
-
42resources/3rdparty/cudd-2.5.0/CMakeLists.txt
-
323resources/3rdparty/cudd-2.5.0/Makefile
-
177resources/3rdparty/cudd-2.5.0/README
-
131resources/3rdparty/cudd-2.5.0/RELEASE.NOTES
-
18resources/3rdparty/cudd-2.5.0/setup.sh
-
2resources/3rdparty/cudd-2.5.0/shutdown.sh
-
124resources/3rdparty/cudd-2.5.0/src/cudd/Makefile
-
1090resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h
@ -0,0 +1,4 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,5 @@ |
|||||
|
param x; |
||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=x dorm=0.3; |
||||
@ -0,0 +1,4 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" lambda=0 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,21 @@ |
|||||
|
toplevel "SYSTEM"; |
||||
|
"SYSTEM" or "FDEP" "CPU" "MOTOR" "PUMPS"; |
||||
|
"FDEP" fdep "TRIGGER" "P" "B"; |
||||
|
"TRIGGER" or "CS" "SS"; |
||||
|
"CPU" wsp "P" "B"; |
||||
|
"MOTOR" or "SWITCH" "MOTORS"; |
||||
|
"SWITCH" pand "MS" "MA"; |
||||
|
"MOTORS" csp "MA" "MB"; |
||||
|
"PUMPS" and "PUMP1" "PUMP2"; |
||||
|
"PUMP1" csp "PA" "PS"; |
||||
|
"PUMP2" csp "PB" "PS"; |
||||
|
"P" lambda=5.0e-5 dorm=0; |
||||
|
"B" lambda=5.0e-5 dorm=0.5; |
||||
|
"CS" lambda=2.0e-5 dorm=0; |
||||
|
"SS" lambda=2.0e-5 dorm=0; |
||||
|
"MS" lambda=1.0e-6 dorm=0; |
||||
|
"MA" lambda=1.0e-4 dorm=0; |
||||
|
"MB" lambda=1.0e-4 dorm=0; |
||||
|
"PA" lambda=1.0e-4 dorm=0; |
||||
|
"PB" lambda=1.0e-4 dorm=0; |
||||
|
"PS" lambda=1.0e-4 dorm=0; |
||||
@ -0,0 +1,24 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "CPUfdep" "CPUunit" "Motorunit" "Pumpunit"; |
||||
|
|
||||
|
"CPUfdep" fdep "trigger" "P" "B"; |
||||
|
"trigger" or "CS" "SS"; |
||||
|
"CS" lambda=0.2 dorm=0; |
||||
|
"SS" lambda=0.2 dorm=0; |
||||
|
"CPUunit" wsp "P" "B"; |
||||
|
"P" lambda=0.5 dorm=0; |
||||
|
"B" lambda=0.5 dorm=0.5; |
||||
|
|
||||
|
"Motorunit" or "MP" "Motors"; |
||||
|
"MP" pand "MS" "MA"; |
||||
|
"Motors" csp "MA" "MB"; |
||||
|
"MS" lambda=0.01 dorm=0; |
||||
|
"MA" lambda=1 dorm=0; |
||||
|
"MB" lambda=1 dorm=0; |
||||
|
|
||||
|
"Pumpunit" and "PumpA" "PumpB"; |
||||
|
"PumpA" csp "PA" "PS"; |
||||
|
"PumpB" csp "PB" "PS"; |
||||
|
"PA" lambda=1 dorm=0; |
||||
|
"PB" lambda=1 dorm=0; |
||||
|
"PS" lambda=1 dorm=0; |
||||
@ -0,0 +1,22 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "BUS" "CM"; |
||||
|
"CM" and "CM1" "CM2"; |
||||
|
"CM1" or "DISK1" "POWER1" "MEMORY1"; |
||||
|
"CM2" or "DISK2" "POWER2" "MEMORY2"; |
||||
|
"DISK1" wsp "D11" "D12"; |
||||
|
"DISK2" wsp "D21" "D22"; |
||||
|
"POWER1" or "P1" "PS"; |
||||
|
"POWER2" or "P2" "PS"; |
||||
|
"MEMORY1" wsp "M1" "M3"; |
||||
|
"MEMORY2" wsp "M2" "M3"; |
||||
|
"BUS" lambda=0.0002 dorm=0; |
||||
|
"P1" lambda=0.05 dorm=0; |
||||
|
"P2" lambda=0.05 dorm=0; |
||||
|
"PS" lambda=0.6 dorm=0; |
||||
|
"D11" lambda=8.0 dorm=0; |
||||
|
"D12" lambda=8.0 dorm=0.5; |
||||
|
"D21" lambda=8.0 dorm=0; |
||||
|
"D22" lambda=8.0 dorm=0.5; |
||||
|
"M1" lambda=0.003 dorm=0; |
||||
|
"M2" lambda=0.003 dorm=0; |
||||
|
"M3" lambda=0.003 dorm=0.5; |
||||
@ -0,0 +1,41 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "BUS" "CM"; |
||||
|
"CM" and "CM1" "CM2" "CM3" "CM4"; |
||||
|
"CM1" or "DISK1" "POWER1" "MEMORY1"; |
||||
|
"CM2" or "DISK2" "POWER2" "MEMORY2"; |
||||
|
"CM3" or "DISK3" "POWER3" "MEMORY3"; |
||||
|
"CM4" or "DISK4" "POWER4" "MEMORY4"; |
||||
|
"DISK1" wsp "D11" "D12"; |
||||
|
"DISK2" wsp "D21" "D22"; |
||||
|
"DISK3" wsp "D31" "D32"; |
||||
|
"DISK4" wsp "D41" "D42"; |
||||
|
"POWER1" or "P1" "PS"; |
||||
|
"POWER2" or "P2" "PS"; |
||||
|
"POWER3" or "P3" "PS2"; |
||||
|
"POWER4" or "P4" "PS2"; |
||||
|
"MEMORY1" wsp "M1" "M3" "M4"; |
||||
|
"MEMORY2" wsp "M2" "M3" "M4"; |
||||
|
"MEMORY3" wsp "M31" "M3"; |
||||
|
"MEMORY4" wsp "M41" "M4"; |
||||
|
"BUS" lambda=0.0002 dorm=0; |
||||
|
"P1" lambda=0.05 dorm=0; |
||||
|
"P2" lambda=0.05 dorm=0; |
||||
|
"P3" lambda=0.05 dorm=0; |
||||
|
"P4" lambda=0.05 dorm=0; |
||||
|
"PS" lambda=0.6 dorm=0; |
||||
|
"PS2" lambda=0.6 dorm=0; |
||||
|
"D11" lambda=8.0 dorm=0; |
||||
|
"D12" lambda=8.0 dorm=0.5; |
||||
|
"D21" lambda=8.0 dorm=0; |
||||
|
"D22" lambda=8.0 dorm=0.5; |
||||
|
"D31" lambda=8.0 dorm=0; |
||||
|
"D32" lambda=8.0 dorm=0.5; |
||||
|
"D41" lambda=8.0 dorm=0; |
||||
|
"D42" lambda=8.0 dorm=0.5; |
||||
|
"M1" lambda=0.003 dorm=0; |
||||
|
"M2" lambda=0.003 dorm=0; |
||||
|
"M31" lambda=0.003 dorm=0; |
||||
|
"M41" lambda=0.003 dorm=0; |
||||
|
"M3" lambda=0.003 dorm=0.5; |
||||
|
"M4" lambda=0.003 dorm=0.5; |
||||
|
|
||||
@ -0,0 +1,26 @@ |
|||||
|
toplevel "System"; |
||||
|
|
||||
|
"System" pand "A" "B"; |
||||
|
|
||||
|
"A" and "AA" "AB" "AC" "AD"; |
||||
|
|
||||
|
"B" pand "C" "D"; |
||||
|
|
||||
|
"C" and "CA" "CB" "CC" "CD"; |
||||
|
|
||||
|
"D" and "DA" "DB" "DC" "DD"; |
||||
|
|
||||
|
"AA" lambda=1 dorm=0; |
||||
|
"AB" lambda=1 dorm=0; |
||||
|
"AC" lambda=1 dorm=0; |
||||
|
"AD" lambda=1 dorm=0; |
||||
|
|
||||
|
"CA" lambda=1 dorm=0; |
||||
|
"CB" lambda=1 dorm=0; |
||||
|
"CC" lambda=1 dorm=0; |
||||
|
"CD" lambda=1 dorm=0; |
||||
|
|
||||
|
"DA" lambda=1 dorm=0; |
||||
|
"DB" lambda=1 dorm=0; |
||||
|
"DC" lambda=1 dorm=0; |
||||
|
"DD" lambda=1 dorm=0; |
||||
@ -0,0 +1,16 @@ |
|||||
|
toplevel "DeathEgg"; |
||||
|
"DeathEgg" or "DeathEggProxy" "DeathEggServer" "CampusPowerDependency" "ProxyPowerDependency"; |
||||
|
"DeathEggServer" or "CampusNET" "DES_Disks"; |
||||
|
"DES_Disks" and "DES_Disks_RAID1" "DES_Disks_RAID2"; |
||||
|
"DES_Disks_RAID1" and "DES_Disk_1" "DES_Disk_2"; |
||||
|
"DES_Disks_RAID2" and "DES_Disk_3" "DES_Disk_4"; |
||||
|
"DeathEggProxy" lambda=0.01 dorm=0; |
||||
|
"DES_Disk_1" lambda=0.01 dorm=0; |
||||
|
"DES_Disk_2" lambda=0.01 dorm=0; |
||||
|
"DES_Disk_3" lambda=0.01 dorm=0; |
||||
|
"DES_Disk_4" lambda=0.01 dorm=0; |
||||
|
"CampusPowerDependency" fdep "CampusPower" "DeathEggServer"; |
||||
|
"ProxyPowerDependency" fdep "ProxyPower" "DeathEggProxy"; |
||||
|
"CampusPower" lambda=0.01 dorm=0; |
||||
|
"CampusNET" lambda=0.01 dorm=0; |
||||
|
"ProxyPower" lambda=0.01 dorm=0; |
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "Power" "Machine"; |
||||
|
"Power" fdep "B_Power" "P" "B"; |
||||
|
"Machine" or "P" "B"; |
||||
|
|
||||
|
"B_Power" lambda=0.5 dorm=0; |
||||
|
"P" lambda=0.5 dorm=0; |
||||
|
"B" lambda=0.5 dorm=0.5; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"F" fdep "B" "C"; |
||||
|
"B" lambda=0.5 dorm=0; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C" "F"; |
||||
|
"F" fdep "B" "C"; |
||||
|
"B" lambda=0.4 dorm=0; |
||||
|
"C" lambda=0.8 dorm=0; |
||||
@ -0,0 +1,129 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD"; |
||||
|
|
||||
|
"triadA" 2of3 "aA" "bA" "cA"; |
||||
|
"aA" csp "TAA" "TAS"; |
||||
|
"bA" csp "TAB" "TAS"; |
||||
|
"cA" csp "TAC" "TAS"; |
||||
|
|
||||
|
"triadB" 2of3 "aB" "bB" "cB"; |
||||
|
"aB" csp "TBA" "TBS"; |
||||
|
"bB" csp "TBB" "TBS"; |
||||
|
"cB" csp "TBC" "TBS"; |
||||
|
|
||||
|
"triadC" 2of3 "aC" "bC" "cC"; |
||||
|
"aC" csp "TCA" "TCS"; |
||||
|
"bC" csp "TCB" "TCS"; |
||||
|
"cC" csp "TCC" "TCS"; |
||||
|
|
||||
|
"triadD" 2of3 "aD" "bD" "cD"; |
||||
|
"aD" csp "TDA" "TDS"; |
||||
|
"bD" csp "TDB" "TDS"; |
||||
|
"cD" csp "TDC" "TDS"; |
||||
|
|
||||
|
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; |
||||
|
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; |
||||
|
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; |
||||
|
"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS"; |
||||
|
|
||||
|
|
||||
|
"NEA" lambda=0.017 dorm=1; |
||||
|
"NEB" lambda=0.017 dorm=1; |
||||
|
"NEC" lambda=0.017 dorm=1; |
||||
|
"NED" lambda=0.017 dorm=1; |
||||
|
|
||||
|
"TAA" or "cpuAA" "memAA"; |
||||
|
"memAA" csp "memAA1" "memAA2"; |
||||
|
"cpuAA" lambda=0.11 dorm=0; |
||||
|
"memAA1" lambda=0.11 dorm=0; |
||||
|
"memAA2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TAB" or "cpuAB" "memAB"; |
||||
|
"memAB" csp "memAB1" "memAB2"; |
||||
|
"cpuAB" lambda=0.11 dorm=0; |
||||
|
"memAB1" lambda=0.11 dorm=0; |
||||
|
"memAB2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TAC" or "cpuAC" "memAC"; |
||||
|
"memAC" csp "memAC1" "memAC2"; |
||||
|
"cpuAC" lambda=0.11 dorm=0; |
||||
|
"memAC1" lambda=0.11 dorm=0; |
||||
|
"memAC2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TAS" or "cpuAS" "memAS"; |
||||
|
"memAS" csp "memAS1" "memAS2"; |
||||
|
"cpuAS" lambda=0.11 dorm=0; |
||||
|
"memAS1" lambda=0.11 dorm=0; |
||||
|
"memAS2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBA" or "cpuBA" "memBA"; |
||||
|
"memBA" csp "memBA1" "memBA2"; |
||||
|
"cpuBA" lambda=0.11 dorm=0; |
||||
|
"memBA1" lambda=0.11 dorm=0; |
||||
|
"memBA2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBB" or "cpuBB" "memBB"; |
||||
|
"memBB" csp "memBB1" "memBB2"; |
||||
|
"cpuBB" lambda=0.11 dorm=0; |
||||
|
"memBB1" lambda=0.11 dorm=0; |
||||
|
"memBB2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBC" or "cpuBC" "memBC"; |
||||
|
"memBC" csp "memBC1" "memBC2"; |
||||
|
"cpuBC" lambda=0.11 dorm=0; |
||||
|
"memBC1" lambda=0.11 dorm=0; |
||||
|
"memBC2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBS" or "cpuBS" "memBS"; |
||||
|
"memBS" csp "memBS1" "memBS2"; |
||||
|
"cpuBS" lambda=0.11 dorm=0; |
||||
|
"memBS1" lambda=0.11 dorm=0; |
||||
|
"memBS2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCA" or "cpuCA" "memCA"; |
||||
|
"memCA" csp "memCA1" "memCA2"; |
||||
|
"cpuCA" lambda=0.11 dorm=0; |
||||
|
"memCA1" lambda=0.11 dorm=0; |
||||
|
"memCA2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCB" or "cpuCB" "memCB"; |
||||
|
"memCB" csp "memCB1" "memCB2"; |
||||
|
"cpuCB" lambda=0.11 dorm=0; |
||||
|
"memCB1" lambda=0.11 dorm=0; |
||||
|
"memCB2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCC" or "cpuCC" "memCC"; |
||||
|
"memCC" csp "memCC1" "memCC2"; |
||||
|
"cpuCC" lambda=0.11 dorm=0; |
||||
|
"memCC1" lambda=0.11 dorm=0; |
||||
|
"memCC2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCS" or "cpuCS" "memCS"; |
||||
|
"memCS" csp "memCS1" "memCS2"; |
||||
|
"cpuCS" lambda=0.11 dorm=0; |
||||
|
"memCS1" lambda=0.11 dorm=0; |
||||
|
"memCS2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDA" or "cpuDA" "memDA"; |
||||
|
"memDA" csp "memDA1" "memDA2"; |
||||
|
"cpuDA" lambda=0.11 dorm=0; |
||||
|
"memDA1" lambda=0.11 dorm=0; |
||||
|
"memDA2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDB" or "cpuDB" "memDB"; |
||||
|
"memDB" csp "memDB1" "memDB2"; |
||||
|
"cpuDB" lambda=0.11 dorm=0; |
||||
|
"memDB1" lambda=0.11 dorm=0; |
||||
|
"memDB2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDC" or "cpuDC" "memDC"; |
||||
|
"memDC" csp "memDC1" "memDC2"; |
||||
|
"cpuDC" lambda=0.11 dorm=0; |
||||
|
"memDC1" lambda=0.11 dorm=0; |
||||
|
"memDC2" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDS" or "cpuDS" "memDS"; |
||||
|
"memDS" csp "memDS1" "memDS2"; |
||||
|
"cpuDS" lambda=0.11 dorm=0; |
||||
|
"memDS1" lambda=0.11 dorm=0; |
||||
|
"memDS2" lambda=0.11 dorm=0; |
||||
@ -0,0 +1,63 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD" "fE"; |
||||
|
|
||||
|
"triadA" 3of4 "aA" "bA" "cA" "dA"; |
||||
|
"aA" csp "TAA" "TAS"; |
||||
|
"bA" csp "TAB" "TAS"; |
||||
|
"cA" csp "TAC" "TAS"; |
||||
|
"dA" csp "TAD" "TAS"; |
||||
|
|
||||
|
"triadB" 3of4 "aB" "bB" "cB" "dB"; |
||||
|
"aB" csp "TBA" "TBS"; |
||||
|
"bB" csp "TBB" "TBS"; |
||||
|
"cB" csp "TBC" "TBS"; |
||||
|
"dB" csp "TBD" "TBS"; |
||||
|
|
||||
|
"triadC" 3of4 "aC" "bC" "cC" "dC"; |
||||
|
"aC" csp "TCA" "TCS"; |
||||
|
"bC" csp "TCB" "TCS"; |
||||
|
"cC" csp "TCC" "TCS"; |
||||
|
"dC" csp "TCD" "TCS"; |
||||
|
|
||||
|
"triadD" 3of4 "aD" "bD" "cD" "dD"; |
||||
|
"aD" csp "TDA" "TDS"; |
||||
|
"bD" csp "TDB" "TDS"; |
||||
|
"cD" csp "TDC" "TDS"; |
||||
|
"dD" csp "TDD" "TDS"; |
||||
|
|
||||
|
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; |
||||
|
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; |
||||
|
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; |
||||
|
"fD" fdep "NED" "TAD" "TBD" "TCD" "TDD"; |
||||
|
"fE" fdep "NEE" "TAS" "TBS" "TCS" "TDS"; |
||||
|
|
||||
|
|
||||
|
"NEA" lambda=0.017 dorm=1; |
||||
|
"NEB" lambda=0.017 dorm=1; |
||||
|
"NEC" lambda=0.017 dorm=1; |
||||
|
"NED" lambda=0.017 dorm=1; |
||||
|
"NEE" lambda=0.017 dorm=1; |
||||
|
|
||||
|
"TAA" lambda=0.11 dorm=0; |
||||
|
"TAB" lambda=0.11 dorm=0; |
||||
|
"TAC" lambda=0.11 dorm=0; |
||||
|
"TAD" lambda=0.11 dorm=0; |
||||
|
"TAS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBA" lambda=0.11 dorm=0; |
||||
|
"TBB" lambda=0.11 dorm=0; |
||||
|
"TBC" lambda=0.11 dorm=0; |
||||
|
"TBD" lambda=0.11 dorm=0; |
||||
|
"TBS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCA" lambda=0.11 dorm=0; |
||||
|
"TCB" lambda=0.11 dorm=0; |
||||
|
"TCC" lambda=0.11 dorm=0; |
||||
|
"TCD" lambda=0.11 dorm=0; |
||||
|
"TCS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDA" lambda=0.11 dorm=0; |
||||
|
"TDB" lambda=0.11 dorm=0; |
||||
|
"TDC" lambda=0.11 dorm=0; |
||||
|
"TDD" lambda=0.11 dorm=0; |
||||
|
"TDS" lambda=0.11 dorm=0; |
||||
@ -0,0 +1,53 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD"; |
||||
|
|
||||
|
"triadA" 2of3 "aA" "bA" "cA"; |
||||
|
"aA" csp "TAA" "TAS"; |
||||
|
"bA" csp "TAB" "TAS"; |
||||
|
"cA" csp "TAC" "TAS"; |
||||
|
|
||||
|
"triadB" 2of3 "aB" "bB" "cB"; |
||||
|
"aB" csp "TBA" "TBS"; |
||||
|
"bB" csp "TBB" "TBS"; |
||||
|
"cB" csp "TBC" "TBS"; |
||||
|
|
||||
|
"triadC" 2of3 "aC" "bC" "cC"; |
||||
|
"aC" csp "TCA" "TCS"; |
||||
|
"bC" csp "TCB" "TCS"; |
||||
|
"cC" csp "TCC" "TCS"; |
||||
|
|
||||
|
"triadD" 2of3 "aD" "bD" "cD"; |
||||
|
"aD" csp "TDA" "TDS"; |
||||
|
"bD" csp "TDB" "TDS"; |
||||
|
"cD" csp "TDC" "TDS"; |
||||
|
|
||||
|
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; |
||||
|
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; |
||||
|
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; |
||||
|
"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS"; |
||||
|
|
||||
|
|
||||
|
"NEA" lambda=0.017 dorm=1; |
||||
|
"NEB" lambda=0.017 dorm=1; |
||||
|
"NEC" lambda=0.017 dorm=1; |
||||
|
"NED" lambda=0.017 dorm=1; |
||||
|
|
||||
|
"TAA" lambda=0.11 dorm=0; |
||||
|
"TAB" lambda=0.11 dorm=0; |
||||
|
"TAC" lambda=0.11 dorm=0; |
||||
|
"TAS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TBA" lambda=0.11 dorm=0; |
||||
|
"TBB" lambda=0.11 dorm=0; |
||||
|
"TBC" lambda=0.11 dorm=0; |
||||
|
"TBS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TCA" lambda=0.11 dorm=0; |
||||
|
"TCB" lambda=0.11 dorm=0; |
||||
|
"TCC" lambda=0.11 dorm=0; |
||||
|
"TCS" lambda=0.11 dorm=0; |
||||
|
|
||||
|
"TDA" lambda=0.11 dorm=0; |
||||
|
"TDB" lambda=0.11 dorm=0; |
||||
|
"TDC" lambda=0.11 dorm=0; |
||||
|
"TDS" lambda=0.11 dorm=0; |
||||
@ -0,0 +1,22 @@ |
|||||
|
toplevel "n12"; |
||||
|
"n12" or "n1" "n103" "n7"; |
||||
|
"n103" wsp "n106" "n14"; |
||||
|
"n7" and "n18" "n26"; |
||||
|
"n26" or "n28" "n19" "n23"; |
||||
|
"n19" wsp "n16" "n13"; |
||||
|
"n23" wsp "n0" "n17"; |
||||
|
"n18" or "n15" "n9" "n3"; |
||||
|
"n3" wsp "n2" "n17"; |
||||
|
"n9" wsp "n8" "n27"; |
||||
|
"n16" lambda=8.0 dorm=0.0; |
||||
|
"n0" lambda=0.003 dorm=0.0; |
||||
|
"n13" lambda=8.0 dorm=0.5; |
||||
|
"n2" lambda=0.003 dorm=0.0; |
||||
|
"n17" lambda=0.003 dorm=0.5; |
||||
|
"n15" lambda=0.05 dorm=0.0; |
||||
|
"n106" lambda=1.2 dorm=0.0; |
||||
|
"n14" lambda=0.6 dorm=0.0; |
||||
|
"n1" lambda=2.0E-4 dorm=0.0; |
||||
|
"n27" lambda=8.0 dorm=0.5; |
||||
|
"n8" lambda=8.0 dorm=0.0; |
||||
|
"n28" lambda=0.05 dorm=0.0; |
||||
@ -0,0 +1,26 @@ |
|||||
|
toplevel "System"; |
||||
|
|
||||
|
"System" or "S" "N"; |
||||
|
|
||||
|
"N" lambda=2e-5 dorm=0; |
||||
|
|
||||
|
"S" and "CMA" "CMB"; |
||||
|
|
||||
|
"CMA" or "DiskA" "PA" "MemA"; |
||||
|
"DiskA" wsp "DAA" "DAB"; |
||||
|
"PA" lambda=500e-5 dorm=0; |
||||
|
"MemA" wsp "MA" "MC"; |
||||
|
"DAA" lambda=80000e-5 dorm=0.5; |
||||
|
"DAB" lambda=80000e-5 dorm=0.5; |
||||
|
"MA" lambda=30e-5 dorm=0; |
||||
|
|
||||
|
"CMB" or "DiskB" "PB" "MemB"; |
||||
|
"DiskB" wsp "DBA" "DBB"; |
||||
|
"PB" lambda=500e-5 dorm=0; |
||||
|
"MemB" wsp "MB" "MC"; |
||||
|
"DBA" lambda=80000e-5 dorm=0.5; |
||||
|
"DBB" lambda=80000e-5 dorm=0.5; |
||||
|
"MB" lambda=30e-5 dorm=0; |
||||
|
|
||||
|
"MC" lambda=30e-5 dorm=0.5; |
||||
|
|
||||
@ -0,0 +1,19 @@ |
|||||
|
toplevel "System"; |
||||
|
"System" or "S" "N"; |
||||
|
"N" lambda=0.0000200000 dorm=0.0000000000; |
||||
|
"S" and "CMA" "CMB"; |
||||
|
"CMA" or "DiskA" "PA" "MemA"; |
||||
|
"DiskA" wsp "DAA" "DAB"; |
||||
|
"PA" lambda=0.0049999999 dorm=0.0000000000; |
||||
|
"MemA" wsp "MA" "MC"; |
||||
|
"DAA" lambda=0.8000000119 dorm=0.5000000000; |
||||
|
"DAB" lambda=0.8000000119 dorm=0.5000000000; |
||||
|
"MA" lambda=0.0003000000 dorm=0.0000000000; |
||||
|
"CMB" or "DiskB" "PB" "MemB"; |
||||
|
"DiskB" wsp "DBA" "DBB"; |
||||
|
"PB" lambda=0.0049999999 dorm=0.0000000000; |
||||
|
"MemB" wsp "MB" "MC"; |
||||
|
"DBA" lambda=0.8000000119 dorm=0.5000000000; |
||||
|
"DBB" lambda=0.8000000119 dorm=0.5000000000; |
||||
|
"MB" lambda=0.0003000000 dorm=0.0000000000; |
||||
|
"MC" lambda=0.0003000000 dorm=0.5000000000; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" or "D" "E"; |
||||
|
"C" or "F" "E"; |
||||
|
"D" lambda=0.1 dorm=0; |
||||
|
"E" lambda=0.2 dorm=0; |
||||
|
"F" lambda=0.3 dorm=0; |
||||
@ -0,0 +1,8 @@ |
|||||
|
param x; |
||||
|
param y; |
||||
|
toplevel "A"; |
||||
|
"A" or "B" "Z"; |
||||
|
"B" pand "D" "S"; |
||||
|
"Z" lambda=y dorm=0; |
||||
|
"D" lambda=100 dorm=0; |
||||
|
"S" lambda=100*x dorm=0; |
||||
@ -0,0 +1,4 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,4 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "B" "C"; |
||||
|
"B" lambda=0.4 dorm=0.3; |
||||
|
"C" lambda=0.2 dorm=0.3; |
||||
@ -0,0 +1,6 @@ |
|||||
|
param x; |
||||
|
param y; |
||||
|
toplevel "A"; |
||||
|
"A" pand "B" "C"; |
||||
|
"B" lambda=x dorm=0.3; |
||||
|
"C" lambda=y dorm=0.3; |
||||
@ -0,0 +1,12 @@ |
|||||
|
// From Junges2015 |
||||
|
// Example 3.19 |
||||
|
|
||||
|
toplevel "SF"; |
||||
|
"SF" or "A" "B" "PDEP"; |
||||
|
"A" pand "S" "MA"; |
||||
|
"B" and "MA" "MB"; |
||||
|
"PDEP" pdep=0.2 "MA" "S"; |
||||
|
|
||||
|
"S" lambda=0.5 dorm=0; |
||||
|
"MA" lambda=0.5 dorm=0; |
||||
|
"MB" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "SF"; |
||||
|
"SF" or "A" "B" "PDEP"; |
||||
|
"A" pand "S" "MA"; |
||||
|
"B" and "MA" "MB"; |
||||
|
"PDEP" pdep=0.2 "MA" "S" "MB"; |
||||
|
|
||||
|
"S" lambda=0.5 dorm=0; |
||||
|
"MA" lambda=0.5 dorm=0; |
||||
|
"MB" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C" "F"; |
||||
|
"F" pdep=0.3 "B" "C"; |
||||
|
"B" lambda=0.4 dorm=0; |
||||
|
"C" lambda=0.8 dorm=0; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "SF"; |
||||
|
"SF" pand "S" "A" "B"; |
||||
|
"PDEP" pdep=0.2 "S" "A" "B"; |
||||
|
|
||||
|
"S" lambda=0.5 dorm=0; |
||||
|
"A" lambda=0.5 dorm=0; |
||||
|
"B" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,11 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" and "C" "D" "PDEP"; |
||||
|
"B'" and "C'" "D'" "PDEP'"; |
||||
|
"PDEP" pdep=0.6 "C" "D"; |
||||
|
"PDEP'" pdep=0.6 "C'" "D'"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=0.5 dorm=0; |
||||
|
|
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" por "B" "C" "D"; |
||||
|
"B" lambda=0.4 dorm=0.0; |
||||
|
"C" lambda=0.2 dorm=0.0; |
||||
|
"D" lambda=0.2 dorm=0.0; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"X" seq "B" "C" |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C" "D"; |
||||
|
"X" seq "B" "C" "D"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
|
"D" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "C" "D"; |
||||
|
"X" seq "B" "C" "D"; |
||||
|
"B" lambda=0.5 dorm=0.3; |
||||
|
"C" lambda=0.5 dorm=0.3; |
||||
|
"D" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "T1" "B3"; |
||||
|
"T1" or "B1" "B2"; |
||||
|
"X" seq "B1" "B2" "B3"; |
||||
|
"B1" lambda=0.5 dorm=0.3; |
||||
|
"B2" lambda=0.5 dorm=0.3; |
||||
|
"B3" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "T1" "T2"; |
||||
|
"T1" pand "B1" "B2"; |
||||
|
"T2" pand "B3" "B4"; |
||||
|
"X" seq "B4" "B3"; |
||||
|
"B1" lambda=0.7 dorm=0.3; |
||||
|
"B2" lambda=0.5 dorm=0.3; |
||||
|
"B3" lambda=0.5 dorm=0.3; |
||||
|
"B4" lambda=0.7 dorm=0.3; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "I" "M"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"M" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" wsp "I" "J"; |
||||
|
"C" wsp "M" "J"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"M" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,10 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C" "D"; |
||||
|
"B" wsp "I" "M"; |
||||
|
"C" wsp "J" "M"; |
||||
|
"D" wsp "K" "M"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"K" lambda=0.5 dorm=0.3; |
||||
|
"M" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" wsp "I" "J" "K"; |
||||
|
"C" wsp "M" "J"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"K" lambda=0.5 dorm=0.3; |
||||
|
"M" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "I" "B"; |
||||
|
"B" or "C" "J"; |
||||
|
"C" or "K" "L"; |
||||
|
"I" lambda=0.5 dorm=0; |
||||
|
"J" lambda=0.5 dorm=0; |
||||
|
"K" lambda=0.5 dorm=0; |
||||
|
"L" lambda=0.5 dorm=0; |
||||
|
|
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "I" "B"; |
||||
|
"B" wsp "J" "M"; |
||||
|
"I" lambda=0.5 dorm=0.5; |
||||
|
"J" lambda=0.5 dorm=0.5; |
||||
|
"M" lambda=0.5 dorm=0.5; |
||||
|
|
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "K" "J" "I"; |
||||
|
"I" lambda=0.5 dorm=0.5; |
||||
|
"J" lambda=1 dorm=0.5; |
||||
|
"K" lambda=0.5 dorm=0.5; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "I" "B"; |
||||
|
"B" wsp "J" "K"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"K" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" wsp "I" "M"; |
||||
|
"I" lambda=0.5 dorm=0.0; |
||||
|
"M" lambda=0.5 dorm=0.0; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
param x; |
||||
|
param y; |
||||
|
toplevel "SF"; |
||||
|
"SF" or "FW" "BW"; |
||||
|
"FW" wsp "W1" "WS"; |
||||
|
"BW" wsp "W2" "WS"; |
||||
|
"W1" lambda=x dorm=0; |
||||
|
"W2" lambda=1 dorm=0; |
||||
|
"WS" lambda=y dorm=0; |
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" wsp "I" "J"; |
||||
|
"C" wsp "K" "L"; |
||||
|
"I" lambda=0.5 dorm=0.3; |
||||
|
"J" lambda=0.5 dorm=0.3; |
||||
|
"K" lambda=0.5 dorm=0.3; |
||||
|
"L" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" and "C" "D"; |
||||
|
"B'" and "C'" "D'"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" and "C" "D"; |
||||
|
"B'" and "C'" "D'"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=2 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=2 dorm=0; |
||||
@ -0,0 +1,12 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'" "B''"; |
||||
|
"B" and "C" "D"; |
||||
|
"B'" and "C'" "D'"; |
||||
|
"B''" and "C''" "D''"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=0.5 dorm=0; |
||||
|
"C''" lambda=0.5 dorm=0; |
||||
|
"D''" lambda=0.5 dorm=0; |
||||
|
|
||||
@ -0,0 +1,12 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'" "C" "C'"; |
||||
|
"B" and "D" "E"; |
||||
|
"B'" and "D'" "E'"; |
||||
|
"C" or "F"; |
||||
|
"C'" or "F'"; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"E" lambda=0.5 dorm=0; |
||||
|
"D'" lambda=0.5 dorm=0; |
||||
|
"E'" lambda=0.5 dorm=0; |
||||
|
"F" lambda=0.5 dorm=0; |
||||
|
"F'" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,21 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "BA" "BB" "BC" "BD" "BE" "BF"; |
||||
|
"BA" and "CA" "DA"; |
||||
|
"BB" and "CB" "DB"; |
||||
|
"BC" and "CC" "DC"; |
||||
|
"BD" and "CD" "DD"; |
||||
|
"BE" and "CE" "DE"; |
||||
|
"BF" and "CF" "DF"; |
||||
|
"CA" lambda=0.5 dorm=0; |
||||
|
"DA" lambda=0.5 dorm=0; |
||||
|
"CB" lambda=0.5 dorm=0; |
||||
|
"DB" lambda=0.5 dorm=0; |
||||
|
"CC" lambda=0.5 dorm=0; |
||||
|
"DC" lambda=0.5 dorm=0; |
||||
|
"CD" lambda=0.5 dorm=0; |
||||
|
"DD" lambda=0.5 dorm=0; |
||||
|
"CE" lambda=0.5 dorm=0; |
||||
|
"DE" lambda=0.5 dorm=0; |
||||
|
"CF" lambda=0.5 dorm=0; |
||||
|
"DF" lambda=0.5 dorm=0; |
||||
|
|
||||
@ -0,0 +1,10 @@ |
|||||
|
param x; |
||||
|
param y; |
||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" and "C" "D"; |
||||
|
"B'" and "C'" "D'"; |
||||
|
"C" lambda=x dorm=0; |
||||
|
"D" lambda=y dorm=0; |
||||
|
"C'" lambda=x dorm=0; |
||||
|
"D'" lambda=y dorm=0; |
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "B'"; |
||||
|
"B" wsp "C" "D"; |
||||
|
"B'" wsp "C'" "D"; |
||||
|
"C" lambda=0.5 dorm=0; |
||||
|
"D" lambda=0.5 dorm=0; |
||||
|
"C'" lambda=0.5 dorm=0; |
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" and "BE1" "BE2"; |
||||
|
"C" and "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=0.3; |
||||
|
"BE2" lambda=0.5 dorm=0.3; |
||||
|
"BE3" lambda=0.5 dorm=0.3; |
||||
|
"BE4" lambda=0.5 dorm=0.3; |
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "B" "C"; |
||||
|
"B" and "BE1" "BE2"; |
||||
|
"C" and "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=0.3; |
||||
|
"BE2" lambda=0.5 dorm=0.3; |
||||
|
"BE3" lambda=0.5 dorm=0.3; |
||||
|
|
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "BE1" "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" and "BE1" "BE2" "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" or "BE1" "BE2"; |
||||
|
"C" or "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "B" "C"; |
||||
|
"B" or "BE1" "BE2"; |
||||
|
"C" or "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "BE1" "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" or "BE1" "BE2" "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,9 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "B" "BE4"; |
||||
|
"B" pand "C" "BE3"; |
||||
|
"C" pand "BE1" "BE2"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,8 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "B" "C"; |
||||
|
"B" pand "BE1" "BE2"; |
||||
|
"C" pand "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,6 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "BE1" "BE2" "BE3"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,7 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" pand "BE1" "BE2" "BE3" "BE4"; |
||||
|
"BE1" lambda=0.5 dorm=3; |
||||
|
"BE2" lambda=0.5 dorm=3; |
||||
|
"BE3" lambda=0.5 dorm=3; |
||||
|
"BE4" lambda=0.5 dorm=3; |
||||
|
|
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" 1of3 "B" "C" "D"; |
||||
|
"B" lambda=0.1 dorm=0; |
||||
|
"C" lambda=0.2 dorm=0; |
||||
|
"D" lambda=0.3 dorm=0; |
||||
@ -0,0 +1,5 @@ |
|||||
|
toplevel "A"; |
||||
|
"A" 1of3 "B" "C" "D"; |
||||
|
"B" lambda=0.3 dorm=0; |
||||
|
"C" lambda=0.4 dorm=0; |
||||
|
"D" lambda=1 dorm=0; |
||||
2604
examples/jani-examples/beb.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,27 @@ |
|||||
|
Peak memory usage: 38 MB |
||||
|
Analysis results for beb.jani |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 4528 |
||||
|
Transitions: 4874 |
||||
|
Branches: 6899 |
||||
|
Time: 0.0 s |
||||
|
Rate: 92408 states/s |
||||
|
|
||||
|
+ LineSeized |
||||
|
Probability: 0.9166259765625 |
||||
|
Time: 0.1 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 8 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ GaveUp |
||||
|
Probability: 0.0833740234375 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 9 |
||||
|
Time: 0.0 s |
||||
@ -0,0 +1,64 @@ |
|||||
|
// Modest MDP model of the bounded exponential backoff procedure (BEB) |
||||
|
// [BFHH11] |
||||
|
action tick, tack, tock; |
||||
|
|
||||
|
const int K = 4; // maximum value for backoff |
||||
|
const int N = 3; // number of tries before giving up |
||||
|
const int H = 3; // number of hosts (must correspond to the number of Host() instantiations in the global composition) |
||||
|
|
||||
|
int(0..2) cr; // count how many hosts attempt to seize the line in a slot (zero, one, many) |
||||
|
bool line_seized; |
||||
|
bool gave_up; |
||||
|
|
||||
|
property LineSeized = Pmax(<> line_seized); // some host managed to seize the line before any other gave up |
||||
|
property GaveUp = Pmax(<> gave_up); // some host gave up before any other managed to seize the line (does not work with POR) |
||||
|
|
||||
|
process Clock() |
||||
|
{ |
||||
|
tick; tack; tau {= cr = 0 =}; tock; Clock() |
||||
|
} |
||||
|
|
||||
|
process Host() |
||||
|
{ |
||||
|
int(0..N) na; // nr_attempts 0..N |
||||
|
int(0..K) ev = 2; // exp_val 0..K |
||||
|
int(0..K) wt; // slots_to_wait 0..K |
||||
|
|
||||
|
do |
||||
|
{ |
||||
|
if(wt > 0) |
||||
|
{ |
||||
|
// wait this slot |
||||
|
tick {= wt-- =} |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
tau {= cr = min(2, cr + 1) =}; // attempt to seize the line |
||||
|
tick; |
||||
|
if(cr == 1) |
||||
|
{ |
||||
|
// someone managed to seize the line |
||||
|
tau {= line_seized = true =}; stop |
||||
|
} |
||||
|
else if(na >= N) |
||||
|
{ |
||||
|
// maximum number of attempts exceeded |
||||
|
tau {= gave_up = true =}; stop |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
// backoff |
||||
|
tau {= na++, wt = DiscreteUniform(0, max(0, ev - 1)), ev = min(2 * ev, K) =} |
||||
|
} |
||||
|
}; |
||||
|
tack; tock |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
par |
||||
|
{ |
||||
|
:: Clock() |
||||
|
:: Host() |
||||
|
:: Host() |
||||
|
:: Host() |
||||
|
} |
||||
@ -0,0 +1,27 @@ |
|||||
|
Peak memory usage: 39 MB |
||||
|
Analysis results for beb.modest |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 4528 |
||||
|
Transitions: 4874 |
||||
|
Branches: 6899 |
||||
|
Time: 0.0 s |
||||
|
Rate: 94333 states/s |
||||
|
|
||||
|
+ LineSeized |
||||
|
Probability: 0.9166259765625 |
||||
|
Time: 0.1 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 8 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ GaveUp |
||||
|
Probability: 0.0833740234375 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 9 |
||||
|
Time: 0.0 s |
||||
2092
examples/jani-examples/brp.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,63 @@ |
|||||
|
Peak memory usage: 39 MB |
||||
|
Analysis results for brp.jani |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 3959 |
||||
|
Transitions: 4244 |
||||
|
Branches: 4593 |
||||
|
Time: 0.1 s |
||||
|
Rate: 74698 states/s |
||||
|
|
||||
|
+ P_A |
||||
|
Probability: 0 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 1 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_B |
||||
|
Probability: 0 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 1 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_1 |
||||
|
Probability: 0.000423333443357766 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 2.35005704803786E-07 |
||||
|
Iterations: 13 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_2 |
||||
|
Probability: 2.64530890961023E-05 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 2.05561452068843E-07 |
||||
|
Iterations: 14 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_3 |
||||
|
Probability: 0.000185191226393368 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 3.32462409056221E-07 |
||||
|
Iterations: 13 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_4 |
||||
|
Probability: 8E-06 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 2 |
||||
|
Time: 0.0 s |
||||
@ -0,0 +1,213 @@ |
|||||
|
// Modest PTA model of the bounded retransmission protocol (BRP) |
||||
|
// [HH09], http://www.modestchecker.net/CaseStudies/BRP/ |
||||
|
action put, get, put_k, get_k, put_l, get_l; |
||||
|
action new_file; |
||||
|
action s_ok, s_dk, s_nok, s_restart; |
||||
|
action r_ok, r_inc, r_fst, r_nok, r_timeout; |
||||
|
exception error; |
||||
|
|
||||
|
const int N = 16; // number of frames per file |
||||
|
const int MAX = 2; // maximum number of retransmissions per frame |
||||
|
const int TD = 1; // transmission delay |
||||
|
const int TS = 2 * TD + 1; // sender timeout |
||||
|
const int TR = 2 * MAX * TS + 3 * TD; // receiver timeout |
||||
|
const int SYNC = TR; |
||||
|
|
||||
|
bool ff, lf, ab; // channel data: first/last frame, alternating bit |
||||
|
int(0..N) i; // sender chunk counter |
||||
|
bool inTransitK = false; |
||||
|
bool inTransitL = false; |
||||
|
|
||||
|
bool first_file_done = false; |
||||
|
bool get_k_seen, s_ok_seen, s_nok_seen, s_dk_seen, s_restart_seen, r_ok_seen, r_timeout_seen; |
||||
|
|
||||
|
// Invariant (timed) properties (from [BrpOnTime], the TA model) |
||||
|
bool premature_timeout, channel_k_overflow, channel_l_overflow; |
||||
|
// "there is at most one message in transit for each channel" |
||||
|
property T_1 = A[] (!(channel_k_overflow || channel_l_overflow)); |
||||
|
// "there is at most one message in transit in total" |
||||
|
property T_2 = A[] (!(inTransitK && inTransitL)); |
||||
|
// Assumption (A1): "no premature timeouts" |
||||
|
property T_A1 = A[] (!premature_timeout); |
||||
|
// Assumption (A2): "sender starts new file only after receiver reacted to failure" |
||||
|
// Note that receiver can only notice failure if it received at least one chunk, i.e. get_k_seen |
||||
|
property T_A2 = A[] (!s_restart_seen || !get_k_seen || r_timeout_seen); |
||||
|
|
||||
|
// Probabilistic reachability properties (from [D'AJJL01], the RAPTURE/PRISM model) |
||||
|
// property A of [D'AJJL01]: "the maximum probability that eventually the sender reports |
||||
|
// a certain unsuccessful transmission but the receiver got the complete file" |
||||
|
property P_A = Pmax(<>(s_nok_seen && r_ok_seen)); |
||||
|
// property B of [D'AJJL01]: "the maximum probability that eventually the sender reports |
||||
|
// a certain successful transmission but the receiver did not get the complete file" |
||||
|
property P_B = Pmax(<>(s_ok_seen && !r_ok_seen)); |
||||
|
// property 1 of [D'AJJL01]: "the maximum probability that eventually the sender |
||||
|
// does not report a successful transmission" |
||||
|
property P_1 = Pmax(<>(s_nok_seen || s_dk_seen)); |
||||
|
// property 2 of [D'AJJL01]: "the maximum probability that eventually the sender |
||||
|
// reports an uncertainty on the success of the transmission" |
||||
|
property P_2 = Pmax(<>(s_dk_seen)); |
||||
|
// property 3 of [D'AJJL01]: "the maximum probability that eventually the sender |
||||
|
// reports an unsuccessful transmission after more than 8 chunks have been sent successfully" |
||||
|
property P_3 = Pmax(<>(s_nok_seen && i > 8)); |
||||
|
// property 4 of [D'AJJL01]: "the maximum probability that eventually the receiver |
||||
|
// does not receive any chunk and the sender tried to send a chunk" |
||||
|
property P_4 = Pmax(<>((s_ok_seen || s_nok_seen || s_dk_seen) && !get_k_seen)); |
||||
|
|
||||
|
|
||||
|
process Sender() |
||||
|
{ |
||||
|
bool bit; |
||||
|
int(0..MAX) rc; |
||||
|
clock c; |
||||
|
|
||||
|
try |
||||
|
{ |
||||
|
do { |
||||
|
:: when urgent(i < N) {= i++ =}; |
||||
|
do |
||||
|
{ |
||||
|
// send frame |
||||
|
invariant(c <= 0) put_k {= ff = (i == 1), lf = (i == N), ab = bit, c = 0 =}; |
||||
|
invariant(c <= TS) alt { |
||||
|
:: // receive ack |
||||
|
get_l {= bit = !bit, rc = 0, c = 0 =}; |
||||
|
urgent break |
||||
|
:: // timeout |
||||
|
when(c >= TS) |
||||
|
if(rc < MAX) |
||||
|
{ |
||||
|
// retry |
||||
|
{= rc++, c = 0 =} |
||||
|
} |
||||
|
else if(i < N) |
||||
|
{ |
||||
|
// no retries left |
||||
|
s_nok {= rc = 0, c = 0 =}; |
||||
|
urgent throw(error) |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
// no retries left |
||||
|
s_dk {= rc = 0, c = 0 =}; |
||||
|
urgent throw(error) |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
:: when(i == N) |
||||
|
// file transmission successfully completed |
||||
|
invariant(c <= 0) s_ok {= first_file_done = true =}; |
||||
|
urgent break |
||||
|
} |
||||
|
} |
||||
|
catch error |
||||
|
{ |
||||
|
// File transfer did not succeed: wait, then restart with next file |
||||
|
invariant(c <= SYNC) when(c >= SYNC) |
||||
|
s_restart {= bit = false, first_file_done = true =} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
process Receiver() |
||||
|
{ |
||||
|
bool r_ff, r_lf, r_ab; |
||||
|
bool bit; |
||||
|
clock c; |
||||
|
|
||||
|
// receive first frame |
||||
|
if(ff) { get_k {= c = 0, bit = ab, r_ff = ff, r_lf = lf, r_ab = ab =} } |
||||
|
else { get_k {= c = 0, premature_timeout = true =}; stop }; |
||||
|
do |
||||
|
{ |
||||
|
invariant(c <= 0) |
||||
|
{ |
||||
|
if(r_ab != bit) |
||||
|
{ |
||||
|
// repetition, re-ack |
||||
|
put_l |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
// report frame |
||||
|
if(r_lf) { r_ok } |
||||
|
else if(r_ff) { r_fst } |
||||
|
else { r_inc }; |
||||
|
put_l {= bit = !bit =} |
||||
|
} |
||||
|
}; |
||||
|
invariant(c <= TR) |
||||
|
{ |
||||
|
alt { |
||||
|
:: // receive next frame |
||||
|
get_k {= c = 0, r_ff = ff, r_lf = lf, r_ab = ab =} |
||||
|
:: // timeout |
||||
|
when(c == TR) |
||||
|
if(r_lf) |
||||
|
{ |
||||
|
// we just got the last frame, though |
||||
|
r_timeout; break |
||||
|
} |
||||
|
else |
||||
|
{ |
||||
|
r_nok; |
||||
|
// abort transfer |
||||
|
r_timeout; break |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
}; |
||||
|
Receiver() |
||||
|
} |
||||
|
|
||||
|
process ChannelK() |
||||
|
{ |
||||
|
clock c; |
||||
|
|
||||
|
put_k palt |
||||
|
{ |
||||
|
:98: {= c = 0, inTransitK = true =}; |
||||
|
invariant(c <= TD) alt { |
||||
|
:: get_k {= inTransitK = false =} |
||||
|
:: put_k {= channel_k_overflow = true =}; stop |
||||
|
} |
||||
|
: 2: {==} |
||||
|
}; |
||||
|
ChannelK() |
||||
|
} |
||||
|
|
||||
|
process ChannelL() |
||||
|
{ |
||||
|
clock c; |
||||
|
|
||||
|
put_l palt |
||||
|
{ |
||||
|
:99: {= c = 0, inTransitL = true =}; |
||||
|
invariant(c <= TD) alt { |
||||
|
:: get_l {= inTransitL = false =} |
||||
|
:: put_l {= channel_l_overflow = true =}; stop |
||||
|
} |
||||
|
: 1: {==} |
||||
|
}; |
||||
|
ChannelL() |
||||
|
} |
||||
|
|
||||
|
process Observer() |
||||
|
{ |
||||
|
alt { |
||||
|
:: get_k {= get_k_seen = true =} |
||||
|
:: s_ok {= s_ok_seen = true =} |
||||
|
:: s_nok {= s_nok_seen = true =} |
||||
|
:: s_dk {= s_dk_seen = true =} |
||||
|
:: s_restart {= s_restart_seen = true =} |
||||
|
:: r_ok {= r_ok_seen = true =} |
||||
|
:: r_timeout {= r_timeout_seen = true =} |
||||
|
}; |
||||
|
Observer() |
||||
|
} |
||||
|
|
||||
|
par { |
||||
|
:: Sender() |
||||
|
:: Receiver() |
||||
|
:: ChannelK() |
||||
|
:: ChannelL() |
||||
|
:: Observer() |
||||
|
} |
||||
@ -0,0 +1,63 @@ |
|||||
|
Peak memory usage: 40 MB |
||||
|
Analysis results for brp.modest |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 3959 |
||||
|
Transitions: 4244 |
||||
|
Branches: 4593 |
||||
|
Time: 0.1 s |
||||
|
Rate: 73315 states/s |
||||
|
|
||||
|
+ P_A |
||||
|
Probability: 0 |
||||
|
Time: 0.1 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 1 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_B |
||||
|
Probability: 0 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 1 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_1 |
||||
|
Probability: 0.000423333443357766 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 2.35005704803786E-07 |
||||
|
Iterations: 13 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_2 |
||||
|
Probability: 2.64530890961023E-05 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 2.05561452068843E-07 |
||||
|
Iterations: 14 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_3 |
||||
|
Probability: 0.000185191226393368 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 3.32462409056221E-07 |
||||
|
Iterations: 13 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ P_4 |
||||
|
Probability: 8E-06 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 0 |
||||
|
Iterations: 2 |
||||
|
Time: 0.0 s |
||||
2129
examples/jani-examples/consensus-6.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,27 @@ |
|||||
|
Peak memory usage: 530 MB |
||||
|
Analysis results for consensus-6.jani |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 2345194 |
||||
|
Transitions: 9418584 |
||||
|
Branches: 13891248 |
||||
|
Time: 8.7 s |
||||
|
Rate: 270964 states/s |
||||
|
|
||||
|
+ C1 |
||||
|
Result: True |
||||
|
Time for min. prob. 0 states: 1.6 s |
||||
|
Time for min. prob. 1 states: 0.1 s |
||||
|
Time: 1.7 s |
||||
|
Min. probability: 1 |
||||
|
|
||||
|
+ C2 |
||||
|
Probability: 0.395776147642961 |
||||
|
Time for min. prob. 0 states: 2.0 s |
||||
|
Time for min. prob. 1 states: 0.1 s |
||||
|
Time: 125.8 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 9.96634356860147E-07 |
||||
|
Iterations: 2137 |
||||
|
Time: 123.8 s |
||||
@ -0,0 +1,157 @@ |
|||||
|
// Modest version of http://www.prismmodelchecker.org/casestudies/consensus_prism.php |
||||
|
// Command line: mcsta.exe consensus-6.modest -S Memory --nochainopt --bounded-alg StateElimination -E "K=2" |
||||
|
|
||||
|
action done; |
||||
|
|
||||
|
// constants |
||||
|
const int N = 6; |
||||
|
const int K = 4; |
||||
|
const int range = 2 * (K + 1) * N; |
||||
|
const int counter_init = (K + 1) * N; |
||||
|
const int left = N; |
||||
|
const int right = 2 * (K + 1) * N - N; |
||||
|
|
||||
|
// shared coin |
||||
|
int(0..range) counter = counter_init; |
||||
|
reward coin_flips; |
||||
|
|
||||
|
property C1 = P(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1)) >= 1; |
||||
|
property C2 = Pmin(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1 && coin1 == 1 && coin2 == 1 && coin3 == 1 && coin4 == 1 && coin5 == 1 && coin6 == 1)); |
||||
|
|
||||
|
int(0..1) fin1, fin2, fin3, fin4, fin5, fin6; |
||||
|
int(0..1) coin1, coin2, coin3, coin4, coin5, coin6; |
||||
|
|
||||
|
process Tourist1() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin1 = 0, coin_flips++ =} :1: {= coin1 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin1 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin1 == 1 && counter < range) {= counter++, coin1 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin1 = 0, fin1 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin1 = 1, fin1 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist1() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist2() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin2 = 0, coin_flips++ =} :1: {= coin2 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin2 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin2 == 1 && counter < range) {= counter++, coin2 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin2 = 0, fin2 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin2 = 1, fin2 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist2() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist3() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin3 = 0, coin_flips++ =} :1: {= coin3 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin3 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin3 == 1 && counter < range) {= counter++, coin3 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin3 = 0, fin3 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin3 = 1, fin3 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist3() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist4() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin4 = 0, coin_flips++ =} :1: {= coin4 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin4 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin4 == 1 && counter < range) {= counter++, coin4 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin4 = 0, fin4 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin4 = 1, fin4 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist4() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist5() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin5 = 0, coin_flips++ =} :1: {= coin5 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin5 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin5 == 1 && counter < range) {= counter++, coin5 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin5 = 0, fin5 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin5 = 1, fin5 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist5() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
process Tourist6() |
||||
|
{ |
||||
|
process Flip() { palt { :1: {= coin6 = 0, coin_flips++ =} :1: {= coin6 = 1, coin_flips++ =} }; Write() } |
||||
|
process Write() { |
||||
|
alt { |
||||
|
:: when(coin6 == 0 && counter > 0) {= counter-- =}; Check() |
||||
|
:: when(coin6 == 1 && counter < range) {= counter++, coin6 = 0 =}; Check() |
||||
|
} |
||||
|
} |
||||
|
process Check() { |
||||
|
alt { |
||||
|
:: when(counter <= left) {= coin6 = 0, fin6 = 1 =}; Finished() |
||||
|
:: when(counter >= right) {= coin6 = 1, fin6 = 1 =}; Finished() |
||||
|
:: when(counter > left && counter < right) Tourist6() |
||||
|
} |
||||
|
} |
||||
|
process Finished() { done; Finished() } |
||||
|
|
||||
|
Flip() |
||||
|
} |
||||
|
|
||||
|
par { |
||||
|
:: Tourist1() |
||||
|
:: Tourist2() |
||||
|
:: Tourist3() |
||||
|
:: Tourist4() |
||||
|
:: Tourist5() |
||||
|
:: Tourist6() |
||||
|
} |
||||
@ -0,0 +1,27 @@ |
|||||
|
Peak memory usage: 531 MB |
||||
|
Analysis results for consensus-6.modest |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 2345194 |
||||
|
Transitions: 9418584 |
||||
|
Branches: 13891248 |
||||
|
Time: 8.2 s |
||||
|
Rate: 287507 states/s |
||||
|
|
||||
|
+ C1 |
||||
|
Result: True |
||||
|
Time for min. prob. 0 states: 1.5 s |
||||
|
Time for min. prob. 1 states: 0.2 s |
||||
|
Time: 1.7 s |
||||
|
Min. probability: 1 |
||||
|
|
||||
|
+ C2 |
||||
|
Probability: 0.395776147642961 |
||||
|
Time for min. prob. 0 states: 2.0 s |
||||
|
Time for min. prob. 1 states: 0.1 s |
||||
|
Time: 126.8 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 9.96634356860147E-07 |
||||
|
Iterations: 2137 |
||||
|
Time: 124.7 s |
||||
@ -0,0 +1,354 @@ |
|||||
|
{ |
||||
|
"jani-version": 1, |
||||
|
"name": "dice", |
||||
|
"type" : "mdp", |
||||
|
"actions" : [], |
||||
|
"variables" : [ |
||||
|
{ |
||||
|
"name": "thrownSix", |
||||
|
"type": "bool", |
||||
|
"initial-value": false |
||||
|
}, |
||||
|
{ |
||||
|
"name": "terminated", |
||||
|
"type": "bool", |
||||
|
"initial-value": false |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"name" : "step" |
||||
|
} |
||||
|
], |
||||
|
"properties" : [ |
||||
|
{ |
||||
|
"name" : "ProbThrowSix", |
||||
|
"reach" : "thrownSix", |
||||
|
"type": "probability-max-query" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "StepsUntilReach", |
||||
|
"reach" : "terminated", |
||||
|
"reward": "step", |
||||
|
"type": "expected-reachability-reward-max-query" |
||||
|
} |
||||
|
], |
||||
|
"automata" : [ |
||||
|
{ |
||||
|
"name" : "dice", |
||||
|
"variables" : [ |
||||
|
{ |
||||
|
"name" : "d", |
||||
|
"type" : { |
||||
|
"kind": "bounded", |
||||
|
"base": "int", |
||||
|
"lower-bound" : 0, |
||||
|
"upper-bound" : 6 |
||||
|
}, |
||||
|
"initial-value" : 0 |
||||
|
} |
||||
|
], |
||||
|
"locations" : [ |
||||
|
{ |
||||
|
"name" : "s0" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s1" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s2" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s3" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s4" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s5" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s6" |
||||
|
}, |
||||
|
{ |
||||
|
"name" : "s7" |
||||
|
} |
||||
|
], |
||||
|
"initial-location" : "s0", |
||||
|
"edges" : [ |
||||
|
{ |
||||
|
"location" : "s0", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s1", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s2", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s1", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s3", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s4", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s2", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s5", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s6", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s3", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s1", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 1 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s4", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 2 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 3 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s5", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 4 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 5 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s6", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s2", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"probability" : 0.5, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [ |
||||
|
{ |
||||
|
"ref" : "d", |
||||
|
"value" : 6 |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "thrownSix", |
||||
|
"value" : true |
||||
|
}, |
||||
|
{ |
||||
|
"ref" : "terminated", |
||||
|
"value" : true |
||||
|
} |
||||
|
], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
}, |
||||
|
{ |
||||
|
"location" : "s7", |
||||
|
"guard" : true, |
||||
|
"destinations" : [ |
||||
|
{ |
||||
|
"probability" : 1, |
||||
|
"location" : "s7", |
||||
|
"assignments" : [], |
||||
|
"rewards" : [ |
||||
|
{ |
||||
|
"ref" : "step", |
||||
|
"value" : 1 |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
] |
||||
|
} |
||||
|
], |
||||
|
"system" : "dice" |
||||
|
} |
||||
@ -0,0 +1,29 @@ |
|||||
|
Peak memory usage: 36 MB |
||||
|
Analysis results for dice.jani |
||||
|
|
||||
|
+ State space exploration |
||||
|
States: 8 |
||||
|
Transitions: 8 |
||||
|
Branches: 14 |
||||
|
Time: 0.0 s |
||||
|
Rate: 190 states/s |
||||
|
|
||||
|
+ ProbThrowSix |
||||
|
Probability: 0.166666626930237 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 7.15255907834985E-07 |
||||
|
Iterations: 11 |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ StepsUntilReach |
||||
|
Value: 3.66666650772095 |
||||
|
Time for min. prob. 0 states: 0.0 s |
||||
|
Time for min. prob. 1 states: 0.0 s |
||||
|
Time: 0.0 s |
||||
|
|
||||
|
+ Value iteration |
||||
|
Final error: 4.08717619857464E-07 |
||||
|
Iterations: 12 |
||||
|
Time: 0.0 s |
||||
@ -0,0 +1,16 @@ |
|||||
|
dtmc |
||||
|
|
||||
|
module tiny |
||||
|
s : [0 .. 3] init 0; |
||||
|
|
||||
|
[] s = 0 -> 1/3 : (s'=1) + 1/3 : (s'=2) + 1/3 : (s'=3); |
||||
|
[] s = 1 -> 1 : (s'=2); |
||||
|
[] s = 2 -> 1/2 : (s'=2) + 1/2 : (s'=1); |
||||
|
[] s = 3 -> 1 : (s'=3); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards |
||||
|
s=1 : 10; |
||||
|
s=3 : 5; |
||||
|
endrewards |
||||
@ -0,0 +1,2 @@ |
|||||
|
#!/bin/bash |
||||
|
pip install -ve . --install-option="--cmake=" --install-option="--make=" |
||||
@ -1,9 +1,83 @@ |
|||||
include(ExternalProject) |
|
||||
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 |
|
||||
PREFIX ${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2 |
|
||||
BUILD_COMMAND make |
|
||||
BUILD_IN_SOURCE 1 |
|
||||
) |
|
||||
|
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 |
||||
|
) |
||||
|
|
||||
|
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 |
||||
|
) |
||||
|
|
||||
|
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" |
||||
|
) |
||||
|
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) |
||||
|
|
||||
|
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" |
||||
|
# 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 |
||||
|
# 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" |
||||
|
# 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) |
||||
|
# 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) |
||||
@ -1,42 +0,0 @@ |
|||||
cmake_minimum_required (VERSION 2.8.6) |
|
||||
|
|
||||
# Set project name |
|
||||
project (cudd C CXX) |
|
||||
|
|
||||
# Main Sources |
|
||||
file(GLOB_RECURSE CUDD_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h) |
|
||||
file(GLOB_RECURSE CUDD_HEADERS_CXX ${PROJECT_SOURCE_DIR}/src/*.hh) |
|
||||
file(GLOB_RECURSE CUDD_SOURCES ${PROJECT_SOURCE_DIR}/src/*.c) |
|
||||
file(GLOB_RECURSE CUDD_SOURCES_CXX ${PROJECT_SOURCE_DIR}/src/*.cc) |
|
||||
|
|
||||
|
|
||||
# Add base folder for better inclusion paths |
|
||||
include_directories("${PROJECT_SOURCE_DIR}/src") |
|
||||
include_directories("${PROJECT_SOURCE_DIR}/src/cudd") |
|
||||
include_directories("${PROJECT_SOURCE_DIR}/src/dddmp") |
|
||||
include_directories("${PROJECT_SOURCE_DIR}/src/epd") |
|
||||
include_directories("${PROJECT_SOURCE_DIR}/src/mtr") |
|
||||
include_directories("${PROJECT_SOURCE_DIR}/src/nanotrav") |
|
||||
include_directories("${PROJECT_SOURCE_DIR}/src/st") |
|
||||
include_directories("${PROJECT_SOURCE_DIR}/src/util") |
|
||||
|
|
||||
if(CMAKE_COMPILER_IS_GNUCC) |
|
||||
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-function") |
|
||||
elseif(MSVC) |
|
||||
# required for GMM to compile, ugly error directive in their code |
|
||||
add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS) |
|
||||
else(CLANG) |
|
||||
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-newline-eof -Wno-unneeded-internal-declaration -Wno-unused-variable -Wno-unused-const-variable") |
|
||||
endif() |
|
||||
|
|
||||
# Since we do not target Alphas, this symbol is always set |
|
||||
add_definitions(-DHAVE_IEEE_754) |
|
||||
|
|
||||
if(CMAKE_SIZEOF_VOID_P EQUAL 8) |
|
||||
message(STATUS "CUDD: Targeting 64bit architecture") |
|
||||
add_definitions(-DSIZEOF_VOID_P=8) |
|
||||
add_definitions(-DSIZEOF_LONG=8) |
|
||||
endif() |
|
||||
|
|
||||
# Add the library |
|
||||
add_library(cudd ${CUDD_SOURCES} ${CUDD_HEADERS} ${CUDD_HEADERS_CXX} ${CUDD_SOURCES_CXX}) |
|
||||
@ -1,323 +0,0 @@ |
|||||
# $Id$
|
|
||||
#
|
|
||||
# Makefile for the CUDD distribution kit
|
|
||||
#---------------------------------------------------------------------------
|
|
||||
|
|
||||
# Beginning of the configuration section. These symbol definitions can
|
|
||||
# be overridden from the command line.
|
|
||||
|
|
||||
# C++ compiler
|
|
||||
#CXX = g++
|
|
||||
#CXX = icpc
|
|
||||
#CXX = ecpc
|
|
||||
#CXX = CC
|
|
||||
#CXX = /usr/local/opt/SUNWspro/bin/CC
|
|
||||
#CXX = cxx
|
|
||||
CXX = clang++ |
|
||||
|
|
||||
# Specific options for compilation of C++ files.
|
|
||||
CXXFLAGS = -std=c++11 -stdlib=libc++ |
|
||||
# Stricter standard conformance for g++.
|
|
||||
#CXXFLAGS = -std=c++98
|
|
||||
# For Sun CC version 5, this invokes compatibility mode.
|
|
||||
#CXXFLAGS = -compat
|
|
||||
# On some versions of UP-UX, it is necessary to pass the option +a1
|
|
||||
# to CC for the C++ test program to compile successfully.
|
|
||||
#CXXFLAGS = +a1
|
|
||||
|
|
||||
# C compiler used for all targets except optimize_dec, which always uses cc.
|
|
||||
#CC = cc
|
|
||||
#CC = /usr/local/opt/SUNWspro/bin/cc
|
|
||||
#CC = gcc
|
|
||||
#CC = icc
|
|
||||
#CC = ecc
|
|
||||
#CC = /usr/ucb/cc
|
|
||||
#CC = c89
|
|
||||
#CC = $(CXX)
|
|
||||
CC = clang |
|
||||
|
|
||||
# On some machines ranlib is either non-existent or redundant.
|
|
||||
# Use the following definition if your machine has ranlib and you think
|
|
||||
# it is needed.
|
|
||||
RANLIB = ranlib |
|
||||
# Use the following definition if your machine either does not have
|
|
||||
# ranlib (e.g., SUN running solaris) or can do without it (e.g., DEC Alpha).
|
|
||||
#RANLIB = :
|
|
||||
|
|
||||
# Use ICFLAGS to specify machine-independent compilation flags.
|
|
||||
# These three are typical settings for cc.
|
|
||||
#ICFLAGS = -g
|
|
||||
#ICFLAGS = -O
|
|
||||
#ICFLAGS =
|
|
||||
# These two are typical settings for optimized code with gcc.
|
|
||||
#ICFLAGS = -g -O3 -Wall
|
|
||||
ICFLAGS = -O4 |
|
||||
|
|
||||
# Use XCFLAGS to specify machine-dependent compilation flags.
|
|
||||
# For some platforms no special flags are needed.
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DBSD
|
|
||||
#
|
|
||||
#==========================
|
|
||||
# Linux
|
|
||||
#
|
|
||||
# Gcc 4.2.4 or higher on i686.
|
|
||||
XCFLAGS = -arch x86_64 -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 |
|
||||
# Gcc 3.2.2 or higher on i686.
|
|
||||
#XCFLAGS = -mtune=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD
|
|
||||
# Gcc 2.8.1 on i686.
|
|
||||
#XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
|
|
||||
# Gcc 4.2.4 or higher on x86_64 (64-bit compilation)
|
|
||||
#XCFLAGS = -mtune=native -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
|
|
||||
# Gcc 4.2.4 or higher on x86_64 (32-bit compilation)
|
|
||||
#XCFLAGS = -m32 -mtune=native -malign-double -DHAVE_IEEE_754 -DBSD
|
|
||||
# Icc on i686 (older versions may not support -xHost).
|
|
||||
#XCFLAGS = -ansi -xHost -align -ip -DHAVE_IEEE_754 -DBSD
|
|
||||
# Icc on x86_64 (64-bit compilation).
|
|
||||
#XCFLAGS = -ansi -xHost -align -ip -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
|
|
||||
# Gcc on ia64.
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
|
|
||||
# Icc/ecc on ia64.
|
|
||||
#XCFLAGS = -ansi -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
|
|
||||
#
|
|
||||
#==========================
|
|
||||
# Solaris
|
|
||||
#
|
|
||||
# For Solaris, BSD should not be replaced by UNIX100.
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -DEPD_BIG_ENDIAN
|
|
||||
# Gcc 2.8.1 or higher on Ultrasparc.
|
|
||||
#XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100 -DEPD_BIG_ENDIAN
|
|
||||
# For Solaris 2.5 and higher, optimized code with /usr/bin/cc or CC.
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -xO5 -native -dalign -DEPD_BIG_ENDIAN
|
|
||||
# On IA platforms, -dalign is not supported and causes warnings.
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -xO5 -native
|
|
||||
# Recent Sun compilers won't let you use -native on old Ultras.
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -xO5 -dalign -xlibmil -DEPD_BIG_ENDIAN
|
|
||||
# For Solaris 2.4, optimized code with /usr/bin/cc.
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -xO4 -dalign -DEPD_BIG_ENDIAN
|
|
||||
# For Solaris 2.5 and higher, optimized code with /usr/ucb/cc.
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DBSD -xO5 -native -dalign -DEPD_BIG_ENDIAN
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DBSD -xO5 -dalign -xlibmil -DEPD_BIG_ENDIAN
|
|
||||
# For Solaris 2.4, optimized code with /usr/ucb/cc.
|
|
||||
#XCFLAGS = -DHAVE_IEEE_754 -DBSD -xO4 -dalign -DEPD_BIG_ENDIAN
|
|
||||
#
|
|
||||
#==========================
|
|
||||
# DEC Alphas running Digital Unix
|
|
||||
#
|
|
||||
# For DEC Alphas either -ieee_with_inexact or -ieee_with_no_inexact is
|
|
||||
# needed. If you use only BDDs, -ieee_with_no_inexact is enough.
|
|
||||
# In the following, we consider three different compilers:
|
|
||||
# - the old native compiler (the one of MIPS ancestry that produces u-code);
|
|
||||
# - the new native compiler;
|
|
||||
# - gcc
|
|
||||
# On the Alphas, gcc (as of release 2.7.2) does not support 32-bit pointers
|
|
||||
# and IEEE 754 floating point arithmetic. Therefore, for this architecture
|
|
||||
# only, the native compilers provide a substatial advantage.
|
|
||||
# With the native compilers, specify -xtaso for 32-bit pointers.
|
|
||||
# Do not use -xtaso_short because explicit reference to stdout and stderr
|
|
||||
# does not work with this option. (Among other things.)
|
|
||||
# Notice that -taso must be included in LDFLAGS for -xtaso to work.
|
|
||||
# Given the number of possible choices, only some typical configurations
|
|
||||
# are proposed here.
|
|
||||
#
|
|
||||
# Old native compiler for the Alphas; 64-bit pointers.
|
|
||||
#XCFLAGS = -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
|
|
||||
# Old native compiler for the Alphas; 32-bit pointers.
|
|
||||
#XCFLAGS = -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -xtaso -DSIZEOF_LONG=8
|
|
||||
# New native compiler for the Alphas; 64-bit pointers.
|
|
||||
#XCFLAGS = -g3 -O4 -std -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
|
|
||||
# New native compiler for the Alphas; 32-bit pointers.
|
|
||||
#XCFLAGS = -g3 -O4 -std -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -xtaso -DSIZEOF_LONG=8
|
|
||||
# gcc for the Alphas: compile without HAVE_IEEE_754.
|
|
||||
#XCFLAGS = -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
|
|
||||
#
|
|
||||
#==========================
|
|
||||
#
|
|
||||
# IBM RS6000
|
|
||||
#
|
|
||||
# For the IBM RS6000 -qstrict is necessary when specifying -O3 with cc.
|
|
||||
#XCFLAGS = -DBSD -DHAVE_IEEE_754 -DEPD_BIG_ENDIAN -O3 -qstrict
|
|
||||
#
|
|
||||
#==========================
|
|
||||
#
|
|
||||
# HP-UX
|
|
||||
#
|
|
||||
# I haven't figured out how to enable IEEE 754 on the HPs I've tried...
|
|
||||
# For HP-UX using gcc.
|
|
||||
#XCFLAGS = -DUNIX100 -DEPD_BIG_ENDIAN
|
|
||||
# For HP-UX using c89.
|
|
||||
#XCFLAGS = +O3 -DUNIX100 -DEPD_BIG_ENDIAN
|
|
||||
#
|
|
||||
#==========================
|
|
||||
#
|
|
||||
# Windows 95/98/NT/XP/Vista/7 with Cygwin tools
|
|
||||
#
|
|
||||
# The value of RLIMIT_DATA_DEFAULT should reflect the amount of
|
|
||||
# available memory (expressed in bytes).
|
|
||||
# Recent versions of cygwin have getrlimit, but the datasize limit
|
|
||||
# cannot be set.
|
|
||||
#XCFLAGS = -mtune=native -malign-double -DHAVE_IEEE_754 -DHAVE_GETRLIMIT=0 -DRLIMIT_DATA_DEFAULT=268435456
|
|
||||
|
|
||||
|
|
||||
# Define the level of self-checking and verbosity of the CUDD package.
|
|
||||
#DDDEBUG = -DDD_DEBUG -DDD_VERBOSE -DDD_STATS -DDD_CACHE_PROFILE -DDD_UNIQUE_PROFILE -DDD_COUNT
|
|
||||
DDDEBUG = |
|
||||
|
|
||||
# Define the level of self-checking and verbosity of the MTR package.
|
|
||||
#MTRDEBUG = -DMTR_DEBUG
|
|
||||
MTRDEBUG = |
|
||||
|
|
||||
# Loader options.
|
|
||||
LDFLAGS = |
|
||||
# This may produce faster code on the DECstations.
|
|
||||
#LDFLAGS = -jmpopt -Olimit 1000
|
|
||||
# This may be necessary under some old versions of Linux.
|
|
||||
#LDFLAGS = -static
|
|
||||
# This normally makes the program faster on the DEC Alphas.
|
|
||||
#LDFLAGS = -non_shared -om
|
|
||||
# This is for 32-bit pointers on the DEC Alphas.
|
|
||||
#LDFLAGS = -non_shared -om -taso
|
|
||||
#LDFLAGS = -non_shared -taso
|
|
||||
|
|
||||
# Define PURE as purify to link with purify.
|
|
||||
# Define PURE as quantify to link with quantify.
|
|
||||
# Remember to compile with -g if you want line-by-line info with quantify.
|
|
||||
PURE = |
|
||||
#PURE = purify
|
|
||||
#PURE = quantify
|
|
||||
|
|
||||
# Define EXE as .exe for MS-DOS and derivatives. Not required by recent
|
|
||||
# versions of cygwin.
|
|
||||
EXE = |
|
||||
#EXE = .exe
|
|
||||
|
|
||||
# End of the configuration section.
|
|
||||
#---------------------------------------------------------------------------
|
|
||||
|
|
||||
MFLAG = -DMNEMOSYNE |
|
||||
MNEMLIB = ../mnemosyne/libmnem.a |
|
||||
|
|
||||
DDWDIR = . |
|
||||
IDIR = $(DDWDIR)/include |
|
||||
INCLUDE = -I$(IDIR) |
|
||||
|
|
||||
BDIRS = cudd dddmp mtr st util epd obj |
|
||||
DIRS = $(BDIRS) |
|
||||
|
|
||||
#------------------------------------------------------------------------
|
|
||||
|
|
||||
.PHONY : build |
|
||||
.PHONY : nanotrav |
|
||||
.PHONY : check_leaks |
|
||||
.PHONY : optimize_dec |
|
||||
.PHONY : testcudd |
|
||||
.PHONY : libobj |
|
||||
.PHONY : testobj |
|
||||
.PHONY : testdddmp |
|
||||
.PHONY : testmtr |
|
||||
.PHONY : lint |
|
||||
.PHONY : all |
|
||||
.PHONY : clean |
|
||||
.PHONY : distclean |
|
||||
|
|
||||
|
|
||||
build: |
|
||||
sh ./setup.sh |
|
||||
@for dir in $(DIRS); do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Making $$dir ...; \
|
|
||||
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
|
|
||||
done |
|
||||
|
|
||||
nanotrav: build |
|
||||
|
|
||||
check_leaks: |
|
||||
sh ./setup.sh |
|
||||
@for dir in mnemosyne $(DIRS); do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Making $$dir ...; \
|
|
||||
make CC=$(CC) RANLIB=$(RANLIB) MFLAG=$(MFLAG) MNEMLIB=$(MNEMLIB) ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" EXE="$(EXE)" )\
|
|
||||
done |
|
||||
|
|
||||
optimize_dec: |
|
||||
sh ./setup.sh |
|
||||
@for dir in $(DIRS); do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Making $$dir ...; \
|
|
||||
make CC=$(CC) RANLIB=$(RANLIB) XCFLAGS="$(XCFLAGS)" LDFLAGS="$(LDFLAGS)" optimize_dec )\
|
|
||||
done |
|
||||
|
|
||||
lint: |
|
||||
sh ./setup.sh |
|
||||
@for dir in $(DIRS) obj; do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Making lint in $$dir ...; \
|
|
||||
make CC=$(CC) lint )\
|
|
||||
done |
|
||||
|
|
||||
tags: |
|
||||
sh ./setup.sh |
|
||||
@for dir in $(DIRS) obj; do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Making tags in $$dir ...; \
|
|
||||
make CC=$(CC) tags )\
|
|
||||
done |
|
||||
|
|
||||
all: |
|
||||
sh ./setup.sh |
|
||||
@for dir in $(DIRS); do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Making all in $$dir ...; \
|
|
||||
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" all )\
|
|
||||
done |
|
||||
|
|
||||
testcudd: |
|
||||
sh ./setup.sh |
|
||||
@for dir in util st mtr epd; do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Making $$dir ...; \
|
|
||||
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
|
|
||||
done |
|
||||
@(cd cudd; \
|
|
||||
echo Making testcudd ...; \
|
|
||||
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testcudd$(EXE) ) |
|
||||
|
|
||||
objlib: |
|
||||
sh ./setup.sh |
|
||||
@for dir in $(BDIRS); do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Making $$dir ...; \
|
|
||||
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
|
|
||||
done |
|
||||
@(cd obj; \
|
|
||||
echo Making obj ...; \
|
|
||||
make CXX=$(CXX) CXXFLAGS=$(CXXFLAGS) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" ) |
|
||||
|
|
||||
testobj: objlib |
|
||||
@(cd obj; \
|
|
||||
echo Making testobj ...; \
|
|
||||
make CXX=$(CXX) CXXFLAGS=$(CXXFLAGS) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testobj$(EXE) ) |
|
||||
|
|
||||
testdddmp: build |
|
||||
@(cd dddmp; \
|
|
||||
echo Making testdddmp ...; \
|
|
||||
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testdddmp$(EXE) ) |
|
||||
|
|
||||
testmtr: build |
|
||||
@(cd mtr; \
|
|
||||
echo Making testmtr ...; \
|
|
||||
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testmtr$(EXE) ) |
|
||||
|
|
||||
clean: |
|
||||
@for dir in mnemosyne $(DIRS) obj; do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Cleaning $$dir ...; \
|
|
||||
make -s clean ) \
|
|
||||
done |
|
||||
|
|
||||
distclean: |
|
||||
@for dir in mnemosyne $(DIRS) obj; do \
|
|
||||
(cd $$dir; \
|
|
||||
echo Cleaning $$dir ...; \
|
|
||||
make -s EXE="$(EXE)" distclean ) \
|
|
||||
done |
|
||||
sh ./shutdown.sh |
|
||||
@ -1,177 +0,0 @@ |
|||||
$Id$ |
|
||||
|
|
||||
This directory contains a set of packages that allow you to build a toy |
|
||||
application based on the CUDD package. |
|
||||
|
|
||||
The CUDD package is a package written in C for the manipulation of |
|
||||
decision diagrams. It supports binary decision diagrams (BDDs), |
|
||||
algebraic decision diagrams (ADDs), and Zero-Suppressed BDDs (ZDDs). |
|
||||
|
|
||||
The toy application provided in this kit is called nanotrav and is a |
|
||||
simple-minded FSM traversal program. (See the README file and the man |
|
||||
page nanotrav.1 in the nanotrav directory for the details.) It is |
|
||||
included so that you can run a sanity check on your installation. |
|
||||
|
|
||||
INSTALLATION |
|
||||
|
|
||||
Before you build the libraries and programs, you need to check the |
|
||||
Makefile in the top directory. Go through the definitions contained in the |
|
||||
configuration section, and select the desired compiler and compilation |
|
||||
flags. Instructions are provided in the comments of the Makefile. |
|
||||
|
|
||||
You can always specify the options on the command line. For instance, |
|
||||
on some machines you can build a "fast" version of the program by typing: |
|
||||
|
|
||||
make DDDEBUG= MTRDEBUG= ICFLAGS=-O2 |
|
||||
|
|
||||
The Makefile supports several targets: |
|
||||
|
|
||||
make: |
|
||||
Creates a "plain" version of the program. |
|
||||
|
|
||||
make testdddmp: |
|
||||
Builds a test program (testdddmp) for BDD loading from and |
|
||||
storing to disk. See file README.test in the dddmp directory for |
|
||||
how to run the program. |
|
||||
|
|
||||
make testobj: |
|
||||
Builds a test program for the C++ interface. Requires a C++ |
|
||||
compiler. To run the program, run obj/testobj. |
|
||||
|
|
||||
make testcudd: |
|
||||
Builds a test program for CUDD. To run the program, go to the |
|
||||
cudd directory and type "./testcudd -p 2 r7x8.1.mat". The result |
|
||||
can be compared to r7x7.1.out. |
|
||||
|
|
||||
make testmtr: |
|
||||
Builds a test program for the mtr package. To run the program, |
|
||||
go to the mtr directory and type "./testmtr -p 1 test.groups". |
|
||||
|
|
||||
make clean: |
|
||||
Cleans directories, but leaves libraries and programs. |
|
||||
|
|
||||
make distclean: |
|
||||
Cleans thoroughly, returning the directories to their pristine |
|
||||
state. |
|
||||
|
|
||||
The following targets are more or less obsolete and may disappear or |
|
||||
change in the future. |
|
||||
|
|
||||
make check_leaks: |
|
||||
Creates a version of the program with the mnemosyne library |
|
||||
linked to it. It also builds the mnemalyse program, which |
|
||||
helps in finding memory leaks. This target does not work on the |
|
||||
IBM RS6000. The makefile also supports purify. To use purify, |
|
||||
set the PURE variable in the Makefile, and use the standard |
|
||||
target. |
|
||||
|
|
||||
make optimize_dec: |
|
||||
Builds a version of the program using the u-code compiler |
|
||||
available on DEC machines (DECstations and Alphas). The newer |
|
||||
native compiler on the Alphas does not use u-code, though. |
|
||||
Therefore the standard target should be used with it. |
|
||||
|
|
||||
make lint: |
|
||||
Runs lint on all subdirectories except mnemosyne. Creates lint |
|
||||
libraries for all object libraries. |
|
||||
|
|
||||
make tags: |
|
||||
Builds ctags-style tag files for all subdirectories except |
|
||||
mnemosyne. |
|
||||
|
|
||||
make all: |
|
||||
Makes all of the above, except check_leaks, which is |
|
||||
incompatible with a plain "make." |
|
||||
|
|
||||
All targets, except clean and distclean, will create the include |
|
||||
directory if it does not already exist. |
|
||||
|
|
||||
The Makefile does not compile the SIS interface (cuddBddPort.c and |
|
||||
cuddPwPt.c found in subdirectory sis). To compile the interface, you |
|
||||
also need array.h and var_set.h, which are not part of this |
|
||||
distribution, but come with SIS. Detailed instructions on how to |
|
||||
integrate the CUDD package in SIS can be found in the documentation |
|
||||
(cudd/doc). |
|
||||
|
|
||||
PLATFORMS |
|
||||
|
|
||||
This kit has been successfully built on the following configurations: |
|
||||
|
|
||||
PC (ia32 and ia64) running Ubuntu with gcc |
|
||||
PC (ia32 and ia64) running Ubuntu with g++ |
|
||||
PC (ia32 and ia64) running Linux RedHat with gcc |
|
||||
PC (ia32 and ia64) running Linux RedHat with g++ |
|
||||
PC (ia64) running Cygwin on Windows 7 and Vista with gcc |
|
||||
PC (ia64) running Cygwin on Windows 7 and Vista with g++ |
|
||||
|
|
||||
Platforms to which I have no longer access and therefore are no longer |
|
||||
supported. |
|
||||
|
|
||||
PC (ia32) running Linux RedHat with icc |
|
||||
PC (ia32) running Linux RedHat with icpc |
|
||||
PC (ia64) running Linux RedHat with ecc |
|
||||
PC (ia64) running Linux RedHat with ecpc |
|
||||
SUN running Solaris 2.8 with cc |
|
||||
SUN running Solaris 2.8 with CC |
|
||||
SUN running Solaris 2.8 with gcc |
|
||||
SUN running Solaris 2.8 with g++ |
|
||||
DECstation running Ultrix with cc |
|
||||
DECstation running Ultrix with gcc |
|
||||
IBM RS6000 running AIX 3.2.4 with cc (**) |
|
||||
IBM RS6000 running AIX 3.2.4 with gcc |
|
||||
IBM RS6000 running AIX 3.2.4 with g++ |
|
||||
SUN running SunOS with gcc |
|
||||
DEC Alpha running Digital Unix with cc |
|
||||
DEC Alpha running Digital Unix with cxx |
|
||||
DEC Alpha running Digital Unix with gcc |
|
||||
HP 9000/770 running HP-UX with c89 |
|
||||
HP 9000/770 running HP-UX with CC |
|
||||
HP 9000/770 running HP-UX with gcc |
|
||||
HP 9000/770 running HP-UX with g++ (*) |
|
||||
SUN running Solaris 2.8 with /usr/ucb/cc |
|
||||
PC running Solaris 2.8 with /usr/bin/cc |
|
||||
PC running Solaris 2.8 with /usr/ucb/cc |
|
||||
PC running Solaris 2.8 with CC |
|
||||
PC running Solaris 2.8 with gcc |
|
||||
PC running Solaris 2.8 with g++ |
|
||||
|
|
||||
NOTES |
|
||||
(*) C programs were compiled with g++, but linked with gcc. |
|
||||
|
|
||||
(**) Some old versions of the AIX cc compiler have buggy optimizers: |
|
||||
Try compiling with -O2 instead of -O3 if the program crashes. |
|
||||
|
|
||||
Running lint and compiling with gcc -Wall still produces warnings. |
|
||||
Running `purify' under Solaris 2.8 generates no messages. |
|
||||
|
|
||||
SANITY CHECK |
|
||||
|
|
||||
The directory `nanotrav' contains a very simple application based on the |
|
||||
CUDD package. The `nanotrav' directory contains a man page that |
|
||||
describes the options nanotrav supports. The files *.blif are sample |
|
||||
input files for nanotrav. |
|
||||
|
|
||||
If you have built the mnemosyne library (make check_leaks), you can do |
|
||||
cd mnemosyne |
|
||||
make runmtest |
|
||||
This does not work on machines running SunOS, but the version of |
|
||||
nanotrav that uses mnemosyne may work. |
|
||||
|
|
||||
DOCUMENTATION |
|
||||
|
|
||||
Directory cudd-2.5.0/cudd/doc contains HTML documentation for the CUDD |
|
||||
package. The recommended starting point is cuddIntro.html. Documentation |
|
||||
in both postscript(tm) format and plain text format is also provided. |
|
||||
Documentation for the auxiliary libraries (except for the util library) |
|
||||
is in the doc subdirectories. |
|
||||
|
|
||||
FEEDBACK: |
|
||||
|
|
||||
Send feedback to: |
|
||||
|
|
||||
Fabio Somenzi |
|
||||
University of Colorado at Boulder |
|
||||
ECE Dept. |
|
||||
Boulder, CO 80309-0425 |
|
||||
Fabio@Colorado.EDU |
|
||||
http://vlsi.colorado.edu/~fabio |
|
||||
@ -1,131 +0,0 @@ |
|||||
Release 2.5.0 of Cudd introduces the ability to set timeouts. The |
|
||||
function that is interrupted returns NULL (which the application must |
|
||||
be prepared to handle,) but the BDDs are uncorrupted and the invoking |
|
||||
program can continue to use the manager. |
|
||||
|
|
||||
In addition, reordering is now aware of timeouts, so that it gives up |
|
||||
when a timeout is approaching to give the invoking program a chance to |
|
||||
obtain some results. |
|
||||
|
|
||||
The response time to the timeout is not immediate, though most of the time |
|
||||
it is well below one second. Checking for timeouts has a small overhead. |
|
||||
In experiments, less than 1% has been observed on average. |
|
||||
|
|
||||
Creation of BDD managers with many variables (e.g., tens or hundreds |
|
||||
of thousands) is now much more efficient. Computing small supports of |
|
||||
BDDs when there are many variables is also much more efficient, but |
|
||||
this has been at the cost of separating the function for BDDs and ADDs |
|
||||
(Cudd_Support) from that for ZDDs (Cudd_zddSupport). |
|
||||
|
|
||||
The C++ interface has undergone a major upgrade. |
|
||||
|
|
||||
The handling of variable gruops in reordering has been much improved. |
|
||||
(Thanks to Arie Gurfinkel for a very detailed bug report!) A handful |
|
||||
of other bugs have been fixed as well. |
|
||||
|
|
||||
|
|
||||
New Functions: |
|
||||
|
|
||||
unsigned long Cudd_ReadStartTime(DdManager *unique); |
|
||||
|
|
||||
unsigned long Cudd_ReadElapsedTime(DdManager *unique); |
|
||||
|
|
||||
void Cudd_SetStartTime(DdManager *unique, unsigned long st); |
|
||||
|
|
||||
void Cudd_ResetStartTime(DdManager *unique); |
|
||||
|
|
||||
unsigned long Cudd_ReadTimeLimit(DdManager *unique); |
|
||||
|
|
||||
void Cudd_SetTimeLimit(DdManager *unique, unsigned long tl); |
|
||||
|
|
||||
void Cudd_UpdateTimeLimit(DdManager * unique); |
|
||||
|
|
||||
void Cudd_IncreaseTimeLimit(DdManager * unique, unsigned long increase); |
|
||||
|
|
||||
void Cudd_UnsetTimeLimit(DdManager *unique); |
|
||||
|
|
||||
int Cudd_TimeLimited(DdManager *unique); |
|
||||
|
|
||||
unsigned int Cudd_ReadMaxReorderings (DdManager *dd); |
|
||||
|
|
||||
void Cudd_SetMaxReorderings (DdManager *dd, unsigned int mr); |
|
||||
|
|
||||
unsigned int Cudd_ReadOrderRandomization(DdManager * dd); |
|
||||
|
|
||||
void Cudd_SetOrderRandomization(DdManager * dd, unsigned int factor); |
|
||||
|
|
||||
int Cudd_PrintGroupedOrder(DdManager * dd, const char *str, void *data); |
|
||||
|
|
||||
int Cudd_EnableOrderingMonitoring(DdManager *dd); |
|
||||
|
|
||||
int Cudd_DisableOrderingMonitoring(DdManager *dd); |
|
||||
|
|
||||
int Cudd_OrderingMonitoring(DdManager *dd); |
|
||||
|
|
||||
DdNode * Cudd_bddExistAbstractLimit(DdManager * manager, DdNode * f, DdNode * cube, unsigned int limit); |
|
||||
|
|
||||
DdNode * Cudd_bddIteLimit (DdManager *dd, DdNode *f, DdNode *g, DdNode *h, unsigned int limit); |
|
||||
|
|
||||
DdNode * Cudd_bddOrLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit); |
|
||||
|
|
||||
DdNode * Cudd_bddXnorLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit); |
|
||||
|
|
||||
int Cudd_CheckCube (DdManager *dd, DdNode *g); |
|
||||
|
|
||||
DdNode * Cudd_bddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f); |
|
||||
|
|
||||
DdNode * Cudd_bddLargestPrimeUnate(DdManager *dd , DdNode *f, DdNode *phaseBdd); |
|
||||
|
|
||||
int Cudd_Reserve(DdManager *manager, int amount); |
|
||||
|
|
||||
int Cudd_SupportIndices(DdManager * dd, DdNode * f, int **indices); |
|
||||
|
|
||||
int Cudd_VectorSupportIndices(DdManager * dd, DdNode ** F, int n, int **indices); |
|
||||
|
|
||||
DdNode * Cudd_zddSupport(DdManager * dd, DdNode * f); |
|
||||
|
|
||||
|
|
||||
Changed prototypes: |
|
||||
|
|
||||
unsigned int Cudd_ReadReorderings (DdManager *dd); |
|
||||
|
|
||||
---------------------------------------------------------------------- |
|
||||
|
|
||||
Release 2.4.2 of Cudd features several bug fixes. The most important |
|
||||
are those that prevented Cudd from making full use of up to 4 GB of |
|
||||
memory when using 32-bit pointers. A handful of bugs were discovered by |
|
||||
Coverity. (Thanks to Christian Stangier!) |
|
||||
|
|
||||
This release can be compiled with either 64-bit pointers or 32-bit |
|
||||
pointers on x86_64 platforms if sizeof(long) = sizeof(void *) = 8 and |
|
||||
sizeof(int) = 4. This is known as the LP64 model. For 32-bit pointers, |
|
||||
one usually needs supplementary libraries. On Ubuntu and Debian Linux, |
|
||||
one needs g++-multilib, which can be installed with |
|
||||
"apt-get install g++-multilib." |
|
||||
|
|
||||
Added functions |
|
||||
|
|
||||
DdNode *Cudd_Inequality (DdManager * dd, int N, int c, DdNode ** x, |
|
||||
DdNode ** y); |
|
||||
|
|
||||
DdNode * Cudd_Disequality (DdManager * dd, int N, int c, DdNode ** x, |
|
||||
DdNode ** y); |
|
||||
|
|
||||
DdNode * Cudd_bddInterval (DdManager * dd, int N, DdNode ** x, |
|
||||
unsigned int lowerB, unsigned int upperB); |
|
||||
|
|
||||
Changed prototypes: |
|
||||
|
|
||||
int Cudd_DumpBlif (DdManager *dd, int n, DdNode **f, char |
|
||||
**inames, char **onames, char *mname, FILE *fp, int mv); |
|
||||
|
|
||||
int Cudd_DumpBlifBody (DdManager *dd, int n, DdNode **f, char |
|
||||
**inames, char **onames, FILE *fp, int mv); |
|
||||
|
|
||||
The additional parameter allows the caller to choose between plain blif |
|
||||
and blif-MV. |
|
||||
|
|
||||
---------------------------------------------------------------------- |
|
||||
|
|
||||
Release 2.4.1 of Cudd features one major change with respect to previous |
|
||||
releases. The licensing terms are now explicitly stated. |
|
||||
@ -1,18 +0,0 @@ |
|||||
#! /bin/sh |
|
||||
CREATE="ln -s" |
|
||||
if test -d include |
|
||||
then |
|
||||
: |
|
||||
else |
|
||||
mkdir include |
|
||||
cd include |
|
||||
$CREATE ../cudd/cudd.h . |
|
||||
$CREATE ../cudd/cuddInt.h . |
|
||||
$CREATE ../epd/epd.h . |
|
||||
$CREATE ../dddmp/dddmp.h . |
|
||||
$CREATE ../mtr/mtr.h . |
|
||||
$CREATE ../obj/cuddObj.hh . |
|
||||
$CREATE ../st/st.h . |
|
||||
$CREATE ../util/util.h . |
|
||||
$CREATE ../mnemosyne/mnemosyne.h . |
|
||||
fi |
|
||||
@ -1,2 +0,0 @@ |
|||||
#! /bin/sh |
|
||||
rm -rf include *.bak *~ |
|
||||
@ -1,124 +0,0 @@ |
|||||
# $Id$
|
|
||||
#
|
|
||||
# Cudd - DD package
|
|
||||
#---------------------------
|
|
||||
.SUFFIXES: .o .c .u |
|
||||
|
|
||||
CC = gcc |
|
||||
RANLIB = ranlib |
|
||||
PURE = |
|
||||
# Define EXE as .exe for MS-DOS and derivatives.
|
|
||||
EXE = |
|
||||
#EXE = .exe
|
|
||||
|
|
||||
MFLAG = |
|
||||
ICFLAGS = -g |
|
||||
XCFLAGS = -DDD_STATS |
|
||||
CFLAGS = $(ICFLAGS) $(MFLAG) $(XCFLAGS) |
|
||||
#DDDEBUG = -DDD_DEBUG -DDD_CACHE_PROFILE -DDD_VERBOSE -DDD_UNIQUE_PROFILE
|
|
||||
DDDEBUG = |
|
||||
|
|
||||
LINTFLAGS = -u -n -DDD_STATS -DDD_CACHE_PROFILE -DDD_VERBOSE -DDD_DEBUG -DDD_UNIQUE_PROFILE |
|
||||
|
|
||||
# this is to create the lint library
|
|
||||
LINTSWITCH = -o |
|
||||
|
|
||||
WHERE = .. |
|
||||
|
|
||||
INCLUDE = $(WHERE)/include |
|
||||
|
|
||||
LIBS = ./libcudd.a $(WHERE)/mtr/libmtr.a \
|
|
||||
$(WHERE)/st/libst.a $(WHERE)/util/libutil.a $(WHERE)/epd/libepd.a |
|
||||
|
|
||||
MNEMLIB = |
|
||||
|
|
||||
BLIBS = -kL. -klcudd -kL$(WHERE)/mtr -klmtr \
|
|
||||
-kL$(WHERE)/st -klst -kL$(WHERE)/util -klutil -kL$(WHERE)/epd -klepd |
|
||||
|
|
||||
LINTLIBS = ./llib-lcudd.ln $(WHERE)/mtr/llib-lmtr.ln \
|
|
||||
$(WHERE)/st/llib-lst.ln $(WHERE)/util/llib-lutil.ln \
|
|
||||
$(WHERE)/epd/llib-lepd.ln |
|
||||
|
|
||||
LDFLAGS = |
|
||||
|
|
||||
# files for the package
|
|
||||
P = cudd |
|
||||
PSRC = cuddAPI.c cuddAddAbs.c cuddAddApply.c cuddAddFind.c cuddAddIte.c \
|
|
||||
cuddAddInv.c cuddAddNeg.c cuddAddWalsh.c cuddAndAbs.c \
|
|
||||
cuddAnneal.c cuddApa.c cuddApprox.c cuddBddAbs.c cuddBddCorr.c \
|
|
||||
cuddBddIte.c cuddBridge.c cuddCache.c cuddCheck.c cuddClip.c \
|
|
||||
cuddCof.c cuddCompose.c cuddDecomp.c cuddEssent.c \
|
|
||||
cuddExact.c cuddExport.c cuddGenCof.c cuddGenetic.c \
|
|
||||
cuddGroup.c cuddHarwell.c cuddInit.c cuddInteract.c \
|
|
||||
cuddLCache.c cuddLevelQ.c \
|
|
||||
cuddLinear.c cuddLiteral.c cuddMatMult.c cuddPriority.c \
|
|
||||
cuddRead.c cuddRef.c cuddReorder.c cuddSat.c cuddSign.c \
|
|
||||
cuddSolve.c cuddSplit.c cuddSubsetHB.c cuddSubsetSP.c cuddSymmetry.c \
|
|
||||
cuddTable.c cuddUtil.c cuddWindow.c cuddZddCount.c cuddZddFuncs.c \
|
|
||||
cuddZddGroup.c cuddZddIsop.c cuddZddLin.c cuddZddMisc.c \
|
|
||||
cuddZddPort.c cuddZddReord.c cuddZddSetop.c cuddZddSymm.c \
|
|
||||
cuddZddUtil.c |
|
||||
PHDR = cudd.h cuddInt.h |
|
||||
POBJ = $(PSRC:.c=.o) |
|
||||
PUBJ = $(PSRC:.c=.u) |
|
||||
TARGET = test$(P)$(EXE) |
|
||||
TARGETu = test$(P)-u |
|
||||
|
|
||||
# files for the test program
|
|
||||
SRC = test$(P).c |
|
||||
OBJ = $(SRC:.c=.o) |
|
||||
UBJ = $(SRC:.c=.u) |
|
||||
|
|
||||
#------------------------------------------------------
|
|
||||
|
|
||||
lib$(P).a: $(POBJ) |
|
||||
ar rv $@ $? |
|
||||
$(RANLIB) $@ |
|
||||
|
|
||||
.c.o: $(PSRC) $(PHDR) |
|
||||
$(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG) |
|
||||
|
|
||||
optimize_dec: lib$(P).b |
|
||||
|
|
||||
lib$(P).b: $(PUBJ) |
|
||||
ar rv $@ $? |
|
||||
$(RANLIB) $@ |
|
||||
|
|
||||
.c.u: $(PSRC) $(PHDR) |
|
||||
cc -j $< -I$(INCLUDE) $(XCFLAGS) |
|
||||
|
|
||||
# if the header files change, recompile
|
|
||||
$(POBJ): $(PHDR) |
|
||||
$(PUBJ): $(PHDR) |
|
||||
$(OBJ): $(PHDR) |
|
||||
$(UBJ): $(PHDR) |
|
||||
|
|
||||
$(TARGET): $(SRC) $(OBJ) $(HDR) $(LIBS) $(MNEMLIB) |
|
||||
$(PURE) $(CC) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm |
|
||||
|
|
||||
# optimize (DECstations and Alphas only: uses u-code)
|
|
||||
$(TARGETu): $(SRC) $(UBJ) $(HDR) $(LIBS:.a=.b) |
|
||||
$(CC) -O3 -Olimit 1000 $(XCFLAGS) $(LDFLAGS) -o $@ $(UBJ) $(BLIBS) -lm |
|
||||
|
|
||||
lint: llib-l$(P).ln |
|
||||
|
|
||||
llib-l$(P).ln: $(PSRC) $(PHDR) |
|
||||
lint $(LINTFLAGS) $(LINTSWITCH)$(P) -I$(INCLUDE) $(PSRC) |
|
||||
|
|
||||
lintpgm: lint |
|
||||
lint $(LINTFLAGS) -I$(INCLUDE) $(SRC) $(LINTLIBS) |
|
||||
|
|
||||
tags: $(PSRC) $(PHDR) |
|
||||
ctags $(PSRC) $(PHDR) |
|
||||
|
|
||||
all: lib$(P).a lib$(P).b llib-l$(P).ln tags |
|
||||
|
|
||||
programs: $(TARGET) $(TARGETu) lintpgm |
|
||||
|
|
||||
clean: |
|
||||
rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
|
|
||||
.pure core *.warnings |
|
||||
|
|
||||
distclean: clean |
|
||||
rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
|
|
||||
*.bak *~ tags .gdb_history *.qv *.qx |
|
||||
1090
resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
Some files were not shown because too many files changed in this diff
Write
Preview
Loading…
Cancel
Save
Reference in new issue