[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> class/14
[Index] || [Contents] || [Grades] Mon Mar 3 14:43:02 PST 2003
656/556 2003 1w 14 ctl+SMV
Assigned work:Exercises 3.2 (p163-164) #1b (v)(vi)(vii)(viii)
review homework: 

3.5 algorithm for SAT

3.6 tool: SMV
Warning:   Look out for SMVs notation.
	eg: + and - are done before 'mod'
	http://www.csci.csusb.edu/dick/cs556/class/14SMVpriorities
	    If several cases with same condition only first is used.
As well as CTL errors
	eg: p->q true when p false.
	    A[ p U q] is true if q is true and p false.

Examples( some handed out last time) and demos on JB359 system
	http://ftp.csci.csusb.edu/dick/cs656/smv/examples/14ex.gif
      Translation(?) into SMV:
        http://www.csci.csusb.edu/dick/cs656/class/14ex.smv
		Error: ____  see above!
	Improved solutions:
        http://www.csci.csusb.edu/dick/cs656/smv/examples/14ex2.smv
        http://www.csci.csusb.edu/dick/cs656/smv/examples/14ex3.smv


        http://www.csci.csusb.edu/dick/cs656/class/14fig3dot2.smv
		Problems?
		

	http://www.csci.csusb.edu/dick/cs656/haunting.smv
	Conclusion
  To find a solution:
	  Specify that there is NO solution and let SMV find counter examples.
  Like:
          To prove p, assume not p and derive contradictions.

3.10 further reading
        http://www.cis.ksu.edu/~huth/lics/ancillary/bib_url.html

Exercises: Some of
	Ex 3.7 (page 176)
	Express fig 3.10 (p163) in SMV.
	Express fig 3.11 (p164) in SMV.

Assigned work: 3.2 #1b (fig 3.10)

lab
Review CTL (use Netscape)
        http://www.cis.ksu.edu/~huth/lics/tutor/chap3/questions.html

Use SMV.  Download examples from
	http://www.csci.csusb.edu/dick/cs656/smv/examples/
and test them out.  Using my 'Q' command is the easiest way:
	Q short.smv

Use SMV to do some of the exercises in 3.2 #1b (fig 3.10) #1c (fig 3.10)
	#2 (Fig 3.11) #3 (Fig 3.11)
	

next: Section 6.3 Model checking with OBDDs but not circuits
        pages 351-358
http://www.csci.csusb.edu/dick/cs656/class/15.html