\documentclass[a4paper,10pt]{article} \usepackage{a4wide} \usepackage{longtable} \usepackage{xcolor} \begin{document} \textbf{Coverage Report (Regression Tests, generated 19.8.2018 6:19, commit ce702ba99f667cb03de8ed41ab58ba72db9112c3)} \\\\ analysis \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{847} & \textbf{459} & \textbf{0} & \textbf{54.2} & \textbf{331} & \textbf{214} & \textbf{0} & \textbf{64.7} \\ \hline b\_machine\_hierarchy.pl & 165 & 85 & 3 & 52.5 & 91 & 56 & 0 & 61.5 \\ \hline bvisual2.pl & 322 & 87 & 0 & 27.0 & 111 & 44 & 0 & 39.6 \\ \hline interval\_calc.pl & 8 & 7 & 0 & 87.5 & 6 & 5 & 0 & 83.3 \\ \hline predicate\_analysis.pl & 352 & 280 & 0 & 79.5 & 123 & 109 & 0 & 88.6 \\ \hline \end{longtable} animator \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{691} & \textbf{495} & \textbf{5} & \textbf{72.2} & \textbf{353} & \textbf{287} & \textbf{0} & \textbf{81.3} \\ \hline b\_operation\_cache.pl & 20 & 13 & 0 & 65.0 & 11 & 10 & 0 & 90.9 \\ \hline coverage\_statistics.pl & 65 & 41 & 0 & 63.1 & 36 & 21 & 0 & 58.3 \\ \hline hashing.pl & 3 & 2 & 0 & 66.7 & 3 & 2 & 0 & 66.7 \\ \hline specfile.pl & 261 & 185 & 1 & 71.2 & 103 & 91 & 0 & 88.3 \\ \hline state\_packing.pl & 92 & 68 & 4 & 77.3 & 32 & 27 & 0 & 84.4 \\ \hline state\_space.pl & 139 & 109 & 0 & 78.4 & 109 & 91 & 0 & 83.5 \\ \hline state\_space\_dijkstra.pl & 11 & 8 & 0 & 72.7 & 8 & 6 & 0 & 75.0 \\ \hline state\_space\_open\_nodes\_c.pl & 29 & 22 & 0 & 75.9 & 20 & 16 & 0 & 80.0 \\ \hline xtl\_interface.pl & 71 & 47 & 0 & 66.2 & 31 & 23 & 0 & 74.2 \\ \hline \end{longtable} cbc \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{535} & \textbf{331} & \textbf{5} & \textbf{62.5} & \textbf{261} & \textbf{188} & \textbf{0} & \textbf{72.0} \\ \hline random\_permutations.pl & 7 & 7 & 0 & 100.0 & 5 & 5 & 0 & 100.0 \\ \hline b\_state\_model\_check.pl & 138 & 108 & 2 & 79.4 & 70 & 55 & 0 & 78.6 \\ \hline cbc\_refinement\_checks.pl & 34 & 34 & 0 & 100.0 & 23 & 23 & 0 & 100.0 \\ \hline disprover.pl & 22 & 16 & 0 & 72.7 & 14 & 9 & 0 & 64.3 \\ \hline disprover\_test\_runner.pl & 94 & 25 & 0 & 26.6 & 43 & 17 & 0 & 39.5 \\ \hline enabling\_analysis.pl & 134 & 66 & 2 & 50.0 & 59 & 39 & 0 & 66.1 \\ \hline solver\_interface.pl & 56 & 39 & 0 & 69.6 & 26 & 22 & 0 & 84.6 \\ \hline weakest\_preconditions.pl & 50 & 36 & 1 & 73.5 & 21 & 18 & 0 & 85.7 \\ \hline \end{longtable} cli \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{581} & \textbf{41} & \textbf{6} & \textbf{7.1} & \textbf{376} & \textbf{36} & \textbf{0} & \textbf{9.6} \\ \hline eclipse\_interface.pl & 149 & 19 & 1 & 12.8 & 120 & 19 & 0 & 15.8 \\ \hline \textcolor[HTML]{FF0000}{prob2\_interface.pl} & \textcolor[HTML]{FF0000}{385} & \textcolor[HTML]{FF0000}{22} & \textcolor[HTML]{FF0000}{6} & \textcolor[HTML]{FF0000}{5.8} & \textcolor[HTML]{FF0000}{231} & \textcolor[HTML]{FF0000}{17} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{7.4} \\ \hline \textcolor[HTML]{FF0000}{prob\_socketserver.pl} & \textcolor[HTML]{FF0000}{47} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{25} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} coverage\_analysis \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{163} & \textbf{37} & \textbf{0} & \textbf{22.7} & \textbf{90} & \textbf{14} & \textbf{0} & \textbf{15.6} \\ \hline coverage\_term\_expander.pl & 36 & 36 & 0 & 100.0 & 13 & 13 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{coverage\_tools.pl} & \textcolor[HTML]{FF0000}{84} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{54} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{prob\_cov.pl} & \textcolor[HTML]{FF0000}{43} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2.3} & \textcolor[HTML]{FF0000}{23} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{4.3} \\ \hline \end{longtable} csp \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1610} & \textbf{1332} & \textbf{49} & \textbf{85.3} & \textbf{593} & \textbf{529} & \textbf{1} & \textbf{89.4} \\ \hline csp\_basic.pl & 5 & 5 & 0 & 100.0 & 5 & 5 & 0 & 100.0 \\ \hline csp\_sequences.pl & 58 & 37 & 3 & 67.3 & 21 & 20 & 0 & 95.2 \\ \hline csp\_sets.pl & 268 & 215 & 15 & 85.0 & 99 & 92 & 0 & 92.9 \\ \hline csp\_tuples.pl & 94 & 80 & 3 & 87.9 & 37 & 33 & 0 & 89.2 \\ \hline haskell\_csp.pl & 727 & 578 & 22 & 82.0 & 243 & 205 & 1 & 84.7 \\ \hline haskell\_csp\_analyzer.pl & 290 & 261 & 4 & 91.3 & 95 & 88 & 0 & 92.6 \\ \hline refinement\_checker.pl & 168 & 156 & 2 & 94.0 & 93 & 86 & 0 & 92.5 \\ \hline \end{longtable} dot \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{541} & \textbf{221} & \textbf{1} & \textbf{40.9} & \textbf{299} & \textbf{135} & \textbf{0} & \textbf{45.2} \\ \hline bvisual.pl & 135 & 90 & 0 & 66.7 & 62 & 55 & 0 & 88.7 \\ \hline \textcolor[HTML]{FF0000}{bvisual\_any\_maxsolver.pl} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline dot\_graph\_generator.pl & 58 & 23 & 0 & 39.7 & 26 & 16 & 0 & 61.5 \\ \hline \textcolor[HTML]{FF0000}{maxsolver.pl} & \textcolor[HTML]{FF0000}{38} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{24} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline reduce\_graph\_state\_space.pl & 151 & 64 & 0 & 42.4 & 99 & 42 & 0 & 42.4 \\ \hline \textcolor[HTML]{FF0000}{state\_custom\_dot\_graph.pl} & \textcolor[HTML]{FF0000}{26} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline visualize\_graph.pl & 128 & 44 & 0 & 34.4 & 69 & 22 & 0 & 31.9 \\ \hline \end{longtable} experimental \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{470} & \textbf{32} & \textbf{1} & \textbf{6.8} & \textbf{234} & \textbf{6} & \textbf{0} & \textbf{2.6} \\ \hline \textcolor[HTML]{FF0000}{cvc4interface.pl} & \textcolor[HTML]{FF0000}{30} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ltsmin.pl} & \textcolor[HTML]{FF0000}{168} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{106} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{satsolver.pl} & \textcolor[HTML]{FF0000}{40} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{21} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline z3interface.pl & 31 & 31 & 0 & 100.0 & 5 & 5 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{master.pl} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{worker.pl} & \textcolor[HTML]{FF0000}{28} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{19} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{zmq.pl} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{flow.pl} & \textcolor[HTML]{FF0000}{155} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.6} & \textcolor[HTML]{FF0000}{73} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1.4} \\ \hline \end{longtable} external\_functions \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1502} & \textbf{604} & \textbf{0} & \textbf{40.2} & \textbf{554} & \textbf{302} & \textbf{0} & \textbf{54.5} \\ \hline external\_functions.pl & 914 & 446 & 11 & 49.4 & 411 & 236 & 0 & 57.4 \\ \hline xml2b.pl & 28 & 20 & 0 & 71.4 & 10 & 10 & 0 & 100.0 \\ \hline xml\_prob.pl & 560 & 138 & 0 & 24.6 & 133 & 56 & 0 & 42.1 \\ \hline \end{longtable} infrastructure \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{6894} & \textbf{4844} & \textbf{29} & \textbf{70.6} & \textbf{1768} & \textbf{1080} & \textbf{7} & \textbf{61.3} \\ \hline probhash.pl & 21 & 5 & 0 & 23.8 & 19 & 4 & 0 & 21.1 \\ \hline user\_signal.pl & 12 & 9 & 0 & 75.0 & 9 & 6 & 0 & 66.7 \\ \hline bmachine.pl & 472 & 372 & 4 & 79.5 & 263 & 216 & 0 & 82.1 \\ \hline debug.pl & 74 & 27 & 0 & 36.5 & 64 & 25 & 0 & 39.1 \\ \hline debugging\_calls.pl & 15 & 10 & 0 & 66.7 & 9 & 5 & 0 & 55.6 \\ \hline debugging\_calls\_te.pl & 4 & 1 & 0 & 25.0 & 4 & 1 & 0 & 25.0 \\ \hline error\_manager.pl & 246 & 164 & 6 & 68.3 & 148 & 110 & 6 & 77.5 \\ \hline eventhandling.pl & 24 & 18 & 1 & 78.3 & 9 & 7 & 0 & 77.8 \\ \hline junit\_tests.pl & 18 & 14 & 1 & 82.4 & 11 & 11 & 0 & 100.0 \\ \hline logger.pl & 75 & 33 & 2 & 45.2 & 39 & 20 & 0 & 51.3 \\ \hline module\_information.pl & 6 & 2 & 0 & 33.3 & 5 & 2 & 0 & 40.0 \\ \hline pathes.pl & 16 & 15 & 0 & 93.8 & 14 & 13 & 0 & 92.9 \\ \hline plugins.pl & 108 & 66 & 0 & 61.1 & 62 & 34 & 0 & 54.8 \\ \hline preferences.pl & 1479 & 867 & 0 & 58.6 & 93 & 44 & 0 & 47.3 \\ \hline prob\_cli.pl & 972 & 501 & 8 & 52.0 & 357 & 235 & 0 & 65.8 \\ \hline self\_check.pl & 86 & 13 & 0 & 15.1 & 69 & 13 & 0 & 18.8 \\ \hline state\_space\_exploration\_modes.pl & 57 & 30 & 0 & 52.6 & 25 & 18 & 0 & 72.0 \\ \hline succeed\_max.pl & 12 & 12 & 0 & 100.0 & 8 & 8 & 0 & 100.0 \\ \hline tcltk\_interface.pl & 462 & 178 & 6 & 39.0 & 305 & 121 & 1 & 39.8 \\ \hline testcases.pl & 2099 & 2087 & 0 & 99.4 & 7 & 6 & 0 & 85.7 \\ \hline tools.pl & 333 & 217 & 1 & 65.4 & 142 & 111 & 0 & 78.2 \\ \hline tools\_files.pl & 7 & 7 & 0 & 100.0 & 5 & 5 & 0 & 100.0 \\ \hline tools\_io.pl & 1 & 1 & 0 & 100.0 & 1 & 1 & 0 & 100.0 \\ \hline tools\_lists.pl & 3 & 3 & 0 & 100.0 & 2 & 2 & 0 & 100.0 \\ \hline tools\_matching.pl & 79 & 77 & 0 & 97.5 & 8 & 7 & 0 & 87.5 \\ \hline tools\_meta.pl & 18 & 10 & 0 & 55.6 & 14 & 8 & 0 & 57.1 \\ \hline tools\_printing.pl & 140 & 64 & 0 & 45.7 & 43 & 21 & 0 & 48.8 \\ \hline tools\_strings.pl & 34 & 30 & 0 & 88.2 & 16 & 16 & 0 & 100.0 \\ \hline tools\_timeout.pl & 6 & 5 & 0 & 83.3 & 5 & 4 & 0 & 80.0 \\ \hline user\_interrupts.pl & 4 & 1 & 0 & 25.0 & 4 & 1 & 0 & 25.0 \\ \hline version.pl & 11 & 5 & 0 & 45.5 & 8 & 5 & 0 & 62.5 \\ \hline \end{longtable} \textbf{interpreter }\begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1843} & \textbf{1614} & \textbf{25} & \textbf{88.8} & \textbf{794} & \textbf{729} & \textbf{0} & \textbf{91.8} \\ \hline b\_compiler.pl & 241 & 216 & 1 & 90.0 & 61 & 58 & 0 & 95.1 \\ \hline b\_enumerate.pl & 98 & 94 & 0 & 95.9 & 42 & 41 & 0 & 97.6 \\ \hline b\_interpreter.pl & 613 & 533 & 16 & 89.3 & 296 & 276 & 0 & 93.2 \\ \hline b\_interpreter\_check.pl & 389 & 347 & 5 & 90.4 & 111 & 103 & 0 & 92.8 \\ \hline b\_interpreter\_components.pl & 70 & 70 & 0 & 100.0 & 51 & 51 & 0 & 100.0 \\ \hline b\_interpreter\_eventb.pl & 75 & 73 & 2 & 100.0 & 49 & 49 & 0 & 100.0 \\ \hline store.pl & 176 & 152 & 2 & 87.4 & 71 & 69 & 0 & 97.2 \\ \hline value\_persistance.pl & 181 & 129 & 0 & 71.3 & 113 & 82 & 0 & 72.6 \\ \hline \end{longtable} \textbf{kernel }\begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{5175} & \textbf{4389} & \textbf{79} & \textbf{86.1} & \textbf{2253} & \textbf{2056} & \textbf{2} & \textbf{91.3} \\ \hline avl\_tools.pl & 23 & 22 & 0 & 95.7 & 14 & 13 & 0 & 92.9 \\ \hline b\_global\_sets.pl & 206 & 181 & 2 & 88.7 & 98 & 97 & 0 & 99.0 \\ \hline bool\_pred.pl & 29 & 22 & 0 & 75.9 & 20 & 15 & 0 & 75.0 \\ \hline bsets\_clp.pl & 680 & 610 & 4 & 90.2 & 353 & 325 & 0 & 92.1 \\ \hline closures.pl & 100 & 70 & 1 & 70.7 & 38 & 37 & 0 & 97.4 \\ \hline clpfd\_interface.pl & 161 & 136 & 0 & 84.5 & 90 & 79 & 0 & 87.8 \\ \hline clpfd\_lists.pl & 123 & 93 & 7 & 80.2 & 36 & 32 & 0 & 88.9 \\ \hline clpfd\_tables.pl & 47 & 47 & 0 & 100.0 & 24 & 24 & 0 & 100.0 \\ \hline custom\_explicit\_sets.pl & 1359 & 1179 & 25 & 88.4 & 550 & 523 & 0 & 95.1 \\ \hline delay.pl & 31 & 31 & 0 & 100.0 & 22 & 22 & 0 & 100.0 \\ \hline fd\_utils\_clpfd.pl & 11 & 9 & 0 & 81.8 & 9 & 9 & 0 & 100.0 \\ \hline inf\_arith.pl & 51 & 39 & 0 & 76.5 & 21 & 17 & 0 & 81.0 \\ \hline kernel\_dif.pl & 10 & 10 & 0 & 100.0 & 5 & 5 & 0 & 100.0 \\ \hline kernel\_equality.pl & 166 & 156 & 5 & 96.9 & 74 & 71 & 0 & 95.9 \\ \hline kernel\_frozen\_info.pl & 17 & 8 & 0 & 47.1 & 6 & 6 & 0 & 100.0 \\ \hline kernel\_mappings.pl & 409 & 359 & 0 & 87.8 & 95 & 88 & 0 & 92.6 \\ \hline kernel\_objects.pl & 1105 & 921 & 8 & 84.0 & 525 & 461 & 1 & 88.0 \\ \hline kernel\_ordering.pl & 41 & 28 & 0 & 68.3 & 15 & 11 & 0 & 73.3 \\ \hline kernel\_propagation.pl & 4 & 4 & 0 & 100.0 & 3 & 3 & 0 & 100.0 \\ \hline kernel\_records.pl & 21 & 19 & 1 & 95.0 & 15 & 14 & 0 & 93.3 \\ \hline kernel\_strings.pl & 103 & 90 & 1 & 88.2 & 64 & 61 & 0 & 95.3 \\ \hline kernel\_tools.pl & 244 & 214 & 6 & 89.9 & 38 & 36 & 0 & 94.7 \\ \hline kernel\_waitflags.pl & 211 & 120 & 19 & 62.5 & 126 & 95 & 1 & 76.0 \\ \hline static\_symmetry\_reduction.pl & 23 & 21 & 0 & 91.3 & 12 & 12 & 0 & 100.0 \\ \hline \end{longtable} kodkod \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{713} & \textbf{552} & \textbf{2} & \textbf{77.6} & \textbf{321} & \textbf{270} & \textbf{0} & \textbf{84.1} \\ \hline kodkod.pl & 91 & 56 & 0 & 61.5 & 48 & 34 & 0 & 70.8 \\ \hline kodkod2.pl & 67 & 65 & 0 & 97.0 & 38 & 38 & 0 & 100.0 \\ \hline kodkod\_integer\_recalc.pl & 23 & 17 & 0 & 73.9 & 8 & 8 & 0 & 100.0 \\ \hline kodkod\_printer.pl & 121 & 105 & 0 & 86.8 & 43 & 42 & 0 & 97.7 \\ \hline kodkod\_process.pl & 65 & 53 & 2 & 84.1 & 44 & 38 & 0 & 86.4 \\ \hline kodkod\_rewrite.pl & 26 & 18 & 0 & 69.2 & 11 & 10 & 0 & 90.9 \\ \hline kodkod\_test.pl & 50 & 11 & 0 & 22.0 & 39 & 11 & 0 & 28.2 \\ \hline kodkod\_tools.pl & 27 & 26 & 0 & 96.3 & 18 & 18 & 0 & 100.0 \\ \hline kodkod\_translate.pl & 158 & 132 & 0 & 83.5 & 47 & 46 & 0 & 97.9 \\ \hline kodkod\_typing.pl & 85 & 69 & 0 & 81.2 & 25 & 25 & 0 & 100.0 \\ \hline \end{longtable} ltl \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{878} & \textbf{598} & \textbf{22} & \textbf{69.9} & \textbf{372} & \textbf{301} & \textbf{0} & \textbf{80.9} \\ \hline ltl2ba.pl & 5 & 5 & 0 & 100.0 & 5 & 5 & 0 & 100.0 \\ \hline ltlc.pl & 92 & 86 & 0 & 93.5 & 31 & 30 & 0 & 96.8 \\ \hline ctl.pl & 69 & 51 & 3 & 77.3 & 29 & 23 & 0 & 79.3 \\ \hline ltl.pl & 146 & 96 & 5 & 68.1 & 81 & 65 & 0 & 80.2 \\ \hline ltl\_fairness.pl & 56 & 38 & 3 & 71.7 & 31 & 25 & 0 & 80.6 \\ \hline ltl\_propositions.pl & 66 & 29 & 3 & 46.0 & 26 & 15 & 0 & 57.7 \\ \hline ltl\_safety.pl & 88 & 57 & 2 & 66.3 & 25 & 20 & 0 & 80.0 \\ \hline ltl\_tools.pl & 151 & 125 & 1 & 83.3 & 59 & 53 & 0 & 89.8 \\ \hline \textcolor[HTML]{FF0000}{ltl\_translate.pl} & \textcolor[HTML]{FF0000}{64} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{12} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline ltl\_verification.pl & 70 & 64 & 0 & 91.4 & 32 & 32 & 0 & 100.0 \\ \hline safety\_mc.pl & 61 & 39 & 5 & 69.6 & 35 & 27 & 0 & 77.1 \\ \hline state\_space\_explorer.pl & 10 & 8 & 0 & 80.0 & 6 & 6 & 0 & 100.0 \\ \hline \end{longtable} misc \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{391} & \textbf{197} & \textbf{2} & \textbf{50.6} & \textbf{217} & \textbf{113} & \textbf{0} & \textbf{52.1} \\ \hline b\_show\_history.pl & 38 & 30 & 1 & 81.1 & 23 & 19 & 0 & 82.6 \\ \hline before\_after\_predicates.pl & 54 & 30 & 2 & 57.7 & 26 & 18 & 0 & 69.2 \\ \hline \textcolor[HTML]{FF0000}{evalstores.pl} & \textcolor[HTML]{FF0000}{49} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{4.1} & \textcolor[HTML]{FF0000}{34} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{5.9} \\ \hline predicate\_debugger.pl & 117 & 53 & 0 & 45.3 & 60 & 22 & 0 & 36.7 \\ \hline predicate\_evaluator.pl & 89 & 63 & 0 & 70.8 & 50 & 39 & 0 & 78.0 \\ \hline unsat\_cores.pl & 44 & 19 & 0 & 43.2 & 24 & 13 & 0 & 54.2 \\ \hline \end{longtable} model\_checker \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{359} & \textbf{171} & \textbf{2} & \textbf{47.9} & \textbf{218} & \textbf{124} & \textbf{0} & \textbf{56.9} \\ \hline model\_checker.pl & 44 & 42 & 0 & 95.5 & 19 & 19 & 0 & 100.0 \\ \hline pge\_algo.pl & 62 & 43 & 1 & 70.5 & 41 & 34 & 0 & 82.9 \\ \hline ample\_sets.pl & 84 & 58 & 0 & 69.0 & 64 & 48 & 0 & 75.0 \\ \hline \textcolor[HTML]{FF0000}{b\_simplifier.pl} & \textcolor[HTML]{FF0000}{53} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{20} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline dot\_graphs\_static\_analysis.pl & 9 & 2 & 0 & 22.2 & 9 & 2 & 0 & 22.2 \\ \hline \textcolor[HTML]{FF0000}{enable\_graph.pl} & \textcolor[HTML]{FF0000}{35} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{22} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{enabling\_predicates.pl} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline static\_analysis.pl & 41 & 26 & 1 & 65.0 & 27 & 21 & 0 & 77.8 \\ \hline \end{longtable} other \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1792} & \textbf{685} & \textbf{10} & \textbf{38.4} & \textbf{759} & \textbf{293} & \textbf{1} & \textbf{38.7} \\ \hline brp\_3\_true.pl & 63 & 63 & 0 & 100.0 & 4 & 4 & 0 & 100.0 \\ \hline M0\_AOO\_mch.pl & 31 & 31 & 0 & 100.0 & 4 & 4 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{Farmer\_temp.pl} & \textcolor[HTML]{FF0000}{36} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline LOCKR1\_mch.pl & 14 & 14 & 0 & 100.0 & 4 & 4 & 0 & 100.0 \\ \hline train\_ctx5\_ctx.pl & 3 & 3 & 0 & 100.0 & 3 & 3 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{alloy2b.pl} & \textcolor[HTML]{FF0000}{189} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{81} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline counter.pl & 8 & 8 & 0 & 100.0 & 4 & 4 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{ltsmin\_c\_interface.pl} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ltsmin\_trace.pl} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{12} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{msg\_interop.pl} & \textcolor[HTML]{FF0000}{47} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{21} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline myheap.pl & 33 & 19 & 0 & 57.6 & 14 & 4 & 0 & 28.6 \\ \hline plspec.pl & 126 & 25 & 0 & 19.8 & 60 & 14 & 0 & 23.3 \\ \hline b\_to\_cnf.pl & 22 & 2 & 2 & 10.0 & 6 & 1 & 0 & 16.7 \\ \hline avl\_ugraphs.pl & 6 & 5 & 0 & 83.3 & 6 & 5 & 0 & 83.3 \\ \hline b\_arithmetic\_expressions.pl & 8 & 7 & 0 & 87.5 & 3 & 3 & 0 & 100.0 \\ \hline b\_expression\_sharing.pl & 335 & 263 & 2 & 79.0 & 126 & 106 & 0 & 84.1 \\ \hline chr\_integer\_inequality.pl & 31 & 28 & 0 & 90.3 & 24 & 22 & 0 & 91.7 \\ \hline chr\_set\_membership.pl & 6 & 1 & 0 & 16.7 & 6 & 1 & 0 & 16.7 \\ \hline \textcolor[HTML]{FF0000}{coverage\_tools\_annotations.pl} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} \\ \hline hit\_profiler.pl & 30 & 9 & 0 & 30.0 & 14 & 8 & 0 & 57.1 \\ \hline input\_syntax\_tree.pl & 54 & 41 & 1 & 77.4 & 20 & 17 & 0 & 85.0 \\ \hline \textcolor[HTML]{FF0000}{json.pl} & \textcolor[HTML]{FF0000}{102} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{37} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline performance\_messages.pl & 10 & 7 & 0 & 70.0 & 6 & 4 & 0 & 66.7 \\ \hline prob\_startup.pl & 1 & 1 & 0 & 100.0 & 1 & 1 & 0 & 100.0 \\ \hline runtime\_profiler.pl & 7 & 2 & 0 & 28.6 & 7 & 2 & 0 & 28.6 \\ \hline source\_profiler.pl & 5 & 1 & 0 & 20.0 & 5 & 1 & 0 & 20.0 \\ \hline state\_space\_reduction.pl & 73 & 38 & 0 & 52.1 & 54 & 31 & 0 & 57.4 \\ \hline ce\_replay.pl & 5 & 4 & 0 & 80.0 & 3 & 3 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{logging.pl} & \textcolor[HTML]{FF0000}{34} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{synthesis\_util.pl} & \textcolor[HTML]{FF0000}{278} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{139} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline table\_tools.pl & 84 & 46 & 2 & 56.1 & 36 & 26 & 0 & 72.2 \\ \hline test\_typechecker.pl & 25 & 24 & 0 & 96.0 & 16 & 15 & 0 & 93.8 \\ \hline \textcolor[HTML]{FF0000}{tools\_commands.pl} & \textcolor[HTML]{FF0000}{37} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{17} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline typing\_tools.pl & 60 & 43 & 0 & 71.7 & 13 & 10 & 0 & 76.9 \\ \hline \end{longtable} pltables \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{84} & \textbf{0} & \textbf{0} & \textbf{0.0} & \textbf{60} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables.pl} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export.pl} & \textcolor[HTML]{FF0000}{20} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_csv.pl} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_html.pl} & \textcolor[HTML]{FF0000}{11} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_latex.pl} & \textcolor[HTML]{FF0000}{21} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{11} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_tools.pl} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_xml.pl} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} plugin \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{6} & \textbf{1} & \textbf{0} & \textbf{16.7} & \textbf{6} & \textbf{1} & \textbf{0} & \textbf{16.7} \\ \hline testaddon.pl & 6 & 1 & 0 & 16.7 & 6 & 1 & 0 & 16.7 \\ \hline \end{longtable} plugin\_absint \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{175} & \textbf{7} & \textbf{7} & \textbf{4.2} & \textbf{92} & \textbf{6} & \textbf{0} & \textbf{6.5} \\ \hline absint.pl & 16 & 2 & 0 & 12.5 & 12 & 2 & 0 & 16.7 \\ \hline \textcolor[HTML]{FF0000}{b\_abstract\_interpreter.pl} & \textcolor[HTML]{FF0000}{34} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{b\_abstract\_interpreter\_helpers.pl} & \textcolor[HTML]{FF0000}{32} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{20} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline b\_abstract\_mappings.pl & 19 & 5 & 3 & 31.3 & 12 & 4 & 0 & 33.3 \\ \hline \textcolor[HTML]{FF0000}{interval.pl} & \textcolor[HTML]{FF0000}{74} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{35} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} plugin\_units \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{458} & \textbf{322} & \textbf{14} & \textbf{72.5} & \textbf{132} & \textbf{113} & \textbf{2} & \textbf{86.9} \\ \hline unit\_parser.pl & 22 & 15 & 0 & 68.2 & 7 & 6 & 0 & 85.7 \\ \hline units.pl & 41 & 29 & 7 & 85.3 & 25 & 19 & 2 & 82.6 \\ \hline units\_alias.pl & 18 & 18 & 0 & 100.0 & 3 & 3 & 0 & 100.0 \\ \hline units\_conversions.pl & 6 & 6 & 0 & 100.0 & 2 & 2 & 0 & 100.0 \\ \hline units\_domain.pl & 79 & 68 & 0 & 86.1 & 27 & 25 & 0 & 92.6 \\ \hline units\_interpreter.pl & 159 & 83 & 3 & 53.2 & 17 & 17 & 0 & 100.0 \\ \hline units\_interpreter\_helpers.pl & 68 & 57 & 3 & 87.7 & 30 & 27 & 0 & 90.0 \\ \hline units\_prettyprint.pl & 38 & 20 & 1 & 54.1 & 10 & 4 & 0 & 40.0 \\ \hline units\_tools.pl & 27 & 26 & 0 & 96.3 & 11 & 10 & 0 & 90.9 \\ \hline \end{longtable} plugin\_xtl \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{14} & \textbf{5} & \textbf{0} & \textbf{35.7} & \textbf{12} & \textbf{4} & \textbf{0} & \textbf{33.3} \\ \hline xtl.pl & 13 & 5 & 0 & 38.5 & 11 & 4 & 0 & 36.4 \\ \hline \textcolor[HTML]{FF0000}{xtl\_program.pl} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} promela \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{247} & \textbf{75} & \textbf{0} & \textbf{30.4} & \textbf{87} & \textbf{38} & \textbf{0} & \textbf{43.7} \\ \hline h\_int.pl & 213 & 75 & 0 & 35.2 & 60 & 38 & 0 & 63.3 \\ \hline \textcolor[HTML]{FF0000}{promela\_ncprinter.pl} & \textcolor[HTML]{FF0000}{20} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{promela\_tools.pl} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{11} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} proz \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1354} & \textbf{1176} & \textbf{0} & \textbf{86.9} & \textbf{469} & \textbf{420} & \textbf{0} & \textbf{89.6} \\ \hline kernel\_freetypes.pl & 62 & 45 & 0 & 72.6 & 35 & 27 & 0 & 77.1 \\ \hline kernel\_z.pl & 15 & 14 & 0 & 93.3 & 11 & 11 & 0 & 100.0 \\ \hline consistencycheck.pl & 125 & 110 & 0 & 88.0 & 16 & 14 & 0 & 87.5 \\ \hline dependence.pl & 31 & 22 & 0 & 71.0 & 6 & 6 & 0 & 100.0 \\ \hline fuzzfile.pl & 44 & 44 & 0 & 100.0 & 25 & 25 & 0 & 100.0 \\ \hline proz.pl & 293 & 268 & 0 & 91.5 & 113 & 98 & 0 & 86.7 \\ \hline schemaexpansion.pl & 92 & 77 & 0 & 83.7 & 40 & 37 & 0 & 92.5 \\ \hline schemavars.pl & 23 & 8 & 0 & 34.8 & 6 & 4 & 0 & 66.7 \\ \hline subexpressions.pl & 186 & 171 & 0 & 91.9 & 48 & 47 & 0 & 97.9 \\ \hline z\_tools.pl & 43 & 39 & 0 & 90.7 & 30 & 27 & 0 & 90.0 \\ \hline z\_typechecker.pl & 264 & 218 & 0 & 82.6 & 64 & 53 & 0 & 82.8 \\ \hline zenvironment.pl & 11 & 10 & 0 & 90.9 & 7 & 7 & 0 & 100.0 \\ \hline zparameters.pl & 9 & 1 & 0 & 11.1 & 3 & 1 & 0 & 33.3 \\ \hline ztransformations.pl & 156 & 149 & 0 & 95.5 & 65 & 63 & 0 & 96.9 \\ \hline \end{longtable} repl \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{288} & \textbf{150} & \textbf{0} & \textbf{52.1} & \textbf{132} & \textbf{89} & \textbf{0} & \textbf{67.4} \\ \hline eval\_strings.pl & 288 & 150 & 1 & 52.3 & 132 & 89 & 0 & 67.4 \\ \hline \end{longtable} smt\_solvers \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{433} & \textbf{212} & \textbf{4} & \textbf{49.4} & \textbf{134} & \textbf{98} & \textbf{0} & \textbf{73.1} \\ \hline \textcolor[HTML]{FF0000}{atelierb\_provers\_interface.pl} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline ast\_cleanup\_for\_smt.pl & 91 & 56 & 0 & 61.5 & 25 & 22 & 0 & 88.0 \\ \hline model\_translation.pl & 77 & 47 & 1 & 61.8 & 27 & 19 & 0 & 70.4 \\ \hline prob\_state\_predicates.pl & 16 & 10 & 0 & 62.5 & 4 & 4 & 0 & 100.0 \\ \hline seq\_rewriter.pl & 35 & 12 & 0 & 34.3 & 12 & 10 & 0 & 83.3 \\ \hline smt\_common\_predicates.pl & 1 & 1 & 0 & 100.0 & 1 & 1 & 0 & 100.0 \\ \hline smt\_solvers\_interface.pl & 191 & 83 & 3 & 44.1 & 49 & 39 & 0 & 79.6 \\ \hline solver\_dispatcher.pl & 6 & 3 & 0 & 50.0 & 3 & 3 & 0 & 100.0 \\ \hline \end{longtable} smtlib \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{271} & \textbf{171} & \textbf{0} & \textbf{63.1} & \textbf{91} & \textbf{58} & \textbf{0} & \textbf{63.7} \\ \hline smtlib2\_cli.pl & 6 & 4 & 0 & 66.7 & 4 & 3 & 0 & 75.0 \\ \hline smtlib2\_environment.pl & 17 & 9 & 0 & 52.9 & 14 & 8 & 0 & 57.1 \\ \hline smtlib2\_interpreter.pl & 42 & 17 & 0 & 40.5 & 10 & 6 & 0 & 60.0 \\ \hline smtlib2\_parser.pl & 98 & 83 & 0 & 84.7 & 38 & 32 & 0 & 84.2 \\ \hline smtlib2\_translation.pl & 108 & 58 & 0 & 53.7 & 25 & 9 & 0 & 36.0 \\ \hline \end{longtable} symbolic\_model\_checker \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{275} & \textbf{145} & \textbf{1} & \textbf{52.9} & \textbf{171} & \textbf{102} & \textbf{0} & \textbf{59.6} \\ \hline bmc.pl & 23 & 17 & 0 & 73.9 & 14 & 11 & 0 & 78.6 \\ \hline \textcolor[HTML]{FF0000}{cbc\_ba.pl} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ctigar.pl} & \textcolor[HTML]{FF0000}{49} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{32} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline ic3.pl & 52 & 38 & 1 & 74.5 & 34 & 27 & 0 & 79.4 \\ \hline kinduction.pl & 32 & 21 & 0 & 65.6 & 19 & 13 & 0 & 68.4 \\ \hline mic\_generation.pl & 20 & 5 & 0 & 25.0 & 10 & 3 & 0 & 30.0 \\ \hline \textcolor[HTML]{FF0000}{predicate\_abstraction.pl} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline predicate\_handling.pl & 47 & 43 & 0 & 91.5 & 31 & 31 & 0 & 100.0 \\ \hline solver\_handling.pl & 26 & 19 & 0 & 73.1 & 17 & 15 & 0 & 88.2 \\ \hline unsat\_core\_generalization.pl & 3 & 2 & 0 & 66.7 & 2 & 2 & 0 & 100.0 \\ \hline \end{longtable} symmetry \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{291} & \textbf{210} & \textbf{1} & \textbf{72.4} & \textbf{121} & \textbf{99} & \textbf{0} & \textbf{81.8} \\ \hline graphiso.pl & 11 & 11 & 0 & 100.0 & 5 & 5 & 0 & 100.0 \\ \hline graph\_canon.pl & 94 & 67 & 0 & 71.3 & 43 & 36 & 0 & 83.7 \\ \hline graph\_iso\_nauty.pl & 62 & 39 & 0 & 62.9 & 32 & 21 & 0 & 65.6 \\ \hline state\_permuter.pl & 32 & 21 & 0 & 65.6 & 10 & 9 & 0 & 90.0 \\ \hline symmetry\_marker.pl & 92 & 72 & 1 & 79.1 & 31 & 28 & 0 & 90.3 \\ \hline \end{longtable} synthesis \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{534} & \textbf{0} & \textbf{0} & \textbf{0.0} & \textbf{213} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{b\_synthesis.pl} & \textcolor[HTML]{FF0000}{113} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{56} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{constraints.pl} & \textcolor[HTML]{FF0000}{225} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{95} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{library\_setup.pl} & \textcolor[HTML]{FF0000}{130} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{location\_vars\_to\_program.pl} & \textcolor[HTML]{FF0000}{25} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{symmetry\_reduction.pl} & \textcolor[HTML]{FF0000}{41} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{23} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} tcltk \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{42} & \textbf{0} & \textbf{0} & \textbf{0.0} & \textbf{18} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{prologTasks.pl} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{tcltk\_tree\_inspector.pl} & \textcolor[HTML]{FF0000}{27} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{11} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} test\_generation \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{379} & \textbf{234} & \textbf{3} & \textbf{62.2} & \textbf{240} & \textbf{168} & \textbf{0} & \textbf{70.0} \\ \hline \textcolor[HTML]{FF0000}{mcdc\_coverage.pl} & \textcolor[HTML]{FF0000}{59} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{22} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline sap.pl & 320 & 234 & 3 & 73.8 & 218 & 168 & 0 & 77.1 \\ \hline \end{longtable} testing \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{492} & \textbf{152} & \textbf{0} & \textbf{30.9} & \textbf{197} & \textbf{81} & \textbf{0} & \textbf{41.1} \\ \hline b\_trace\_checking.pl & 125 & 92 & 1 & 74.2 & 57 & 44 & 0 & 77.2 \\ \hline test\_runner.pl & 252 & 42 & 0 & 16.7 & 114 & 32 & 0 & 28.1 \\ \hline typechecker.pl & 115 & 18 & 0 & 15.7 & 26 & 5 & 0 & 19.2 \\ \hline \end{longtable} tools \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1825} & \textbf{954} & \textbf{6} & \textbf{52.4} & \textbf{528} & \textbf{341} & \textbf{0} & \textbf{64.6} \\ \hline \textcolor[HTML]{FF0000}{fdr\_csp\_generator.pl} & \textcolor[HTML]{FF0000}{72} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{39} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline gensym.pl & 10 & 8 & 0 & 80.0 & 8 & 6 & 0 & 75.0 \\ \hline pref\_definitions.pl & 25 & 16 & 0 & 64.0 & 11 & 8 & 0 & 72.7 \\ \hline static\_ordering.pl & 15 & 14 & 0 & 93.3 & 8 & 7 & 0 & 87.5 \\ \hline system\_call.pl & 14 & 10 & 1 & 76.9 & 13 & 10 & 0 & 76.9 \\ \hline translate.pl & 1551 & 904 & 5 & 58.5 & 442 & 308 & 0 & 69.7 \\ \hline \textcolor[HTML]{FF0000}{translate\_keywords.pl} & \textcolor[HTML]{FF0000}{138} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1.4} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{28.6} \\ \hline \end{longtable} typechecker \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{3507} & \textbf{2971} & \textbf{33} & \textbf{85.5} & \textbf{1556} & \textbf{1452} & \textbf{0} & \textbf{93.3} \\ \hline b\_ast\_cleanup.pl & 674 & 598 & 2 & 89.0 & 226 & 221 & 0 & 97.8 \\ \hline b\_read\_write\_info.pl & 138 & 104 & 2 & 76.5 & 68 & 64 & 0 & 94.1 \\ \hline bmachine\_construction.pl & 455 & 416 & 7 & 92.9 & 285 & 276 & 0 & 96.8 \\ \hline bmachine\_eventb.pl & 451 & 382 & 3 & 85.3 & 269 & 264 & 0 & 98.1 \\ \hline bmachine\_static\_checks.pl & 43 & 37 & 0 & 86.0 & 25 & 25 & 0 & 100.0 \\ \hline bmachine\_structure.pl & 23 & 23 & 0 & 100.0 & 17 & 17 & 0 & 100.0 \\ \hline bsyntaxtree.pl & 756 & 623 & 9 & 83.4 & 259 & 223 & 0 & 86.1 \\ \hline btypechecker.pl & 616 & 537 & 2 & 87.5 & 208 & 189 & 0 & 90.9 \\ \hline parsercall.pl & 164 & 96 & 9 & 61.9 & 94 & 72 & 0 & 76.6 \\ \hline partition\_detection.pl & 26 & 25 & 0 & 96.2 & 17 & 17 & 0 & 100.0 \\ \hline pragmas.pl & 11 & 3 & 0 & 27.3 & 5 & 3 & 0 & 60.0 \\ \hline record\_detection.pl & 96 & 92 & 1 & 96.8 & 68 & 68 & 0 & 100.0 \\ \hline b\_ast\_cleanup\_rewrite\_rules.pl & 27 & 16 & 0 & 59.3 & 13 & 12 & 0 & 92.3 \\ \hline rewrite\_rules\_db.pl & 27 & 19 & 0 & 70.4 & 2 & 1 & 0 & 50.0 \\ \hline \end{longtable} visualization \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{461} & \textbf{133} & \textbf{1} & \textbf{28.9} & \textbf{160} & \textbf{51} & \textbf{0} & \textbf{31.9} \\ \hline \textcolor[HTML]{FF0000}{ast\_inspector.pl} & \textcolor[HTML]{FF0000}{24} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline latex\_processor.pl & 111 & 86 & 0 & 77.5 & 49 & 39 & 0 & 79.6 \\ \hline meta\_interface.pl & 188 & 47 & 1 & 25.1 & 24 & 12 & 0 & 50.0 \\ \hline \textcolor[HTML]{FF0000}{state\_viewer\_images.pl} & \textcolor[HTML]{FF0000}{138} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{80} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} \end{document}