PropErでの並列ステートフルテストの実現方法推測メモ
コマンド列が並列に処理された場合に、モデルの更新をどう行っているのか、を推測してみたメモ。
案1: 実行結果をモデル管理プロセスに送信する
コマンドの実行が終わった時点で、そのコマンドと実行結果をモデル管理プロセスに送信して、処理を行う。
ただし「実行が終わってメッセージを送信した順」が「実際に操作が実行された順(線形化点)」と一致する保証はないので、これではタイミング依存で、モデルが実体から乖離してしまいそう。
案2: 並列実行の組み合わせ分だけモデルを分岐させる
例えばAとBのコマンドが並列して実行された場合には、その度にモデルの複製を用意して「A=>B」と「B=>A」の二通りの順番で、モデルにコマンドを適用する。
また、その際に、事後条件が崩れたバージョンは捨ててしまう。全てのモデルで事後条件が崩れた場合には、全体の失敗とみなす。
これは上手く動作しそうだが、並列度が高いとメモリ使用量や計算量が極端に増えてしまいそうなのが気になる。