[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> class/15
[Index] || [Contents] || [Grades] Mon Mar 3 16:42:35 PST 2003
```656/556 2003 1w 15 OBDDs
Assigned work:3.2 #1b (fig 3.10) using SMV
Study Section 6.3 Model checking with OBDDs (pages 351-358)

6.3 Applications of OBDDs
BDDs made model checking highly feasible.
OBDDs are a good way to express complex boolean functions.
6.3.1 Coding sets of states as OBDDs
(1) code each element as a bit-vector
(2) code a set as a bit-vlaued function of the bit-vector.
(3) code the function using OBDD
Ex 6.11 (page 354)
Warning.  Typo in some books.  Arrowhead missing.
There is transition from s1 to s3.
6.3.2 Coding transition relations
(1) Code a set of pairs.
Each pair becomes two concatenated vectors
(2) Transition is a boolean function of double length vectors.
6.3.3 Coding backtracing operators
Operators: pre[some] and pre[all].
Only need pre[some]
use exists and apply algorithms.
Ex 6.12(p 657)
6.3.4 Calculate OBDDS directly from SMV expressions
(and/or circuit/logic diagrams).
Use the apply algorithm.
Ex 6.13 p360

Exercises:
Assigned work: Ex6.12 (p657) #1(a) & #1(b).

lab:
A fun example of SMV: goat+wolf+cabbage
http://www.cis.ksu.edu/~kolluri/cis301/fall02/huth/puzzle.html
(Thanks Chris!)

Study the SMV source code:
http://ftp.csci.csusb.edu/dick/cs656/smv/
What can you discover.

next: Verifying programs
http://www.csci.csusb.edu/dick/cs656/class/16.html
```