SHARE
TWEET

Untitled

a guest May 19th, 2017 37 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. void get_rock_paper_or_scissors_async(struct rps_session* rps_session) //@ : thread_run_joinable
  2.  
  3.   //@ requires thread_run_pre(get_rock_paper_or_scissors_async)(rps_session, ?info);
  4.  
  5.   //@ ensures thread_run_post(get_rock_paper_or_scissors_async)(rps_session, info);
  6.  
  7. {
  8.  
  9.   //@ open thread_run_pre(get_rock_paper_or_scissors_async)(rps_session, info);
  10.  
  11.   int tmp = get_rock_paper_or_scissors(rps_session->socket);
  12.  
  13.   rps_session->result = tmp;
  14.  
  15.   //@ close thread_run_post(get_rock_paper_or_scissors_async)(rps_session, info);
  16.  
  17. }
  18.  
  19.  
  20.  
  21.  
  22.  
  23.  
  24.  
  25. /*@
  26.  
  27. predicate play_game_predicate(struct rps_session* rpssession) =
  28.    malloc_block_rps_session(rpssession);
  29.  
  30.    
  31.  
  32. predicate_family_instance thread_run_pre(get_rock_paper_or_scissors_async)(struct rps_session *rps_session, any info) =
  33.  
  34.   [1/2]rps_session->socket|-> ?socket &*& socket(socket) &*& rps_session->result |-> _;
  35.  
  36.  
  37.  
  38. predicate_family_instance thread_run_post(get_rock_paper_or_scissors_async)(struct rps_session *rps_session, any info) =
  39.  
  40.   [1/2]rps_session->socket|-> ?socket &*& socket(socket) &*& rps_session->result |-> _;
  41.  
  42.  
  43. @*/
  44.  
  45.  
  46.  
  47.  
  48.  
  49. //thread_run_post(get_rock_paper_or_scissors_async)(session, info);
  50.  
  51. void play_game(struct socket* socket1, struct socket* socket2)
  52.  
  53. //@ requires socket(socket1) &*& socket(socket2);
  54.  
  55. //@ ensures socket(socket1) &*& socket(socket2);
  56.  
  57. {
  58.  
  59.   bool finished = false;
  60.  
  61.   while(! finished)
  62.  
  63.   //@ invariant socket(socket1) &*& socket(socket2);
  64.  
  65.   {
  66.  
  67.     int choice1; int choice2; struct thread* thread;
  68.  
  69.     struct rps_session* rps_session = malloc(sizeof(struct rps_session));
  70.  
  71.     if(rps_session == 0) abort();
  72.  
  73.     rps_session->socket = socket1;
  74.  
  75.     //@ close thread_run_pre(get_rock_paper_or_scissors_async)(rps_session, unit);
  76.  
  77.     thread = thread_start_joinable(get_rock_paper_or_scissors_async, rps_session);
  78.  
  79.     choice2 = get_rock_paper_or_scissors(socket2);
  80.  
  81.     thread_join(thread);
  82.  
  83.     //@ open thread_run_post(get_rock_paper_or_scissors_async)(rps_session, _);
  84.  
  85.     choice1 = rps_session->result;
  86.  
  87.     free(rps_session);
  88.  
  89.     if(choice1 == choice2) {
  90.  
  91.       socket_write_string(socket1, "A draw! Try again.\r\n");
  92.  
  93.       socket_write_string(socket2, "A draw! Try again.\r\n");
  94.  
  95.     } else {
  96.  
  97.       finished = true;
  98.  
  99.       if(choice1 == rock && choice2 == scissors ||
  100.  
  101.          choice1 == paper && choice2 == rock ||
  102.  
  103.          choice1 == scissors && choice2 == paper)
  104.  
  105.       {
  106.  
  107.         socket_write_string(socket1, "You win.\r\n");
  108.  
  109.         socket_write_string(socket2, "You lose.\r\n");
  110.  
  111.       } else {
  112.  
  113.         socket_write_string(socket2, "You win.\r\n");
  114.  
  115.         socket_write_string(socket1, "You lose.\r\n");
  116.  
  117.       }
  118.  
  119.     }
  120.  
  121.   }
  122.  
  123. }
  124.  
  125.  
  126.  
  127.  
  128.  
  129.  
  130.  
  131. /*@
  132.  
  133. predicate_family_instance thread_run_data(start_session)(struct session* session) =
  134.  
  135.   session->socket |-> ?socket &*& socket(socket) &*& [1/2]session->mutex |-> ?mutex &*& session->games |-> ?games &*&
  136.  
  137.   malloc_block_session(session) &*& game_list(games);
  138.  
  139. @*/
  140.  
  141.  
  142.  
  143.  
  144.  
  145. void start_session(struct session* session) //@ : thread_run
  146.  
  147. //@ requires thread_run_data(start_session)(session);
  148.  
  149. //@ ensures true;
  150.  
  151. {
  152.  
  153.   //@ open thread_run_data(start_session)(session);
  154.  
  155.   main_menu(session->socket, session->mutex, session->games);
  156.  
  157.   free(session);
  158.  
  159. }
  160.  
  161.  
  162.  
  163. void join_game_core(struct socket* socket, struct mutex* mutex, struct game_list* games, struct game* joined_game)
  164.  
  165. //@ requires socket(socket) &*& game_name(joined_game, ?name) &*& string_buffer(name) &*& game_socket(joined_game, ?other_socket) &*& socket(other_socket);//string_buffer(socket);
  166.  
  167. //@ ensures true;
  168.  
  169. {
  170.  
  171.   struct session* session; struct thread* thread;
  172.  
  173.   socket_write_string(socket, "You have joined ");
  174.  
  175.   socket_write_string_buffer(socket, joined_game->name);
  176.  
  177.   socket_write_string(socket, ".\r\n");
  178.  
  179.   socket_write_string(joined_game->socket, "Another player joined your game.\r\n");
  180.  
  181.   string_buffer_dispose(joined_game->name);
  182.  
  183.   play_game(joined_game->socket, socket);
  184.  
  185.   session = malloc(sizeof(struct session));
  186.  
  187.   if(session == 0) abort();
  188.  
  189.   session->socket = joined_game->socket;
  190.  
  191.   session->mutex = mutex;
  192.  
  193.   session->games = games;
  194.  
  195.   //@ close thread_run_data(start_session)(session);
  196.  
  197.   thread_start(start_session, session);
  198.  
  199.   free(joined_game);
  200.  
  201. }
RAW Paste Data
Want to get better at C?
Learn to code C in 2017
Top