module checNoNestedAltStatements {
    altstep as_0 ()
    runs on myComponent {

        //nesting within an altstep
        [] p2.receive ( msg_b ) {
        }
        [] p2.receive ( msg_c ) {
            setverdict ( pass );

            // nested alt, level 1
            alt {
                [] p2.receive ( msg_b ) {
                }
                [] p2.receive ( msg_c ) {
                    setverdict ( pass );
                }
                [] p2.receive {
                }
            }
        }
        [] p2.receive {

            // nested alt, level 1
            alt {
                [] p2.receive ( msg_b ) {
                }
                [] p2.receive ( msg_c ) {
                    setverdict ( pass );
                }
                [] p2.receive {

                    // nested alt, level 2
                    alt {
                        [] p2.receive ( msg_b ) {
                        }
                        [] p2.receive ( msg_c ) {
                            setverdict ( pass );
                        }
                        [] p2.receive {
                        }
                    }
                }
            }
        }
    }

    testcase t_sendMsg ()
    runs on myComponent {

        //nesting within alt statement
        p1.send ( msg_a );
        alt {
            [] p2.receive ( msg_b ) {
            }
            [] p2.receive ( msg_c ) {
                setverdict ( pass );

                // nested alt, level 1
                alt {
                    [] p2.receive ( msg_b ) {
                    }
                    [] p2.receive ( msg_c ) {
                        setverdict ( pass );
                    }
                    [] p2.receive {
                    }
                }
            }
            [] p2.receive {

                // nested alt, level 1
                alt {
                    [] p2.receive ( msg_b ) {
                    }
                    [] p2.receive ( msg_c ) {
                        setverdict ( pass );
                    }
                    [] p2.receive {

                        // nested alt level 2
                        alt {
                            [] p2.receive ( msg_b ) {
                            }
                            [] p2.receive ( msg_c ) {
                                setverdict ( pass );
                            }
                            [] p2.receive {
                            }
                        }
                    }
                }
            }
        }
    }

}