interface
  # beginning state
  state user-unknown
    begin here
    subject must not have attribute "username"

  # end state
  state user-account
    subject must have attribute "username"

  # process that needs to be implemented
  process user-new-account
    required as input "email", "username", and "passphrase"
    produces attribute user "username"  

  # transition between beginning and end states 
  transition
    from user-unknown
    to user-account
    via user-new-account