Wiki

イベント機構

登録

登録されているイベントの観測：

#!python

module DECLARED-EVENT
{
  imports {
    ex(OBSERVATION2EVENTS)
  }
  signature {
    op declaredEvent : -> Observation2Events
  }
}

イベント登録：

#!python

module DECLARE-EVENT
{
  imports {
    ex(REGISTRATION)
    ex(DECLARE)
    ex(INTERFACE)
  }
  signature {
    op DeclareEvent : Event -> Registration
  }
  axioms {
    vars C : System
    vars E : Event
    eq state(DeclareEvent(E)(C)) = declare(E)(state(C)) .
  }
}

遷移

実際にイベントに係るシステムサービスを実際に記述するには，具体的な遷移を項として宣言しておく必要がある．

イベント生起：

#!python

module OCCUR
{
  imports {
    ex(RAISE)
    pr(EXTENDED)
  }
  signature {
    op occur : Extended Mask -> Raise
  }
  axioms {
    vars C : State
    vars T : Extended
    vars M : Mask
    eq owner(event(occur(T,M))) = T .
    eq mask(event(occur(T,M))) = M .
  }
}

イベント解消：

#!python

module REMOVE
{
  imports {
    ex(CLEAR)
    pr(EXTENDED)
    pr(CURRENT)
  }
  signature {
    op remove : Extended Mask -> Clear
  }
  axioms {
    vars C : State
    vars T : Extended
    vars M : Mask
    eq owner(event(remove(T,M))) = T .
    eq mask(event(remove(T,M))) = M .
    cq (current(C) = owner(event(remove(T,M)))) = true
       if pre(remove(T,M),C) .
  }
}

システムサービス

イベント生起：

#!python

module SET-EVENT
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(EVENT-COMPOSITION)
    pr(OCCUR)
    pr(RELEASE)
    pr(SUSPENDED)
    pr(ISR)
    pr(CURRENT)
    pr(OCCURRENCE)
    pr(WAITING-MASK)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op SetEvent : Extended Mask -> SystemService
  }
  axioms {
    vars C : System
    vars X : Extended
    vars M : Mask
    cq pre(occur(X,M)(state(C))) = true
       if pre(SetEvent(X,M)(C)) .
    cq occurrence(X(state(C)) > 0 = true
       if pre(SetEvent(X,M)(C)) .
    cq isExtended(X) = true
       if pre(SetEvent(X,M)(C)) .
    cq not(suspended(X)(state(C))) = true 
    if pre(SetEvent(X,M)(C)) .
    cq (isISR(current(state(C))) or isTask(current(state(C)))) = true
       if pre(SetEvent(X,M)(C)) .
    cq state(SetEvent(X,M)(C)) = release(X),occur(X,M)(state(C))) 
       if pre(SetEvent(X,M)(C) and waiting(X)(state(C)) and mask(X)(state(C)) == M  .
    cq state(SetEvent(X,M)(C)) = occur(X,M)(state(C)) 
       if pre(SetEvent(X,M)(C) and (~(waiting(X)(state(C))) or      mask(X)(state(C)) =/= M)  .
    cq status(SetEvent(X,M)(C)) = E-OK 
       if pre(SetEvent(X,M)(C) .
    cq status(SetEvent(X,M)(C)) = E-OS-ID 
       if occurrence(X(state(C)) == 0 .
    cq status(SetEvent(X,M)(C)) = E-OS-ACCESS 
       if not(isExtended(X)) .
    cq status(SetEvent(X,M)(C)) = E-OS-STATE 
       if suspended(X)(state(C)) .
  }
}

イベント解消：

#!python

module CLEAR-EVENT
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(EVENT-COMPOSITION)
    pr(REMOVE)
    pr(SUSPENDED)
    pr(ISR)
    pr(CURRENT)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op ClearEvent : Mask -> SystemService
  }
  axioms {
    vars C : System
    vars M : Mask
    cq pre(remove(current(state(C)),M)(state(C)) = true
       if pre(ClearEvent(M)(C)) .
    cq state(ClearEvent(M)(C)) = remove(current(state(C)),M)(state(C)) 
       if pre(ClearEvent(M)(C) .
    cq status(ClearEvent(M)(C)) = E-OK 
       if pre(ClearEvent(M)(C) .
    cq status(ClearEvent(M)(C)) = E-OS-ACCESS 
       if isTask(current(state(C))) andnot(isExtended(current(state(C)))) .
    cq status(ClearEvent(M)(C)) = E-OS-CALLEVEL 
       if isISR(current(state(C))) .
  }
}

イベント検索：

#!python

module GET-EVENT
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(RESULT-MASK-STATE)
    pr(WAITING-MASK)
    pr(SUSPENDED)
    pr(OCCURRENCE)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op GetEvent : Extended -> SystemService
  }
  axioms {
    vars C : System
    vars X : Extended
    cq occurrence(X(state(C)) > 0 = true
       if pre(GetEvent(X)(C)) .
    cq isExtended(X) and not(suspended(X)(state(C))) true
       if pre(GetEvent(X)(C) .
    eq state(GetEvent(X)(C)) = state(C) .
    cq maskState,result(GetEvent(X)(C))) = mask(X)(state(C)) 
       if pre(GetEvent(X)(C) .
    cq status(GetEvent(X)(C)) = E-OK 
       if pre(GetEvent(X)(C) .
    cq status(GetEvent(X)(C)) = E-OS-ID 
       if occurrence(X(state(C)) == 0 .
    cq status(GetEvent(X)(C)) = E-OS-ACCESS 
       if not(isExtended(X)) .
    cq status(GetEvent(X)(C)) = E-OS-STATE
       if suspended(X)(state(C)) .
  }
}

イベントの生起待ち：

#!python

module WAIT-EVENT
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(WAIT)
    pr(RELEASE)
    pr(RAISED)
    pr(ISR)
    pr(EVENT-COMPOSITION)
    pr(CURRENT)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op WaitEvent : Mask -> SystemService
  }
  axioms {
    vars C : System
    vars X : Extended
    vars M : Mask
    cq pre(wait(current(state(C)),M)(state(C)) = true
       if pre(WaitEvent(M)(C) .
    cq state(WaitEvent(M)(C)) = release(current(state(C))),wait(current(state(C)),M)(state(C))) 
       if pre(WaitEvent(M)(C) and comp(current(state(C)),M) @ raised(state(C)) .
    cq state(WaitEvent(M)(C)) = wait(current(state(C)),M)(state(C)) 
       if pre(WaitEvent(M)(C) andnot(comp(current(state(C)),M) @ raised(state(C))) .
    cq status(WaitEvent(M)(C)) = E-OK 
       if pre(WaitEvent(M)(C) .
    cq status(WaitEvent(M)(C)) = E-OS-ACCESS 
       if isTask(current(state(C))) andnot(isExtended(current(state(C)))) .
    cq status(WaitEvent(M)(C)) = E-OS-RESOURCE 
       if occupied(current(state(C)))(state(C)) =/= nil .
    cq status(WaitEvent(M)(C)) = E-OS-CALLEVEL 
       if isISR(current(state(C))) .
  }
}