pbft.maude

*** 时间相关
fmod NAT-TIME is pr NAT .
    sorts Time NzTime TimeInf . subsort NzTime < Time < TimeInf .
    subsort Nat < Time . 
    subsort NzNat < NzTime .
    op oo : -> TimeInf [ctor] . --- infinity value
    vars T T1 : Time . var TI : TimeInf . vars N N1 : Nat .
    --- extend operators to infinity:
    op _<=_ : Time TimeInf -> Bool [ditto] .
    op min : TimeInf TimeInf -> TimeInf [ditto] .
    op _monus_ : TimeInf Time -> TimeInf .
    eq T <= oo = true . eq min(oo, TI) = TI .
    eq N monus N1 = if N1 <= N then sd(N, N1) else 0 fi .
    eq oo monus N = oo .
endfm

*** 重新定义configuration以用来重新定义格式
mod CONFIGURATION is
  sorts Attribute AttributeSet .
  subsort Attribute < AttributeSet .
  op none : -> AttributeSet  [ctor] .
  op _,_ : AttributeSet AttributeSet -> AttributeSet [ctor assoc comm id: none] .

  sorts Oid Cid Object Msg Portal Configuration .
  subsort Object Msg Portal < Configuration .
  op <_:_|_> : Oid Cid AttributeSet -> Object [ctor object] .
  op none : -> Configuration [ctor] .
  op __ : Configuration Configuration -> Configuration [ctor config assoc comm id: none  format(n n o)] .
  op <> : -> Portal [ctor] .
endm


mod OO-TIMED-PRELUDE is pr NAT-TIME .
    including CONFIGURATION .
    pr RANDOM .
    sorts GlobalState ClockedState .
    subsort GlobalState < ClockedState .
    op `{_`} : Configuration -> GlobalState [ctor] .
    op _in`time_ : GlobalState Time -> ClockedState [ctor format(d d d g o)] .
    var CLS : ClockedState . vars T T1 T2 : Time .
    vars CONF1 CONF2 : Configuration .
    eq (CLS in time T1) in time T2 = CLS in time (T1 + T2) .
    op timeEffect : Configuration Time -> Configuration .  ***将时间作用于Configuration
    eq timeEffect(none,T) = none .
    ceq timeEffect(CONF1 CONF2 , T ) = timeEffect(CONF1, T) timeEffect(CONF2, T)
        if CONF1 =/= none /\ CONF2 =/= none .
    *** 求一个configuration能经过最长的时间
    op mte : Configuration -> TimeInf [frozen (1)] .
    eq mte(none) = oo .
    ceq mte(CONF1 CONF2) = min(mte(CONF1), mte(CONF2))
                 if CONF1 =/= none /\ CONF2 =/= none .

    var CONF : Configuration .
    var N : Nat .
    ***var T : Time .
    op time-seed : -> Nat .
    eq time-seed = 12 .
    op max-time-interval : -> Nat .
    eq max-time-interval = 100 .
    op _%_ : Nat NzNat -> Nat .
    var NZN : NzNat .
    eq N % NZN = N rem NZN . *** 取余数用更清晰的表记法
    *** add nonexec to disable the rewriting rules 设置nonexec避免maude调用
    rl [tick-start] :
    {CONF} => if mte(CONF) == oo 
                              then {timeEffect(CONF, ( random(time-seed) % max-time-interval ) )} in time (random(time-seed) % max-time-interval)
                              else {timeEffect(CONF, (random(time-seed) % mte(CONF)))} in time (random(time-seed) % mte(CONF))
                              fi [nonexec] .
    rl [tick] :
    {CONF} in time N => if mte(CONF) == oo 
                              then {timeEffect(CONF,random(N) % max-time-interval)} in time (random(N) % max-time-interval) + N
                              else {timeEffect(CONF,random(N) % mte(CONF))} in time ( N + ( random(N) % mte(CONF) ))
                              fi [nonexec] .

endm

***( 将 TRIV 映射到 CONFIGURATION 的 Oid ，便于使用 Set{Oid} )

view Oid from TRIV to CONFIGURATION is
  sort Elt to Oid .
endv

mod INTERFACE is
  pr OO-TIMED-PRELUDE .
  pr SET{Oid} .
  sort MsgCont .
  *** State是消息的类型，也是当前节点的状态
  sort State .
  ops pre-prepare prepare commit commit-local complete view-change reply : -> State [ctor format(b o)].
  ops request-start request : -> State [ctor format(b o)] .
  sort MsgType .
  subsort State < MsgType .
  op <_|_>  : MsgType AttributeSet -> MsgCont [ctor] . ***定义消息的内容
  op msg_from_to_ : MsgCont Oid Oid -> Msg [ctor format (yu ou u u u u o)] .
  
  sort Log .
  subsort MsgCont < Log .
  *** define the list of msg
  sort Msgs .
  subsort Msg < Msgs .
  *** to avoid ambiguousity.( could not use List{Msg} ) 因为用不了List{Msg}，所以只能定义一个Msgs类型
  op empty : -> Msgs [ctor] .
  op _,_ : Msgs Msgs -> Msgs [ ctor assoc id: empty format(o r o o)] .
  op multicast_from_to_ : MsgCont Oid Set{Oid} -> Msgs . *** 群发消息
  
  
  var M : MsgCont .
  vars O O2 : Oid .
  var OS : Set{Oid} .
  eq multicast M from O to empty = empty .
  eq multicast M from O to (O2 , OS) = (msg M from O to O2),multicast M from O to OS . 
  
  
  op Clock : -> Cid [ctor] .
  op time`:_ : Time -> Attribute [ctor] .
  vars T T1 : Time .
  var AS : AttributeSet .
  
  eq mte(< O : Clock | time : T >) = oo .
  eq timeEffect(< O : Clock | time : T1 , AS > , T ) = < O : Clock | time : (T1 + T) , AS > .

endm


view Log from TRIV to INTERFACE is
  sort Elt to Log .
endv

view State from TRIV to INTERFACE is
  sort Elt to State .
endv
view MsgCont from TRIV to INTERFACE is
  sort Elt to MsgCont .
endv

*** 定义节点共有的部分
mod NODE is
    pr INTERFACE .
    pr LIST{Log} . *** use like the template in C++ 空的是nil 用空格连接
    pr LIST{Nat} .
    pr MAP{Nat,State} .
    pr MAP{MsgCont,List{Log}} .
    subsort Nat < Oid .
    op Node : -> Cid [ctor] .
    sort NodeType .
    *** define the role of the node 
    ops BACKUP CLIENT PRIMARY : -> NodeType [ctor format (!b o)] .
    op nodeType`:_ : NodeType -> Attribute [ctor] . 
    
    op view`:_ : Nat -> Attribute [ctor] . *** current view
    op seq`:_ : Nat -> Attribute [ctor] . *** the msg sequence number
    op original-msg`:_ : MsgCont -> Attribute [ctor] . *** the original msg
    op rcv-buffer`:_ : Msgs -> Attribute [ctor] . *** receive buffer where sent msg is saved
    op snd-buffer`:_ : Msgs -> Attribute [ctor] . *** send buffer where 
    op timestamp`:_ : Nat -> Attribute [ctor] . *** the time when the msg is sent
    op r-num`:_ : Nat -> Attribute [ctor] . *** the number of replicas 
    op states`:_ : Map{Nat,State} -> Attribute [ctor format(u o b o)] . *** the current state
    op trust-num`:_ : Nat -> Attribute [ctor] . *** the trust number
    op logs`:_ : Map{MsgCont,List{Log}} -> Attribute [ctor] . *** the logs in backup
    op operation`:_ : Nat -> Attribute [ctor] . *** the operation client request . for convenience，we assume the operation is writing a number .
    op current-num`:_ : List{Nat} -> Attribute [ctor format(o o g o)] . *** the current num the replica save .
    op client`:_ : Oid -> Attribute [ctor] . *** client number
    op source`:_ : Oid -> Attribute [ctor] . *** the SOURCE OF msg
	***( 
    function that can judge whether a node could accept a msg(same view v and seq n but different digest) 
    )
    vars MSG MSG1 : Msg .
    vars MSGS MSGS1 : Msgs .
    vars LOGS LOGS1 : List{Log} .
    vars MTYPE MTYPE1 : MsgType .
    vars O O1 O2 O3 : Oid .
    vars N1 N2 N VIEW1 VIEW2 VIEW : Nat .
    vars AS AS1 : AttributeSet .
    vars MCONT MCONT1 : MsgCont . 
    
    op _contains_ : List{Log} Log -> Bool .
    eq (LOGS MCONT1) contains MCONT1 = true .
    eq (LOGS MCONT) contains MCONT1 = LOGS contains MCONT1 [owise].
    eq nil contains MCONT = false .

    op operation : MsgCont -> Nat .
    eq operation( < MTYPE | operation : N , AS > ) = N .

    op cli : MsgCont -> Oid .
    eq cli( < MTYPE | (client : O) , AS > ) = O .

    op countMsg : List{Log} MsgType Nat Nat MsgCont -> Nat .
    eq countMsg(LOGS < MTYPE1 | view : VIEW1 , original-msg : MCONT1 , AS > ,MTYPE,VIEW,N,MCONT) = 
        if MTYPE == MTYPE1 and VIEW == VIEW1 and MCONT1 == MCONT  
               then s countMsg(LOGS ,MTYPE,VIEW,N,MCONT)
                else countMsg(LOGS ,MTYPE,VIEW,N,MCONT) fi .
    eq countMsg(LOGS < MTYPE1 | AS >,MTYPE,VIEW,N,MCONT) = countMsg(LOGS,MTYPE,VIEW,N,MCONT) [owise] .
    eq countMsg(nil,MTYPE,VIEW,N,MCONT) = 0 .
    op range : Nat Nat -> Set{Oid} . *** to generate receiver set for multicast 为了multicast目的地址来写了range生成。
    eq range(N,N1) = if N < N1 then N,range(s N,N1) else empty fi .
    eq timeEffect(< O : Node |  AS >, N1) =  < O : Node |  AS > .
    eq mte(< O : Node |  AS >) = oo .
endm

*** 修改了primary和backup的一部分rl，本意是想减少状态数，后来分析还是没有减少状态数。

mod PRIMARY-EX is 
    ex NODE .
    
    vars O O1 O2 : Oid .
    vars C C1 C2 : Configuration .
    vars MSGS MSGS1 : Msgs .
    vars MSG1 MSG : Msg .
    vars MCONT MCONT1 MCONT2 MCONT3 : MsgCont .
    vars AS AS1 AS2 AS3  : AttributeSet .
    vars LOGS LOGS1 : Map{MsgCont,List{Log}} .
    vars LOGLIST LOGLIST1 LOGLIST2 : List{Log} .
    vars CURNUMS CURNUMS1 : List{Nat} .
    vars MTYPE MTYPE1 : MsgType .
    vars SMAP SMAP1 : Map{Nat,State} .
    vars T T1 : Time .
    eq timeEffect(< O : Node |  nodeType : PRIMARY  , AS > ,T) = < O : Node |  nodeType : PRIMARY  , AS > .
    eq mte(< O : Node |  nodeType : PRIMARY  , AS >) = oo .
    vars N N1 N2 N3 VIEW VIEW1 VIEW2 : Nat .
    *** rcv the request and multicast the pre-prepare msg 接收到请求消息，然后转换成pre=prepare发送pre-prepare消息
    rl [rcv-client-request]:
    < O : Node |  nodeType : PRIMARY ,
                 seq : N,
                 rcv-buffer : ((msg < request | AS1 > from O1 to O), MSGS) ,
                 snd-buffer : MSGS1,
                 view : VIEW ,
                 states : SMAP ,
                 logs : LOGS ,  
                 r-num : N1,
                 AS > =>
    < O : Node |  nodeType : PRIMARY ,
                  seq : s N, 
                  r-num : N1,
                  view : VIEW,
                  logs : (LOGS,< request | AS1 > |-> <  pre-prepare | original-msg : ( <  request | AS1 > ) ,
                                                                        seq : N  ,
                                                                        source : O ,
                                                                        view : VIEW >) ,
                  rcv-buffer : MSGS ,
                  states : (SMAP,N |-> prepare) ,
                  snd-buffer : (MSGS1,multicast <  pre-prepare | original-msg : ( <  request | AS1 > ) ,
                                                                        seq : N  ,
                                                                        source : O ,
                                                                        view : VIEW > from O to range(0,N1) \ O ),
                  AS > [print "primary " O " receives the request and multicast it to other backups"] .
    *** defines how primary acts when having received prepare msg. PRIMARY节点接受prepare消息
    rl [primary-rcv-prepare-msg] :
        < O : Node |  nodeType : PRIMARY ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : ((msg <  MTYPE | view : VIEW1 , seq : N , original-msg : MCONT1 , source : N3 , AS1 > from O1 to O), MSGS ) ,
                  states : SMAP,
                  logs : (LOGS,MCONT1 |-> LOGLIST) ,
                  AS > =>
    *** 预准备消息的序号n必须在水线（watermark）上下限h和H之间。（暂时忽略）
    *** if same v and the request has not been accepted by the node .请求和预准备消息的签名正确,摘要也相同(这里直接变成判断消息是否相等)
        if VIEW == VIEW1 
          and SMAP[N] == prepare
          and MTYPE == prepare
          and not ( LOGLIST contains <  prepare | seq : N , view : VIEW1 , original-msg : MCONT1 , source : N3 , AS1 >  )
        then
        < O : Node |  nodeType : PRIMARY ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  states : SMAP,
                  logs : (LOGS , MCONT1 |-> (LOGLIST < prepare | seq : N , view : VIEW1 , original-msg : MCONT1 , source : N3 , AS1 >) ) ,
                  AS >
        else
        < O : Node |  nodeType : PRIMARY ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  states : SMAP,
                  logs : (LOGS,MCONT1 |-> LOGLIST) ,
                  AS >
        fi [print "primary " O " receives the prepare msg from " O1 ] .
    *** nodes having received enough msgs will turn into commit state 接收到足够的消息，转换成commit状态
    crl [primary-into-commit]:
        < O : Node |  nodeType : PRIMARY ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  snd-buffer : MSGS1 ,
                  states : (SMAP , N |-> prepare),
                  logs : (LOGS,(MCONT |-> (LOGLIST < prepare | seq : N , view : VIEW , original-msg : MCONT , AS1 > LOGLIST1))) ,
                  AS > =>
        < O : Node |  nodeType : PRIMARY ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  snd-buffer : ( MSGS1 , multicast < commit | seq : N ,view : VIEW , original-msg : MCONT , source : O > from O to range(0,N1) \ O ) ,
                  states : (SMAP , N |-> commit),
                  logs : (LOGS,(MCONT |-> (LOGLIST < prepare | seq : N , view : VIEW , original-msg : MCONT , AS1 > LOGLIST1))) ,
                  AS >
        if (sd(N1,1) quo 3) * 2 <= 
           countMsg(LOGLIST < prepare | seq : N , view : VIEW , original-msg : MCONT , AS1 > LOGLIST1 , prepare,VIEW,N,MCONT) [print "primary " O " turns into commit " ].
        *** f = (N1 - 1) / 3 receiving more than 2f msgs will turn backup to commit 接收到2f个消息。
    *** 这里接受条件暂时变成接受2f个commit消息
    rl [primary-rcv-commit-msg]:
        < O : Node |  nodeType : PRIMARY ,
                  view : VIEW,
                  rcv-buffer : ((msg <  MTYPE | seq : N , view : VIEW1 , original-msg : MCONT , source : O1 , AS1 > from O1 to O), MSGS ) ,
                  states : SMAP ,
                  logs : (LOGS,(MCONT |-> LOGLIST)) ,
                  AS > =>
    *** if same v , same seq n and same msg digest ,accept it .
    if VIEW == VIEW1 
       and SMAP[N] == commit
       and MTYPE == commit
       and not (LOGLIST contains <  commit | seq : N , view : VIEW1 , original-msg : MCONT , source : O1 , AS1 > )
        then
        < O : Node |  nodeType : PRIMARY ,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  states : SMAP,
                  logs : (LOGS,(MCONT |-> LOGLIST < commit | seq : N , view : VIEW1 , seq : N , original-msg : MCONT , source : O1 , AS1 >)  ) ,
                  AS >
        else
        < O : Node |  nodeType : PRIMARY ,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  states : SMAP,
                  logs : LOGS ,
                  AS >
        fi [print "primary " O " receives the commit msg" ].
    *** when the node receives enough msgs , operate and respond to the client
    crl [primary-respond-client-request]:
        < O : Node |  nodeType : PRIMARY ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  snd-buffer : MSGS1 ,
                  states : (SMAP,N |-> commit),
                  current-num : CURNUMS ,
                  logs : (LOGS,(MCONT |-> LOGLIST < commit | seq : N ,view : VIEW1 , original-msg : < request | client : O1 , operation : VIEW2 , AS2 > , AS1 > LOGLIST1)) ,
                  AS > =>
        < O : Node |  nodeType : PRIMARY ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  snd-buffer : (MSGS1,msg < reply | seq : N , view : VIEW , original-msg : < request | client : O1 , operation : VIEW2 , AS2 >  > from O to O1 ) ,
                  states : (SMAP,N |-> complete),
                  current-num : (CURNUMS VIEW2) ,
                  logs : (LOGS,(MCONT |-> LOGLIST < commit | seq : N ,view : VIEW1 , original-msg : < request | client : O1 , operation : VIEW2 , AS2 > , AS1 > LOGLIST1)) ,
                  AS >
        if (sd(N1,1) quo 3) * 2 <= 
           countMsg(LOGLIST < commit | seq : N , view : VIEW , original-msg : < request | client : O1 , operation : VIEW2 , AS2 > ,AS1 > LOGLIST1 , commit,VIEW,N,< request | client : O1 , operation : VIEW2 , AS2 >) 
        [print "primary " O " respond to the client " O1 ] . *** f = (N1 - 1) / 3 receiving more than 2f msgs will turn backup to commit 
endm

mod BACKUP-EX is
    ex NODE .
    
    vars O O1 O2 : Oid .
    vars C C1 C2 : Configuration .
    vars MSGS MSGS1 : Msgs .
    vars MSG1 MSG : Msg .
    vars MTYPE MTYPE1 : MsgType .
    vars MCONT MCONT1 MCONT2 MCONT3 : MsgCont .
    vars AS AS1 AS2 AS3  : AttributeSet .
    vars LOGS LOGS1 : Map{MsgCont,List{Log}} .
    vars LOGLIST LOGLIST1 LOGLIST2 : List{Log} .
    vars CURNUMS CURNUMS1 : List{Nat} .
    vars SMAP SMAP1 : Map{Nat,State} .
    vars T T1 : Time .
    eq timeEffect(< O : Node |  nodeType : PRIMARY  , AS > ,T) = < O : Node |  nodeType : PRIMARY  , AS > .
    eq mte(< O : Node |  nodeType : PRIMARY  , AS >) = oo .
    vars N N1 N2 N3 VIEW VIEW1 VIEW2 : Nat .

    *** ( receive pre-prepare msg and turn into prepare state )
    rl [rcv-pre-prepare]:
    < O : Node |  nodeType : BACKUP ,
                  r-num : N1 ,
                  view : VIEW,
                  rcv-buffer : ((msg <  pre-prepare | seq : N2 , original-msg : MCONT , view : VIEW1 , source : O1 , AS1 > from O1 to O), MSGS) ,
                  states : SMAP ,
                  snd-buffer : MSGS1 ,
                  logs : LOGS ,
                  AS > =>
    *** 预准备消息的序号n必须在水线（watermark）上下限h和H之间。（暂时忽略）
    *** if same v and the request has not been accepted by the node .请求和预准备消息的签名正确,摘要也相同(这里直接变成判断消息是否相等)
    if VIEW == VIEW1 
       and SMAP[N2] == undefined
       and LOGS[MCONT] == undefined
    then 
    < O : Node |  nodeType : BACKUP ,
                  r-num : N1 ,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  snd-buffer : ( MSGS1 , multicast <  prepare | seq : N2 , view : VIEW1 , original-msg : MCONT , source : O > from O to range(0,N1) \ O ) ,
                  states : (SMAP,N2 |-> prepare),
                  logs : (LOGS,MCONT |->(<  pre-prepare | seq : N2 , original-msg : MCONT , view : VIEW1 , source : O1 , AS1 > )),
                  AS >
    else
    < O : Node |  nodeType : BACKUP ,
                  r-num : N1 ,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  states : SMAP ,
                  snd-buffer : MSGS1 ,
                  logs : LOGS ,
                  AS >
    fi [print "backup " O " receives the pre-prepare msg " ] .
    ***(For convenience，we receive an prepare msg by determining whether view v and seq n are same) 
    *** 是否是同样的view v 序号n满足水线限制（这里变成是否相等），消息签名是否一样（这里直接判断消息是否一样）
    *** defines how backup acts when having received prepare msg. BACKUP节点接受prepare消息
    rl [backup-rcv-prepare-msg] :
        < O : Node |  nodeType : BACKUP ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : ((msg <  MTYPE | view : VIEW1 , seq : N , original-msg : MCONT1 , source : N3 , AS1 > from O1 to O), MSGS ) ,
                  states : SMAP,
                  logs : (LOGS,MCONT1 |-> LOGLIST) ,
                  AS > =>
    *** 预准备消息的序号n必须在水线（watermark）上下限h和H之间。（暂时忽略）
    *** if same v and the request has not been accepted by the node .请求和预准备消息的签名正确,摘要也相同(这里直接变成判断消息是否相等)
        if VIEW == VIEW1 
          and SMAP[N] == prepare
          and MTYPE == prepare  
          and not ( LOGLIST contains <  prepare | seq : N , view : VIEW1 , original-msg : MCONT1 , source : N3 , AS1 >  )
        then
        < O : Node |  nodeType : BACKUP ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  states : SMAP,
                  logs : (LOGS , MCONT1 |-> (LOGLIST < prepare | seq : N , view : VIEW1 , original-msg : MCONT1 , source : N3 , AS1 >) ) ,
                  AS >
        else
        < O : Node |  nodeType : BACKUP ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  states : SMAP,
                  logs : (LOGS,MCONT1 |-> LOGLIST) ,
                  AS >
        fi [print "backup " O " receives the prepare msg from " O1 ] .
    *** nodes having received enough msgs will turn into commit state 接收到足够的消息，转换成commit状态
    crl [backup-into-commit]:
        < O : Node |  nodeType : BACKUP ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  snd-buffer : MSGS1 ,
                  states : (SMAP , N |-> prepare),
                  logs : (LOGS,(MCONT |-> (LOGLIST < prepare | seq : N , view : VIEW , original-msg : MCONT , AS1 > LOGLIST1))) ,
                  AS > =>
        < O : Node |  nodeType : BACKUP ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  snd-buffer : ( MSGS1 , multicast < commit | seq : N ,view : VIEW , original-msg : MCONT , source : O > from O to range(0,N1) \ O ) ,
                  states : (SMAP , N |-> commit),
                  logs : (LOGS,(MCONT |-> (LOGLIST < prepare | seq : N , view : VIEW , original-msg : MCONT , AS1 > LOGLIST1))) ,
                  AS >
        if (sd(N1,1) quo 3) * 2 <= 
           countMsg(LOGLIST < prepare | seq : N , view : VIEW , original-msg : MCONT , AS1 > LOGLIST1 , prepare,VIEW,N,MCONT) [print "backup " O " turns into commit " ].
        *** f = (N1 - 1) / 3 receiving more than 2f msgs will turn backup to commit 接收到2f个消息。
    *** 这里接受条件暂时变成接受2f个commit消息
    rl [backup-rcv-commit-msg]:
        < O : Node |  nodeType : BACKUP ,
                  view : VIEW,
                  rcv-buffer : ((msg <  MTYPE | seq : N , view : VIEW1 , original-msg : MCONT , source : O1 , AS1 > from O1 to O), MSGS ) ,
                  states : SMAP ,
                  logs : (LOGS,(MCONT |-> LOGLIST)) ,
                  AS > =>
    *** if same v , same seq n and same msg digest ,accept it .
    if VIEW == VIEW1 
       and SMAP[N] == commit
       and MTYPE == commit
       and not (LOGLIST contains <  commit | seq : N , view : VIEW1 , original-msg : MCONT , source : O1 , AS1 > )
        then
        < O : Node |  nodeType : BACKUP ,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  states : SMAP,
                  logs : (LOGS,(MCONT |-> LOGLIST < commit | seq : N , view : VIEW1 , seq : N , original-msg : MCONT , source : O1 , AS1 >)  ) ,
                  AS >
        else
        < O : Node |  nodeType : BACKUP ,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  states : SMAP,
                  logs : (LOGS,(MCONT |-> LOGLIST)) ,
                  AS >
        fi [print "backup " O " receives the commit msg" ].
    *** when the node receives enough msgs , operate and respond to the client
    crl [backup-respond-client-request]:
        < O : Node |  nodeType : BACKUP ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  snd-buffer : MSGS1 ,
                  states : (SMAP,N |-> commit),
                  current-num : CURNUMS ,
                  logs : (LOGS,(MCONT |-> LOGLIST < commit | seq : N ,view : VIEW1 , original-msg : < request | client : O1 , operation : VIEW2 , AS2 > , AS1 > LOGLIST1)) ,
                  AS > =>
        < O : Node |  nodeType : BACKUP ,
                  r-num : N1,
                  view : VIEW,
                  rcv-buffer : MSGS ,
                  snd-buffer : (MSGS1,msg < reply | seq : N , view : VIEW , original-msg : < request | client : O1 , operation : VIEW2 , AS2 >  > from O to O1 ) ,
                  states : (SMAP,N |-> complete),
                  current-num : (CURNUMS VIEW2) ,
                  logs : (LOGS,(MCONT |-> LOGLIST < commit | seq : N ,view : VIEW1 , original-msg : < request | client : O1 , operation : VIEW2 , AS2 > , AS1 > LOGLIST1)) ,
                  AS >
        if (sd(N1,1) quo 3) * 2 <= 
           countMsg(LOGLIST < commit | seq : N , view : VIEW , original-msg : < request | client : O1 , operation : VIEW2 , AS2 > ,AS1 > LOGLIST1 , commit,VIEW,N,< request | client : O1 , operation : VIEW2 , AS2 >) 
        [print "backup " O " respond to the client " O1 ] . *** f = (N1 - 1) / 3 receiving more than 2f msgs will turn backup to commit 
endm

mod CLIENT-EX is
    ex NODE .
    vars O O1 O2 : Oid .
    vars C C1 C2 : Configuration .
    vars MSGS MSGS1 : Msgs .
    vars AS AS1 : AttributeSet .
    vars MCONT MCONT1 MCONT2 : MsgCont .
    op wait-for-reply : Nat -> State [ctor] .
    op wait-timeout : -> State [ctor] .
    op request-start : -> State [ctor format(b o)] .
    op max-waittime : -> Nat .
    eq max-waittime = 300 .
    op current-request`:_ : MsgCont -> Attribute [ctor] .
    op state`:_ : State -> Attribute [ctor] .
    op times`:_ : Nat -> Attribute [ctor] .
    vars N RN N1 N2 N3 : Nat .
    rl [snd-request]:
    < O : Node | view : N , times : s N1, state : request-start , r-num : RN , (snd-buffer : MSGS) , nodeType : CLIENT  , AS > =>
    < O : Node | view : N , times : N1 , state : wait-for-reply(max-waittime) , r-num : RN ,
                             trust-num : 0 ,
                             current-request : <  request | operation : random(O + N1) , client : O > ,
                             snd-buffer : ( MSGS,msg <  request | operation : random(O + N1) , client : O > from O to ( N % RN ) ) , nodeType : CLIENT , AS > 
                              [print "client " O " sends a request"] .
    rl [rcv-reply]:
    < O : Node | view : N , 
                 state : wait-for-reply(N2) , 
                trust-num : N1 , 
                r-num : RN , 
                current-request : MCONT ,
                rcv-buffer : ((msg < reply | original-msg : MCONT1 , AS1 > from O1 to O),MSGS) , 
                nodeType : CLIENT  , AS > =>
    if MCONT == MCONT1 then
    < O : Node | view : N , current-request : MCONT , state : wait-for-reply(N2) , trust-num : s N1 , r-num : RN , rcv-buffer : MSGS , nodeType : CLIENT  , AS > 
    else
    < O : Node | view : N , 
                 state : wait-for-reply(N2) , 
                trust-num : N1 , 
                r-num : RN , 
                current-request : MCONT ,
                rcv-buffer : MSGS , 
                nodeType : CLIENT  , AS >
    fi
                [print "client " O " receives a reply"] .
    ***client接受完回复消息后的操作
    crl [return-request-start]:
    < O : Node | view : N , state : wait-for-reply(N2) , current-request : MCONT ,trust-num : N1 , r-num : RN , rcv-buffer : MSGS , nodeType : CLIENT  , AS > =>
    < O : Node | view : N , state : request-start , r-num : RN , rcv-buffer : MSGS , nodeType : CLIENT  , AS > 
    if (sd(RN,1) quo 3) * 2 <= N1 .
    var T : Time .
    eq timeEffect(< O : Node |  nodeType : CLIENT , state : wait-for-reply(N) , AS >, N1) = 
                                 if N <= N1 then < O : Node |  nodeType : CLIENT , state : wait-timeout , AS >
                                        else < O : Node |  nodeType : CLIENT , state : wait-for-reply(sd(N1,N)) , AS > fi .
    --- eq timeEffect(< O : Node |  nodeType : CLIENT  , AS >,T) = < O : Node |  nodeType : CLIENT  , AS > .
    eq mte(< O : Node |  nodeType : CLIENT , state : wait-for-reply(N) , AS >) = N .
    eq mte(< O : Node |  nodeType : CLIENT , state : wait-timeout , AS >) = oo .
    eq mte(< O : Node |  nodeType : CLIENT , state : request-start , AS >) = oo .
endm
***为了减少状态量，直接将
mod NETWORK is
  ex CLIENT-EX + PRIMARY-EX + BACKUP-EX .
  sort Network .
  op [_|_] : ClockedState Msgs -> Network [ ctor format (n n n n n n)] . *** the nodes and the msgs list waiting to be sent
  vars MSG MSG1 : Msg .
  vars OBJ OBJ1 : Object .
  vars C C1 : Configuration .
  vars MSGS MSGS1 MSGS2 : Msgs .
  vars AS AS1 : AttributeSet .
  vars O O1 O2 : Oid .
  var M : MsgCont .
  vars T T1 : Time .
  var CLS : ClockedState .
  *** 因为network里有CokckedState，也有可能是GlobalConfiguration,所以写了两个

  *** 因为存储消息和发送消息会被视为两个，所以这里直接将snd-buffer中的消息直接传到目标的rcv-buffer中，缓解状态爆炸
  rl [trans-msg]:
    [ { C < O2 : Node | rcv-buffer : MSGS2 , AS1 > < O : Node |  snd-buffer : ( (msg M from O to O2) , MSGS ) , AS > }  | MSGS1 ]
      =>
    [ { C < O2 : Node | rcv-buffer : (MSGS2,(msg M from O to O2)) , AS1 > < O : Node | snd-buffer :  MSGS , AS > }  | MSGS1 ] .
  
  rl [rcv-msg] :
    [ { C < O : Node |   (snd-buffer : ( (msg M from O to O2) , MSGS )) , AS > } in time T | MSGS1 ] 
        =>
    [ { C < O : Node |   (snd-buffer : MSGS) , AS > } in time T | (MSGS1,msg M from O to O2) ] [nonexec] . 

  rl [rcv-msg] :
    [ { C < O : Node |   (snd-buffer : ( (msg M from O to O2) , MSGS )) , AS > }  | MSGS1 ] 
        =>
    [ { C < O : Node |   (snd-buffer : MSGS) , AS > } | (MSGS1,msg M from O to O2) ] [nonexec] . 

  crl [discard-improper-msg]:
    [ { C < O : Node |   (snd-buffer : ((msg M from O1 to O2) , MSGS)) , AS > } in time T | MSGS1 ] 
        =>
    [ { C < O : Node |   snd-buffer : MSGS , AS > } in time T | MSGS1 ] 
    if O =/= O1 [nonexec].

  rl [transfer-msg] :
    [ { C < O : Node |   rcv-buffer : MSGS , AS > } in time T | (msg M from O2 to O),MSGS1 ] 
        =>
    [ { C < O : Node |   rcv-buffer : (MSGS, msg M from O2 to O) , AS > } in time T | MSGS1 ] [nonexec] .

  rl [transfer-msg] :
    [ { C < O : Node |   rcv-buffer : MSGS , AS > }  | (msg M from O2 to O),MSGS1 ] 
        =>
    [ { C < O : Node |   rcv-buffer : (MSGS, msg M from O2 to O) , AS > }  | MSGS1 ] [nonexec] .

  *** current disable the rules below
  *** 网络可能会丢失消息，也有可能会错位发送消息，这里暂时先用nonexec屏蔽掉，之后可以用策略控制。
  rl [discard-msg] :
    [ CLS | MSG,MSGS1 ] =>  [ CLS | MSGS1 ] [nonexec]. *** discard the msg
    
  rl [exchange-msg]:
    [ CLS | MSG,MSG1,MSGS1 ] => [ CLS | MSG1,MSG,MSGS1 ] [nonexec].
    
endm


mod INIT-PBFT is
    pr NETWORK .
    vars N N1 N2 VIEW VIEW1 VIEW2  : Nat .
    vars O O1 O2 : Oid . 
    vars AS AS1 AS2 : AttributeSet .
    vars CONF1 CONF2 : Configuration .
    vars LOGS LOGS1 LOGS2 : Map{MsgCont,List{Log}} .
    vars LOGLIST LOGLIST1 LOGLIST2 : List{Log} .
    vars MTYPE MTYPE1 MTYPE2 : MsgType .
    vars MCONT MCONT1 MCONT2 : MsgCont .
    op init : -> Network .
    op init-clock : Nat -> Object .
    op init-nodes : Nat Nat -> Configuration .
    op init-node : Nat Nat -> Object .
    op isAllSame : Configuration -> Bool . ***determine whether all nodes have updated the values they save 判断所有的节点是否执行了操作
    eq isAllSame(none) = true .
    eq isAllSame(CONF1 < O : Clock | AS >) = isAllSame(CONF1) .
    eq isAllSame(CONF1 < O : Node | current-num : N1 , AS > < O1 : Node | current-num : N2 , AS1 > ) = 
           if N1 == N2 then isAllSame(CONF1 < O : Node | current-num : N1 , AS >)
           else false fi .
    eq isAllSame(< O : Node | AS >) = true .
    eq isAllSame(CONF1 < O : Node | nodeType : CLIENT , AS >) = isAllSame(CONF1) .

    *** init the primary , backups and a client .( N is the number of the backups , not the number of the Byzantine fault )
    eq init-nodes(N,N1) = init-node(N,N) init-clients(N,N1) init-clock(s N + N1 ) . 
    ceq init-node(s N , N1 ) =
        < N : Node | rcv-buffer : empty , current-num : nil , states : empty , snd-buffer : empty , logs : empty , nodeType : BACKUP , view : 0 , r-num : N1 > init-node( N , N1 ) if N > 0 .
    eq init-node(1 , N) = < 0 : Node | rcv-buffer : empty , seq : random(N) , current-num : nil , logs : empty , snd-buffer : empty , nodeType : PRIMARY , view : 0 , states : empty , r-num : N > .
    op init-clients : Nat Nat -> Object .
    eq init-clients(N,s N1) = init-clients(s N , N1) init-client(N) .
    eq init-clients(N,0) = none .
    op init-client : Nat -> Object .
    eq init-client(N) = 
                     < N : Node | times : 5 ,rcv-buffer : empty , snd-buffer : empty , nodeType : CLIENT , r-num : N , view : 0 , state : request-start > .
    eq init-clock(N) = 
                     < N : Clock | time : 0 > .
    eq init = [ {  init-nodes(4,1) } | empty ] .
    op _includes_ : List{Log} MsgCont -> Bool .
    eq nil includes MCONT = false .
    eq LOGLIST < MTYPE1 | view : VIEW1 , seq : N1 , original-msg : MCONT1 , AS1 > includes < MTYPE | view : VIEW , seq : N , original-msg : MCONT , AS1 > = 
                      if MTYPE == MTYPE1 and N1 == N and MCONT1 == MCONT and VIEW1 == VIEW
                      then true 
                      else LOGLIST includes < MTYPE | view : VIEW , seq : N , original-msg : MCONT , AS1 > fi .

    op prepared : MsgCont Nat Nat Object -> Bool .
    eq prepared(< request | AS > , VIEW , N , < O : Node | logs : LOGS , r-num : N1 ,AS1 >) = 
                LOGS[< request | AS >] =/= undefined  and
                LOGS[< request | AS >] includes < pre-prepare | view : VIEW , seq : N ,original-msg : < request | AS > > and
                countMsg( LOGS[< request | AS >], prepare , VIEW , N , < request | AS > ) >= 2 * (sd(N1,1) quo 3) .

    op Seq : List{Log} -> Nat .
    eq Seq(< MTYPE | seq : N , AS > LOGLIST) = N .
endm

smod PBFT-ACTION is 
  pr INIT-PBFT .
  strat rcv-transfer-all : @ Network .
  sd rcv-transfer-all :=  one( (rcv-msg ; transfer-msg )! )  .
  strat main-strat : @ Network .
  sd main-strat := one(snd-request !) ; rcv-transfer-all ;
                   rcv-client-request !  ; rcv-transfer-all ; 
                   one(rcv-pre-prepare !) ; rcv-transfer-all ; 
                   one(primary-rcv-prepare-msg ! ) ; primary-into-commit ! ;   
                   one(backup-rcv-prepare-msg !) ; one( backup-into-commit !) ; rcv-transfer-all ; 
                   one(backup-rcv-commit-msg !) ; one(primary-rcv-commit-msg !) ; backup-respond-client-request ! ; 
                   one(primary-respond-client-request !) ; rcv-transfer-all   .
endsm


set print attribute off .
*** srew init using one(main-strat) .
*** frew init .
set print attribute off .


***(search init =>+ [ { C:Configuration 
                    < O:Oid : Node | logs : (LOGS:Map{MsgCont,List{Log}},
                                            < request | view : VIEW:Nat , AS1:AttributeSet > |-> LOGLIST:List{Log},
                                            < request | view : VIEW:Nat , AS2:AttributeSet > |-> LOGLIST1:List{Log}),
                                              AS:AttributeSet > } | MSGS:Msgs ]
         such that ( prepared(< request | view : VIEW:Nat , AS1:AttributeSet >,VIEW:Nat,Seq(LOGLIST:List{Log}),< O:Oid : Node | logs : (LOGS:Map{MsgCont,List{Log}},
                                            < request | view : VIEW:Nat , AS1:AttributeSet > |-> LOGLIST:List{Log},
                                            < request | view : VIEW:Nat , AS2:AttributeSet > |-> LOGLIST1:List{Log}),
                                              AS:AttributeSet >) 
              implies 
                     prepared(< request | view : VIEW:Nat , AS2:AttributeSet >,VIEW:Nat,Seq(LOGLIST:List{Log}),< O:Oid : Node | logs : (LOGS:Map{MsgCont,List{Log}},
                                            < request | view : VIEW:Nat , AS1:AttributeSet > |-> LOGLIST:List{Log},
                                            < request | view : VIEW:Nat , AS2:AttributeSet > |-> LOGLIST1:List{Log}),
                                              AS:AttributeSet >)) =/= false .
*** 搜索所有最后不可修改的最终状态
search init =>! [{C:Configuration} | MSGS:Msgs] .
show path labels 3023 .
show path labels 7811681 .
)