Line 2,258: |
Line 2,258: |
| ==Note 27== | | ==Note 27== |
| | | |
− | <pre>
| + | ===Interpretation of the Propositional Program (cont.)=== |
− | Interpretation of the Propositional Program (cont.) | + | |
| + | '''State Partition''' |
| | | |
− | State Partition:
| + | {| align="center" cellpadding="8" width="90%" |
| + | | |
| + | <math>\begin{array}{l} |
| + | \texttt{((~p0\_q0~),(~p0\_q1~),(~p0\_q\#~),(~p0\_q*~))} |
| + | \\ |
| + | \texttt{((~p1\_q0~),(~p1\_q1~),(~p1\_q\#~),(~p1\_q*~))} |
| + | \\ |
| + | \texttt{((~p2\_q0~),(~p2\_q1~),(~p2\_q\#~),(~p2\_q*~))} |
| + | \end{array}</math> |
| + | |} |
| | | |
− | (( p0_q0 ),( p0_q1 ),( p0_q# ),( p0_q* ))
| + | In cactus syntax, an expression of the form <math>\texttt{((} e_1 \texttt{),(} e_2 \texttt{),(} \ldots \texttt{),(} e_k \texttt{))}</math> expresses a statement to the effect that ''exactly one of the expressions <math>e_j\!</math> is true, for <math>j = 1 ~\mathit{to}~ k.</math>'' Expressions of this form are called ''universal partition'' expressions, and the corresponding ''painted and rooted cactus'' (PARC) has the following shape: |
− | (( p1_q0 ),( p1_q1 ),( p1_q# ),( p1_q* ))
| |
− | (( p2_q0 ),( p2_q1 ),( p2_q# ),( p2_q* ))
| |
| | | |
− | In cactus syntax, an expression of the form "((e_1),(e_2),(...),(e_k))"
| + | <br> |
− | expresses the fact that "exactly one of the e_j is true, for j = 1 to k".
| |
− | Expressions of this form are called "universal partition" expressions, and
| |
− | the corresponding "painted and rooted cactus" (PARC) has the following shape:
| |
| | | |
| + | <pre> |
| o---------------------------------------o | | o---------------------------------------o |
| | | | | | | |
Line 2,291: |
Line 2,297: |
| | ((e_1),(e_2),(...),(e_k)) | | | | ((e_1),(e_2),(...),(e_k)) | |
| o---------------------------------------o | | o---------------------------------------o |
| + | </pre> |
| | | |
− | The State Partition segment of the propositional program
| + | <br> |
− | consists of three universal partition expressions, taken
| |
− | in conjunction expressing the condition that M has to be
| |
− | in one and only one of its states at each point in time
| |
− | under consideration. In short, we have the constraint:
| |
| | | |
− | At each of the points in time p_i, for i in the set {0, 1, 2}
| + | The State Partition segment of the propositional program consists of three universal partition expressions, taken in conjunction expressing the condition that <math>M\!</math> has to be in one and only one of its states at each point in time under consideration. In short, we have the constraint: |
− | M can be in exactly one state q_j, for j in the set {0, 1, #, *}.
| + | |
− | </pre> | + | {| align="center" cellpadding="8" width="90%" |
| + | | |
| + | <p>At each of the points in time <math>p_i,\!</math> for <math>i\!</math> in the set <math>\{ 0, 1, 2 \},\!</math></p> |
| + | |
| + | <p><math>M\!</math> can be in exactly one state <math>q_j,\!</math> for <math>j\!</math> in the set <math>\{ 0, 1, \#, * \}.</math></p> |
| + | |} |
| | | |
| ==Note 28== | | ==Note 28== |