##### Differences

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

 cs-486:homework-5 [2017/02/14 15:45]egm [Problems] cs-486:homework-5 [2017/02/14 15:45]egm [Problems] Both sides previous revision Previous revision 2017/02/14 15:45 egm [Problems] 2017/02/14 15:45 egm [Problems] 2017/02/14 15:36 egm 2017/02/14 09:55 egm created2017/01/11 12:11 egm removed2014/10/31 14:03 egm [Using CUDD as an Oracle] 2014/10/31 09:30 egm [Obtaining the Source Distribution] 2014/10/31 09:29 egm [Obtaining the Source Distribution] 2014/10/31 09:29 egm [Obtaining the Source Distribution] 2014/10/28 09:59 egm [Using CUDD as an Oracle] 2014/10/28 09:23 egm [bddToDot and Restrict] 2014/09/02 10:31 egm 2014/09/02 10:30 egm created 2017/02/14 15:45 egm [Problems] 2017/02/14 15:45 egm [Problems] 2017/02/14 15:36 egm 2017/02/14 09:55 egm created2017/01/11 12:11 egm removed2014/10/31 14:03 egm [Using CUDD as an Oracle] 2014/10/31 09:30 egm [Obtaining the Source Distribution] 2014/10/31 09:29 egm [Obtaining the Source Distribution] 2014/10/31 09:29 egm [Obtaining the Source Distribution] 2014/10/28 09:59 egm [Using CUDD as an Oracle] 2014/10/28 09:23 egm [bddToDot and Restrict] 2014/09/02 10:31 egm 2014/09/02 10:30 egm created Line 14: Line 14: '''​3. (20 points)'''​ Apply double-depth-first search to the automaton from the intersection in Problem 1 to detect a cycle in the intersection. Always visit the 0-input edge first. Assign each state a pre-order visit number. States that are visited twice (once if the first search and again in the second search) should have two pre-order visit numbers. If a cycle is detected, then clearly indicate that cycle. Grading is on the pre-order visit numbers. ​ '''​3. (20 points)'''​ Apply double-depth-first search to the automaton from the intersection in Problem 1 to detect a cycle in the intersection. Always visit the 0-input edge first. Assign each state a pre-order visit number. States that are visited twice (once if the first search and again in the second search) should have two pre-order visit numbers. If a cycle is detected, then clearly indicate that cycle. Grading is on the pre-order visit numbers. ​ - '''​4. (20 points)'''​ Repeat Problem 2, only this time use a double-depth-first search to detect a cycle '''​at the same time'''​ that the intersection is being computed. This is often referred to as '''​on-the-fly'''​ model checking. As in the previous problem, always visit the 0-input edge first. Assign each state a pre-order visit number. States that are visited twice (once if the first search and again in the second search) should have two pre-order visit numbers. If a cycle is detected, then clearly indicate that cycle. Grading is on the pre-order visit numbers. '''​Did the entire intersection get enumerated ''​before''​ a cycle is detected? + '''​4. (20 points)'''​ Repeat Problem 2, only this time use a double-depth-first search to detect a cycle '''​at the same time'''​ that the intersection is being computed. This is often referred to as '''​on-the-fly'''​ model checking. As in the previous problem, always visit the 0-input edge first. Assign each state a pre-order visit number. States that are visited twice (once if the first search and again in the second search) should have two pre-order visit numbers. If a cycle is detected, then clearly indicate that cycle. Grading is on the pre-order visit numbers. '''​Did the entire intersection get enumerated ''​before''​ a cycle is detected?'''​ '''​5. (20 points)'''​ Consider the states space and never-claim in [http://​faculty.cs.byu.edu/​~egm/​downloads/​cs486-homework5-figures.pdf Figure 5]. Perform on-the-fly model checking to see if an accepting cycle exists. Visit edge-labels in alphabetical order (e.g., A, then B, and then C). If there is a non-deterministic choice of edges, the visit the edge leading the least state-label first (e.g., $s_3$ is visited ''​before''​ $s_5$). '''​5. (20 points)'''​ Consider the states space and never-claim in [http://​faculty.cs.byu.edu/​~egm/​downloads/​cs486-homework5-figures.pdf Figure 5]. Perform on-the-fly model checking to see if an accepting cycle exists. Visit edge-labels in alphabetical order (e.g., A, then B, and then C). If there is a non-deterministic choice of edges, the visit the edge leading the least state-label first (e.g., $s_3$ is visited ''​before''​ $s_5$).