Alarms23 : CONTEXT = BEGIN %Type definitions TIME : TYPE = {X : REAL | X >= 0}; % in seconds VOLUME : TYPE = {X : REAL | X >= 0}; % in dB FREQUENCY: TYPE = {X : REAL | X >= 0}; % in Hz %Constant definitions deltaConst: VOLUME = 14.5; bigMax: TIME = 60; bark(f: FREQUENCY): REAL = IF f <= 5 THEN 0 ELSIF f <= 15 THEN 0.1 ELSIF f <= 25 THEN 0.2 ELSIF f <= 35 THEN 0.3 ELSIF f <= 45 THEN 0.4 ELSIF f <= 55 THEN 0.5 ELSIF f <= 65 THEN 0.6 ELSIF f <= 75 THEN 0.7 ELSIF f <= 86 THEN 0.8 ELSIF f <= 96 THEN 0.9 ELSIF f <= 106 THEN 1 ELSIF f <= 116 THEN 1.1 ELSIF f <= 126 THEN 1.2 ELSIF f <= 137 THEN 1.3 ELSIF f <= 147 THEN 1.4 ELSIF f <= 157 THEN 1.5 ELSIF f <= 167 THEN 1.6 ELSIF f <= 178 THEN 1.7 ELSIF f <= 188 THEN 1.8 ELSIF f <= 198 THEN 1.9 ELSIF f <= 208 THEN 2 ELSIF f <= 219 THEN 2.1 ELSIF f <= 229 THEN 2.2 ELSIF f <= 240 THEN 2.3 ELSIF f <= 250 THEN 2.4 ELSIF f <= 261 THEN 2.5 ELSIF f <= 271 THEN 2.6 ELSIF f <= 282 THEN 2.7 ELSIF f <= 292 THEN 2.8 ELSIF f <= 303 THEN 2.9 ELSIF f <= 313 THEN 3 ELSIF f <= 324 THEN 3.1 ELSIF f <= 335 THEN 3.2 ELSIF f <= 345 THEN 3.3 ELSIF f <= 356 THEN 3.4 ELSIF f <= 367 THEN 3.5 ELSIF f <= 378 THEN 3.6 ELSIF f <= 389 THEN 3.7 ELSIF f <= 400 THEN 3.8 ELSIF f <= 411 THEN 3.9 ELSIF f <= 422 THEN 4 ELSIF f <= 433 THEN 4.1 ELSIF f <= 444 THEN 4.2 ELSIF f <= 456 THEN 4.3 ELSIF f <= 467 THEN 4.4 ELSIF f <= 478 THEN 4.5 ELSIF f <= 490 THEN 4.6 ELSIF f <= 501 THEN 4.7 ELSIF f <= 513 THEN 4.8 ELSIF f <= 524 THEN 4.9 ELSIF f <= 536 THEN 5 ELSIF f <= 548 THEN 5.1 ELSIF f <= 559 THEN 5.2 ELSIF f <= 571 THEN 5.3 ELSIF f <= 583 THEN 5.4 ELSIF f <= 595 THEN 5.5 ELSIF f <= 607 THEN 5.6 ELSIF f <= 620 THEN 5.7 ELSIF f <= 632 THEN 5.8 ELSIF f <= 644 THEN 5.9 ELSIF f <= 657 THEN 6 ELSIF f <= 669 THEN 6.1 ELSIF f <= 682 THEN 6.2 ELSIF f <= 695 THEN 6.3 ELSIF f <= 708 THEN 6.4 ELSIF f <= 721 THEN 6.5 ELSIF f <= 734 THEN 6.6 ELSIF f <= 747 THEN 6.7 ELSIF f <= 760 THEN 6.8 ELSIF f <= 774 THEN 6.9 ELSIF f <= 787 THEN 7 ELSIF f <= 801 THEN 7.1 ELSIF f <= 814 THEN 7.2 ELSIF f <= 828 THEN 7.3 ELSIF f <= 842 THEN 7.4 ELSIF f <= 856 THEN 7.5 ELSIF f <= 871 THEN 7.6 ELSIF f <= 885 THEN 7.7 ELSIF f <= 900 THEN 7.8 ELSIF f <= 914 THEN 7.9 ELSIF f <= 929 THEN 8 ELSIF f <= 944 THEN 8.1 ELSIF f <= 959 THEN 8.2 ELSIF f <= 975 THEN 8.3 ELSIF f <= 990 THEN 8.4 ELSIF f <= 1006 THEN 8.5 ELSIF f <= 1022 THEN 8.6 ELSIF f <= 1037 THEN 8.7 ELSIF f <= 1054 THEN 8.8 ELSIF f <= 1070 THEN 8.9 ELSIF f <= 1087 THEN 9 ELSIF f <= 1103 THEN 9.1 ELSIF f <= 1120 THEN 9.2 ELSIF f <= 1137 THEN 9.3 ELSIF f <= 1155 THEN 9.4 ELSIF f <= 1172 THEN 9.5 ELSIF f <= 1190 THEN 9.6 ELSIF f <= 1208 THEN 9.7 ELSIF f <= 1226 THEN 9.8 ELSIF f <= 1245 THEN 9.9 ELSIF f <= 1264 THEN 10 ELSIF f <= 1283 THEN 10.1 ELSIF f <= 1302 THEN 10.2 ELSIF f <= 1322 THEN 10.3 ELSIF f <= 1341 THEN 10.4 ELSIF f <= 1362 THEN 10.5 ELSIF f <= 1382 THEN 10.6 ELSIF f <= 1403 THEN 10.7 ELSIF f <= 1424 THEN 10.8 ELSIF f <= 1445 THEN 10.9 ELSIF f <= 1467 THEN 11 ELSIF f <= 1489 THEN 11.1 ELSIF f <= 1511 THEN 11.2 ELSIF f <= 1534 THEN 11.3 ELSIF f <= 1557 THEN 11.4 ELSIF f <= 1580 THEN 11.5 ELSIF f <= 1604 THEN 11.6 ELSIF f <= 1628 THEN 11.7 ELSIF f <= 1652 THEN 11.8 ELSIF f <= 1677 THEN 11.9 ELSIF f <= 1703 THEN 12 ELSIF f <= 1729 THEN 12.1 ELSIF f <= 1755 THEN 12.2 ELSIF f <= 1782 THEN 12.3 ELSIF f <= 1809 THEN 12.4 ELSIF f <= 1837 THEN 12.5 ELSIF f <= 1865 THEN 12.6 ELSIF f <= 1893 THEN 12.7 ELSIF f <= 1923 THEN 12.8 ELSIF f <= 1953 THEN 12.9 ELSIF f <= 1983 THEN 13 ELSIF f <= 2014 THEN 13.1 ELSIF f <= 2045 THEN 13.2 ELSIF f <= 2077 THEN 13.3 ELSIF f <= 2110 THEN 13.4 ELSIF f <= 2143 THEN 13.5 ELSIF f <= 2178 THEN 13.6 ELSIF f <= 2212 THEN 13.7 ELSIF f <= 2248 THEN 13.8 ELSIF f <= 2284 THEN 13.9 ELSIF f <= 2320 THEN 14 ELSIF f <= 2358 THEN 14.1 ELSIF f <= 2396 THEN 14.2 ELSIF f <= 2435 THEN 14.3 ELSIF f <= 2475 THEN 14.4 ELSIF f <= 2516 THEN 14.5 ELSIF f <= 2558 THEN 14.6 ELSIF f <= 2600 THEN 14.7 ELSIF f <= 2643 THEN 14.8 ELSIF f <= 2688 THEN 14.9 ELSIF f <= 2733 THEN 15 ELSIF f <= 2779 THEN 15.1 ELSIF f <= 2826 THEN 15.2 ELSIF f <= 2874 THEN 15.3 ELSIF f <= 2923 THEN 15.4 ELSIF f <= 2973 THEN 15.5 ELSIF f <= 3024 THEN 15.6 ELSIF f <= 3076 THEN 15.7 ELSIF f <= 3129 THEN 15.8 ELSIF f <= 3183 THEN 15.9 ELSIF f <= 3239 THEN 16 ELSIF f <= 3295 THEN 16.1 ELSIF f <= 3353 THEN 16.2 ELSIF f <= 3412 THEN 16.3 ELSIF f <= 3471 THEN 16.4 ELSIF f <= 3533 THEN 16.5 ELSIF f <= 3595 THEN 16.6 ELSIF f <= 3658 THEN 16.7 ELSIF f <= 3723 THEN 16.8 ELSIF f <= 3789 THEN 16.9 ELSIF f <= 3856 THEN 17 ELSIF f <= 3924 THEN 17.1 ELSIF f <= 3993 THEN 17.2 ELSIF f <= 4064 THEN 17.3 ELSIF f <= 4136 THEN 17.4 ELSIF f <= 4209 THEN 17.5 ELSIF f <= 4283 THEN 17.6 ELSIF f <= 4359 THEN 17.7 ELSIF f <= 4436 THEN 17.8 ELSIF f <= 4514 THEN 17.9 ELSIF f <= 4593 THEN 18 ELSIF f <= 4674 THEN 18.1 ELSIF f <= 4756 THEN 18.2 ELSIF f <= 4839 THEN 18.3 ELSIF f <= 4923 THEN 18.4 ELSIF f <= 5009 THEN 18.5 ELSIF f <= 5096 THEN 18.6 ELSIF f <= 5184 THEN 18.7 ELSIF f <= 5274 THEN 18.8 ELSIF f <= 5365 THEN 18.9 ELSIF f <= 5458 THEN 19 ELSIF f <= 5552 THEN 19.1 ELSIF f <= 5647 THEN 19.2 ELSIF f <= 5744 THEN 19.3 ELSIF f <= 5842 THEN 19.4 ELSIF f <= 5942 THEN 19.5 ELSIF f <= 6044 THEN 19.6 ELSIF f <= 6147 THEN 19.7 ELSIF f <= 6252 THEN 19.8 ELSIF f <= 6359 THEN 19.9 ELSIF f <= 6468 THEN 20 ELSIF f <= 6579 THEN 20.1 ELSIF f <= 6692 THEN 20.2 ELSIF f <= 6807 THEN 20.3 ELSIF f <= 6924 THEN 20.4 ELSIF f <= 7044 THEN 20.5 ELSIF f <= 7166 THEN 20.6 ELSIF f <= 7291 THEN 20.7 ELSIF f <= 7419 THEN 20.8 ELSIF f <= 7550 THEN 20.9 ELSIF f <= 7684 THEN 21 ELSIF f <= 7822 THEN 21.1 ELSIF f <= 7963 THEN 21.2 ELSIF f <= 8108 THEN 21.3 ELSIF f <= 8257 THEN 21.4 ELSIF f <= 8411 THEN 21.5 ELSIF f <= 8569 THEN 21.6 ELSIF f <= 8733 THEN 21.7 ELSIF f <= 8902 THEN 21.8 ELSIF f <= 9076 THEN 21.9 ELSIF f <= 9257 THEN 22 ELSIF f <= 9445 THEN 22.1 ELSIF f <= 9640 THEN 22.2 ELSIF f <= 9844 THEN 22.3 ELSIF f <= 10055 THEN 22.4 ELSIF f <= 10277 THEN 22.5 ELSIF f <= 10508 THEN 22.6 ELSIF f <= 10751 THEN 22.7 ELSIF f <= 11006 THEN 22.8 ELSIF f <= 11275 THEN 22.9 ELSIF f <= 11559 THEN 23 ELSIF f <= 11859 THEN 23.1 ELSIF f <= 12177 THEN 23.2 ELSIF f <= 12516 THEN 23.3 ELSIF f <= 12878 THEN 23.4 ELSIF f <= 13265 THEN 23.5 ELSIF f <= 13681 THEN 23.6 ELSIF f <= 14130 THEN 23.7 ELSIF f <= 14616 THEN 23.8 ELSIF f <= 15145 THEN 23.9 ELSE 24 ENDIF; spread(dz: REAL): REAL = IF dz <= -24 THEN -572 ELSIF dz <= -23.9 THEN -570 ELSIF dz <= -23.8 THEN -567 ELSIF dz <= -23.7 THEN -565 ELSIF dz <= -23.6 THEN -562 ELSIF dz <= -23.5 THEN -560 ELSIF dz <= -23.4 THEN -557 ELSIF dz <= -23.3 THEN -555 ELSIF dz <= -23.2 THEN -552 ELSIF dz <= -23.1 THEN -550 ELSIF dz <= -23 THEN -547 ELSIF dz <= -22.9 THEN -545 ELSIF dz <= -22.8 THEN -542 ELSIF dz <= -22.7 THEN -540 ELSIF dz <= -22.6 THEN -537 ELSIF dz <= -22.5 THEN -535 ELSIF dz <= -22.4 THEN -532 ELSIF dz <= -22.3 THEN -530 ELSIF dz <= -22.2 THEN -527 ELSIF dz <= -22.1 THEN -525 ELSIF dz <= -22 THEN -522 ELSIF dz <= -21.9 THEN -520 ELSIF dz <= -21.8 THEN -517 ELSIF dz <= -21.7 THEN -515 ELSIF dz <= -21.6 THEN -512 ELSIF dz <= -21.5 THEN -510 ELSIF dz <= -21.4 THEN -507 ELSIF dz <= -21.3 THEN -505 ELSIF dz <= -21.2 THEN -502 ELSIF dz <= -21.1 THEN -500 ELSIF dz <= -21 THEN -497 ELSIF dz <= -20.9 THEN -495 ELSIF dz <= -20.8 THEN -492 ELSIF dz <= -20.7 THEN -490 ELSIF dz <= -20.6 THEN -487 ELSIF dz <= -20.5 THEN -485 ELSIF dz <= -20.4 THEN -482 ELSIF dz <= -20.3 THEN -480 ELSIF dz <= -20.2 THEN -477 ELSIF dz <= -20.1 THEN -475 ELSIF dz <= -20 THEN -472 ELSIF dz <= -19.9 THEN -470 ELSIF dz <= -19.8 THEN -467 ELSIF dz <= -19.7 THEN -465 ELSIF dz <= -19.6 THEN -462 ELSIF dz <= -19.5 THEN -460 ELSIF dz <= -19.4 THEN -457 ELSIF dz <= -19.3 THEN -455 ELSIF dz <= -19.2 THEN -452 ELSIF dz <= -19.1 THEN -450 ELSIF dz <= -19 THEN -447 ELSIF dz <= -18.9 THEN -445 ELSIF dz <= -18.8 THEN -442 ELSIF dz <= -18.7 THEN -440 ELSIF dz <= -18.6 THEN -437 ELSIF dz <= -18.5 THEN -435 ELSIF dz <= -18.4 THEN -432 ELSIF dz <= -18.3 THEN -430 ELSIF dz <= -18.2 THEN -427 ELSIF dz <= -18.1 THEN -425 ELSIF dz <= -18 THEN -422 ELSIF dz <= -17.9 THEN -420 ELSIF dz <= -17.8 THEN -417 ELSIF dz <= -17.7 THEN -415 ELSIF dz <= -17.6 THEN -412 ELSIF dz <= -17.5 THEN -410 ELSIF dz <= -17.4 THEN -407 ELSIF dz <= -17.3 THEN -405 ELSIF dz <= -17.2 THEN -402 ELSIF dz <= -17.1 THEN -400 ELSIF dz <= -17 THEN -397 ELSIF dz <= -16.9 THEN -395 ELSIF dz <= -16.8 THEN -392 ELSIF dz <= -16.7 THEN -390 ELSIF dz <= -16.6 THEN -387 ELSIF dz <= -16.5 THEN -385 ELSIF dz <= -16.4 THEN -382 ELSIF dz <= -16.3 THEN -380 ELSIF dz <= -16.2 THEN -377 ELSIF dz <= -16.1 THEN -375 ELSIF dz <= -16 THEN -372 ELSIF dz <= -15.9 THEN -370 ELSIF dz <= -15.8 THEN -367 ELSIF dz <= -15.7 THEN -365 ELSIF dz <= -15.6 THEN -362 ELSIF dz <= -15.5 THEN -360 ELSIF dz <= -15.4 THEN -357 ELSIF dz <= -15.3 THEN -355 ELSIF dz <= -15.2 THEN -352 ELSIF dz <= -15.1 THEN -350 ELSIF dz <= -15 THEN -347 ELSIF dz <= -14.9 THEN -345 ELSIF dz <= -14.8 THEN -342 ELSIF dz <= -14.7 THEN -340 ELSIF dz <= -14.6 THEN -337 ELSIF dz <= -14.5 THEN -335 ELSIF dz <= -14.4 THEN -332 ELSIF dz <= -14.3 THEN -330 ELSIF dz <= -14.2 THEN -327 ELSIF dz <= -14.1 THEN -325 ELSIF dz <= -14 THEN -322 ELSIF dz <= -13.9 THEN -320 ELSIF dz <= -13.8 THEN -317 ELSIF dz <= -13.7 THEN -315 ELSIF dz <= -13.6 THEN -313 ELSIF dz <= -13.5 THEN -310 ELSIF dz <= -13.4 THEN -308 ELSIF dz <= -13.3 THEN -305 ELSIF dz <= -13.2 THEN -303 ELSIF dz <= -13.1 THEN -300 ELSIF dz <= -13 THEN -298 ELSIF dz <= -12.9 THEN -295 ELSIF dz <= -12.8 THEN -293 ELSIF dz <= -12.7 THEN -290 ELSIF dz <= -12.6 THEN -288 ELSIF dz <= -12.5 THEN -285 ELSIF dz <= -12.4 THEN -283 ELSIF dz <= -12.3 THEN -280 ELSIF dz <= -12.2 THEN -278 ELSIF dz <= -12.1 THEN -275 ELSIF dz <= -12 THEN -273 ELSIF dz <= -11.9 THEN -270 ELSIF dz <= -11.8 THEN -268 ELSIF dz <= -11.7 THEN -265 ELSIF dz <= -11.6 THEN -263 ELSIF dz <= -11.5 THEN -260 ELSIF dz <= -11.4 THEN -258 ELSIF dz <= -11.3 THEN -255 ELSIF dz <= -11.2 THEN -253 ELSIF dz <= -11.1 THEN -250 ELSIF dz <= -11 THEN -248 ELSIF dz <= -10.9 THEN -245 ELSIF dz <= -10.8 THEN -243 ELSIF dz <= -10.7 THEN -240 ELSIF dz <= -10.6 THEN -238 ELSIF dz <= -10.5 THEN -235 ELSIF dz <= -10.4 THEN -233 ELSIF dz <= -10.3 THEN -230 ELSIF dz <= -10.2 THEN -228 ELSIF dz <= -10.1 THEN -225 ELSIF dz <= -10 THEN -223 ELSIF dz <= -9.9 THEN -220 ELSIF dz <= -9.8 THEN -218 ELSIF dz <= -9.7 THEN -215 ELSIF dz <= -9.6 THEN -213 ELSIF dz <= -9.5 THEN -210 ELSIF dz <= -9.4 THEN -208 ELSIF dz <= -9.3 THEN -205 ELSIF dz <= -9.2 THEN -203 ELSIF dz <= -9.1 THEN -200 ELSIF dz <= -9 THEN -198 ELSIF dz <= -8.9 THEN -195 ELSIF dz <= -8.8 THEN -193 ELSIF dz <= -8.7 THEN -190 ELSIF dz <= -8.6 THEN -188 ELSIF dz <= -8.5 THEN -185 ELSIF dz <= -8.4 THEN -183 ELSIF dz <= -8.3 THEN -180 ELSIF dz <= -8.2 THEN -178 ELSIF dz <= -8.1 THEN -175 ELSIF dz <= -8 THEN -173 ELSIF dz <= -7.9 THEN -171 ELSIF dz <= -7.8 THEN -168 ELSIF dz <= -7.7 THEN -166 ELSIF dz <= -7.6 THEN -163 ELSIF dz <= -7.5 THEN -161 ELSIF dz <= -7.4 THEN -158 ELSIF dz <= -7.3 THEN -156 ELSIF dz <= -7.2 THEN -153 ELSIF dz <= -7.1 THEN -151 ELSIF dz <= -7 THEN -148 ELSIF dz <= -6.9 THEN -146 ELSIF dz <= -6.8 THEN -143 ELSIF dz <= -6.7 THEN -141 ELSIF dz <= -6.6 THEN -138 ELSIF dz <= -6.5 THEN -136 ELSIF dz <= -6.4 THEN -133 ELSIF dz <= -6.3 THEN -131 ELSIF dz <= -6.2 THEN -128 ELSIF dz <= -6.1 THEN -126 ELSIF dz <= -6 THEN -123 ELSIF dz <= -5.9 THEN -121 ELSIF dz <= -5.8 THEN -118 ELSIF dz <= -5.7 THEN -116 ELSIF dz <= -5.6 THEN -114 ELSIF dz <= -5.5 THEN -111 ELSIF dz <= -5.4 THEN -109 ELSIF dz <= -5.3 THEN -106 ELSIF dz <= -5.2 THEN -104 ELSIF dz <= -5.1 THEN -101 ELSIF dz <= -5 THEN -99 ELSIF dz <= -4.9 THEN -96 ELSIF dz <= -4.8 THEN -94 ELSIF dz <= -4.7 THEN -91 ELSIF dz <= -4.6 THEN -89 ELSIF dz <= -4.5 THEN -86 ELSIF dz <= -4.4 THEN -84 ELSIF dz <= -4.3 THEN -82 ELSIF dz <= -4.2 THEN -79 ELSIF dz <= -4.1 THEN -77 ELSIF dz <= -4 THEN -74 ELSIF dz <= -3.9 THEN -72 ELSIF dz <= -3.8 THEN -69 ELSIF dz <= -3.7 THEN -67 ELSIF dz <= -3.6 THEN -65 ELSIF dz <= -3.5 THEN -62 ELSIF dz <= -3.4 THEN -60 ELSIF dz <= -3.3 THEN -57 ELSIF dz <= -3.2 THEN -55 ELSIF dz <= -3.1 THEN -53 ELSIF dz <= -3 THEN -50 ELSIF dz <= -2.9 THEN -48 ELSIF dz <= -2.8 THEN -45 ELSIF dz <= -2.7 THEN -43 ELSIF dz <= -2.6 THEN -41 ELSIF dz <= -2.5 THEN -38 ELSIF dz <= -2.4 THEN -36 ELSIF dz <= -2.3 THEN -34 ELSIF dz <= -2.2 THEN -32 ELSIF dz <= -2.1 THEN -29 ELSIF dz <= -2 THEN -27 ELSIF dz <= -1.9 THEN -25 ELSIF dz <= -1.8 THEN -23 ELSIF dz <= -1.7 THEN -21 ELSIF dz <= -1.6 THEN -18 ELSIF dz <= -1.5 THEN -16 ELSIF dz <= -1.4 THEN -14 ELSIF dz <= -1.3 THEN -13 ELSIF dz <= -1.2 THEN -11 ELSIF dz <= -1.1 THEN -9 ELSIF dz <= -1 THEN -7 ELSIF dz <= -0.9 THEN -6 ELSIF dz <= -0.8 THEN -5 ELSIF dz <= -0.7 THEN -3 ELSIF dz <= -0.6 THEN -2 ELSIF dz <= -0.4 THEN -1 ELSIF dz <= 0.4 THEN 0 ELSIF dz <= 0.6 THEN -1 ELSIF dz <= 0.8 THEN -2 ELSIF dz <= 0.9 THEN -3 ELSIF dz <= 1 THEN -4 ELSIF dz <= 1.2 THEN -5 ELSIF dz <= 1.3 THEN -6 ELSIF dz <= 1.4 THEN -7 ELSIF dz <= 1.6 THEN -8 ELSIF dz <= 1.7 THEN -9 ELSIF dz <= 1.8 THEN -10 ELSIF dz <= 1.9 THEN -11 ELSIF dz <= 2 THEN -12 ELSIF dz <= 2.1 THEN -13 ELSIF dz <= 2.3 THEN -14 ELSIF dz <= 2.4 THEN -15 ELSIF dz <= 2.5 THEN -16 ELSIF dz <= 2.6 THEN -17 ELSIF dz <= 2.7 THEN -18 ELSIF dz <= 2.8 THEN -19 ELSIF dz <= 2.9 THEN -20 ELSIF dz <= 3 THEN -21 ELSIF dz <= 3.1 THEN -22 ELSIF dz <= 3.2 THEN -23 ELSIF dz <= 3.3 THEN -24 ELSIF dz <= 3.4 THEN -25 ELSIF dz <= 3.5 THEN -26 ELSIF dz <= 3.7 THEN -27 ELSIF dz <= 3.8 THEN -28 ELSIF dz <= 3.9 THEN -29 ELSIF dz <= 4 THEN -30 ELSIF dz <= 4.1 THEN -31 ELSIF dz <= 4.2 THEN -32 ELSIF dz <= 4.3 THEN -33 ELSIF dz <= 4.4 THEN -34 ELSIF dz <= 4.5 THEN -35 ELSIF dz <= 4.6 THEN -36 ELSIF dz <= 4.7 THEN -37 ELSIF dz <= 4.8 THEN -38 ELSIF dz <= 4.9 THEN -39 ELSIF dz <= 5 THEN -40 ELSIF dz <= 5.1 THEN -41 ELSIF dz <= 5.2 THEN -42 ELSIF dz <= 5.3 THEN -43 ELSIF dz <= 5.4 THEN -44 ELSIF dz <= 5.5 THEN -45 ELSIF dz <= 5.6 THEN -46 ELSIF dz <= 5.7 THEN -47 ELSIF dz <= 5.8 THEN -48 ELSIF dz <= 5.9 THEN -49 ELSIF dz <= 6 THEN -50 ELSIF dz <= 6.1 THEN -51 ELSIF dz <= 6.2 THEN -52 ELSIF dz <= 6.3 THEN -53 ELSIF dz <= 6.4 THEN -54 ELSIF dz <= 6.5 THEN -55 ELSIF dz <= 6.6 THEN -56 ELSIF dz <= 6.7 THEN -57 ELSIF dz <= 6.8 THEN -58 ELSIF dz <= 6.9 THEN -59 ELSIF dz <= 7 THEN -60 ELSIF dz <= 7.1 THEN -61 ELSIF dz <= 7.2 THEN -62 ELSIF dz <= 7.3 THEN -63 ELSIF dz <= 7.4 THEN -64 ELSIF dz <= 7.5 THEN -65 ELSIF dz <= 7.7 THEN -66 ELSIF dz <= 7.8 THEN -67 ELSIF dz <= 7.9 THEN -68 ELSIF dz <= 8 THEN -69 ELSIF dz <= 8.1 THEN -70 ELSIF dz <= 8.2 THEN -71 ELSIF dz <= 8.3 THEN -72 ELSIF dz <= 8.4 THEN -73 ELSIF dz <= 8.5 THEN -74 ELSIF dz <= 8.6 THEN -75 ELSIF dz <= 8.7 THEN -76 ELSIF dz <= 8.8 THEN -77 ELSIF dz <= 8.9 THEN -78 ELSIF dz <= 9 THEN -79 ELSIF dz <= 9.1 THEN -80 ELSIF dz <= 9.2 THEN -81 ELSIF dz <= 9.3 THEN -82 ELSIF dz <= 9.4 THEN -83 ELSIF dz <= 9.5 THEN -84 ELSIF dz <= 9.6 THEN -85 ELSIF dz <= 9.7 THEN -86 ELSIF dz <= 9.8 THEN -87 ELSIF dz <= 9.9 THEN -88 ELSIF dz <= 10 THEN -89 ELSIF dz <= 10.1 THEN -90 ELSIF dz <= 10.2 THEN -91 ELSIF dz <= 10.3 THEN -92 ELSIF dz <= 10.4 THEN -93 ELSIF dz <= 10.5 THEN -94 ELSIF dz <= 10.6 THEN -95 ELSIF dz <= 10.7 THEN -96 ELSIF dz <= 10.8 THEN -97 ELSIF dz <= 10.9 THEN -98 ELSIF dz <= 11 THEN -99 ELSIF dz <= 11.1 THEN -100 ELSIF dz <= 11.2 THEN -101 ELSIF dz <= 11.3 THEN -102 ELSIF dz <= 11.4 THEN -103 ELSIF dz <= 11.5 THEN -104 ELSIF dz <= 11.6 THEN -105 ELSIF dz <= 11.7 THEN -106 ELSIF dz <= 11.8 THEN -107 ELSIF dz <= 11.9 THEN -108 ELSIF dz <= 12 THEN -109 ELSIF dz <= 12.1 THEN -110 ELSIF dz <= 12.2 THEN -111 ELSIF dz <= 12.3 THEN -112 ELSIF dz <= 12.4 THEN -113 ELSIF dz <= 12.5 THEN -114 ELSIF dz <= 12.6 THEN -115 ELSIF dz <= 12.7 THEN -116 ELSIF dz <= 12.8 THEN -117 ELSIF dz <= 12.9 THEN -118 ELSIF dz <= 13 THEN -119 ELSIF dz <= 13.1 THEN -120 ELSIF dz <= 13.2 THEN -121 ELSIF dz <= 13.3 THEN -122 ELSIF dz <= 13.4 THEN -123 ELSIF dz <= 13.5 THEN -124 ELSIF dz <= 13.6 THEN -125 ELSIF dz <= 13.7 THEN -126 ELSIF dz <= 13.8 THEN -127 ELSIF dz <= 13.9 THEN -128 ELSIF dz <= 14 THEN -129 ELSIF dz <= 14.1 THEN -130 ELSIF dz <= 14.2 THEN -131 ELSIF dz <= 14.3 THEN -132 ELSIF dz <= 14.4 THEN -133 ELSIF dz <= 14.5 THEN -134 ELSIF dz <= 14.6 THEN -135 ELSIF dz <= 14.7 THEN -136 ELSIF dz <= 14.8 THEN -137 ELSIF dz <= 14.9 THEN -138 ELSIF dz <= 15 THEN -139 ELSIF dz <= 15.1 THEN -140 ELSIF dz <= 15.2 THEN -141 ELSIF dz <= 15.3 THEN -142 ELSIF dz <= 15.4 THEN -143 ELSIF dz <= 15.5 THEN -144 ELSIF dz <= 15.6 THEN -145 ELSIF dz <= 15.7 THEN -146 ELSIF dz <= 15.8 THEN -147 ELSIF dz <= 15.9 THEN -148 ELSIF dz <= 16 THEN -149 ELSIF dz <= 16.1 THEN -150 ELSIF dz <= 16.2 THEN -151 ELSIF dz <= 16.3 THEN -152 ELSIF dz <= 16.4 THEN -153 ELSIF dz <= 16.5 THEN -154 ELSIF dz <= 16.6 THEN -155 ELSIF dz <= 16.7 THEN -156 ELSIF dz <= 16.8 THEN -157 ELSIF dz <= 16.9 THEN -158 ELSIF dz <= 17 THEN -159 ELSIF dz <= 17.1 THEN -160 ELSIF dz <= 17.2 THEN -161 ELSIF dz <= 17.3 THEN -162 ELSIF dz <= 17.4 THEN -163 ELSIF dz <= 17.5 THEN -164 ELSIF dz <= 17.6 THEN -165 ELSIF dz <= 17.7 THEN -166 ELSIF dz <= 17.8 THEN -167 ELSIF dz <= 17.9 THEN -168 ELSIF dz <= 18 THEN -169 ELSIF dz <= 18.1 THEN -170 ELSIF dz <= 18.2 THEN -171 ELSIF dz <= 18.3 THEN -172 ELSIF dz <= 18.4 THEN -173 ELSIF dz <= 18.5 THEN -174 ELSIF dz <= 18.6 THEN -175 ELSIF dz <= 18.7 THEN -176 ELSIF dz <= 18.8 THEN -177 ELSIF dz <= 18.9 THEN -178 ELSIF dz <= 19 THEN -179 ELSIF dz <= 19.1 THEN -180 ELSIF dz <= 19.2 THEN -181 ELSIF dz <= 19.3 THEN -182 ELSIF dz <= 19.4 THEN -183 ELSIF dz <= 19.5 THEN -184 ELSIF dz <= 19.6 THEN -185 ELSIF dz <= 19.7 THEN -186 ELSIF dz <= 19.8 THEN -187 ELSIF dz <= 19.9 THEN -188 ELSIF dz <= 20 THEN -189 ELSIF dz <= 20.1 THEN -190 ELSIF dz <= 20.2 THEN -191 ELSIF dz <= 20.3 THEN -192 ELSIF dz <= 20.4 THEN -193 ELSIF dz <= 20.5 THEN -194 ELSIF dz <= 20.6 THEN -195 ELSIF dz <= 20.7 THEN -196 ELSIF dz <= 20.8 THEN -197 ELSIF dz <= 20.9 THEN -198 ELSIF dz <= 21 THEN -199 ELSIF dz <= 21.1 THEN -200 ELSIF dz <= 21.2 THEN -201 ELSIF dz <= 21.3 THEN -202 ELSIF dz <= 21.4 THEN -203 ELSIF dz <= 21.5 THEN -204 ELSIF dz <= 21.6 THEN -205 ELSIF dz <= 21.7 THEN -206 ELSIF dz <= 21.8 THEN -207 ELSIF dz <= 21.9 THEN -208 ELSIF dz <= 22 THEN -209 ELSIF dz <= 22.1 THEN -210 ELSIF dz <= 22.2 THEN -211 ELSIF dz <= 22.3 THEN -212 ELSIF dz <= 22.4 THEN -213 ELSIF dz <= 22.5 THEN -214 ELSIF dz <= 22.6 THEN -215 ELSIF dz <= 22.7 THEN -216 ELSIF dz <= 22.8 THEN -217 ELSIF dz <= 22.9 THEN -218 ELSIF dz <= 23 THEN -219 ELSIF dz <= 23.1 THEN -220 ELSIF dz <= 23.2 THEN -221 ELSIF dz <= 23.3 THEN -222 ELSIF dz <= 23.4 THEN -223 ELSIF dz <= 23.5 THEN -224 ELSIF dz <= 23.6 THEN -225 ELSIF dz <= 23.7 THEN -226 ELSIF dz <= 23.8 THEN -227 ELSIF dz <= 23.9 THEN -228 ELSE -229 ENDIF; masking(sMasker: BOOLEAN, fMasker: FREQUENCY, vMasker: VOLUME, sMaskee: BOOLEAN, fMaskee: FREQUENCY, vMaskee: VOLUME): BOOLEAN = IF NOT(sMasker AND sMaskee) THEN FALSE ELSIF vMaskee = 0 THEN TRUE ELSE ((spread(bark(fMaskee) - bark(fMasker)) + vMasker - (deltaConst + bark(fMasker))) >= vMaskee) ENDIF; clock : MODULE = BEGIN INPUT maxNextTime : TIME OUTPUT globalTime : TIME INITIALIZATION globalTime = 0; TRANSITION globalTime' IN {X: TIME | (X > globalTime) AND (X <= maxNextTime)}; END; alarm2 : MODULE = BEGIN INPUT globalTime : TIME LOCAL alarm2StartTime : TIME LOCAL alarm2CycleTime : TIME LOCAL alarm2TimeInCycle : TIME OUTPUT alarm2Sounding : BOOLEAN OUTPUT alarm2Frequency : FREQUENCY OUTPUT alarm2Volume : VOLUME OUTPUT alarm2NextTime : TIME INITIALIZATION alarm2StartTime = 0; DEFINITION alarm2CycleTime = 0.35; alarm2TimeInCycle = globalTime - alarm2StartTime; alarm2Sounding = alarm2StartTime > 0; alarm2Frequency = IF alarm2Sounding AND (alarm2TimeInCycle < 0.15) THEN 277 ELSIF alarm2Sounding AND (alarm2TimeInCycle < 0.2) THEN 0 ELSIF alarm2Sounding AND (alarm2TimeInCycle < alarm2CycleTime) THEN 277 ELSE 0 ENDIF; alarm2Volume = IF alarm2Sounding AND (alarm2Frequency > 0) THEN 60 ELSE 0 ENDIF; alarm2NextTime = IF NOT alarm2Sounding THEN bigMax ELSIF alarm2Sounding AND (alarm2TimeInCycle < 0.15) THEN alarm2StartTime + 0.15 ELSIF alarm2Sounding AND (alarm2TimeInCycle < 0.2) THEN alarm2StartTime + 0.2 ELSE alarm2StartTime + alarm2CycleTime ENDIF; TRANSITION alarm2StartTime' IN {X: TIME | ((alarm2StartTime = 0) AND ((X = globalTime') OR (X = 0))) OR ((alarm2StartTime > 0) AND (globalTime' < (alarm2StartTime + alarm2CycleTime)) AND (X = alarm2StartTime)) OR ((alarm2StartTime > 0) AND (globalTime' >= (alarm2StartTime + alarm2CycleTime)) AND (X = 0)) }; END; alarm3 : MODULE = BEGIN INPUT globalTime : TIME LOCAL alarm3StartTime : TIME LOCAL alarm3CycleTime : TIME LOCAL alarm3TimeInCycle : TIME OUTPUT alarm3Sounding : BOOLEAN OUTPUT alarm3Frequency : FREQUENCY OUTPUT alarm3Volume : VOLUME OUTPUT alarm3NextTime : TIME INITIALIZATION alarm3StartTime = 0; DEFINITION alarm3CycleTime = 0.475; alarm3TimeInCycle = globalTime - alarm3StartTime; alarm3Sounding = alarm3StartTime > 0; alarm3Frequency = IF alarm3Sounding AND (alarm3TimeInCycle < 0.2) THEN 524 ELSIF alarm3Sounding AND (alarm3TimeInCycle < 0.275) THEN 0 ELSIF alarm3Sounding AND (alarm3TimeInCycle < 0.475) THEN 294 ELSE 0 ENDIF; alarm3Volume = IF alarm3Sounding AND (alarm3Frequency > 0) THEN 85 ELSE 0 ENDIF; alarm3NextTime = IF NOT alarm3Sounding THEN bigMax ELSIF alarm3Sounding AND (alarm3TimeInCycle < 0.2) THEN alarm3StartTime + 0.2 ELSIF alarm3Sounding AND (alarm3TimeInCycle < 0.275) THEN alarm3StartTime + 0.275 ELSE alarm3StartTime + alarm3CycleTime ENDIF; TRANSITION alarm3StartTime' IN {X: TIME | ((alarm3StartTime = 0) AND ((X = globalTime') OR (X = 0))) OR ((alarm3StartTime > 0) AND (globalTime' < (alarm3StartTime + alarm3CycleTime)) AND (X = alarm3StartTime)) OR ((alarm3StartTime > 0) AND (globalTime' >= (alarm3StartTime + alarm3CycleTime)) AND (X = 0)) }; END; maskingComputation : MODULE = BEGIN INPUT alarm2Volume : VOLUME INPUT alarm2Frequency : FREQUENCY INPUT alarm2Sounding : BOOLEAN INPUT alarm2NextTime : TIME INPUT alarm3Volume : VOLUME INPUT alarm3Frequency : FREQUENCY INPUT alarm3Sounding : BOOLEAN INPUT alarm3NextTime : TIME INPUT globalTime : TIME OUTPUT alarm2Masked : BOOLEAN OUTPUT alarm3Masked : BOOLEAN OUTPUT maxNextTime : TIME DEFINITION alarm2Masked = masking(alarm3Sounding,alarm3Frequency,alarm3Volume,alarm2Sounding,alarm2Frequency,alarm2Volume); alarm3Masked = masking(alarm2Sounding,alarm2Frequency,alarm2Volume,alarm3Sounding,alarm3Frequency,alarm3Volume); maxNextTime IN {X: TIME | (X = alarm2NextTime OR X = alarm3NextTime) AND (X <= alarm2NextTime AND X <= alarm3NextTime)}; END; system : MODULE = clock || alarm2 || alarm3 || maskingComputation; Alarm2PartialMasking : THEOREM system |- G (NOT(alarm2Volume > 0 AND alarm2Masked)); Alarm3PartialMasking : THEOREM system |- G (NOT(alarm3Volume > 0 AND alarm3Masked)); Alarm2TotalMasking : THEOREM system |- G(NOT((NOT alarm2Sounding) AND X(alarm2Sounding AND alarm2Masked AND U(alarm2Sounding AND alarm2Masked, NOT alarm2Sounding)))); Alarm3TotalMasking : THEOREM system |- G(NOT((NOT alarm3Sounding) AND X(alarm3Sounding AND alarm3Masked AND U(alarm3Sounding AND alarm3Masked, NOT alarm3Sounding)))); END