equal
deleted
inserted
replaced
9 Your tool should run only a specified amount of time.\smallskip |
9 Your tool should run only a specified amount of time.\smallskip |
10 |
10 |
11 {\bf Solution:} This can be achieved using the function |
11 {\bf Solution:} This can be achieved using the function |
12 @{ML timeLimit in TimeLimit}.\smallskip |
12 @{ML timeLimit in TimeLimit}.\smallskip |
13 |
13 |
14 Assume the following infamous function: |
14 Assume you defined the Ackermann function: |
15 |
15 |
16 *} |
16 *} |
17 |
17 |
18 ML {* |
18 ML {* |
19 fun ackermann (0, n) = n + 1 |
19 fun ackermann (0, n) = n + 1 |
25 |
25 |
26 Now the call |
26 Now the call |
27 |
27 |
28 @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"} |
28 @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"} |
29 |
29 |
30 takes a bit of time to finish. To avoid this, the call can be encapsulated |
30 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
31 in a time limit of five seconds. For this you have to write: |
31 in a time limit of five seconds. For this you have to write: |
32 |
32 |
33 @{ML_response [display] |
33 @{ML_response [display] |
34 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
34 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
35 handle TimeOut => ~1" |
35 handle TimeOut => ~1" |