suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add exit message with counts

Browse Source
This commit is contained in:
Burke Fetscher 2014-03-19 12:59:40 -05:00
parent 4612775a75
commit 190ef41661
1 changed files with 12 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt
View File

@ -110,6 +110,7 @@
(collect-garbage) (collect-garbage)
(define s-time (current-process-milliseconds)) (define s-time (current-process-milliseconds))
(define terms 0) (define terms 0)
(define counterexamples 0)
(let trials-loop ([t 0] (let trials-loop ([t 0]
[g (get-gen)]) [g (get-gen)])
(define t-time (current-process-milliseconds)) (define t-time (current-process-milliseconds))
@ -117,10 +118,7 @@
(define tot-time (- (current-process-milliseconds) s-time)) (define tot-time (- (current-process-milliseconds) s-time))
(cond (cond
[((/ tot-time 1000) . > . seconds) [((/ tot-time 1000) . > . seconds)
(when verbose? (exit-message fname type (+ i terms) tot-time counterexamples)]
(printf "Quitting after ~s iterations and ~s milliseconds\n ~s terms/sec\n"
(+ i terms) tot-time (exact->inexact (/ (+ i terms) (/ tot-time 1000)))))
(void)]
[else [else
(define term (with-timeout (* 5 60 1000) g (define term (with-timeout (* 5 60 1000) g
(λ () (printf "\nTimed out generating a test term in: ~a, ~a\n" (λ () (printf "\nTimed out generating a test term in: ~a, ~a\n"
@ -133,6 +131,7 @@
(trials-loop t g)))) (trials-loop t g))))
(cond (cond
[(not ok?) [(not ok?)
(set! counterexamples (add1 counterexamples))
(when verbose? (when verbose?
(printf "~a: counterexample: ~s\n ~s iterations and ~s milliseconds\n" (printf "~a: counterexample: ~s\n ~s iterations and ~s milliseconds\n"
fname term i me-time)) fname term i me-time))
@ -147,10 +146,18 @@
(begin (begin
(set! terms (+ i terms)) (set! terms (+ i terms))
(trials-loop (add1 t) (get-gen))) (trials-loop (add1 t) (get-gen)))
(void))] (exit-message fname type (+ i terms) tot-time counterexamples))]
[else [else
(loop (add1 i))])])))) (loop (add1 i))])]))))
(define (exit-message file type terms time countxmps)
(printf "----------\n~a, ~s\n" file type)
(printf "Quitting after ~s iterations and ~s milliseconds\n ~s terms/sec\n"
terms time (exact->inexact (/ terms (/ time 1000))))
(printf "~s counterexamples, ~s tries... ratio: ~s\n-----------------\n"
countxmps terms (exact->inexact (/ terms countxmps))))
(define (update-results time fname type verbose?) (define (update-results time fname type verbose?)
(set! results (hash-set results type (cons time (hash-ref results type)))) (set! results (hash-set results type (cons time (hash-ref results type))))
(define new-stats (update-statistics (hash-ref stats type) time)) (define new-stats (update-statistics (hash-ref stats type) time))