void get_rock_paper_or_scissors_async(struct rps_session* rps_session) //@ : thread_run_joinable

  //@ requires thread_run_pre(get_rock_paper_or_scissors_async)(rps_session, ?info);

  //@ ensures thread_run_post(get_rock_paper_or_scissors_async)(rps_session, info);

{

  //@ open thread_run_pre(get_rock_paper_or_scissors_async)(rps_session, info);

  int tmp = get_rock_paper_or_scissors(rps_session->socket);

  rps_session->result = tmp;

  //@ close thread_run_post(get_rock_paper_or_scissors_async)(rps_session, info);

}







/*@

predicate play_game_predicate(struct rps_session* rpssession) =
   malloc_block_rps_session(rpssession);



predicate_family_instance thread_run_pre(get_rock_paper_or_scissors_async)(struct rps_session *rps_session, any info) =

  [1/2]rps_session->socket|-> ?socket &*& socket(socket) &*& rps_session->result |-> _;



predicate_family_instance thread_run_post(get_rock_paper_or_scissors_async)(struct rps_session *rps_session, any info) =

  [1/2]rps_session->socket|-> ?socket &*& socket(socket) &*& rps_session->result |-> _;


@*/





//thread_run_post(get_rock_paper_or_scissors_async)(session, info);

void play_game(struct socket* socket1, struct socket* socket2)

//@ requires socket(socket1) &*& socket(socket2);

//@ ensures socket(socket1) &*& socket(socket2);

{

  bool finished = false;

  while(! finished)

  //@ invariant socket(socket1) &*& socket(socket2);

  {

    int choice1; int choice2; struct thread* thread;

    struct rps_session* rps_session = malloc(sizeof(struct rps_session));

    if(rps_session == 0) abort();

    rps_session->socket = socket1;

    //@ close thread_run_pre(get_rock_paper_or_scissors_async)(rps_session, unit);

    thread = thread_start_joinable(get_rock_paper_or_scissors_async, rps_session);

    choice2 = get_rock_paper_or_scissors(socket2);

    thread_join(thread);

    //@ open thread_run_post(get_rock_paper_or_scissors_async)(rps_session, _);

    choice1 = rps_session->result;

    free(rps_session);

    if(choice1 == choice2) {

      socket_write_string(socket1, "A draw! Try again.\r\n");

      socket_write_string(socket2, "A draw! Try again.\r\n");

    } else {

      finished = true;

      if(choice1 == rock && choice2 == scissors ||

         choice1 == paper && choice2 == rock ||

         choice1 == scissors && choice2 == paper)

      {

        socket_write_string(socket1, "You win.\r\n");

        socket_write_string(socket2, "You lose.\r\n");

      } else {

        socket_write_string(socket2, "You win.\r\n");

        socket_write_string(socket1, "You lose.\r\n");

      }

    }

  }

}







/*@

predicate_family_instance thread_run_data(start_session)(struct session* session) =

  session->socket |-> ?socket &*& socket(socket) &*& [1/2]session->mutex |-> ?mutex &*& session->games |-> ?games &*&

  malloc_block_session(session) &*& game_list(games);

@*/





void start_session(struct session* session) //@ : thread_run

//@ requires thread_run_data(start_session)(session);

//@ ensures true;

{

  //@ open thread_run_data(start_session)(session);

  main_menu(session->socket, session->mutex, session->games);

  free(session);

}



void join_game_core(struct socket* socket, struct mutex* mutex, struct game_list* games, struct game* joined_game)

//@ requires socket(socket) &*& game_name(joined_game, ?name) &*& string_buffer(name) &*& game_socket(joined_game, ?other_socket) &*& socket(other_socket);//string_buffer(socket);

//@ ensures true;

{

  struct session* session; struct thread* thread;

  socket_write_string(socket, "You have joined ");

  socket_write_string_buffer(socket, joined_game->name);

  socket_write_string(socket, ".\r\n");

  socket_write_string(joined_game->socket, "Another player joined your game.\r\n");

  string_buffer_dispose(joined_game->name);

  play_game(joined_game->socket, socket);

  session = malloc(sizeof(struct session));

  if(session == 0) abort();

  session->socket = joined_game->socket;

  session->mutex = mutex;

  session->games = games;

  //@ close thread_run_data(start_session)(session);

  thread_start(start_session, session);

  free(joined_game);

}