Manual/Description/HolBdd.tex

100 `LCF-style' combinations of HOL theorem proving and BDD-based symbolic
105 {\tt{PrimitiveBddRules}}. Several useful and example  derived rules are in the
130 Coudert, Berthet and Madre simplification to be represented as a primitive
137 due to Ken Friis Larsen and Jakob Lichtenberg, and is described in Section~\ref{muddy}.
138 {\tt HolBddLib} is built on top of \Muddy{} and
144 whose primitive operations are the axioms and inference rules of a
153 and $b$ is a BDD. Such a judgement is valid if under the assumptions
154 $a$, the BDD representing $t$ with respect to $\rho$ is $b$, and we
164 which defines a protected type \termbddty and rules for generating
165 values of this type, and \t{DerivedBddRules} that contains derived
168 reachability and fixed points needed by the derived rules,
169 and two small subsidiary structures \t{Varmap} and \t{PrintBdd}.
174 The Voss system \cite{SegerVoss} has strongly influenced and inspired
177 Quantified boolean formulae can be input and are parsed to BDDs.
182 Joyce and Seger interfaced an early HOL system (HOL88) to Voss and in
184 combination of theorem proving deduction and symbolic trajectory
186 deduction with BDD computations.  BDD tools are programmed in FL and
189 the HOL88 and Voss term representations.
191 In later work Lee, Seger and Greenstreet \cite{LeeGreenstreetSeger}
197 idea, called VossProver, was developed by Carl Seger and his student
203 impressive integer and floating-point examples (see the DAC98
204 paper by Aagaard, Jones and Seger \cite{aagaard-dac-98} for further
205 discussion and references).
207 After Seger and Aagaard moved to Intel, the development of the Voss and
211 used both as a specification language and as an LCF-style
213 and proof is obtained via a tactic {\tt{Eval\_tac}} that converts the
216 smaller subgoals that are tractable for model checking, and to
219 The combination of \HOL{} and \Buddy{} in Version~1 of
221 to Voss's FL (though with eager rather than lazy evaluation and no
224 $\exists$ and the \HOL{} term parser plus \ml{termToBdd} provides a
232 Joyce and Seger \cite{JoyceSeger} and it appears that the Forte system
237 providing a clean and simple API allowing implementers to create their
238 own `fully-expansive' combinations of model checking and theorem
246 \Muddy{} is the Moscow ML interface to \Buddy{}. It provides ML functions for constructing and
252 \t{bdd} representing BDDs and associated operations derived from \Buddy{};
262 The current \HolBuddy{} system only uses \t{bdd} and so
263 the documentation of \t{fdd} and \t{bvec} provided here is minimal
264 (see Sections~\ref{fdd} and \ref{bvec} below).
266 \subsection{Initialisation, termination and tuning sessions}\label{init}\index{HolBddLib!session!initialisation}\index{HolBddLib!session!termination}
276 nodetable and a cachesize of $n$.
278 initialises the nodetable to 1000000 and cachesize to
298 Too few nodes will only result in reduced performance and this
315 frees all memory used by \Buddy{} and resets the
318 The functions \t{init} and \t{done} should only be called once per session.
327 \Buddy{} is running (i.e.~\t{init} has been called and \t{done} has not been called). It is
330 The functions \t{init} and \t{done} should only be called once in a session.
365 The management of the node table and internal caches can be tuned
381 \subsection{BDDs representing {\t{true}} and {\t{false}}}\index{HolBddLib!BDD!constants}
384 identifiers \t{TRUE} and \t{FALSE}, both of type \t{bdd}.
386 Functions for mapping from ML Booleans to BDDs and vice versa are, respectively
393 The function \t{toBool} returns \t{true} on TRUE and \t{false} on FALSE.
400 tests the equality of two BDDs. Thus \t{TRUE} is \t{equal} to \t{fromBool(true)} and
405 In \Buddy{}, BDD variables are encoded as integers (type \t{int} in ML) and the BDD variable ordering
437 corresponding to the integer and
453 \subsection{Sets of variables and quantification}\label{varSet}\index{HolBddLib!BDD!quantification}
457 sets with, respectively, a constructor and two destructors:
466 set and the destructor \t{fromSet} returns a BDD representing the
476 \subsection{Assignments, composition, replacement and restriction}\label{replace}\index{HolBddLib!BDD!assignments}\index{HolBddLib!BDD!composition}\index{HolBddLib!BDD!replacement}\index{HolBddLib!BDD!restriction}
480 provides and three optimised special cases: substituting for a single
481 variable (\t{compose}), renaming variables (\t{replace}) and
521 (which has a constructor \t{assignment} and destructor \t{getAssignment}).
563 The functions \t{satone} and \t{findSat} do not necessarily find the
582 result of performing a Boolean operation and then quantifying the
591 Boolean operation and \t{appex} existentially quantifies it.
593 \Muddy{} provides ten operations of type \t{bddop} and for each of
616 \Muddy{} also provides a unary negation operator and ternary conditional operator.
623 $\t{NOT}~b$ is the BDD corresponding to  `$\neg b$' and $\t{ITE}~b~b_1~b_2$ is the BDD corresponding
629 \subsection{Inspecting and counting nodes and states}\index{HolBddLib!BDD!nodes}\index{HolBddLib!BDD!states}
631 The integer labelling a BDD node and the BDDs corresponding to the high
632 (i.e.~{\t{true}}) and low (i.e.~{\t{false}}) nodes are obtained,
643 $\t{high}~b$ will return the BDD of $t_1$ and $\t{low}~b$ will return
646 Note that \t{var}, \t{high} and \t{low} raise an exception if applied
660 ({\t{false}}) node in the vector and $h$ points to the high
662 they represent {\t{true}} and {\t{false}}, respectively, and arbitrarily have
681 and so is space-efficient.
744 the relationship between $b_1$, $b_2$ and $b_2'$ is that
746 (or, equivalently, that \t{AND($b_1$,$b_2$)} and \t{AND($b_1$,$b_2'$)}
751 the algorithm underlying \t{simplify} is described and attributed to a paper by
752 Coudert, Berthet and Madre \cite{CoudertBerthetMadre}.
754 \subsection{Saving, hashing and printing BDDs}\label{printing}\index{HolBddLib!BDD!saving}\index{HolBddLib!BDD!hashing}\index{HolBddLib!BDD!printing}
766 the root node to the {\it{true}} node and (ii) to the format used by
787 \t{printset} and \t{printdot} print to standard output, whilst
788 \t{fnprintset} and \t{fnprintdot} print to a file with the supplied
791 \t{printset} and \t{fnprintset} print out a sequence of paths, each one having the form
800 \t{1} and indicate that the next node in the path is reached by
838 types and functions provided in ML via \Muddy{} are in the structure \t{bdd} and are
878 $v_0=0$, $v_1=0$, $v_2=1$ and $v_3=1$.
945 \subsection{Storage allocation and garbage collection}\index{HolBddLib!BDD!garbage collection}
949 \Buddy{} API and takes care of translating C values into SML values and
958 \verb+bdd_addref+) and wraps it into a finalized value.
961 first component is the \emph{destructor} (a function pointer) and the
965 \verb+bdd_delref+ and the data is the node-index returned by \Buddy{}.
975 $pregc$ when a BuDDy GC is initiated and print $postgc$ when the
997 and also for finding shortest paths to states  satisfying a given property;
999 \item \t{MachineTransitionTheory} contains HOL reachability and fixedpoint theorems needed
1016 loades these five modules and
1018 and cachesize of 10000.
1021 values, then instead of loading \t{HolBddLib}, load \t{bdd} and then
1036 Strings are the names of HOL boolean variables and the integers associated with them
1039 The following operations and predicates on varmaps are provided:
1103 is created, and the BDD is labelled with the string $label$.
1110 is created, and the BDD is labelled by default with a representation
1156 and \t{getBdd} for values of type \termbddty are described in Section~\ref{misc}
1184 The notation $a_1 \cup a_2$ denotes the union of $a_1$ and $a_2$
1191 $\setass{t_1, \ldots ,t_n}$  and
1196 \subsection{Extending and contracting the varmap}
1289 \subsection{Variables and constants}
1460 corresponding to the \Buddy{} BDD operation $bddop$ to terms $t_1$ and $t_2$
1621 \subsection{Composition, repacement and restriction}
1736 and $\hat{\t{T}}$ denotes the ML value \t{true} and
1884 Such theorems, and any theorems deduced from them, are tagged with
1885 \t{HolBdd} and so can be easily identified.
1994 corresponding to $bddop$ to $t_1$ and $t_2$.
2046 \hbc{BddEqualTest : \termbddty -> \termbddty -> bool}{Test equality of BDD component of two term\_bdds and return true or false}
2072 \hbc{GenTermToTermBdd : (term -> \termbddty) -> varmap -> term -> \termbddty}{Scan a term and construct a term\_bdd using the primitive operations when applicable, and a supplied function on leaves when all else fails.}
2148 where t1 can be instantiated to t1' and t2' is the corresponding instance of t2.}
2158 where boolean variables in t can be renamed to get t' and b' is the corresponding replacement of BDD variables in b.}
2186  $\termbdd{a}{\rho}{v_p}{b_p}$ where $v_p$ is a variable, and the varmaps are distinct
2201 where boolean variables in t can be instantiated to get t' and b' is the corresponding replacement of BDD variables in b.}
2245 \subsection{Fixed points and traces}
2255 and the function reportfn is applied to the iteration level and current
2256 term\_bdd and can be used for tracing.
2259 previous term\_bdd tb and the current one tb'. The initial state