1\documentclass[12pt,fleqn]{article}
2\usepackage{latexsym}
3%\usepackage{amsmath}
4\usepackage{amssymb}
5%\usepackage{amsbsy}
6%\usepackage{amsthm}
7\usepackage{makeidx}
8\usepackage{alltt}
9\usepackage{../LaTeX/layout}
10\usepackage{graphicx}
11\usepackage{url}
12
13% ---------------------------------------------------------------------
14% Input defined macros and commands
15% ---------------------------------------------------------------------
16\input{../LaTeX/commands}
17
18\newcommand{\tsu}[1]{\textsf{\textup{#1}}}
19\newcommand{\semb}[1]{\ensuremath{[\![#1]\!]}}
20\newcommand{\rvset}{\ensuremath{V\!\!AR}}
21\newcommand{\wff}{\ensuremath{w\!f\!\!f}}
22\newcommand{\nnf}{\ensuremath{N\!N\!F\,}}
23\newcommand{\ctl}{\textsf{CTL}\,}
24\newcommand{\hc}{HolCheck}
25\newcommand{\hand}{\texttt{/\char'134}}
26\newcommand{\hor}{\texttt{\char'134/}}
27\newcommand{\hnot}{\texttt{\~{}}}
28\setcounter{sessioncount}{0}
29\makeindex
30\title{HolCheck}
31\date{}
32\begin{document}
33\maketitle
34\index{holCheckLib|(}\index{model checking|see {holCheckLib}}
35This is a brief description of the \hc{}\index{holCheckLib!\hc{}} model checker, version 1.0. It assumes the reader is familiar with symbolic model checking, with \HOL{}, and, ideally, with \texttt{HolBddLib}, the \HOL{} interface to BDDs. It should be read with a working \HOL{} installation at hand.
36
37\subsection{Introduction}\label{sec:intro}
38
39\hc{} is a BDD-based model checker embedded in the \HOL{} theorem prover, interfaced to an external BDD engine for efficiency. It currently has the following features:
40
41\begin{itemize}
42\item All steps of the algorithm are proved in \HOL{}, with BDD operations considered atomic.
43\item Results are returned as \HOL{} theorems.
44\item Model checking for the propositional \(\mu\)-calculus and \ctl is supported.
45\item Counterexamples and witnesses are generated when appropriate.
46\item A fully-automatic counterexample-guided abstraction refinement framework is included.
47\end{itemize}
48
49The user inputs a model and a list of properties to be checked, and the model checker returns theorems, counterexamples and/or witnesses for each property with respect to the model. Models are formally treated as Kripke structures\index{holCheckLib!models!Kripke structure} described by the quintuple \( (S, S_0, T, P, L) \) where
50
51\begin{itemize}
52\item \( S \) is the set of states of the model. Each state is modelled as a tuple of state variables. Currently only boolean state variables are supported.
53\item \( S_0\) is the set of initial states.
54\item \( T \) is the set of actions or program letters, such that for each \( a \in T \), we have \( R_a \subseteq S \times S\). This says that the model has a transition labelled \( a \) from a state \( s \) to a state \( s' \) if and only if \( R_a(s,s') \). Next state variables are distinguished from current state variables by priming.
55\item \( P \) is the set of atomic propositions.
56\item \( L:S\rightarrow 2^P \) labels each state with those propositions that are true in it.
57\end{itemize}
58
59See \S\ref{sec:models} for details. The user is required to supply only \( S_0 \) and \( T \) as the remaining components can be calculated from these. Properties are input as \HOL{} terms of type \(\mathtt{mu}\) or \(\mathtt{ctl}\), \HOL{} datatypes for which have been defined (see \S\ref{sec:prop} for details). A property is satisfied by a model if the set of initial states of the model is a subset of the set of states satisfying the property.
60
61\subsection{Quick Usage Overview}
62
63This section provides a quick look at a typical use of \hc{}. We choose a simple mod-8 counter as our example, which starts at 0 and counts up to 7, and then loops from 0 again. We wish to show that the most significant bit eventually goes high.
64
65First we load the \hc{} library:
66\begin{session}\begin{verbatim}
67- load "holCheckLib"; open holCheckLib;
68  (* we don't show the output from the "open" here *)
69> val it = () : unit
70\end{verbatim}\end{session}
71Now we specify the labelled transition system as a list of
72(string, term) pairs, where each string is a transition label and
73each term represents a transition relation (three booleans
74required to encode numbers 0-7; next-state variable values
75indicated by priming; note we expand the xor, since \hc{}
76currently requires purely propositional terms) :
77\begin{session}\begin{verbatim}
78- val xor_def = Define `xor x y = (x \/ y) /\ ~(x=y)`;
79  val TS = List.map (I ## (rhs o concl o
80           (fn tm => REWRITE_CONV [xor_def] tm handle ex => REFL tm)))
81                [("v0",``(v0'=~v0)``),("v1",``v1' = xor v0 v1``),
82                 ("v2",``v2' = xor (v0 /\ v1) v2``)]
83Definition has been stored under "xor_def".
84> val xor_def = |- !x y. xor x y = (x \/ y) /\ ~(x = y) : thm
85> val TS =
86    [("v0", ``v0' = ~v0``), ("v1", ``v1' = (v0 \/ v1) /\ ~(v0 = v1)``),
87     ("v2", ``v2' = (v0 /\ v1 \/ v2) /\ ~(v0 /\ v1 = v2)``)] :
88  (string * term) list
89\end{verbatim}\end{session}
90Next we specify the initial states (counter starts at 0):
91\begin{session}\begin{verbatim}
92- val S0 = ``~v0 /\ ~v1 /\ ~v2``;
93> val S0 = ``~v0 /\ ~v1 /\ ~v2`` : term
94\end{verbatim}\end{session}
95Now we say whether the transitions happen synchronously (they do):
96\begin{session}\begin{verbatim}
97- val ric = true;
98> val ric = true : bool
99\end{verbatim}\end{session}
100Then we set up the state tuple:\index{holCheckLib!ML bindings!mk\_state@\ml{mk\_state}}
101\begin{session}\begin{verbatim}
102- val state = mk_state S0 TS;
103> val state = ``(v0,v1,v2)`` : term
104\end{verbatim}\end{session}
105Next we specify a property (there exists a future in which the most significant bit, v2, will go high). Note how atomic propositions are represented as functions on the state :
106\begin{session}\begin{verbatim}
107- val ctlf = ("ef_msb_high",``C_EF (C_BOOL
108(B_PROP ^(pairSyntax.mk_pabs(state,``v2:bool``))))``);
109> val ctlf = ("ef_msb_high",``C_EF (C_BOOL(B_PROP(\(v0,v1,v2). v2))``)
110  : string * term
111\end{verbatim}\end{session}
112Now we can create the model. This is done by starting with the supplied \texttt{empty\_model} value and filling it using the \texttt{set\_*} functions:
113\index{holCheckLib!ML bindings!set\_init@\ml{set\_init}}
114\index{holCheckLib!ML bindings!set\_trans@\ml{set\_trans}}
115\index{holCheckLib!ML bindings!set\_flag\_ric@\ml{set\_flag\_ric}}
116\index{holCheckLib!ML bindings!set\_state@\ml{set\_state}}
117\index{holCheckLib!ML bindings!set\_props@\ml{set\_props}}
118\index{holCheckLib!ML bindings!empty\_model@\ml{empty\_model}}\index{holCheckLib!models!empty\_model@\ml{empty\_model}}
119\index{holCheckLib!models!creating}
120\begin{session}\begin{verbatim}
121- val m = ((set_init S0) o (set_trans TS) o (set_flag_ric ric) o
122           (set_state state) o  (set_props [ctlf])) empty_model;
123> val m = <model> : model
124\end{verbatim}\end{session}
125At last we can call the model checker...
126\index{holCheckLib!ML bindings!holCheck@\ml{holCheck}}
127\begin{session}\begin{verbatim}
128- val m2 = holCheck m;
129> val m2 = model : <model>
130\end{verbatim}\end{session}
131...and examine the results:
132\index{holCheckLib!ML bindings!get\_results@\ml{get\_results}}\index{holCheckLib!traces}
133\begin{session}\begin{verbatim}
134- get_results m2;
135> val it =
136  SOME [(<term_bdd>,
137   SOME [............................]
138    |- CTL_MODEL_SAT ctlKS (C_EF (C_BOOL (B_PROP (\(v0,v1,v2). v2)))),
139   SOME [``(~v0,~v1,~v2)``, ``(v0,~v1,~v2)``, ``(~v0,v1,~v2)``,
140                 ``(v0,v1,~v2)``, ``(~v0,~v1,v2)``])] :
141  (term_bdd * thm option * term list option) list option
142\end{verbatim}\end{session}
143The result is a list of triples, one triple per property checked. The first component contains the BDD representation of the set of states satisfying the property. The second component contains a theorem certifying that the property holds in the model i.e. it holds in the initial states. The third contains a witness trace that counts up to 4, at which point v2 goes high.
144
145Note that since we did not supply a name for the model, the system has chosen the default name \texttt{ctlKS}, which stands for ``CTL Kripke structure''. Names can be given via \texttt{set\_name}\index{holCheckLib!ML bindings!set\_name@\ml{set\_name}}\index{holCheckLib!models!naming}. See \S\ref{sec:formal_models} for more on how \hc{} represents formal models.
146
147Note also that the theorem created has several assumptions. This is because \hc{}\, creates proofs lazily. We can verify the proof...\index{holCheckLib!ML bindings!prove\_model@\ml{prove\_model}}
148\begin{session}\begin{verbatim}
149- val m3 = prove_model m2;
150  (* we don't show the prove_model "chatting" messages here *)
151> val m3 = <model> : model\end{verbatim}\end{session}
152...and examine the verified results:
153\begin{session}\begin{verbatim}
154- get_results m3;
155> val it =
156   SOME [(<term_bdd>,
157    SOME|- CTL_MODEL_SAT ctlKS (C_EF(C_BOOL(B_PROP(\(v0,v1,v2). v2)))),
158    SOME [``(~v0,~v1,~v2)``, ``(v0,~v1,~v2)``, ``(~v0,v1,~v2)``,
159                 ``(v0,v1,~v2)``, ``(~v0,~v1,v2)``])] :
160  (term_bdd * thm option * term list option) list option
161\end{verbatim}\end{session}
162The theorem component now has no assumptions. Any assumptions to the term\_bdd would also have been discharged.
163
164\subsection{Detailed Usage}
165
166This section describes the usage of \hc{} in more detail. As a running example we will take the children's game of tic-tac-toe or noughts-and-crosses, usually played on a 3-by-3 grid. For simplicity and to keep the formulas under consideration manageable, we consider the trivial 1-by-1 variant. Thus, the grid starts off empty, the player to go first makes a move and immediately wins, ending the game.
167
168For this model, we need one state variable to track whose move it is, and we shall call this \(m\), which is true if the first player (call her A) is to move and false if the second player (call him B) is to move. We also need two state variables to keep track of the moves already played. The state variable \(u_{0,0}\) is true if A has claimed grid cell \((0,0)\) and false otherwise, and similarly the state variable \(v_{0,0}\) tracks B's moves. It is easy to see how this scheme can be generalised to arbitrary grids.
169
170The state is described by the tuple \( (m,u_{0,0},v_{0,0}) \). \(S_0\) is \( \{ (T,F,F) \} \) and \( T \) is
171
172\begin{eqnarray*}
173 [&(&''{u_{0,0}}'',(\lnot u_{0,0} \land \lnot v_{0,0} \land m) \land \lnot((\lnot m \land u_{0,0}) \lor (m \land v_{0,0}))\\
174       &&\land (u_{0,0}' \land \lnot m' \land (v_{0,0}' = v_{0,0}))),\\
175     &(&''{v_{0,0}}'',(\lnot v_{0,0} \land \lnot u_{0,0} \land \lnot m) \land \lnot((\lnot m \land u_{0,0}) \lor (m \land v_{0,0}))\\
176        &&\land (v_{0,0}' \land m' \land (u_{0,0}' = u_{0,0})))]
177\end{eqnarray*}
178
179This says for instance that the move \(''{u_{0,0}}''\) may be played if and only if the board is empty and it is A's turn AND the game is not already over AND in the next state A will have claimed \((0,0)\) and it will be B's turn, whose status will remained unchanged. And similarly for the move \(''{v_{0,0}}''\).
180
181Note that although there are eight possible states, only two (\((T,F,F)\) and \((F,T,F) \)) are actually reachable.
182
183For our running example, we use \texttt{ttt.sml} from \texttt{src/HolCheck/examples}. Build this (and others\footnote{The AMBA examples are large and take a while to build. To skip them, see the README file in the same folder.}) by typing \texttt{Holmake} in \texttt{src/HolCheck/examples}. Now start \HOL{} from this directory (or use the -I command-line parameter).
184
185The first step after loading \HOL{} is to load \hc{}. \HOL{} messages have been elided.
186
187\setcounter{sessioncount}{0}
188
189\begin{session}\begin{verbatim}
190- app load ["holCheckLib","ttt"];
191> val it = () : unit
192\end{verbatim}\end{session}
193
194The user interacts with \hc{} through a single ML function \texttt{holCheck}\index{holCheckLib!ML bindings!holCheck@\ml{holCheck}}, found in the library \texttt{holCheckLib}.
195
196\begin{session}\begin{verbatim}
197- holCheckLib.holCheck;
198> val holCheck = fn : model -> model
199\end{verbatim}\end{session}
200
201The function takes a \hc{} model as an argument, and returns a model which is the same as the argument, but additionally contains the results of the model checking. We now describe how a \hc{} model is constructed.
202
203\subsubsection{The Input Model}
204
205A \hc{} model is a data structure that contains all the information required for model checking. We use the model construction function provided in the \texttt{ttt} example to create the model.
206
207\begin{session}\begin{verbatim}
208- val ttt1 = ttt.makeTTT 1;
209> val ttt1 = <model> : model
210\end{verbatim}\end{session}
211
212The numeric argument to \(\mathtt{ttt.makeTTT}\) gives the size of grid required.  Now we consider each component of the model \texttt{ttt1}, using the \texttt{holCheckLib.get\_*} family of functions. The corresponding \texttt{holCheckLib.set\_*} functions were used to actually construct the model. The argument to each \texttt{set} function is precisely the return value of the corresponding \texttt{get} function as seen below. The only difference is that the values of optional model components are returned as option types. See the source code of \texttt{mod8.sml} in the HolCheck \texttt{examples} directory for a simple example of how this is done. See \S\ref{sec:models} for general details on model construction.
213
214\begin{session}\begin{verbatim}
215- val S0 = holCheckLib.get_init ttt1;
216> val S0 = ``~u0_0 /\ ~v0_0 /\ m`` : term
217\end{verbatim}\end{session}
218\index{holCheckLib!ML bindings!get\_init@\ml{get\_init}}
219\(\mathtt{S0}\) is a term over the state variables of the model, such that only those assignments to the variables that satisfy the initial states of the model also satisfy \(\mathtt{S0}\). Thus \(\mathtt{S0}\) denotes the initial states. Note that since only boolean variables are supported, \(\mathtt{S0}\) must be a purely propositional term.
220
221\begin{session}\begin{verbatim}
222- val TS = holCheckLib.get_trans ttt1;
223> val TS =
224    [("u0_0",
225      ``~u0_0 /\ ~v0_0 /\ m /\
226        ~(~m /\ (u0_0 \/ u0_0 \/ u0_0 \/ u0_0) \/
227          m /\ (v0_0 \/ v0_0 \/ v0_0 \/ v0_0)) /\ u0_0' /\ ~m' /\
228        (v0_0' = v0_0)``),
229     ("v0_0",
230      ``~v0_0 /\ ~u0_0 /\ ~m /\
231        ~(~m /\ (u0_0 \/ u0_0 \/ u0_0 \/ u0_0) \/
232          m /\ (v0_0 \/ v0_0 \/ v0_0 \/ v0_0)) /\ v0_0' /\ m' /\
233        (u0_0' = u0_0)``)] : (string * term) list
234\end{verbatim}\end{session}
235\index{holCheckLib!ML bindings!get\_trans@\ml{get\_trans}}
236\(\mathtt{TS}\) is a list of pairs of the form \( (a,R_a)\), where the string \(a\) is an action name (or transition label) and the \HOL{} term \(R_a\) is a relation over current and next states such that the model has a transition labelled \(a\) from a state \( s \) to a state \(s'\) if and only if the corresponding valuations of current and next state variables satisfy \( R_a \). In this example, there are two actions, corresponding to the two possible moves ``u0\_0'' and ``v0\_0'', as explained earlier. Of course, in this particular case, the second move is never actually played. We have here edited out the redundancy in \(\mathtt{TS}\), which is an artifact of how \(\mathtt{ttt.makeTTT}\) generates the grid.
237
238Thus \(\mathtt{S0}\) and \(\mathtt{TS}\) are just \HOL{} equivalents of \(S_0\) and \(T\) as described in section \ref{sec:intro}. \( \mathtt{TS} \) is named as such to avoid clashing with the global \HOL{} term constant \( \mathtt{T} \).
239
240\begin{session}\begin{verbatim}
241- val ric = holCheckLib.get_flag_ric ttt1;
242> val ric = false : bool
243\end{verbatim}\end{session}
244\index{holCheckLib!ML bindings!get\_flag\_ric@\ml{get\_flag\_ric}}
245\(\mathtt{ric}\) is a boolean which is true if the transition system described by \(\mathtt{TS}\) is synchronous, and false otherwise. In a synchronous transition system, all actions must occur simultaneously. Otherwise \(\mathtt{TS}\) is asynchronous i.e., the actions are interleaved. In the case of our example for instance, \( \mathtt{TS} \) should be asynchronous since the players do not move together but interleave moves. The definition of \( \mathtt{TS} \) ensures that they do not play out of turn, or make illegal moves.
246
247For an asynchronous system, the formal transition relation is internally represented as the disjunction of all the actions. For a synchronous system (e.g., a circuit with a single global clock), it is a conjunction. Indeed, the standard way to specify a synchronous transition relation is using the wildcard ``.'' action, with the corresponding relation being a conjunction over all possible actions. Step through the usage example given at the top of \texttt{alu.sml} in the \hc{} \texttt{examples} directory, and then examine the generated model to see how synchronous transition systems are modelled.
248
249\begin{session}\begin{verbatim}
250- val nm = holCheckLib.get_name ttt1;
251> val nm = SOME "ttt" : string option
252\end{verbatim}\end{session}
253\index{holCheckLib!ML bindings!get\_name@\ml{get\_name}}\index{holCheckLib!models!naming}
254\(\mathtt{nm}\) is an optional argument when constructing the model (hence it is stored internally as an option type). It is a string that names the formal model that is generated internally by \hc{}. Since the resulting theorems are stated in terms of this model, it is useful to have an abbreviation for the term representing the model to keep the theorem statement readable. \hc{} has a default name for models, but if the user expects to be using more than one model in the same session, then setting a name is required to avoid name clashes.
255
256\begin{session}\begin{verbatim}
257- val vord = holCheckLib.get_vord ttt1;
258> val vord = SOME ["m", "m'", "u0_0", "u0_0'", "v0_0", "v0_0'"] :
259  string list option
260\end{verbatim}\end{session}
261\index{holCheckLib!ML bindings!get\_vord@\ml{get\_vord}}\index{holCheckLib!models!variable ordering}
262\(\mathtt{vord}\) is an optional argument to the model. It is a list of current- and next-state variables names, given as strings without any type information. \(\mathtt{vord}\) is used to manually supply a variable ordering to the BDD engine. \hc{} has a default ordering heuristic but it is rather primitive at present (it just interleaves current- and next-state variables).
263
264\begin{session}\begin{verbatim}
265- val st =  holCheckLib.get_state ttt1;
266> val st = SOME``(m,u0_0,v0_0)`` : term option
267\end{verbatim}\end{session}
268\index{holCheckLib!ML bindings!get\_state@\ml{get\_state}}
269\(\mathtt{st}\) is an optional argument. It is a \HOL{} tuple that explicitly describes the order in which state variables appear in the state tuple. \hc{} can automatically calculate the state from \(\mathtt{S0}\) and \(\mathtt{TS}\), but in some cases the user may wish to use the resulting theorems in other work where the state tuple has already been defined in a certain manner. \(\mathtt{st}\) is used in such cases. Note we do not use the identifier \texttt{state} as this already exists in the default HOL interactive session namespace.
270
271At present the user must take care that \(\mathtt{vord}\) and \(\mathtt{st}\) are consistent with the rest of the arguments e.g. there are no missing variables.
272
273\texttt{holCheckLib.get\_props} returns the properties to be model checked. This is simply a list of \ctl or \(\mu\)-calculus formulas. Since the formulas contain atomic propositions, which are modelled as functions on the state, the user inputting the formulas needs to know what the state is going to be. \hc{} provides a function \(\mathtt{mk\_state}\) for this purpose.
274
275\begin{session}
276\begin{verbatim}
277- holCheckLib.mk_state;
278> val it = fn : term -> (string * term) list -> term
279- holCheckLib.mk_state S0 TS;
280> val it = ``(m,u0_0,v0_0)`` : term
281\end{verbatim}
282\end{session}
283
284Thus even though the state is an optional argument when constructing the model, in practice we nearly always use \texttt{mk\_state} and then \texttt{set\_state} to set it.
285
286\(\mathtt{ttt1}\) contains five \ctl properties. We consider these in turn.
287
288\begin{session}
289\begin{verbatim}
290- List.nth(holCheckLib.get_props ttt1,0);
291> val it =
292    ("isInit",
293     ``~C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0)) /\
294       ~C_BOOL (B_PROP (\(m,u0_0,v0_0). v0_0)) /\
295       C_BOOL (B_PROP (\(m,u0_0,v0_0). m))``) : string * term
296\end{verbatim}
297\end{session}
298\index{holCheckLib!ML bindings!get\_props@\ml{get\_props}}
299The first property describes the initial state of the system. Note how atomic propositions are formally modelled as boolean functions on the state. As noted earlier, all atomic propositions are currently just boolean variables. \texttt{C\_BOOL} and \texttt{B\_PROP} are type constructors from the \HOL{} datatype for \ctl formulas. Property specification is considered in more detail in \S\ref{sec:prop}.
300
301\begin{session}
302\begin{verbatim}
303- List.nth(holCheckLib.get_props ttt1,1);
304> val it =
305    ("A_win",
306     ``~C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
307       (C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0)))``) : string * term
308\end{verbatim}
309\end{session}
310
311This property describes a winning position for A. As with \(\mathtt{TS}\) there is some redundancy here which has been edited out. We shall edit this redundancy from the following properties to save space.
312
313\begin{session}
314\begin{verbatim}
315- List.nth(holCheckLib.get_props ttt1,2);
316> val it =
317    ("B_win",
318     ``C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
319       C_BOOL (B_PROP (\(m,u0_0,v0_0). v0_0)``) : string * term
320\end{verbatim}
321\end{session}
322
323The property above similarly describes a winning position for B.
324
325\begin{session}\begin{verbatim}
326- List.nth(holCheckLib.get_props ttt1,3);
327> val it =
328    ("A_canwin",
329     ``C_EG (~C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
330             (C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0))) \/
331             C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
332          C_EF (~C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
333                (C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0)))) \/
334            ~C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
335            C_AF (~C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
336                  (C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0)))))``) :
337  string * term
338\end{verbatim}\end{session}
339
340This property says that A has a winning strategy from the current state. Since we define success if the set of states satisfying the property contains the set of initial states, this suffices to check that A has a winning strategy. Cleaned up, this is the \ctl property \[ \mathbf{EG} (\textup{(A wins)} \lor (\textup{A to move} \land \mathbf{EF} (\textup{A wins})) \lor (\textup{B to move} \land \mathbf{AF} (\textup{A wins})))\] Intuitively, the property says that there exists a path from the current state such that at each step on that path either A has won the game, or it is A's turn and there exists at least one path in which A eventually wins the game, or it is not A's turn and on all paths A eventually wins the game.
341
342The last property similarly says the B has a winning strategy.
343
344\subsubsection{The Output Model}
345
346The model returned by \(\mathtt{ttt.makeTTT}\) can be supplied as the first argument to \(\mathtt{holCheck}\).
347
348\begin{session}\begin{verbatim}
349- val ttt2 = holCheckLib.holCheck ttt1;
350> val ttt2 = <model> : model
351\end{verbatim}\end{session}
352
353\(\mathtt{holCheck}\) returns another model. This model is exactly the same as \texttt{ttt1}, except that it now contains the results of the model checking. These are recovered via the function \texttt{holCheckLib.get\_results}, and return a list in which the n\({}^{th}\) element gives the results of model checking the n\({}^{th}\) property in the list returned by \texttt{holCheckLib.get\_props}. \texttt{holCheckLib.get\_results} returns an option type, since no results are known before model checking takes place.
354
355Each element is a triple of the form \( (term\_bdd,thm,trace) \).\footnote{A \(\textup{term\_bdd}\) is an ML value that contains a \HOL{} term together with its boolean semantics represented as a BDD (see the \texttt{HolBddLib} documentation for details).} These are the BDD semantics of the property, a theorem certifying the property holds (if it does) and a counterexample or witness trace, if one could be recovered.
356
357We consider each result in turn.
358
359\begin{session}\begin{verbatim}
360- List.nth(valOf (holCheckLib.get_results ttt2),0);
361> val it =
362    (<term_bdd>,
363     SOME [.................]
364         |- CTL_MODEL_SAT ctlKS_ttt
365              (~C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0)) /\
366               ~C_BOOL (B_PROP (\(m,u0_0,v0_0). v0_0)) /\
367               C_BOOL (B_PROP (\(m,u0_0,v0_0). m))), NONE) :
368  term_bdd * thm option * term list option
369\end{verbatim}\end{session}
370
371This is the result corresponding to the first property (which described the set of initial states).  The first component is the \(\textup{term\_bdd}\) that corresponds to the set of states of the model satsified by this property. As expected, the set of initial states is contained in the set of initial states and thus the second component is a success theorem attesting to this. The predicate \( \mathtt{CTL\_MODEL\_SAT} \)\index{holCheckLib!CTLMODELSAT@\ml{CTL\_MODEL\_SAT}} says that the property holds in the formal model \( \mathtt{ctlKS\_ttt}\). If the property had not held, the theorem derivation would have failed and the component would have been \( \mathtt{NONE}\). The third component is used to return the counterexample or witness associated with the property. Since we succeeded there is no counterexample, and witnesses are only returned for properties talking about paths, so this component is \( \mathtt{NONE}\). Note that the theorem has some assumptions associated with it. We shall return to these later.
372
373\begin{session}\begin{verbatim}
374- List.nth(valOf (holCheckLib.get_results ttt2),1);
375> val it = (<term_bdd>, NONE, SOME []) :
376  term_bdd * thm option * term list option
377\end{verbatim}\end{session}
378
379The second result corresponds to a win position for A. Since the initial state is not a win position for A, there is no success theorem and as before counterexamples are only provided for properties talking about paths. The third result is exactly the same, since the initial state is not a win position for B either.
380
381\begin{session}\begin{verbatim}
382- List.nth(valOf (holCheckLib.get_results ttt2),3);
383> val it =
384    (<term_bdd>,
385     SOME [....................................]
386         |- CTL_MODEL_SAT ctlKS_ttt
387              (C_EG
388                 (~C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
389                  (C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0))) \/
390                  C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
391                  C_EF
392                    (~C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
393                     (C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0)))) \/
394                  ~C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
395                  C_AF
396                    (~C_BOOL (B_PROP (\(m,u0_0,v0_0). m)) /\
397                     (C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0)))))),
398     SOME [``(m,~u0_0,~v0_0)``]) :
399   term_bdd * thm option * term list option
400\end{verbatim}\end{session}
401
402This result corresponds to the fourth property, that stated that A has a winning strategy. This is true, and we get the success theorem, as well as a witness, which shows that there is such a path from the initial state.
403
404The last result is the same as the second and third, since B does not have a winning strategy, and counterexamples cannot be calculated for properties that assert the existence of specific paths (since the ``counterexample'' would effectively be the entire set of reachable states).\index{holCheckLib!traces}
405
406Finally, note that both success theorems have some assumptions. If the term\_bdd's were examined, they would also have the corresponding assumptions. This is because \hc{} uses postponed proof verification to speed up the model checking work-flow (i.e. no time is wasted proving intermediate lemmas for properties that fail eventually). Any success theorems and term\_bdd's thus end up with several undischarged assumptions. The idea is that the time-consuming proof verification can be postponed to a later time, when the user is otherwise occupied (e.g., asleep).
407
408The assumptions are discharged as follows (chatting messages have been elided).
409
410\begin{session}\begin{verbatim}
411- val ttt3 = holCheckLib.prove_model ttt2;
412> val ttt3 = <model> : model
413\end{verbatim}\end{session}
414
415This returns a model that is exactly the same as \texttt{ttt2}, except that any assumptions introduced due to the postponed proof have been discharged. We can confirm this by looking at say, the first property, again.
416
417\begin{session}\begin{verbatim}
418- List.nth(valOf (holCheckLib.get_results ttt3),0);
419> val it =
420    (<term_bdd>,
421     SOME|- CTL_MODEL_SAT ctlKS_ttt
422              (~C_BOOL (B_PROP (\(m,u0_0,v0_0). u0_0)) /\
423               ~C_BOOL (B_PROP (\(m,u0_0,v0_0). v0_0)) /\
424               C_BOOL (B_PROP (\(m,u0_0,v0_0). m))), NONE) :
425  term_bdd * thm option * term list option
426\end{verbatim}\end{session}
427
428This completes one cycle of the \hc{} work-flow (typically calls to \texttt{prove\_model} are saved for the end of the checking, since  \texttt{prove\_model} just verifies the results fully-expansively; it cannot invalidate them unless there is a bug in \hc{}).
429
430At this point the user would fix either \(\mathtt{S0}\) or \(\mathtt{TS}\) or the properties, and start over, until all expected properties are verified.
431
432\subsection{General Usage Guidelines}
433
434\texttt{holCheckLib} is different from other libraries in that it does not provide tools that fit in with the usual interactive theorem proving workflow. There are no tactics, and it is unlikely (though possible) that \hc{} would be called as a decision procedure during interactive proof. The reason for this is that the models checked by model checkers are represented explicitly as state machines, whereas in \HOL{} interactive proof the underlying ``model'' is simply that of higher-order logic.  Therefore, we need to specify both models and properties explicitly.
435
436\subsubsection{Model construction}\label{sec:models}\index{holCheckLib!models!creating}
437
438We have already seen how to create the ML type \texttt{model} that acts as an input into \hc{}. The three mandatory components of a model are a predicate representing the set of initial states, predicate(s) for the transition system, and the synchronous flag. The following observations should be kept in mind.
439
440\paragraph{Initial states}\index{holCheckLib!models!initial state}
441
442Since \hc{} supports only boolean variables, only those are allowed in the state. Only the variables in the state space are allowed here, and the term must be purely propositional. Primed variables are not allowed.
443
444\paragraph{Transition system}\index{holCheckLib!models!transition relation}
445
446Only the variables in the state space are allowed. They may be primed to indicate the value of that variable in the next state. It is strongly recommended that primed variables not be used for anything other than this function. \hc{} may wander into uncharted territory otherwise.
447
448\hc{} can handle from about 50 to 100 variables currently, depending on the transition system in question. This number should rise as standard model checking optmisations such as partitioning, cone-of-influnce, and symmetry reductions are implemented.
449
450The wildcard ``.'' action represents any action, and is always present. It may only be explicitly defined by the user if it is the only action, to prevent internal inconsistency. If it is not defined, then it is internally generated as a conjunction or disjunction over the defined actions, depending on whether or not the synchronous flag \texttt{ric} is true. It may be used in \(\mu\)-calculus properties, and represents the entire transition system for \ctl properties. Usually, for synchronous transition systems, the user defines just the ``.'' action, since all actions happen simultaneously so there is usually not much call for giving them separate identities.
451
452See the AMBA AHB bus protocol example in the file \texttt{amba\_ahbScript.sml} in the \hc{} \texttt{examples} directory for an example of how to specify a complex transition system in a modular manner, hiding internal details using existential quantifiers.
453
454\paragraph{The ``relation-is-conjunctive'' flag} The \texttt{ric} flag is an ML boolean type that is set to true for synchronous transition systems, and false for asynchronous or interleaved transition systems.
455
456\subsubsection{Formal models}\label{sec:formal_models}\index{holCheckLib!models!formal}
457
458A theorem returned by \hc{} is usually of the form \texttt{CTL\_MODEL\_SAT M f}. We have already explained what the predicate \texttt{CTL\_MODEL\_SAT} is. \texttt{f} is the property that was checked (see \S\ref{sec:prop} below), and \texttt{M} is the formal model.
459
460The model we provide to \hc{} as the ML type \texttt{model} consists of several \HOL{} terms representing various pieces of information used by \hc{}. However, \hc{} does everything by proof, and this requires a formal \HOL{} theory of the \( \mu\)-calculus as well as of Kripke structures. Hence, the terms contained in the ML \texttt{model} type are packaged into a formal \HOL{} datatype that represents a Kripke structure and is assigned a constant name for brevity. It is this name that we see in the theorem statement in place of \texttt{M}. Indeed, a full \HOL{} definition corresponding to that name would exist in the current session's namespace, and the \HOL{} terms we supplied to the ML model would appear (perhaps abbreviated) in the right hand side of that definition.
461
462As long as we are restricted to model checking, this internal formal model is not important. However, \hc{} has some experimental support for model decomposition using \HOL{} (see \S\ref{sec:decomp} for details). This requires manipulation of the formal model and then it becomes important to know what the models contain. For the moment this support is automatic, so in-depth knowledge of formal models is not required. This subsection is here, for the moment, mainly as an explanation for what we see in the \hc{} output theorems.
463
464\subsubsection{Writing properties}\label{sec:prop}\index{holCheckLib!models!properties}
465
466\hc{} supports model checking for \ctl and \(\mu\)-calculus properties. It is beyond the scope of this description to describe these languages in detail here (e.g., see \emph{Model Checking} by Clarke et al, MIT Press, 1999). Properties are specified as \HOL{} terms of type \texttt{ctl} or \texttt{mu}.
467
468\begin{table}
469\caption{\HOL{} \(\mu\)-calculus formula syntax}
470\label{tab_mu}
471\begin{tabular}{|l|l|l|}
472\hline
473\(\mu\)-calculus operator & \HOL{} type constructor & Overloaded syntax \\
474\hline
475true & \texttt{TR} & \texttt{T} \\
476false & \texttt{FL} & \texttt{F} \\
477$\lnot f$ & \texttt{Not} & $\hnot f$  \\
478$f \land g$ & \texttt{And} & $f\, \hand\, g$ \\
479$f \lor g$ & \texttt{Or} & $f\, \hor\, g$ \\
480proposition $p$ & \texttt{AP} & \texttt{AP p} \\
481$\langle a \rangle$ f& \texttt{DIAMOND} & \verb+<<"a">> f+ \\
482$[a] f$  & \texttt{BOX} & \verb+[["a"]] f+ \\
483variable $Q$ & \texttt{RV} & \texttt{RV Q} \\
484$\mu Q . f$ & \texttt{mu} & \texttt{mu Q .. f} \\
485$\nu Q . f$ & \texttt{nu} & \texttt{nu Q .. f} \\
486\hline
487\end{tabular}
488\end{table}
489
490The type constructors for \texttt{mu} \index{holCheckLib!properties!mucalculus@\(\mu\)-calculus} are shown in Table \ref{tab_mu}, together with overloaded syntax for ease of entry. For example, the property saying that there exists a path to a state where \( v_0 \land v_1 \) holds is represented by the \(\mu\)-calculus formula \( \mu Q. (v_0 \land v_1) \lor \langle.\rangle Q \) and would be written in \HOL{} as
491
492\begin{verbatim}
493   mu "Q" .. AP (\(v_0,v_1). v_0 /\ v_1) \/ (<<".">> RV "Q")
494\end{verbatim}
495
496Note that atomic propositions are written as functions on the state, and that \(\mu\)-calculus variables and action names are modelled as \HOL{} strings. For internal reasons, these strings must be alphanumeric with underscores, and begin with a letter, the only exception being the special ``.'' action.
497
498Clearly, \(\mu\)-calculus ``variables'' as modelled above are not treated as variables by \HOL{}. We use strings because \HOL{} does not have native support for variable binding in higher-order abtract syntax (this is an active research area). The treatment of free and bound variables within \hc{} is however consistent with standard definitions.
499
500\begin{table}
501\caption{\HOL{} \ctl formula syntax}
502\label{tab_ctl}
503\begin{tabular}{|l|l|l|}
504\hline
505\ctl operator & \HOL{} type constructor & Overloaded to \\
506\hline
507true & \texttt{B\_TRUE} & \texttt{T} \\
508$\lnot f$ & \texttt{B\_NOT} & $\hnot f $  \\
509$f \land g$ & \texttt{B\_AND} & $f\,\hand\,g$ \\
510proposition $p$ & \texttt{B\_PROP} & \texttt{B\_PROP p} \\
511$\mathbf{EX} f$ & \texttt{C\_EX} & \texttt{C\_EX} f \\
512$\mathbf{EG} f$ & \texttt{C\_EG} & \texttt{C\_EG} f \\
513$\mathbf{E}(f\,\mathbf{U}\,g)$ & \texttt{C\_EU} & \texttt{C\_EU}(f,g) \\
514\hline
515\end{tabular}
516\end{table}
517
518Table \ref{tab_ctl} describes the syntax for \ctl \index{holCheckLib!properties!ctl@\ctl}. Note that some of the operators are missing e.g. \( \mathtt{F} \) and \( \mathbf{AX} \). These are defined indirectly in terms of the rest, with the expected overloaded syntax. The syntax is structured slightly differently in that any subformula from the propositional fragment (i.e., the first four rows of Table \ref{tab_ctl}) is always wrapped within the type constructor \texttt{C\_BOOL}.
519
520The example property above is the \ctl formula \( \mathbf{EF} (v_0 \land v_1) \) and would be written in \HOL{} as
521
522\verb+C_EF (C_BOOL (B_PROP (\(v_0,v_1). v_0 /\ v_1)))+
523
524where \(\mathbf{EF} f\) has the standard definition \( \mathbf{EU}(T,f) \).
525
526\subsubsection{Environments}
527
528\(\mu\)-calculus model checking, in addition to having a model, also requires an environment: a mapping from variables to sets of states. The \hc{} core accepts environments as maps from strings to \texttt{term\_bdd}'s. However, the user interface for the moment has no provision for supplying an environment. This will be added in due course. In the meantime, environments can be ``faked'' by purely propositional subformulas, though this may not be particularly efficient.
529
530\ctl model checking does not require environments.
531
532\subsection{Experimental Support for Decomposition}\label{sec:decomp}
533
534One of the motivations behind \hc{} is to see if tight integration with \HOL{} helps the model checking work flow. In this spirit, \hc{}  includes some experimental support for model decomposition. The basic idea is that if the model consists of several components joined by parallel synchronous composition, then a property holding in one component should hold in the entire model. This seeks to exploit locality in the structure of models and properties.
535
536For those familiar with model checking, this is \emph{not} assume-guarantee reasoning, nor does it use simulation pre-orders. It is considerably more simple: take a product Kripke structure, break up the components, model check each component, re-compose. Unlike assume-guarantee reasoning, this does not apply to properties that address truly global aspects of the system. Also, it is limited to synchronous systems. Nevertheless, there are some applications in hardware verification.
537
538Support is via two functions, \texttt{mk\_gen\_par\_sync\_comp\_thm} and \texttt{mk\_par\_sync\_comp\_thm}. These functions are not part of the \texttt{holCheckLib} signature, as the user interface for decomposition support is considered unstable at the moment. They are instead found in the \texttt{decompTools} structure.
539
540The first function takes initial state and transition system predicates for two models with non-overlapping state spaces, and returns a theorem that says that if any well-formed property holds in the first model, then it holds in the parallel synchronous composition of the two models.
541
542The second function takes the theorem generated by the first function, and a property, and discharges the well-formedness assumptions to return a theorem saying that if the supplied property holds in the first model, then it holds in the composed model.
543
544In time we expect to integrate this fully into \hc{} as a sort of localisation reduction. In the meantime, the interested reader can take a look at the synchronous composition section of \texttt{ambaScript.sml} in the \texttt{examples} directory. Even without any knowledge of AMBA, the ten or so lines give a flavour of how decomposition can be used.
545
546\subsection{\hc{} Internals and Caveats}
547
548This section contains information on some internal details and quirks that may help with creating models and properties for \hc{}.
549
550\subsubsection{Variable ordering}\index{holCheckLib!models!variable ordering}
551
552\hc{} users are strongly recommended to supply a BDD variable ordering for the model using the \texttt{set\_vord} function, even though it is optional. \hc{} does have its own variable ordering heuristic. This just interleaves current- and next-state variables however, and is not very good. Remember that the ordering supplied must include next-state (i.e., primed) variables, and must include all state variables.
553
554\subsubsection{Counterexamples}\index{holCheckLib!traces}
555
556The generation of witness traces for properties of the form \(\mathbf{EG} f \) (or dually, counterexamples for \(\mathbf{AF} f \) style properties) leaves much to be desired: it tries to give the shortest qualifying path which usually turns out to be just the initial state, whereas typically the user is interested in the longest one.
557
558\subsubsection{Abstraction}
559
560\hc{} implements a fully automatic abstraction refinement framework that is invisible to the user. A simple heuristic analysis is used to decide whether or not to apply abstraction for a given property. Sometimes the abstraction may make things worse. If \hc{} appears to be taking overly long on a property, the user may try redoing the check, after turning off abstraction. This can be done by calling \texttt{set\_flag\_abs} on the model. Turning abstraction on and off on a per-property basis is not supported yet.
561
562\subsubsection{Lazy proof}
563
564All steps of the model checking (except BDD operations) are backed up by fully expansive proof. To get around the speed penalty imposed by this proof, \hc{} performs proof lazily. This means that any theorem produced by \hc{} may have several undischarged assumptions (it is then known as a lazy theorem). Typically, once all properties have been checked, the user calls \texttt{prove\_model}\index{holCheckLib!ML bindings!prove\_model@\ml{prove\_model}} on the model to discharge the assumptions. This step may take a while for big models and properties, in which case it is advisable to let it run when computing resources are expected to be free, e.g., overnight.
565
566A failure to discharge all assumptions means a completeness bug in the \hc{} proof verification machinery. However, it does not invalidate the soundness of the theorem, modulo the soundness of \HOL{}.
567
568\texttt{prove\_model}\index{holCheckLib!ML bindings!prove\_model@\ml{prove\_model}} must be used in the same session in which the model checking was done, if the produced theorems are going to be written to permanent storage. This is because the lazy proof machinery is unable to persist lazy theorems, owing to Moscow ML's inability to persist closures.
569
570\subsubsection{Permanent Storage}\index{holCheckLib!models!saving}
571
572For the moment, \hc{} does not support persistence for models. The theorems produced can however be saved to permanent storage as \HOL{} theorems.
573
574\index{holCheckLib|)}
575
576\printindex
577
578\end{document}
579%%% Local Variables:
580%%% mode: latex
581%%% TeX-master: "description"
582%%% End:
583