global protocol Smtp(role S, role C)
{
    220() from S to C;
    choice at C // Choice 0
    {
        Ehlo1() from C to S;
        rec X
        {
            choice at S // Choice 1
            {
                250d() from S to C;
                continue X;
            }
            or
            {
                250() from S to C;
                choice at C // Choice 2
                {
                    StartTls() from C to S;
                    220() from S to C;
                    // Do TLS handshake here: level below the application level protocol (like regular TCP handshake)
                    choice at C // Choice 3
                    {
                         Ehlo2() from C to S;
                         rec X
                        {
                            choice at S // Choice 4
                            {
                                250d1() from S to C;
                                continue X;
                            }
                            or
                            {
                                2501() from S to C;
                                rec Y
                                {
                                    choice at C // Choice 5
                                    {
                                        Auth() from C to S;
                                        choice at S // Choice 6
                                        {
                                            235() from S to C;
                                            rec Z1
                                            {
                                                choice at C // Choice 7
                                                {
                                                    Mail() from C to S; //Mail from:<a@b.com>
                                                    choice at S // Choice 8
                                                    {
                                                        501() from S to C;
                                                        continue Z1;
                                                    }
                                                    or
                                                    {
                                                        2502() from S to C;
                                                        rec Z2
                                                        {
                                                            choice at C // Choice 9
                                                            {
                                                                Rcpt() from C to S; //Rcpt to:<c@d.com>
                                                                choice at S // What is this choice???  // Choice X
                                                                {
                                                                    2503() from S to C;
                                                                    continue Z2;
                                                                }
                                                            }
                                                            or
                                                            {
                                                                Data() from C to S;
                                                                354() from S to C;

                                                                too from C to S; //to:<you>

                                                                froom from C to S; //from:<me>

                                                                rec Z3
                                                                {
                                                                    choice at C // Choice 10
                                                                    {
                                                                        DataLine() from C to S;
                                                                        DataLine() from C to S;
                                                                        continue Z3;
                                                                    }
                                                                    or
                                                                    {
                                                                        Subject() from C to S; //Subject:<my Subject>
                                                                        Subject() from C to S; //Subject:<my Subject>
                                                                        continue Z3;
                                                                    }
                                                                    or
                                                                    {
                                                                        EndOfData() from C to S; // CRLF.CRLF
                                                                        2504() from S to C;
                                                                        continue Z1;
                                                                    }
                                                                }
                                                            }
                                                        }
                                                    }
                                                }
                                                or
                                                {
                                                     Quit5() from C to S;
                                                     221() from S to C;
                                                 }
                                            }
                                        }
                                        or
                                        {
                                            535() from S to C;
                                             continue Y;
                                        }
                                        //.. 501 Invalid base64 Data
                                     }
                                    or
                                    {
                                        Quit4() from C to S
                                    }
                                }
                            }
                        }
                    }
                    or
                    {
                        Quit3() from C to S;
                    }
                }
                or
                {
                    Quit2() from C to S;
                }
            }
        }
    }
    or
    {
        Quit1() from C to S;
    }
}