[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.

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