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

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

Line 1: | Line 1: | ||

+ | This homework is to practice using BDDs to represent Kripke structures and to do symbolic state generation. | ||

+ | ==Paper Pencil== | ||

+ | |||

+ | # ('''5 points''') Create the Boolean formula for the transition relation for the dinning philosophers system in [[Homework 3]]. As before each location should represent a single atomic step or more precisely, each '''when''' statement is one transition in the model. Be sure to encode the program and ''not'' the reachable state space. | ||

+ | # ('''5 points''') Using the transition relation from the prior problem, find the set of states reachable in two transitions from the initial state. Be sure to clearly show the operations on the transition relation. | ||

+ | |||

+ | ==Programming== | ||

+ | |||

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

+ | |||

+ | # ('''5 points''') Write a program that creates a BDD for the transition relation from the dining philosophers model in [[Homework 3]]. | ||

+ | # ('''2 points''') Add to the program code to create a BDD representing the initial state. | ||

+ | # ('''5 points''') Add to the program code to find the BDD representing the reachable state-space of the system. There should only be 10 reachable states. Be sure to treat each '''when''' clause as atomic so it includes the check, change to state, and goto all in a single step. | ||

+ | |||

+ | The CUDD interface is defined in the ''obj'' folder in the CUDD distribution in the file ''cuddObj.hh''. The following following functions are important in that interface: | ||

+ | |||

+ | <code cpp> | ||

+ | BDD BDD::SwapVariables(std::vector<BDD> x, std::vector<BDD> y) const; | ||

+ | |||

+ | BDD AndAbstract(const BDD& g, const BDD& cube, unsigned int limit = 0) const; | ||

+ | |||

+ | double BDD::CountMinterm(int nvars) const; | ||

+ | |||

+ | void Cudd::DumpDot( | ||

+ | const std::vector<BDD>& nodes, | ||

+ | char ** inames = 0, | ||

+ | char ** onames = 0, | ||

+ | FILE * fp = stdout) const; | ||

+ | </code> | ||

+ | For the CUDD interface, '''BDD::SwapVariables''' is equivalent to replace and '''BDD::AndAbstract''' (or '''BDD::ClippingAndAbstract''') is equivalent to relational product. The ''cube'' variable is as expected. '''BDD::AndAbstract''' is direct to use and you may ignore the optional limit parameter. If you use to use '''BDD:ClippingAndAbstract''', ''maxDepth'' may be set to the number of variables in the BDD manager, and ''direction'' to 0. The '''BDD::CountMinterm''' is equivalent to ''SatCount''. The '''Cudd::DumpDot''' dumps any BDDs in the input vector as ''dot'' files. The ''onames'' are the names of each function dumped. The ''inames'' are the names of the variables in the BDD (be sure to include all of them). As FYI for the dot output, CUDD uses complement edges indicated by the small-dash line (as opposed to the long-dash line). You need to count the number of complement edges to figure out the final value: an odd number means the final value is complemented and an even number means the final value is unchanged. See a simple example of ''and''-ing two variables to see what I mean. Or even look at the dump for a single variable. The first complement edge may be on the pointer naming the function and showing its first node! | ||

+ | |||

+ | == Submission == | ||

+ | Please submit a single file with paper pencil work and your program via the ''Homework 6'' link in [http://learningsuite.byu.edu Learning Suite]. |