Lines Matching refs:TIMEOUT
889 `outcome = RESULT of state | ERROR of state | TIMEOUT of state`;
891 (* Some automatically proves theorems relating RESULT, TIMEOUT and ERROR *)
1304 TIMEOUT s -> TIMEOUT s
1337 TIMEOUT s -> TIMEOUT s
1351 (!f f1 f2 a. outcome_case f f1 f2 (TIMEOUT a) = f2 a)``,
1389 `(RUN 0 c s = TIMEOUT s)
1501 (* Corollary relating non-termination and TIMEOUT *)
1506 !n. ?s2. (RUN n c s1 = ERROR s2) \/ (RUN n c s1 = TIMEOUT s2)``,
1513 `!x y. ~(RESULT x = ERROR y) /\ ~(RESULT x = TIMEOUT y)`
1523 then TIMEOUT(s)
1653 ?s. (SND(STEP1 con1 ) = ERROR s) \/ (SND(STEP1 con1 ) = TIMEOUT s)``,
1754 (l, TIMEOUT s) -> (l, TIMEOUT s)
1786 then (l, TIMEOUT s)
1792 ``STEP 0 (l,s) = if l = [] then ([], RESULT s) else (l, TIMEOUT s)``,
1810 (STEP 0 (l,s) = if l = [] then ([], RESULT s) else (l, TIMEOUT s))
1939 (* Corollary relating non-termination and TIMEOUT *)
1947 (STEP n (c :: l1, s1) = (l2,TIMEOUT s2))``,
1957 `!x y. ~(RESULT x = ERROR y) /\ ~(RESULT x = TIMEOUT y)`
1961 (STEP n (c::l1,s1) = (l2,TIMEOUT s2))`
1972 (STEP n ([c], s1) = (l,TIMEOUT s2))``,
2279 ((l, TIMEOUT s), p) -> ((l, TIMEOUT s), p)
2323 (ACC_STEP 0 ((l,s),p) = ((l, TIMEOUT s), p))
2341 then ((l, TIMEOUT s), p)