With the encoding in part (b), \b[$y=A$] is a valid <Moore machine> output equation. Among reachable states, $A=1$ exactly at $S_4$. This uses unused output-table entries as <don't-care conditions>. If one instead wants the output to be zero in every unused state, use $y=A\bar B\bar C$; that extra requirement does not change any output from a valid state.

Solution

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Digital systems, linear algebra, introduction to formal proof / 1 / c / Solution

 Solution (source code)