package Ġde . jos hu agle it ze . transformation network . transform ations . busy be aver 3 Ċ Ċ import Ġde . jos hu agle it ze . transformation network . ch anger ec ording . Change Recording Model Ċ import Ġde . jos hu agle it ze . transformation network . ch anger ec ording . Observable Model Transformation Type Ċ import Ġde . jos hu agle it ze . transformation network . ch anger ec ording . create Checked Ċ import Ġde . jos hu agle it ze . transformation network . met ame tam odel . Model Ċ import Ġde . jos hu agle it ze . transformation network . models . t uring machine . T uring Machine Met amodel Ċ import Ġimplies Ċ Ċ class ĠQ 2 Q 0 ( val Ġq 2 Model : ĠChange Recording Model , Ġval Ġq 0 Model : ĠChange Recording Model ) Ġ: ĊĠĠĠ ĠT uring State Transformation () Ġ{ ĊĠĠĠ Ġoverride Ġval Ġleft Model : ĠChange Recording Model Ġget () Ġ= Ġq 2 Model ĊĠĠĠ Ġoverride Ġval Ġright Model : ĠChange Recording Model Ġget () Ġ= Ġq 0 Model ĊĠĠĠ Ġoverride Ġval Ġtype Ġget () Ġ= ĠType ĊĊĠĠĠ Ġoverride Ġfun Ġis Cons istent () Ġ= Ġstates ?. let Ġ{ Ġ( q 2 , Ġq 0 ) Ġ-> ĊĠĠĠĠĠĠĠ Ġ( q 2 . timestamp Ġ> Ġq 0 . timestamp ) Ġimplies Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġq 2 . current Char Ġ!= Ġ' 1 ' ĊĠĠĠĠĠĠĠ Ġ} Ġ&& Ġ( q 0 . timestamp Ġ== Ġq 2 . timestamp Ġ+ Ġ 1 ) Ġimplies Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġq 0 . is Left Of ( q 2 , Ġ 1 ) ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ&& Ġq 0 . band [ q 0 . band Position Ġ+ Ġ 1 ] Ġ== Ġ' 1 ' ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} Ġ?: Ġtrue ĊĊĠĠĠ Ġ@ Suppress (" PARAMETER _ NAME _ CHANGED _ ON _ OVERRIDE ") ĊĠĠĠ Ġoverride Ġfun Ġcreate Next Right State ( q 2 : ĠNon Null T uring State , Ġq 0 : ĠNon Null T uring State ) Ġ= Ġwhen Ġ( q 2 . current Char ) Ġ{ ĊĠĠĠĠĠĠĠ Ġ' 1 ' Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠ Ġq 2 . copy ( ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġtimestamp Ġ= Ġq 2 . timestamp Ġ+ Ġ 1 , ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġband Position Ġ= Ġq 2 . band Position Ġ- Ġ 1 ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ). fix Band Range (' 0 ') ĊĠĠĠĠĠĠĠ Ġelse Ġ-> Ġq 0 ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġcompanion Ġobject ĠType Ġ: ĠObservable Model Transformation Type Ġ{ ĊĠĠĠĠĠĠĠ Ġoverride Ġval Ġleft Met amodel Ġget () Ġ= ĠT uring Machine Met amodel ĊĠĠĠĠĠĠĠ Ġoverride Ġval Ġright Met amodel Ġget () Ġ= ĠT uring Machine Met amodel ĊĊĠĠĠĠĠĠĠ Ġoverride Ġfun Ġcreate ( left Model : ĠModel , Ġright Model : ĠModel ) Ġ= Ġcreate Checked ( left Model , Ġright Model , Ġ:: Q 2 Q 0 ) ĊĠĠĠ Ġ} Ċ } Ċ