1. (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.
2. (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.

Use the CUDD package for the following problems.

1. (5 points) Write a program that creates a BDD for the transition relation from the dining philosophers model in Homework 3.
2. (2 points) Add to the program code to create a BDD representing the initial state.
3. (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:

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;

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!

Please submit a single file with paper pencil work and your program via the Homework 6 link in Learning Suite.