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?