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