This shows you the differences between two versions of the page.

— |
cs-486:homework-7-2016 [2017/01/11 19:12] (current) egm created |
||
---|---|---|---|

Line 1: | Line 1: | ||

+ | This homework is to practice using BDDs for symbolic model checking. | ||

+ | |||

+ | ==Paper Pencil== | ||

+ | |||

+ | # ('''3 points''') Write a CTL property for the transition relation for the dinning philosophers system in [[Homework 3]]--the property must require a least or greatest fix-point to compute. | ||

+ | # ('''5 points''') At an abstract level, similar to what we did on the board in lecture, perform symbolic model checking for the formula in the prior problem. Be sure to show each step of the fix-pont computation. Please note that if the '''when''' clause is correctly treated as a single atomic action (i.e., the test, state update, and goto are one step), then there are only 10 reachable states. | ||

+ | |||

+ | ==Programming== | ||

+ | |||

+ | Use the CUDD package for the following problems. | ||

+ | |||

+ | # ('''10 points''') Write a program in CUDD using your solution from [[Homework 6]] that does symbolic model checking for your formula in the prior problem. | ||