==Feedback==
    ==And==
        ==Dec==
            ==Seq==
            Control
            Normal
            Visible
            ==States==
            Normal Decomposed 62 88 166 132
            Crash Atomic 522 89 623 131
            ==Transitions==
            Normal Crash crash/{lup,rup} 1 RightofLn
            ==LocalVariables==
            ==EOCSeq==
        ==by==
            Normal
            ==Seq==
            Normal
            Unlocked
            Invisible
            ==States==
            Unlocked Atomic 64 50 165 92
            Unlocking Atomic 349 50 451 92
            Locking Atomic 64 317 165 359
            Locked Atomic 349 317 451 359
            ==Transitions==
            Unlocking Unlocked freeL.freeR 1 RightofLn
            Unlocked Locking but/{ldn,rdn} 1 LeftofLn
            Locking Locked secureL.secureR 1 LeftofLn
            Locked Unlocking but/{lup,rup} 1 LeftofLn
            ==LocalVariables==
            ==EOCSeq==
        ==EOCDec==
    =======
        ==And==
            ==Seq==
            MotorL
            OffL
            Visible
            ==States==
            OffL Atomic 292 203 394 245
            DownL Atomic 63 202 164 244
            UpL Atomic 524 205 626 247
            ==Transitions==
            OffL DownL ldn.-crash 1 RightofLn
            DownL OffL /secureL 2 LeftofLn
            UpL OffL rup 1 RightofLn
            UpL OffL /freeL 2 LeftofLn
            ==LocalVariables==
            ==EOCSeq==
        =======
            ==Seq==
            MotorR
            OffR
            Visible
            ==States==
            OffR Atomic 290 336 391 378
            DownR Atomic 60 333 162 375
            UpR Atomic 521 335 622 377
            ==Transitions==
            OffR DownR rdn.-crash 1 RightofLn
            DownR OffR /secureR 2 LeftofLn
            UpR OffR /freeR 1 RightofLn
            OffR UpR rup 2 LeftofLn
            ==LocalVariables==
            ==EOCSeq==
        ==EOCAnd==
    ==EOCAnd==
==signals==
    {lup,rup,ldn,rdn,secureL,secureR}
==EOCFeedback==