61
|
1 |
theory TimeLimit
|
346
|
2 |
imports "../Appendix"
|
61
|
3 |
begin
|
|
4 |
|
94
|
5 |
section {* Restricting the Runtime of a Function\label{rec:timeout} *}
|
61
|
6 |
|
|
7 |
text {*
|
|
8 |
{\bf Problem:}
|
63
|
9 |
Your tool should run only a specified amount of time.\smallskip
|
61
|
10 |
|
191
|
11 |
{\bf Solution:} In PolyML 5.2.1 and later, this can be achieved
|
|
12 |
using the function @{ML timeLimit in TimeLimit}.\smallskip
|
61
|
13 |
|
168
|
14 |
Assume you defined the Ackermann function on the ML-level.
|
|
15 |
*}
|
61
|
16 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
ML %grayML{*fun ackermann (0, n) = n + 1
|
61
|
18 |
| ackermann (m, 0) = ackermann (m - 1, 1)
|
69
|
19 |
| ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
|
61
|
20 |
|
63
|
21 |
text {*
|
|
22 |
|
|
23 |
Now the call
|
|
24 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
@{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"}
|
61
|
26 |
|
68
|
27 |
takes a bit of time before it finishes. To avoid this, the call can be encapsulated
|
168
|
28 |
in a time limit of five seconds. For this you have to write
|
63
|
29 |
|
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
@{ML_response_fake_both [display,gray]
|
63
|
31 |
"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12)
|
94
|
32 |
handle TimeLimit.TimeOut => ~1"
|
63
|
33 |
"~1"}
|
61
|
34 |
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
where @{text TimeOut} is the exception raised when the time limit
|
63
|
36 |
is reached.
|
|
37 |
|
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML 5.2.1
|
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
or later, because this version of PolyML has the infrastructure for multithreaded
|
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
programming on which @{ML "timeLimit" in TimeLimit} relies.
|
61
|
41 |
|
63
|
42 |
\begin{readmore}
|
|
43 |
The function @{ML "timeLimit" in TimeLimit} is defined in the structure
|
|
44 |
@{ML_struct TimeLimit} which can be found in the file
|
|
45 |
@{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}.
|
|
46 |
\end{readmore}
|
|
47 |
|
|
48 |
|
61
|
49 |
*}
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
end
|