2

HTTP インタラクション、つまり HTTPRequest/HTTPResponse のシーケンスをモデル化したいのですが、これをトランジション システムとしてモデル化しようとしています。以下を使用して、クラス State の順序付けを定義しました。

open util/ordering[State]

ここで、State は単なるメッセージのセットです。

sig State { 
    msgSet: set Message
}

(HTTPRequest->HTTPResponse) と (HTTPResponse->HTTPRequest) の各ペアは、移行システムのルールとして表されます。ルールは、ある状態から別の状態に移動できるようにする述語として Alloy で表現されます。

たとえば、これは特定の HTTPRequest が受信された後に HTTPResponse を生成するルールです。

pred rsp1 [s, s': State] {
    one msg: Request, msg':Response | (

       // Preconditions (previous Request)
    msg.method=get &&
    msg.address.url=sample_com &&

       // Postconditions (next Response)
    msg'.status=OK_200 &&

       // previous Request has to be in previous state
    msg in s.msgSet &&
       // Response generated is added to next state
    s'.msgSet = s.msgSet + msg' 
}

残念ながら、作成されたモデルは複雑すぎるようです。多数のルールがあり (上記のものよりも複雑ですが、同じパターンに従います)、実行は非常に遅くなります。

編集:特に、CNF の生成は非常に遅く、解決にはかなりの時間がかかります。

同様の移行システムをモデル化する方法について何か提案はありますか?

どうもありがとうございました！

4

1 に答える 1