Wiki

イベント管理

イベントは,イベントのオーナである拡張タスクとイベントのマスクで一意に定まる. このことは，CafeOBJで次のように記述できる．

#!python

module MASK
{
  signature
  {
    [ Mask ]
  }
}

#!python

module EVENT
{
  import
  {
    ex(MASK)
    ex(EXTENDED)
  }
  signature
  {
    [ Event ]
    op owner : Event -> Extended
    op mask : Event -> Mask
    op match : Event Event -> Bool
  }
  axioms
  {
    vars E F : Event
    cq (E = F) = true
       if (owner(E) = owner(F)) and (mask(E) = mask(F)) .
  }
}

イベントからは，マスクと，イベントのオーナーである拡張タスクという２つの情報を抽出できる．イベントがオーナーとマスクで一意に定まることは，オーナーとマスクが同じである２つのイベントは等しいと宣言することで表されている．

イベントに係る遷移には，拡張タスクのwait，releaseの他に，イベントの生起（set event），イベントの解消（clear event）がある．これらの遷移を記述するには，生起されているイベントの集合や拡張タスクが待つイベントの集合が必要になる．まず，イベントの集合を返す観測を宣言しよう．

#!python

module EVENTS
{
  imports
  {
    pr(SET(EVENT{ sort Elt -> Event }) * { sort Set -> Events })
  }
  signature
  {
    op exist : Event Events -> Bool
    op inter : Events Events -> Bool
  }
  axioms
  {
    vars S T : Events
    vars X Y : Event
    eq exist(X,nil) = false .
    cq exist(X,(Y,S)) = true
       if X = Y .
    cq exist(X,(Y,S)) = exist(X,S)
       if not(X = Y) .
    eq inter(nil,T) = false .
    cq inter((X,S),T) = true
       if exist(X,T) .
    cq inter((X,S),T) = inter(S,T)
       if not(exist(X,T)) .
  }
}

#!python

module OBSERVATION2EVENTS
{
  imports
  {
    ex(OBSERVATION)
    ex(EVENTS)
  }
  signature
  {
    [ Observation2Events < Observation ]
    [ Events < Value ]
    op __ : Observation2Events Container -> Events
  }
}

これを基に，生起されているイベントの集合や，拡張タスクが待つイベントの集合を返す観測を次のように宣言する．

#!python

module RAISED
{
  imports
  {
    ex(OBSERVATION2EVENTS)
    pr(STATE)
  }
  signature
  {
    op raised : -> Observation2Events
  }
  axioms
  {
    eq raised(init) = nil .
  }
}

raisedが，生起されているイベントの集合を返す観測である．

#!python

module WAITINGFOR
{
  imports
  {
    ex(OBSERVATION2EVENTS)
    pr(STATE)
    pr(EXTENDED)
  }
  signature
  {
    op waitingfor : Extended -> Observation2Events
  }
  axioms
  {
    vars X : Extended
    eq waitingfor(X)(init) = nil .
  }
}

上で宣言した演算waitingforに拡張タスクを与えると，そのタスクが待つイベントの集合を返す観測となる．

それでは，既にタスク管理で宣言したモジュールWAITとRELEASEを，これらの観測を加えて書き換えよう．

#!python

module WAIT
{
  imports
  {
    pr(DISABLE)
    pr(STOP)
    pr(EXTENDED)
    pr(WAITING)
    pr(WAITINGFOR)
    pr(RAISED)
  }
  signature
  {
    [ Wait < Stop Disable ]
    op wait : Extended Event -> Wait
    op sub : Wait -> Extended
    op event : Wait -> Event
  }
  axioms
  {
    vars C : State
    vars X : Extended
    vars T : Wait
    vars E : Event
    eq sub(wait(X,E)) = X .
    eq event(wait(X,E)) = E .
    cq waiting(T(C)) = (waiting(C)),X
       if pre(T,C) .
    cq waitingfor(X)(T(C)) = (waitingfor(X)(C)),event(T)
       if pre(T,C) .
    cq exist(event(T),raised(C)) = false
       if pre(T,C) .
    eq rev(T,waiting) = true .
    cq rev(T,waitingfor(X)) = true
       if sub(T) = X .
  }
}

実行中の拡張タスクをxとすると，遷移waitに伴い， xが待つイベントの集合にイベントが１つ加わる．また，遷移waitでxが待つと宣言するイベントが既に生起されている場合， xはwaiting状態に移らない．遷移waitでは，waitingによる観測結果だけでなく． waitingfor(x)による観測結果も更新される．

#!python

module RELEASE
{
  imports
  {
    pr(ENABLE)
    pr(ENTER)
    pr(EXTENDED)
    pr(WAITING)
    pr(WAITINGFOR)
    pr(RAISED)
  }
  signature
  {
    [ Release < Enter Enable ]
    op release : Extended -> Release
    op sub : Release -> Extended
  }
  axioms
  {
    vars C : State
    vars X : Extended
    vars T : Release
    eq sub(release(X)) = X .
    cq waiting(T(C)) = (waiting(C)) \ X
       if pre(T,C) .
    cq inter(waitingfor(sub(T))(C),raised(C)) = true
       if pre(T,C) .
    eq rev(T,waiting) = true .
  }
}

遷移releaseにより，waiting状態にある拡張タスクがready状態に戻るためには，自身が待つイベントが生起していなければならない．

イベントを生起する遷移は次のように書ける．

#!python

module RAISE
{
  imports
  {
    ex(STATEMACHINE)
    pr(RAISED)
  }
  signature
  {
    [ Raise < Transition ]
    op sub : Raise -> Task
    op event : Raise -> Event
  }
  axioms
  {
    vars C : State
    vars T : Raise
    vars E : Event
    cq raised(T(C)) = (raised(C)),event(T)
       if pre(T,C) .
    eq rev(T,raised) = true .
  }
}

ソートRaiseの項がイベントを生起する遷移を表す．この遷移で生起されたイベントが，生起されたイベントの集合に加えられる．

イベントを解消する遷移は次のように書ける．

#!python

module CLEAR
{
  imports
  {
    ex(STATEMACHINE)
    ex(EXTENDED)
    pr(RAISED)
  }
  signature
  {
    [ Clear < Transition ]
    op sub : Clear -> Extended
    op event : Clear -> Event
  }
  axioms
  {
    vars C : State
    vars T : Clear
    vars E : Event
    cq raised(T(C)) = (raised(C)) \ event(T)
       if pre(T,C) .
    eq rev(T,raised) = true .
  }
}

イベントを解消する遷移は，ソートClearの項として表される．イベントの解消により，解消対象のイベントが生起されているイベントの集合から外れる．イベントの解消は拡張タスクのみが行える．