/usr/share/doc/racket/redex/benchmark.html is in racket-doc 6.1-4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"/><title>3 Automated Testing Benchmark</title><link rel="stylesheet" type="text/css" href="../scribble.css" title="default"/><link rel="stylesheet" type="text/css" href="../racket.css" title="default"/><link rel="stylesheet" type="text/css" href="../manual-style.css" title="default"/><link rel="stylesheet" type="text/css" href="../manual-racket.css" title="default"/><link rel="stylesheet" type="text/css" href="../doc-site.css" title="default"/><script type="text/javascript" src="../scribble-common.js"></script><script type="text/javascript" src="../manual-racket.js"></script><script type="text/javascript" src="../doc-site.js"></script><script type="text/javascript" src="../local-redirect/local-redirect.js"></script><script type="text/javascript" src="../local-redirect/local-user-redirect.js"></script><!--[if IE 6]><style type="text/css">.SIEHidden { overflow: hidden; }</style><![endif]--></head><body id="doc-racket-lang-org"><div class="tocset"><div class="tocview"><div class="tocviewlist tocviewlisttopspace"><div class="tocviewtitle"><table cellspacing="0" cellpadding="0"><tr><td style="width: 1em;"><a href="javascript:void(0);" title="Expand/Collapse" class="tocviewtoggle" onclick="TocviewToggle(this,"tocview_0");">▼</a></td><td></td><td><a href="index.html" class="tocviewlink" data-pltdoc="x">Redex:<span class="mywbr"> </span> Practical Semantics Engineering</a></td></tr></table></div><div class="tocviewsublisttop" style="display: block;" id="tocview_0"><table cellspacing="0" cellpadding="0"><tr><td align="right">1 </td><td><a href="tutorial.html" class="tocviewlink" data-pltdoc="x">Amb:<span class="mywbr"> </span> A Redex Tutorial</a></td></tr><tr><td align="right">2 </td><td><a href="The_Redex_Reference.html" class="tocviewlink" data-pltdoc="x">The Redex Reference</a></td></tr><tr><td align="right">3 </td><td><a href="" class="tocviewselflink" data-pltdoc="x">Automated Testing Benchmark</a></td></tr><tr><td align="right"></td><td><a href="doc-index.html" class="tocviewlink" data-pltdoc="x">Index</a></td></tr></table></div></div><div class="tocviewlist"><table cellspacing="0" cellpadding="0"><tr><td style="width: 1em;"><a href="javascript:void(0);" title="Expand/Collapse" class="tocviewtoggle" onclick="TocviewToggle(this,"tocview_1");">►</a></td><td>3 </td><td><a href="" class="tocviewselflink" data-pltdoc="x">Automated Testing Benchmark</a></td></tr></table><div class="tocviewsublistbottom" style="display: none;" id="tocview_1"><table cellspacing="0" cellpadding="0"><tr><td align="right">3.1 </td><td><a href="#%28part._manage%29" class="tocviewlink" data-pltdoc="x">Managing Benchmark Modules</a></td></tr><tr><td align="right">3.2 </td><td><a href="#%28part._run%29" class="tocviewlink" data-pltdoc="x">Running Benchmark Models</a></td></tr><tr><td align="right">3.3 </td><td><a href="#%28part._log%29" class="tocviewlink" data-pltdoc="x">Logging</a></td></tr><tr><td align="right">3.4 </td><td><a href="#%28part._.Plotting%29" class="tocviewlink" data-pltdoc="x">Plotting</a></td></tr><tr><td align="right">3.5 </td><td><a href="#%28part._.Benchmark_.Models%29" class="tocviewlink" data-pltdoc="x">Benchmark Models</a></td></tr></table></div></div></div><div class="tocsub"><div class="tocsubtitle">On this page:</div><table class="tocsublist" cellspacing="0"><tr><td><span class="tocsublinknumber">3.1<tt> </tt></span><a href="#%28part._manage%29" class="tocsubseclink" data-pltdoc="x">Managing Benchmark Modules</a></td></tr><tr><td><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-<wbr></wbr>rewrite</span></span></a></td></tr><tr><td><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%2Fcompose%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-<wbr></wbr>rewrite/<span class="mywbr"> </span>compose</span></span></a></td></tr><tr><td><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._include%2Frewrite%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">include/<span class="mywbr"> </span>rewrite</span></span></a></td></tr><tr><td><span class="tocsublinknumber">3.2<tt> </tt></span><a href="#%28part._run%29" class="tocsubseclink" data-pltdoc="x">Running Benchmark Models</a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-<wbr></wbr>results</span></span></a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-<wbr></wbr>gen-<wbr></wbr>and-<wbr></wbr>check</span></span></a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%2Fmods%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-<wbr></wbr>gen-<wbr></wbr>and-<wbr></wbr>check/<span class="mywbr"> </span>mods</span></span></a></td></tr><tr><td><span class="tocsublinknumber">3.3<tt> </tt></span><a href="#%28part._log%29" class="tocsubseclink" data-pltdoc="x">Logging</a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-data%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym">bmark-<wbr></wbr>log-<wbr></wbr>data</span></a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._benchmark-logging-to%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">benchmark-<wbr></wbr>logging-<wbr></wbr>to</span></span></a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-directory%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bmark-<wbr></wbr>log-<wbr></wbr>directory</span></span></a></td></tr><tr><td><span class="tocsublinknumber">3.4<tt> </tt></span><a href="#%28part._.Plotting%29" class="tocsubseclink" data-pltdoc="x">Plotting</a></td></tr><tr><td><span class="tocsublinknumber">3.5<tt> </tt></span><a href="#%28part._.Benchmark_.Models%29" class="tocsubseclink" data-pltdoc="x">Benchmark Models</a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._all-mods%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym">all-<wbr></wbr>mods</span></a></td></tr></table></div></div><div class="maincolumn"><div class="main"><div class="navsettop"><span class="navleft"><form class="searchform"><input class="searchbox" style="color: #888;" type="text" value="...search manuals..." title="Enter a search string to search the manuals" onkeypress="return DoSearchKey(event, this, "6.1", "../");" onfocus="this.style.color="black"; this.style.textAlign="left"; if (this.value == "...search manuals...") this.value="";" onblur="if (this.value.match(/^ *$/)) { this.style.color="#888"; this.style.textAlign="center"; this.value="...search manuals..."; }"/></form> <a href="../index.html" title="up to the documentation top" data-pltdoc="x" onclick="return GotoPLTRoot("6.1");">top</a></span><span class="navright"> <a href="The_Redex_Reference.html" title="backward to "2 The Redex Reference"" data-pltdoc="x">← prev</a> <a href="index.html" title="up to "Redex: Practical Semantics Engineering"" data-pltdoc="x">up</a> <a href="doc-index.html" title="forward to "Index"" data-pltdoc="x">next →</a></span> </div><h3 x-source-module="(lib "redex/redex.scrbl")" x-part-tag=""benchmark"">3<tt> </tt><a name="(part._benchmark)"></a><a name="(mod-path._redex/benchmark)"></a>Automated Testing Benchmark</h3><p><table cellspacing="0" cellpadding="0" class="defmodule"><tr><td align="left"><span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._require%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">require</a></span><span class="stt"> </span><a href="" class="RktModLink" data-pltdoc="x"><span class="RktSym">redex/benchmark</span></a><span class="RktPn">)</span></td><td align="right"><span class="RpackageSpec"><span class="Smaller"> package:</span> <span class="stt">redex-benchmark</span></span></td></tr></table></p><p>Redex’s automated testing benchmark provides a collection of buggy models and
utilities to test how efficiently methods of automatic test case
generation are able to find counterexamples for each bug.</p><p>The benchmark is organized by pairs of <span style="font-style: italic">generate</span> and <span style="font-style: italic">check</span> functions,
as described in <a href="#%28part._run%29" data-pltdoc="x">Running Benchmark Models</a>. Usually these are defined on a per-module basis,
using pattern based rewrites applied to existing module definitions, as
described in <a href="#%28part._manage%29" data-pltdoc="x">Managing Benchmark Modules</a>. More specifically, generate and check
functions are written for an existing (non-buggy) model, and then bugs
are individually added to the model; for each bug, the benchmark measures
how long, on average, different generate and check pairs take to find
a counterexample.</p><h4 x-source-module="(lib "redex/redex.scrbl")" x-part-tag=""manage"">3.1<tt> </tt><a name="(part._manage)"></a>Managing Benchmark Modules</h4><p>This section describes utilities for making changes to existing modules to
create new ones, intended to assist in adding bugs to models and keeping
buggy models in sync with changes to the original model.</p><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>syntax</p></div></div><table cellspacing="0" cellpadding="0" class="RktBlk RForeground"><tr><td><span class="RktPn">(</span><a name="(form._((lib._redex/benchmark..rkt)._define-rewrite))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%29%29" class="RktStxDef RktStxLink" data-pltdoc="x">define-rewrite</a></span></span><span class="hspace"> </span><span class="RktVar">id</span><span class="hspace"> </span><span class="RktVar">from</span><span class="hspace"> </span><span class="RktSym">==></span><span class="hspace"> </span><span class="RktVar">to</span></td></tr><tr><td><span class="hspace"> </span><span class="RktPn">[</span><span class="RktPn">#:context</span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktVar">context-id</span><span class="hspace"> </span><span class="RktMeta">...</span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace"> </span><span class="RktPn">#:variables</span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktVar">variable-id</span><span class="hspace"> </span><span class="RktMeta">...</span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace"> </span><span class="RktPn">#:once-only</span></td></tr><tr><td><span class="hspace"> </span><span class="RktPn">#:exactly-once</span><span class="RktPn">]</span><span class="RktPn">)</span></td></tr></table></blockquote></td></tr></table></blockquote><p>Defines a syntax transformer bound to <span class="RktSym">id</span>, the effect of which is
to rewrite syntax matching the pattern <span class="RktSym">from</span> to the result
expression <span class="RktSym">to</span>. The <span class="RktSym">from</span> argument should follow the
grammar of a <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=stx-patterns.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fstxcase-scheme..rkt%2529._syntax-case%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">syntax-case</a></span> pattern, and <span class="RktSym">to</span> acts
as the corresponding result expression. The behavior of the match is the
same as <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=stx-patterns.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fstxcase-scheme..rkt%2529._syntax-case%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">syntax-case</a></span>, except that all identifiers in
<span class="RktSym">from</span> are treated as literals with the exception of an identifier
that has the same binding as a <span class="RktSym">variable-id</span> appearing in the
<span class="RktPn">#:variables</span> keyword argument, which is treated
as a pattern variable. (The reverse of the situation for
<span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=stx-patterns.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fstxcase-scheme..rkt%2529._syntax-case%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">syntax-case</a></span>, where literals must be specified instead.)
The rewrite will only be applied in the context of a <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=module.html%23%2528form._%2528%2528quote._%7E23%7E25kernel%2529._module%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">module</a></span> form,
but it will be applied wherever possible within the module body,
subject to a few constraints.</p><p>The rest of the keyword arguments control where and how often the
rewrite may be applied. The <span class="RktPn">#:once-only</span> option specifies that the
rewrite can be applied no more than once, and the <span class="RktPn">#:exactly-once</span>
option asserts that the rewrite must be applied once (and no more). In both
cases a syntax error is raised if the condition is not met. The
<span class="RktPn">#:context</span> option searches for syntax of the form
<span class="RktPn">(</span><span class="RktSym">some-id</span><span class="stt"> </span><span class="RktPn">. </span><span class="RktSym">rest</span><span class="RktPn">)</span>, where the binding of <span class="RktSym">some-id</span>
matches that of the first <span class="RktSym">context-id</span> in the <span class="RktPn">#:context</span> list,
at which point it recurs on <span class="RktSym">rest</span> but drops the first id from the
list. Once every <span class="RktSym">context-id</span> has been matched, the
rewrite can be applied.</p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>syntax</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(form._((lib._redex/benchmark..rkt)._define-rewrite/compose))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%2Fcompose%29%29" class="RktStxDef RktStxLink" data-pltdoc="x">define-rewrite/compose</a></span></span><span class="hspace"> </span><span class="RktVar">id</span><span class="hspace"> </span><span class="RktVar">rw-id</span><span class="hspace"> </span><span class="RktMeta">...</span><span class="RktPn">)</span></p></blockquote></td></tr></table></blockquote></div><div class="SIntrapara">Defines a syntax transformer bound to <span class="RktSym">id</span>, assuming that
every <span class="RktSym">rw-id</span> also binds a syntax transformer, such that <span class="RktSym">id</span>
has the effect of applying all of the <span class="RktSym">rw-id</span>s.</div></p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>syntax</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(form._((lib._redex/benchmark..rkt)._include/rewrite))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._include%2Frewrite%29%29" class="RktStxDef RktStxLink" data-pltdoc="x">include/rewrite</a></span></span><span class="hspace"> </span><span class="RktVar">path-spec</span><span class="hspace"> </span><span class="RktVar">mod-id</span><span class="hspace"> </span><span class="RktVar">rw-id</span><span class="hspace"> </span><span class="RktMeta">...</span><span class="RktPn">)</span></p></blockquote></td></tr></table></blockquote></div><div class="SIntrapara">If the syntax designated by <span class="RktSym">path-spec</span> is a module, the module syntax
is inlined as a submodule with the identifier <span class="RktSym">mod-id</span>. Assumes each
<span class="RktSym">rw-id</span> binds a syntax transformer, and applies them to the resulting
module syntax. The syntax of <span class="RktSym">path-spec</span> must be same as for
<span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=include.html%23%2528form._%2528%2528lib._racket%252Finclude..rkt%2529._include%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">include</a></span>.</div></p><p><div class="SIntrapara">For example, if the contents of the file mod-fx.rkt are:
</div><div class="SIntrapara"><blockquote class="SCodeFlow"><blockquote class="Rfilebox"><p class="Rfiletitle"><span class="Rfilename"><span class="stt">"mod-fx.rkt"</span></span></p><blockquote class="Rfilecontent"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=guide&rel=Module_Syntax.html%23%2528part._hash-lang%2529&version=6.1" class="RktModLink Sq" data-pltdoc="x"><span class="RktMod">#lang</span></a><span class="hspace"> </span><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=index.html&version=6.1" class="RktModLink Sq" data-pltdoc="x"><span class="RktSym">racket/base</span></a></td></tr><tr><td><span class="hspace"> </span></td></tr><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._provide%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">provide</a></span><span class="hspace"> </span><span class="RktSym">f</span><span class="RktPn">)</span></td></tr><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=define.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._define%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">define</a></span><span class="hspace"> </span><span class="RktSym">x</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">X!</span><span class="RktPn">)</span></td></tr><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=define.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._define%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">define</a></span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym">f</span><span class="hspace"> </span><span class="RktSym">x</span><span class="RktPn">)</span><span class="hspace"> </span><span class="RktSym">x</span><span class="RktPn">)</span></td></tr></table></blockquote></blockquote></blockquote></div><div class="SIntrapara">Then:
</div><div class="SIntrapara"><blockquote class="SCodeFlow"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="stt">> </span><span class="RktPn">(</span><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%29%29" class="RktStxLink" data-pltdoc="x">define-rewrite</a></span><span class="hspace"> </span><span class="RktSym">xy-rw</span></td></tr><tr><td><span class="hspace"> </span><span class="hspace"> </span><span class="RktSym">x</span><span class="hspace"> </span><span class="RktSym">==></span><span class="hspace"> </span><span class="RktSym">y</span></td></tr><tr><td><span class="hspace"> </span><span class="hspace"> </span><span class="RktPn">#:context</span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym">f</span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace"> </span><span class="hspace"> </span><span class="RktPn">#:once-only</span><span class="RktPn">)</span></td></tr></table></td></tr><tr><td><table cellspacing="0" cellpadding="0"><tr><td></td></tr></table></td></tr><tr><td><span class="stt">> </span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._require%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">require</a></span><span class="hspace"> </span><span class="RktVal">"mod-fx.rkt"</span><span class="RktPn">)</span></td></tr><tr><td><table cellspacing="0" cellpadding="0"><tr><td></td></tr></table></td></tr><tr><td><span class="stt">> </span><span class="RktPn">(</span><span class="RktSym">f</span><span class="hspace"> </span><span class="RktVal">3</span><span class="RktPn">)</span></td></tr><tr><td><p><span class="RktRes">3</span></p></td></tr><tr><td><span class="stt">> </span><span class="RktPn">(</span><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._include%2Frewrite%29%29" class="RktStxLink" data-pltdoc="x">include/rewrite</a></span><span class="hspace"> </span><span class="RktVal">"mod-fx.rkt"</span><span class="hspace"> </span><span class="RktSym">submod-fx</span><span class="hspace"> </span><span class="RktSym">xy-rw</span><span class="RktPn">)</span></td></tr><tr><td><table cellspacing="0" cellpadding="0"><tr><td></td></tr></table></td></tr><tr><td><span class="stt">> </span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._require%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">require</a></span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._prefix-in%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">prefix-in</a></span><span class="hspace"> </span><span class="RktSym">s:</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">submod-fx</span><span class="RktPn">)</span><span class="RktPn">)</span></td></tr><tr><td><table cellspacing="0" cellpadding="0"><tr><td></td></tr></table></td></tr><tr><td><span class="stt">> </span><span class="RktPn">(</span><span class="RktSym">s:f</span><span class="hspace"> </span><span class="RktVal">3</span><span class="RktPn">)</span></td></tr><tr><td><p><span class="RktRes">'X!</span></p></td></tr></table></blockquote></div></p><h4 x-source-module="(lib "redex/redex.scrbl")" x-part-tag=""run"">3.2<tt> </tt><a name="(part._run)"></a>Running Benchmark Models</h4><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>struct</p></div></div><p class="RForeground"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=define-struct.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._struct%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">struct</a></span><span class="stt"> </span><a name="(def._((lib._redex/benchmark..rkt)._run-results-cexps))"></a><a name="(def._((lib._redex/benchmark..rkt)._run-results-time))"></a><a name="(def._((lib._redex/benchmark..rkt)._run-results-tries))"></a><a name="(def._((lib._redex/benchmark..rkt)._run-results~3f))"></a><a name="(def._((lib._redex/benchmark..rkt)._struct~3arun-results))"></a><a name="(def._((lib._redex/benchmark..rkt)._run-results))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results%29%29" class="RktValDef RktValLink" data-pltdoc="x">run-results</a></span></span><span class="stt"> </span><span class="RktPn">(</span><span class="RktSym">tries</span><span class="stt"> </span><span class="RktSym">time</span><span class="stt"> </span><span class="RktSym">cexps</span><span class="RktPn">)</span><span class="RktPn">)</span></p></blockquote></td></tr><tr><td><span class="hspace"> </span><span class="RktSym">tries</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym">natural-number/c</span></td></tr><tr><td><span class="hspace"> </span><span class="RktSym">time</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym">natural-number/c</span></td></tr><tr><td><span class="hspace"> </span><span class="RktSym">cexps</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym">natural-number/c</span></td></tr></table></blockquote></div><div class="SIntrapara">Returned by <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValLink" data-pltdoc="x">run-gen-and-check</a></span>. Minimal results for one run of a generate and check pair.</div></p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>procedure</p></div></div><table cellspacing="0" cellpadding="0" class="prototype RForeground"><tr><td><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark..rkt)._run-gen-and-check))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValDef RktValLink" data-pltdoc="x">run-gen-and-check</a></span></span></td><td><span class="hspace"> </span></td><td><span class="RktVar">get-gen</span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td></tr><tr><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="RktVar">check</span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td></tr><tr><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="RktVar">seconds</span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td></tr><tr><td><span class="hspace"> </span></td><td><span class="hspace"> </span>[</td><td><span class="RktPn">#:name</span><span class="hspace"> </span><span class="RktVar">name</span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td></tr><tr><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="RktPn">#:type</span><span class="hspace"> </span><span class="RktVar">type</span>]<span class="RktPn">)</span></td><td><span class="hspace"> </span></td><td>→</td><td><span class="hspace"> </span></td><td><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results~3f%29%29" class="RktValLink" data-pltdoc="x">run-results?</a></span></td></tr></table></blockquote></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">get-gen</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym"><span class="nobreak">-></span></span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym"><span class="nobreak">-></span></span><span class="hspace"> </span><span class="RktSym">any/c</span><span class="RktPn">)</span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">check</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym"><span class="nobreak">-></span></span><span class="hspace"> </span><span class="RktSym">any/c</span><span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=booleans.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._boolean%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">boolean?</a></span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">seconds</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym">natural-number/c</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">name</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=strings.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._string%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">string?</a></span><span class="hspace"> </span>=<span class="hspace"> </span><span class="RktVal">"unknown"</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">type</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=symbols.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._symbol%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">symbol?</a></span><span class="hspace"> </span>=<span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">unknown</span></td></tr></table></blockquote></div><div class="SIntrapara">Repeatedly generates random terms and checks if they are counterexamples
to some property defined by <span class="RktVar">check</span> (a term is considered a counterexample
if <span class="RktVar">check</span> returns <span class="RktVal">#f</span> for that term).
The thunk <span class="RktVar">get-gen</span> is assumed to return a fresh <span style="font-style: italic">generator</span>, which
can then be called repeatedly to generate random terms. (The outer thunk is
assumed to reset the generator, for generators that have internal state. The
generator is reset each time the property is found to be false.)
Each term is passed to <span class="RktVar">check</span> to see if it is a counterexample.
The interval in milliseconds between counterexamples is
tracked, and the process is repeated either until the time specified by
<span class="RktVar">seconds</span> has elapsed or the standard error in the average interval
between counterexamples is less than 10% of the average.</div></p><p>Returns an instance of <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results%29%29" class="RktValLink" data-pltdoc="x">run-results</a></span> containing the total number of
terms generated, the total elapsed time, and the number of counterexamples found.
More detailed information can be obtained using the benchmark logging facilities,
for which <span class="RktVar">name</span> is refers to the name of the model, and <span class="RktVar">type</span>
is a symbol indicating the generation type used.</p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>procedure</p></div></div><table cellspacing="0" cellpadding="0" class="prototype RForeground"><tr><td><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark..rkt)._run-gen-and-check/mods))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%2Fmods%29%29" class="RktValDef RktValLink" data-pltdoc="x">run-gen-and-check/mods</a></span></span></td><td><span class="hspace"> </span></td><td><span class="RktVar">gen-mod-path</span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td></tr><tr><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="RktVar">check-mod-path</span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td></tr><tr><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="RktVar">seconds</span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td><td><span class="hspace"> </span></td></tr><tr><td><span class="hspace"> </span></td><td><span class="hspace"> </span>[</td><td><span class="RktPn">#:name</span><span class="hspace"> </span><span class="RktVar">name</span>]<span class="RktPn">)</span></td><td><span class="hspace"> </span></td><td>→</td><td><span class="hspace"> </span></td><td><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results~3f%29%29" class="RktValLink" data-pltdoc="x">run-results?</a></span></td></tr></table></blockquote></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">gen-mod-path</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=Module_Names_and_Loading.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._module-path%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">module-path?</a></span></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">check-mod-path</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=Module_Names_and_Loading.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._module-path%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">module-path?</a></span></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">seconds</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym">natural-number/c</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">name</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=strings.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._string%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">string?</a></span><span class="hspace"> </span>=<span class="hspace"> </span><span class="RktVal">"unknown"</span></td></tr></table></blockquote></div><div class="SIntrapara">Just like <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValLink" data-pltdoc="x">run-gen-and-check</a></span>, except that <span class="RktVar">gen-mod-path</span> and
<span class="RktVar">check-mod-path</span> are module paths to a <span style="font-style: italic">generator module</span> and a
<span style="font-style: italic">check module</span>, which are assumed to have the following characteristics:
</div><div class="SIntrapara"><ul><li><p>A <span style="font-style: italic">generator module</span> provides the function <span class="RktSym">get-generator</span>,
which meets the specification for the <span class="RktSym">get-gen</span> argument to
<span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValLink" data-pltdoc="x">run-gen-and-check</a></span>, and <span class="RktSym">type</span>, which is a symbol
designating the type of the generator.</p></li><li><p>A <span style="font-style: italic">check module</span> provides the function <span class="RktSym">check</span>, which meets
the specification for the <span class="RktSym">check</span> argument to
<span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValLink" data-pltdoc="x">run-gen-and-check</a></span>.</p></li></ul></div></p><h4 x-source-module="(lib "redex/redex.scrbl")" x-part-tag=""log"">3.3<tt> </tt><a name="(part._log)"></a>Logging</h4><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>struct</p></div></div><p class="RForeground"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=define-struct.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._struct%2529%2529&version=6.1" class="RktStxLink Sq" data-pltdoc="x">struct</a></span><span class="stt"> </span><a name="(def._((lib._redex/benchmark..rkt)._bmark-log-data-data))"></a><a name="(def._((lib._redex/benchmark..rkt)._bmark-log-data~3f))"></a><a name="(def._((lib._redex/benchmark..rkt)._struct~3abmark-log-data))"></a><a name="(def._((lib._redex/benchmark..rkt)._bmark-log-data))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><span class="RktSymDef RktSym">bmark-log-data</span></span></span><span class="stt"> </span><span class="RktPn">(</span><span class="RktSym">data</span><span class="RktPn">)</span><span class="RktPn">)</span></p></blockquote></td></tr><tr><td><span class="hspace"> </span><span class="RktSym">data</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym">any/c</span></td></tr></table></blockquote></div><div class="SIntrapara">Contains data logged by the benchmark, as described below.</div></p><p>Detailed information gathered during a benchmark run is logged to the <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=logging.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._current-logger%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">current-logger</a></span>,
at the <span class="RktVal">'</span><span class="RktVal">info</span> level, with the message <span class="RktVal">"BENCHMARK-LOGGING"</span>. The
<span class="RktSym">data</span> field of the log message contains a <span class="RktSym">bmark-log-data</span> struct, which
wraps data of the form:</p><p><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace"> </span><span class="RktVar">log-data</span></td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktVar">event</span><span class="hspace"> </span><span class="RktVar">timestamp</span><span class="hspace"> </span><span class="RktVar">data-list</span><span class="RktPn">)</span></td></tr></table></p><p>Where <span class="RktSym">event</span> is a symbol that designates the type of event, and
<span class="RktSym">timestamp</span> is symbol that contains the <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=time.html%23%2528def._%2528%2528lib._racket%252Fdate..rkt%2529._current-date%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">current-date</a></span> of the event in
ISO-8601 format.
The information in <span class="RktSym">data-list</span> depends on the event, but must be in the form
of a list alternating between a keyword and a datum, where the keyword is a short description
of the datum.</p><p><div class="SIntrapara">The following events are logged (the symbol designating the event is in parentheses, and
the form of the data logged for each event is shown):
</div><div class="SIntrapara"><ul><li><p><div class="SIntrapara">Run starts (<span class="RktVal">'</span><span class="RktVal">start</span>), logged when beginning a run with a new
generate/check pair.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace"> </span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace"> </span><span class="RktVar">model</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace"> </span><span class="RktVar">gen</span><span class="RktPn">)</span></td></tr></table></div></p></li><li><p><div class="SIntrapara">Run completions (<span class="RktVal">'</span><span class="RktVal">finished</span>), logged at the end of a run.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace"> </span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace"> </span><span class="RktVar">model</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace"> </span><span class="RktVar">gen</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:time-ms</span><span class="hspace"> </span><span class="RktVar">time</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:attempts</span><span class="hspace"> </span><span class="RktVar">tries</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:num-counterexamples</span><span class="hspace"> </span><span class="RktVar">countxmps</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:rate-terms/s</span><span class="hspace"> </span><span class="RktVar">rate</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:attempts/cexp</span><span class="hspace"> </span><span class="RktVar">atts</span><span class="RktPn">)</span></td></tr></table></td></tr></table></div></p></li><li><p><div class="SIntrapara">Every counterexample found (<span class="RktVal">'</span><span class="RktVal">counterexample</span>).
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace"> </span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace"> </span><span class="RktVar">model</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace"> </span><span class="RktVar">gen</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:counterexample</span><span class="hspace"> </span><span class="RktVar">term</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:iterations</span><span class="hspace"> </span><span class="RktVar">tries</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:time</span><span class="hspace"> </span><span class="RktVar">time</span><span class="RktPn">)</span></td></tr></table></td></tr></table></div></p></li><li><p><div class="SIntrapara">New average intervals between counterexamples (<span class="RktVal">'</span><span class="RktVal">new-average</span>), which
are recalculated whenever a counterexample is found.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace"> </span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace"> </span><span class="RktVar">model</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace"> </span><span class="RktVar">gen</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:average</span><span class="hspace"> </span><span class="RktVar">avg</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:stderr</span><span class="hspace"> </span><span class="RktVar">err</span><span class="RktPn">)</span></td></tr></table></td></tr></table></div></p></li><li><p><div class="SIntrapara">Major garbage collections (<span class="RktVal">'</span><span class="RktVal">gc-major</span>).
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace"> </span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:amount</span><span class="hspace"> </span><span class="RktVar">amount</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:time</span><span class="hspace"> </span><span class="RktVar">time</span><span class="RktPn">)</span></td></tr></table></div></p></li><li><p><div class="SIntrapara">Heartbeats (<span class="RktVal">'</span><span class="RktVal">hearbeat</span>) are logged every 10 seconds by the benchmark
as a liveness check.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace"> </span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace"> </span><span class="RktVar">model</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace"> </span><span class="RktVar">gen</span><span class="RktPn">)</span></td></tr></table></div></p></li><li><p><div class="SIntrapara">Timeouts (<span class="RktVal">'</span><span class="RktVal">timeout</span>), which occur when generating or checking a single
takes term longer than 5 minutes.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace"> </span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:during</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">check</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:term</span><span class="hspace"> </span><span class="RktVar">term</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace"> </span><span class="RktVar">model</span></td></tr><tr><td><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace"> </span><span class="RktVar">gen</span><span class="RktPn">)</span></td></tr></table></td></tr><tr><td align="right" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="center" valign="baseline">|</td><td align="left" valign="baseline"><span class="stt"> </span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:during</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">generation</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace"> </span><span class="RktVar">model</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace"> </span><span class="RktVar">gen</span><span class="RktPn">)</span></td></tr></table></div></p></li></ul></div></p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>procedure</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark..rkt)._benchmark-logging-to))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._benchmark-logging-to%29%29" class="RktValDef RktValLink" data-pltdoc="x">benchmark-logging-to</a></span></span><span class="hspace"> </span><span class="RktVar">filename</span><span class="hspace"> </span><span class="RktVar">thunk</span><span class="RktPn">)</span><span class="hspace"> </span>→<span class="hspace"> </span><span class="RktSym">any/c</span></p></blockquote></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">filename</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=strings.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._string%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">string?</a></span></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">thunk</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym"><span class="nobreak">-></span></span><span class="hspace"> </span><span class="RktSym">any/c</span><span class="RktPn">)</span></td></tr></table></blockquote></div><div class="SIntrapara">Intercepts events logged by the benchmark and writes the data specified by
the <span class="RktSym">log-data</span> production above to <span class="RktVar">filename</span>.</div></p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>parameter</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark..rkt)._bmark-log-directory))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-directory%29%29" class="RktValDef RktValLink" data-pltdoc="x">bmark-log-directory</a></span></span><span class="RktPn"></span><span class="RktPn">)</span></p></blockquote></td></tr><tr><td><span class="hspace"> </span>→<span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym">or/c</span><span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=Manipulating_Paths.html%23%2528def._%2528%2528lib._racket%252Fprivate%252Fmisc..rkt%2529._path-string%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">path-string?</a></span><span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=Manipulating_Paths.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._path-for-some-system%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">path-for-some-system?</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">up</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">same</span><span class="RktPn">)</span></td></tr><tr><td><span class="RktPn">(</span><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-directory%29%29" class="RktValDef RktValLink" data-pltdoc="x">bmark-log-directory</a></span></span><span class="hspace"> </span><span class="RktVar">directory</span><span class="RktPn">)</span><span class="hspace"> </span>→<span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=void.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._void%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">void?</a></span></td></tr><tr><td><span class="hspace"> </span><span class="RktVar">directory</span><span class="hspace"> </span>:<span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym">or/c</span><span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=Manipulating_Paths.html%23%2528def._%2528%2528lib._racket%252Fprivate%252Fmisc..rkt%2529._path-string%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">path-string?</a></span><span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=Manipulating_Paths.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._path-for-some-system%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">path-for-some-system?</a></span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">up</span><span class="hspace"> </span><span class="RktVal">'</span><span class="RktVal">same</span><span class="RktPn">)</span></td></tr><tr><td><table cellspacing="0" cellpadding="0" class="argcontract"><tr><td><span class="hspace"> </span>=<span class="hspace"> </span></td><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=Filesystem.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._current-directory%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">current-directory</a></span><span class="RktPn">)</span></td></tr></table></td></tr></table></blockquote></div><div class="SIntrapara">Controls the directory where <span class="RktSym">filename</span> in <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._benchmark-logging-to%29%29" class="RktValLink" data-pltdoc="x">benchmark-logging-to</a></span> is located.</div></p><h4 x-source-module="(lib "redex/redex.scrbl")" x-part-tag=""Plotting"">3.4<tt> </tt><a name="(part._.Plotting)"></a>Plotting</h4><p>Plotting and analysis tools consume data of the form produced by the benchmark
logging facilities (see <a href="#%28part._log%29" data-pltdoc="x">Logging</a>).</p><p><span style="font-style: italic">TODO!</span></p><h4 x-source-module="(lib "redex/redex.scrbl")" x-part-tag=""Benchmark_Models"">3.5<tt> </tt><a name="(part._.Benchmark_.Models)"></a>Benchmark Models</h4><p>The models included in the distribution of the benchmark are in the
<span class="stt">"redex/benchmark/models"</span> subdirectory of the <span class="RktSym">redex-benchmark</span>
package. Each such subdirectory contains an info file named according to the
pattern <span class="stt">"<name>-info.rkt"</span>, defining a module that provides the function:</p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>procedure</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark..rkt)._all-mods))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><span class="RktSymDef RktSym">all-mods</span></span></span><span class="RktPn"></span><span class="RktPn">)</span></p></blockquote></td></tr><tr><td><span class="hspace"> </span>→<span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym">listof</span><span class="hspace"> </span><span class="RktPn">(</span><span class="RktSym">list/c</span><span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=strings.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._string%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">string?</a></span><span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=Module_Names_and_Loading.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._module-path%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">module-path?</a></span><span class="hspace"> </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.1/html/local-redirect/index.html?doc=reference&rel=Module_Names_and_Loading.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._module-path%7E3f%2529%2529&version=6.1" class="RktValLink Sq" data-pltdoc="x">module-path?</a></span><span class="RktPn">)</span><span class="RktPn">)</span></td></tr></table></blockquote></div><div class="SIntrapara">Returns a list of
generate and check pairs for a given model or set of models, such that for each
pair the first element is the name of the model, the second is a module defining a
generator, and the third is a module defining a check function.</div></p><p>The file <span class="stt">"redex/benchmark/models/all-info.rkt"</span> provides an <span class="RktSym">all-mods</span>
function listing all of the generate and check pairs included in the benchmark.</p><p>A command line interface is provided by the file
<span class="stt">"redex/benchmark/run-benchmark.rkt"</span>,
which takes an “info” file as described above as its primary argument and provides
options for running the listed tests. It automatically writes results from each run to
a separate log file, all of which are located in a temporary directory.
(The directory path is printed to standard out at the beginning of the run).</p><div class="navsetbottom"><span class="navleft"><form class="searchform"><input class="searchbox" style="color: #888;" type="text" value="...search manuals..." title="Enter a search string to search the manuals" onkeypress="return DoSearchKey(event, this, "6.1", "../");" onfocus="this.style.color="black"; this.style.textAlign="left"; if (this.value == "...search manuals...") this.value="";" onblur="if (this.value.match(/^ *$/)) { this.style.color="#888"; this.style.textAlign="center"; this.value="...search manuals..."; }"/></form> <a href="../index.html" title="up to the documentation top" data-pltdoc="x" onclick="return GotoPLTRoot("6.1");">top</a></span><span class="navright"> <a href="The_Redex_Reference.html" title="backward to "2 The Redex Reference"" data-pltdoc="x">← prev</a> <a href="index.html" title="up to "Redex: Practical Semantics Engineering"" data-pltdoc="x">up</a> <a href="doc-index.html" title="forward to "Index"" data-pltdoc="x">next →</a></span> </div></div></div><div id="contextindicator"> </div></body></html>
|