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 {
    money x1;
    S1(int x) { // State constructor that builds in the behavior we wanted to implement in Start.t().
      x1 = x;
      ->S2();
    }
  }

  state S2 {
    money m2;
    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, call transaction c and return the resulting int. If you are in S3, call transaction d and return 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?