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

Both sides previous revision Previous revision | |||

cs-486:homework-5 [2017/02/14 15:45] egm [Problems] |
cs-486:homework-5 [2017/02/14 15:45] (current) egm [Problems] |
||
---|---|---|---|

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$). |