From timm@cse.unsw.edu.au Tue Jul 30 10:44:11 1996 Date: Mon, 29 Jul 1996 11:33:23 +1000 (EST) From: Tim Menzies To: Vasilios Tourloupis Subject: Re: Chapter with optimisations Vasilios Tourloupis writes: > > Tim, > > What follows is my (revised) chapter on optimisations. Could you > please spend at least five minutes skimming over it, to see if I have > everything I need, in it. > > Thanks in advance, > > Bill Tourloupis > +-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-+ > | Vasilios E. Tourloupis | vasilios@insect.sd.monash.edu.au | > | Dept. of Software Development | vasilios@hestia.sd.monash.edu.au | > | Monash University, | /\ | > | Caulfield East, Vic., 3145 |___________/\ / \_______________| > | Australia | \/ | > +-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-+ > | Disclaimer: There are some that call me Bill! | > +-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-+ search for all my \btion references \newcommand{\btion}[1]{(\S\ref{#1})} > \chapter{Optimisations} > The previous chapter we demonstrated that developing and implementing HT4 > on a faster platform has significantly improved its performance, while > developing it in C/C++ had not significantly affected its performance, > over the Prolog version. In this chapter we look at different ways of > optimising HT4, for efficiency, and argue that we have increased the > limits to testing, by increasing the efficiency of the HT4 algorithm. > > This chapter is divided into four sections. The first section discusses > code optimisations and results achieved by using the GNU C++ profiler, \textbf{gprof}, to optimise the source code~\btion{sec:opt}. The second section discusses > algorithmic optimisations and results achieved by applying ``clever'' > optimisations~\btion{sec:clev}. The third section discusses a change to the specifications, > which significantly increased the efficiency of the algorithm!\btion{sec:specs}. The final > section discusses the results obtained. > > Note that the results of each program optimisation were generated on both > a Sparc workstation and an Intel Pentium processor running at 133MHz. Some > results were not producable on the Pentium, due to a lack of virual memory. > In such cases, only the results produced on the Sparc workstation are shown. > One may argue that we are comparing apples with oranges, by supplying both > results. Our argument is that, except for the total execution time, the > results produced on both platforms are similar\footnote{In fact, the Intel need a reference here to a table of figures shoing this > Pentium processor, running at 133MHz, produced better runtimes than the Sparc > workstation, by a factor of 2}. Furthermore, the percentage explicable, and > measurements such as the number of assumptions, the number of controversial > assumptions, the percentage of reachable vertices, etc., remain constant, > whichever platform HT4 is executed on. > > > \section{Program Optimizations} > \subsection{Code Optimization} change this to : had some intiail problems due to lack of a memroy management routine in c++. jad to labourously tack down a memory hole, after which... > The initial version of the HT4 program terminated with a segmentation fault, > due to a lack of virtual memory. Even worse was the fact that it had taken > well over 3 hours to execute about 89 percent of the Smythe 89 model. As we > will discuss later~\btion{sec:XXX}, the lack of virtual memory was due to a memory leak. As > for the execution time, the GNU C++ profiler revealed that this was mainly > caused by a function call to the C++ template function pow(), of the bitstring > class. Since we were taking powers of 2, we were able to replace the pow() > function with the left shift operator, so that pow(2,5) would be equivalent > to 1 shifted 5 bits to the left. Table ~\ref{TABLE1} shows that after using > the GNU C++ profiler to optimise HT4, we were able to reduce the total run > time of the program to 773 seconds. Bug fixes and minor modifications, > however, increased the total run time to 811 seconds. This is still a > significant increase in efficiency, compared to the initial version. > Level 3 compiler optimisation reduced the total runtime of this version > even further to about 568 seconds. > > The next significant increase in efficiency occurred by replacing template > lists with intrusive lists \cite{STROUSTRUP95}. Intrusive lists are lists > that contain pointers to specific types. Table ~\ref{TABLE1} shows that > by replacing template lists with intrusive lists, we were able to reduce > the total run time to 362 seconds. need a summary table at the end intially time0 = 100% after X time1 = blah blah percent of time 0 .. final timeN = blah blah % > \subsection{Memory Usage} \subsection{Memory Usage}\label{sec:mem} > As mentioned above~\btion{sec:XXX}, the initial implementation of the HT4 algorithm, failed > to terminate due to a lack of virtual memory. Later experiments revealed that > the program required about 112 megabytes of virtual memory for the program to > produce any useful results and terminate. This was primarily caused by > recursive functions failing to de-allocate redundant structures in memory, > after having completed their task. Table ~\ref{TABLE1} shows that after > initial memory optimisations, we were able to reduce the memory usage to > 31 megabytes. > > This memory optimisation also reduced the execution time by 10 seconds. > Although not significant, it led us to believe that less virtual memory > (swap disk space) the program used, the more efficient it could run. > Further memory and code optimisations, brought the memory usage down > to 25 megabytes, however, it did not significantly reduce the execution > time, as table ~\ref{TABLE2} illustrates. The fact that the program > was still using 25 megabytes of swap disk space, suggested that there > still existed a memory leak. > > > \section{Algorithmic Optimisations} > \subsection{Transitive Closure} > The transitive closure study was motivated by the fact that more time was being > spent in the forward sweep of proof generation. The idea behind this study was > to reduce the forward sweep by caching the transitive closure of all vertices > in the dependency graph, into an adjacency matrix, prior to abductive inference. > The adjacency matrix could then be used in the forward sweep, to mark vertices > as relevant, in linear time. > > \subsubsection{Description of Transitive Closure} > In this section we first provide an example using the transitive closure > implementation, and then give a description of the changes made to the pseudo > code discussed in chapter ~\ref{PSEUDO}. > > As an example to the transitive closure implementation, consider the theory > graph in figure ~\ref{4strin1a}, which expands to the dependency graph in > figure ~\ref{4strin1b}. Also assume that we are given the following behaviour: > > $ > IN = \{aa=arrived, ff=arrived\} > > OUT = \{bb=steady, dd=steady\} > > FACTS = \{aa=arrived, ff=arrived, bb=steady, dd=steady\} > > MAYBES = \{aa=arrived, aa=left, aa=present, aa=absent, > ff=arrived, ff=left, ff=present, ff=absent, > bb=up, bb=steady, bb=down, cc=up, cc=steady, cc=down, > dd=up, dd=steady, dd=down\} > > MISSABLES = \{bb=steady, cc=steady, dd=steady\} > $ > > Normally, executing HT4 over this dependency graph, will result in the following > proof being generated, in the backward sweep: > > $ > P_1 = \{aa=arrived, ff=arrived, cc=up, and8=true, dd=steady\} > $ > > Notice that $bb=steady$ cannot be explained, since it does not have any > competing upstream influences to cause $bb$ to become $steady$. This is > because the sibling vertices of $dd=steady$ (i.e. $dd=up$ and $dd=down$) > have been marked as impossible, in the \verb+setup+ procedure, thus > preventing an explanation from $dd$ to $bb$. > > Also notice that $bb=steady$ cannot be explained via isolation. This is > because its sibling vertex $bb=up$ can be explained using $aa=up$. Furthermore, > notice that there are no controversial assumptions in the generated proof. > This would cause the proof to be stored into a single world that contains > no environment, by the \verb+sort_into_worlds+ function. > > i.e. > $W_1 = \{P_1\}$ contains proofs consistent with the empty environment, > $ENV_1 = \O$. > > Executing the transitive closure implementation over this dependency graph, > however, will cause $bb=steady$ to be explained. This is because the transitive > closure implementation is not \textit{and} node aware. As a result, the > following proofs are generated: > > $ > P_1 = \{aa=arrived, cc=up, and10=true, bb=steady\} > > P_2 = \{aa=arrived, ff=arrived, cc=up, and8=true, dd=steady\} > $ > > Since there are no controversial assumptions, both proofs are stored into the > same world, containing no environment. > > i.e. > $W_1 = \{P_1, P_2\} contains proofs consistent with the empty environment, > $ENV_1 = \O$. > %HERE > > Notice that there should be two upstream influences causing $bb$ to become > $steady$. Here, we only have one upstream influence, namely $cc=up$, causing > $bb$ to become $steady$. Thus, we are trading-off the critiquing ability of > HT4, for a reduction of the relative time spent in the forward sweep. Also > notice that we are increasing the number of reachable vertices in the forward > sweep. As we will see, below, this increase causes an increase in the relative > time spent in the backward sweep, thus (potentially) causing the HT4 algorithm to slow down, -----------------------------------------^^^^^^^^^^^^ > considerably. somewhere where here there should be some statement that the current forward sweep is "and" aware" while the transistive closure is not; i.e. transistve closure treats evertyhign like an or, thus sweeping out a larger space > The transitive closure is calculated by observing that ``if there's a way > to get from node \textit{x} to node \textit{y}, and a way to get from node > \textit{y} to node \textit{j}, then there is a way to get from node \textit{x} > to node \textit{j}''. The trick is to make this observation a little stronger > so that the computation can be done in one pass, through an adjacency matrix. > In particular ``if there's a way to get from node \textit{x} to node \textit{y} > using only nodes with indices less than \textit{y} and a way to get from node > \textit{y} to node \textit{j}, then there's a way to get from node \textit{x} > to node \textit{j} using only nodes with indices less than \textit{y + 1}'' > ~\cite{SEDGEWICK88}. > > Thus, calculating the transitive closure of all vertices involves initially > traversing through the list of vertices in the dependency graph, storing the > child vertices of each vertex in a two dimensional adjacency matrix. Once > this is done, the following algorithm can be applied, which computes the > transitive closure of all vertices in the dependency graph, in cubic time. > > \begin{verbatim} > for y = 1 to V do begin > for x = 1 to V do begin > if closure[x,y] then begin > for j = 1 to V do begin > if closure[y,j] then closure[x,j] = true; > end; > end; > end; > end; > \end{verbatim} > > Having cached the transitive closure of all vertices in the dependency graph, > into an adjacency matrix, we can use this to mark vertices as relevant, in the > forward sweep. Thus, we must modify the procedure \verb+mark_relevant_vertices+, > to cater for the adjacency matrix. > > \begin{verbatim} > procedure mark_relevant_verticies (closure:transitive_closure) > var l:literal; i:integer; > begin > for l in Example.inputs do begin > for i = 1 to V do begin > if closure[l.v.id, i] and not V[i].impossible then > V[i].relevant = true; > end; > end; > end; > \end{verbatim} > > Notice that the transitive closure implementation has eliminated all recursive > calls in the forward sweep. Furthermore, vertices are marked as relevant, in > linear time. Notice, however, that the transitive closure implementation does > not take \textit{and} vertices into consideration, therefore increasing the > number of reachable vertices. > > > \subsubsection{Results of Transitive Closure} > Table ~\ref{TABLE2} illustrates that although the transitive closure > implementation has reduced the forward sweep, it has increased the backward > sweep, considerably. Tests have confirmed that the increase in the backward > sweep is due to the increase of reachable vertices, in the forward sweep. > Where other versions of HT4 were culling 21\% of the search space in the > forward sweep, on average, this version was culling 61\% of the search space > in the forward sweep, on average, thereby slowing down proof generation, > considerably, in the backward sweep (see table ~\ref{TABLE2}). Consequently, > this has increased the total runtime of the program, considerably. > > Also notice that the transitive closure implementation has lost some of its > ability to critique! In particular, the explicable percentage has increased > to about 45\%. This, too, is a result of the increased percentage of reachable > vertices in the forward sweep. An increase in the number of reachable vertices, > has meant an increase in the number of assumptions and controversial assumptions, > in the dependency graph, and, therefore, an increase in the likelihood of more > output vertices being reached. > > Furthermore, notice that this version is also using a lot more virtual memory > than the normal C/C++ version. This is due to memory leaks, and is directly > related to the increase in the relative time spent in the backward sweep. For > this, and other reasons, we suspect that most of the memory leaks occur in the > backward sweep of the program. > > > \subsection{Single World Assumption} > The single world assumption study was motivated by the fact that most of > the proofs being generated were consistent with each other, thus resulting ---------------------------- in the symthe '89 model > in single worlds being generated. The idea behind the single world > assumption implementation was to eliminate the sorting of proofs into an, > otherwise, single world by forcing the generation of consistent proofs. > This was done by isolating the controversial assumptions, and environment > of vertices which have lead to successful proof generation. That way, > only proofs which use the same controversial assumptions, and environment, > can be generated. > > \subsubsection{Description of Single World Assumption} > In this section we first provide an example using the single world assumption > implementation, and then give a description of the changes made to the pseudo > code discussed in chapter ~\ref{PSEUDO}. > > As an example to the single world assumption implementation, consider the > theory in figure ~\ref{8twoxa}, which expands to the dependency graph in > figure ~\ref{8twoxb}. Also assume that we are given the following behaviour: > > $ > IN = \{aa=arrived, bb=arrived\} > > OUT = \{ee=up, ff=down, gg=up, hh=up, ii=down\} > > FACTS = \{aa=arrived, bb=arrived, ee=up, ff=down, gg=up, hh=up, ii=down\} > > MAYBES = \{aa=arrived, aa=left, aa=present, aa=absent, > bb=arrived, bb=left, bb=present, bb=absent, > cc=up, cc=steady, cc=down, dd=up, dd=steady, dd=down, > ee=up, ee=steady, ee=down, ff=up, ff=steady, ff=down, > gg=up, gg=steady, gg=down, hh=up, hh=steady, hh=down, > ii=up, ii=steady, ii=down\} > > MISSABLES = \{cc=steady, dd=steady, ee=steady, > ff=steady, gg=steady, hh=steady, ii=steady\} > $ > > Normally, executing HT4 over this dependency graph, will result in the following > proofs being generated, in the backward sweep: > > $ > P_1 = \{aa=arrived, cc=up, ee=up\} > > P_2 = \{bb=arrived, cc=down, ff=down\} > > P_3 = \{aa=arrived, cc=up, dd=up, gg=up\} > > P_4 = \{aa=arrived, cc=up, dd=up, hh=up\} > > P_5 = \{bb=arrived, cc=down, dd=down, ii=down\} > $ > > Notice that $cc=up$ and $cc=down$ are the base controversial assumptions of > the proofs being generated. Furthermore, they define the environements which > will consequently force the proofs to be sorted into two seperate worlds; > the first world will contain all proofs consistent with the environment > $cc=up$ while the second world will contain all proofs consistent with the > environment $cc=down$. > > i.e. > $W_1 = \{P_1, P_3, P_4\}$ contains all proofs consistent with the environment > $ENV_1 = \{cc=up\}$. > > $W_2 = \{P_2, P_5\}$ contains all proofs consistent with the environment > $ENV_2 = \{cc=down\}$. > > Executing the single world assumption implementation over this dependency > graph, on the other hand, will force consistent proofs to be generated, in > the backward sweep, depending on which output is selected first. Selecting > $ee=up$ will result in proofs consistent with the environment $cc=up$ to be > generated, while selecting $ff=down$ will result in proofs consistent with > the environment $cc=down$ to be generated (i.e. selecting $ee=up$ will result > in proofs $P_1$, $P_3$, and $P_4$, above, to be generated, while selecting > $ff=down$ will result in proofs $P_2$ and $P_5$ to be generated). Once these > proofs are generated, they are stored into one world, without checking for > consistency. > > Notice that the order of the output vertices affect what proofs are being > generated, and what proofs aren't. This was achieved by marking the sibling > vertices, of controversial vertices, visited in the backward sweep, as > impossible, in the sub-procedure which adds vertices to proofs. This > would prevent the (controversial) sibling vertices from being used in proof > generation, and therefore result in consistent proofs being generated. > > \begin{verbatim} > function prove(v: posint; delta_cost: integer; p: proof) : nproofs > var out: nproofs; > procedure add_v_to_proof > var v1:posint; siblings:list of posint; > begin > if (V[v].controversial and Options.single_world_assumption) then > begin > siblings = sibling(v); > for v1 in siblings do V[v1].impossible = true; > end; oh dear, this is your "mark as you go" approach which still worries me. what if the proof fails higher up? how do you remove your marked impossibles? > p.forbid = bunion(p.forbid, V[v].contradicts); > p.route = bset!(p.route,v); > p.cost = p.cost + delta_cost > end; > > function looping : boolean return set?(p.route,v); > > function proved : proof > var p1: proof > begin > p1 = copy(p); > p1.inputs = {v}; > return p1; > end; > begin > if not should_not_use(v) and not looping(p,v) then begin > add_v_to_proof(p,v); > if not illegal(p) and not tooExpensive(p.cost) then begin > if V[v].input then out = [proved(p)]; > if V[v].and then out = out + prove_and(v,p); > else out = out + prove_or(v,p); > end > end; > return out; > end; > \end{verbatim} > > Note that we have added another boolean variable to the \textbf{options} > structure, to indicate that a single world assumption has been selected. > Note that if this boolean variable is set to true, we must not have the > \verb+dodgeControversial+ set to true, since doing so would cause no > controversial vertices to be selected for proof generation, in the > \verb+should_not_use+ function. > > \begin{verbatim} > options = record highCost, enough:posint; > longTime:integer; > dodgeControversial:boolean; > single_world_assumption:boolean; > end; > \end{verbatim} > > The reader may note that choosing one particular (parent) edge over another, > in the backward sweep, may not lead to an input vertex. Consequently, > controversial sibling vertices which have been marked as impossible, in > the backward sweep will prevent other (valid) proofs being generated. > We overcame this problem by cleaning up controversial sibling vertices, > after failing to arrive at an input vertex, in the \verb+prove_or+ > function. phh... this is how... > \begin{verbatim} > function prove_or(v: posint; p:proof): nproofs > var e1: edge; p1: proof; ps, out : nproofs; > successes : integer; fail:boolean; > procedure cleanup_controversial_assumptions(v:posint) > var v1:posint; siblings:list of posint; > begin > siblings = sibling(v); > for v1 in siblings do V[v1].impossible = false; er... not correct. what iv V[v1].impossible was set during the facts sweep? you've just unset it. DON'T rerun the experiments. just fix up the pseudo code and note "subsequent analyis revelaed a small incorrectness in the above algorithm. ... description of the above problems ... a better approach would have been ... better pseduo code... > end; > begin > fail = true; > if V[v].controversial then p.environment = {v}; > for e1 in Upstream(v) do begin > trying({e1},1); > ps = prove(e1.from, e1.cost, p); > if not (size(ps) = 0) and fail = true then fail = false; > successes = successes + size(ps); > success({e1}, size(ps)); > out = out + ps; > if enough(successes) then return out; > end; > if V[v].controversial and fail then > cleanup_controversial_assumptions(v); > return out > end; > \end{verbatim} > > In order to prevent consistent proofs from being sorted into the same > world, we modified the \verb+sort_into_worlds+ function to test for the > \verb+single_world_assumption+ boolean variable being set to true. > > \begin{verbatim} > function sort_into_worlds(ps : nproofs) : nworlds; > var p:proof; w:world; > wda : bitstring; > ws : nworlds; i: integer; > begin > if empty(ps) and not bempty(explainedViaIsolation) then > begin > ws = ws + [one_world(ps)]; > return ws; > end; > > if Options.single_world_assumption then begin > ws = ws + [one_world(ps)]; > return ws; > end; > > if bempty(combine(ps).environment) then > begin > ws = ws + [one_world(ps)]; > return ws; > end; > > i = 0; > for wda in world_defining_assumptions(ps) do > begin > inc(i); > ws[i] = w = new(world); > for p in ps do > begin > if not inconsistent(ps.route, wda) then > add_proof_to_world(w,p); > if tooSlow then return ws; > end; > add_missables_to_world(w); > end; > return ws > end; > \end{verbatim} > > > \subsubsection{Results of Single World Assumption} > Unlike the transitive closure study, this study has revealed a limited > success. Table ~\ref{TABLE2} illustrates that on an Intel Pentium PC, > running at 133 MHz, we have been able to reduce the total run time by > approximately 30 seconds. This is not a significant reduction in > performance, however, what is interesting is that the program produced > a similar explicable result to that of the Smythe 89 study. It would > appear that we can reduce the speed of HT4, without comprimising its > ability to critique! > > This result, and the very nature of the single world assumption implementation > preventing the generation of inconsistent proofs, based on the initial output > vertices selected in the backward sweep, prompted a further study, whereby the > output vertices, were randomized. The idea behind this study was to force > proofs, with different environments, to be generated, and the differences in > results compared. > > > \subsubsection{Results of Randomisation Study} > As mentioned above, the randomisation studies of the single world assumption > implementation, was prompted by the fact that different proofs were being > generated by the selection of different outputs, in the backward sweep. > The idea was to force the generation of proofs, with different environments, > by randomising the output vertices. Furthermore, since the selection of > edges affected the performance of proof generation, in the backward sweep, > the parent edges of vertices, were randomised, in order to observe the > variations in performance. > > Table ~\ref{TABLE3} illustrates that the results produced by the randomisation > study, were very similar to the plain single world assumption implementation > results. In particular, the low standard deviation of explicable data points, > suggests some consistency between the results of different runs. The standard > deviation of the total runtime, on the other hand, could be a result of > executing HT4 on a multi-tasking environment. One way to refute this argument, > is to execute the program on a single-tasking environment. In general, there > seems to be little variation in performance over which edge is selected, in the > backward sweep. > > > \section{Refining the Specifications} > Upon reviewing the pseudo-code, we realized that the function which marks > the controversial assumptions, in the forward sweep, could be implemented > more intuitively. It came as no surprise that we were able to reduce the > runtime, by more than a third of the total execution time. > > \subsection{Description of Refining the Specifications} > Initially, vertices were being marked as controversial if they were relevant, > and their cached set of contradictory (or conflicting) vertices were also > relevant. We were able to refine this requirement by observing that the cached > set of contradictory vertices consisted entirely of sibling vertices. Thus, have you defined sibling vertix anywhere? > vertices could be marked as controversial if they were relevant, and their > sibling vertices were also relevant. > > \begin{verbatim} > procedure mark_controversial_assumptions > var > begin > for v1 in V do begin > if v1.relevant and not bset?(Example.facts, v1.id) then begin > for v2 in siblings(v1) do begin > if v2.relevant then v2.controversial = true > end; > end; > end; > end; > \end{verbatim} > > Note, however, that the above procedure loses generality, in that it cannot > distinguish between non-related conflicting vertices (i.e. vertices which > are not siblings with each other). Since the sets of conflicting vertices > are know prior to program execution, it would be possible to modify the > network parser to test for inconsistency among vertices in the dependency > graph. If each vertex is inconsistent only with its sibling vertices, then > we can use the above procedure. If, however, there exists a vertex which > is inconsistent with another non-related vertex in the dependency graph, > then we should use the original version for marking controversial assumptions. > This would necessarily mean bounding \verb+mark_controversial_assumptions+ > at runtime. > > \subsection{Results of Refining the Specifications} > It came as no surprise that we were able to reduce the total run time of the > algorithm, from 184 seconds to 117 seconds, for the Smythe 89 model, on an > Intel Pentium PC running at 133 MHz (see table ~\ref{TABLE2}). This is just > over a third of the total run time! What came as a surprise was the fact that > this modification had reduced the forward sweep to about 3 percent of the total > execution time. Just as surprising was the simplicity of this modification. > So, where the transitive closure modification failed, this modification > succeeded! > > Further tests confirmed that about 98 percent of the forward sweep was spent > on marking controversial assumptions, in the normal C/C++ implementation, while > this modification was able to reduce this relative time to about 8 percent > (see table ~\ref{TABLE4}). This illustrates that most of the forward sweep > was spent on marking controversial assumptions. We suspect that the overhead > of the set union and set difference operations were the major cause of this > slow down. > > holy shit!!!! > \section{Discussion of Results} > We have demonstrated that optimising the HT4 algorithm for efficiency, has > generally improved its performance, with the exception of the transitive > closure trick. We believe, however, that it is unlikely that algorithmic > optimisations will ever significantly increase the efficiency of HT4. > This is because abductive inference, which HT4 uses to validate models, > is intractible in nature \cite{SELMAN}. And although the above results > do not stress a limit to testing, we believe that we have increased the > limits to testing, by increasing the efficiency of the program. be a little less forward ehre. just becuase bill/timm can't don't it don't mean that some other smart arse might not be able to find some approximate case that is 99% of HT4 which runs FASTER. if (e.g) bohdan reads this, then you could have a picky note here. > The fact that most of the execution time was being spent in the forward sweep, > would explain the limited success of the single world assumption implementation, > which was an attempt to improve the general efficiency of the program by > optimising the backward sweep. This would also explain the greater success > of refining the specifications, which improved the general efficiency of the > algorithm, by optimising the forward sweep. > > The fact that most of the relative execution time was being spent marking > controversial assumptions in the forward sweep, would explain the limited > success of reducing the relative time spent in the forward sweep, of the > transitive closure implementation. > > Tbe single world assumption implementation is useful for when most of the > proofs being generated are consistent, therefore resulting in single world > generation. In the case of multiple world generation, however, we would > like the best worlds to be returned, rather than leaving world generation > to chance in generating the best world. One way to overcome this problem > would be to modify the single world assumption implementation to initially > apply the normal implementation, testing the number of worlds being generated, > using the first few example behaviours. If one world has been generated for > each of the example behaviours, the program should be able to apply the single > world assumption implementation. On the other hand, if more than one world > is generated for any example behaviour, then the normal implementation should > continue to be applied. > > -- Dr. Tim Menzies rm EE339 | timm@cse.unsw.edu.au | "Our friend Dirac, too, has ,-_|\ www.cse.unsw.edu.au/~timm | a religion, and its guiding / \ AI Dept, Com. Sci. & Eng. | principle is 'There is no God \_,-._* Uni.NSW, PO Box 1, Kensington| and Dirac is His prophet.'" v Sydney, NSW, Australia, 2033 | -- Wolfgang Pauli +61-2-385-4034(p)385-5995(f) |