State transition exercises

Below are 3 options for possible ways to write state transitions in Obsidian. All of these example contracts behave identically; the only difference is the code syntax.

Option 1

contract C {
    state Start {
        transaction a(int x) {
            ->S1(x)
        }
    }

    state S1 {
        int x1;
        S1(int x) { // State constructor that builds in the behavior we wanted to implement in Start.t().
            x1 = x;
            ->S2(x1);
        }
    }

    state S2 {
        int x2;
        S2(int x) { // State constructor that builds in the behavior we wanted to implement in S1.S1().
            x2 = x;
        }
    }
}

Option 2

contract C {
    state Start {
        transaction t(int x) {
            this <- S1{x1 = x}
              then toS2();
        }
    }

    state S1 {
        int x1;

        transaction toS2() {
            this <- S2{x2 = x1};
        }
    }

    state S2 {
        int x2;
    }
}

Option 3

contract C {
    state Start {
        transaction t(int x) {
            ->S1({x1 = x})
            in S1 {
            // Asserts that the state is S1 and either proceeds or throws an exception.
                ->S2({x2 = x1})
            }
            in S2 {
            // Actually, we don't need to do anything in this case, but this is here as an example.
            }
            x = … // This code runs only if the current state is Start. This code happens to be unreachable (for which the compiler gives an error).
        }
    }

    state S1 {
        int x1;
    }

    state S2 {
        int x2;
    }
}

You are provided with an unfinished Obsidian contract below. Your task is to implement transactions 'a' and 'b' with the correct behavior. Here is what these transaction should do:

• 'a' transitions to S1, with S1's x1 field equal to x, and whichState1 field equal to whichState.
• 'a' calls transaction 'b'.
  • 'b' transitions to S2 if whichState1 is equal to true (with S2's x2 field equal to x1), and transitions to S3 otherwise (with S3's x3 field equal to x1).
• If you are in S2 after calling 'b', 'a' calls transaction c and returns the resulting int. If you are in S3 after calling 'b', 'a' calls transaction d and returns the resulting int. Implement this transaction once using each style of state transition (so three times total). You can add additional code outside of transaction 'a' if it is necessary. Places where you should add transitions are marked with //TODO.

main contract C {
    state Start {
        transaction a(int x, bool whichState) returns int {
            //a returns c() if you are in S2, and d() if you are in S3.
            //TODO
        }
    }

    state S1 {
        int x1;
        bool whichState1;

        transaction b() {
            //TODO
        }
    }

    state S2 {
        int x2;

        transaction c() returns int {
            x2 = x2 * 2;
            return x2;
        }
    }

    state S3 {
        int x3;

        transaction d() returns int {
            x3 = x3 * 3;
            return x3;
        }
    }
}

Is there anything confusing about each of the styles of state transition? Which do you prefer, and why?