timed global protocol Choice(role A, role B, role C) {
    choice at A
    {
        Test1() from A to B within [0;1] using a and resetting ();
        Test2(payload) from A to B within [0;1] using a and resetting ();
        Test3() from A to B within [0;1] using a and resetting (a);
        Test4(payload) from A to B within [0;1] using a and resetting (a);
        Test5(payload) from A to C within [0;1] using a and resetting ();
    } or {
        Test5(payload) from A to B within [0;1] using a and resetting ();
        Test6(payload) from A to B within [0;1] using a and resetting ();
        Test7() from A to B within [0;1] using a and resetting (a);
        Test8(payload) from A to B within [0;1] using a and resetting (a);
        Test5(payload) from A to C within [0;1] using a and resetting ();
    } or {
        Test5(payload) from A to B within [0;1] using a and resetting ();
        Test6(payload) from A to B within [0;1] using a and resetting ();
        Test7() from A to B within [0;1] using a and resetting (a);
        Test8(payload) from A to B within [0;1] using a and resetting (a);
        Test5(payload) from A to C within [0;1] using a and resetting ();
    }
}