dtmc

module clienttserver
  // 状態 
  t : [1..8] init 1;
  // 再試行回数
  retried : [0..1] init 0;
  // サーバでの実際の結果（0:未実行，1:成功，2：失敗）
  result : [0..2] init 0;

  // 「リクエスト送信」から「サーバ処理中」または「タイムアウト」へ
  [comm_request] (t=1) -> 0.9:(t'=2) + 0.1:(t'=4);
  // 未処理のときは「サーバ処理」から成功または失敗して「結果通知」へ
  [process] (t=2)&(result=0) -> 0.5:(result'=1)&(t'=3) + 0.5:(result'=2)&(t'=3);
  // 処理済みのときは「サーバ処理」から「結果通知」へ
  [skip] (t=2)&(result!=0) -> (t'=3);
  // 「結果通知」から「結果受信」または「タイムアウト」へ
  [comm_reply] (t=3) -> 0.9:(t'=5) + 0.1:(t'=4);
  // 最初の試行のときは「タイムアウト」から「リクエスト送信」へ
  [timeout0] (t=4)&(retried=0) -> (t'=1)&(retried'=1);
  // 再試行のときは「タイムアウト」から「クライアントは結果把握できず」へ
  [timeout1] (t=4)&(retried=1) -> (t'=8);
  // 成功のとき「結果受信」から「クライアントは成功把握」へ
  [receive_success] (t=5)&(result=1) -> (t'=6);
  // 失敗のとき「結果受信」から「クライアントは失敗把握」へ
  [receive_failure] (t=5)&(result=2) -> (t'=7);
  // 「クライアントは成功把握」
  [exit_success] t=6 -> (t'=6);
  // 「クライアントは失敗把握」
  [exit_failure] t=7 -> (t'=7);
  // 「クライアントは結果把握できず」
  [exit_unkown] t=8 -> (t'=8);

endmodule

// サーバー側が成功するがクライアント側は不明となる確率
// P=? [ ( F result=1 ) & ( F t=8 ) ]