Go backward to Another ExampleGo up to TopGo forward to The Next-State Relation |

`Psi`*<=>*`Init`_{Psi}*and*`always`[`A`]_{w}*and*SF(_{w}`A`)_{1}*and*SF(_{w}`A`)_{2}`Init`_{Psi}*<=>*(`pc`= "a")_{1}*and*(`pc`= "a")_{2}*and*(*x=0*)*and*(*y=0*)*and*(`sem`=1)*w**<=>*<*x*,*y*,`sem`,`pc`,_{1}`pc`>_{2}`A`*<=>*`A`_{1}*or*`A`_{2}`A`_{1}*<=>*`alpha`_{1}*or*`beta`_{1}*or*`gamma`_{1}`A`_{2}*<=>*`alpha`_{2}*or*`beta`_{2}*or*`gamma`_{2}`alpha`_{1}*<=>*(`pc`= "a")_{1}*and*(0*<*`sem`)*and*`pc`' = "b"_{1}*and*`sem`' =`sem`-1*and*`Unchanged`<*x*,*y*,`pc`>_{2}`beta`_{1}*<=>*`pc`= "b"_{1}*and*`pc`' = "g"_{1}*and**x'*=*x+1**and*`Unchanged`<*x*,*y*,`pc`>_{2}`gamma`_{1}*<=>*`pc`= "g"_{1}*and*`pc`' = "a"_{1}*and*`sem`' =`sem`+1*and*`Unchanged`<*x*,*y*,`pc`>_{2}`alpha`_{2}*<=>*...,`beta`_{2}*<=>*...,`gamma`_{2}*<=>*...

Author: Wolfgang Schreiner

Last Modification: May 14, 1998