Wiki

タスク管理

ここでは，タスク管理に係るシステムサービスのCafeOBJ記述を紹介する．

定数

タスクの識別子：

#!python

module TASK-ID
{
  imports
  {
    pr(TASK)
    pr(NIL)
  }
  signature
  {
    [ TaskId ]
    op INVALID-TASK : -> TaskId
    op id : Task -> TaskId
    op id : Nil -> TaskId
  }
  axioms {
    eq id(nil) = INVALID-TASK .
  }
}

タスクの状態：

#!python

module TASK-STATE
{
  imports
  {
    ex(RESULT)
  }
  signature
  {
    [ TaskState < Result ]
    op RUNNING : -> TaskState
    op SUSPENDED : -> TaskState
    op READY : -> TaskState
    op WAITING : -> TaskState
  }
}

登録

タスクの登録：

#!python

module DECLARE-TASK
{
  imports {
    ex(REGISTRATION)
    ex(DECLARE)
  }
  signature {
    op DeclareTask : Task -> Registration
  }
  axioms {
    vars C : System
    vars T : Task
    vars F : Filter
    eq state(DeclareTask(T)(C)) = declare(T)(state(C)) .
  }
}

観測

タスク識別子の観測：

#!python

module OBSERVATION2TASKID
{
  imports {
    ex(TASK-ID)
  }
  signature {
    [ Observation2TaskId < Observation ]
    [ TaskId < Value ]
    op __ : Observation2TaskId Container -> Observation2TaskId
  }
}

#!python

module RESULT-TASK-ID
{
  imports {
    ex(OBSERVATION2TASKID)
  }
  signature {
    op taskId : -> Observation2TaskId
  }
}

タスク状態の観測：

#!python

module OBSERVATION2TASKSTATE
{
  imports {
    ex(TASK-STATE)
  }
  signature {
    [ Observation2TaskState < Observation ]
    [ TaskState < Value ]
    op __ : Observation2TaskState Container -> Observation2TaskState
  }
}

#!python

module RESULT-TASK-STATE
{
  imports {
    ex(OBSERVATION2TASKSTATE)
  }
  signature {
    op taskState : -> Observation2TaskState
  }
}

システムサービス

タスク活性化：

#!python

module ACTIVATE-TASK
{
  imports {
    ex(SYSTEM-SERVICE)
    pr(ACTIVATE)
    pr(ISR)
    pr(CURRENT)
    pr(OCCURRENCE)
    pr(MULTIPLICITY)
    pr(SUSPENDED)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op ActivateTask : Task -> SystemService
  }
  axioms {
    vars C : System
    vars T : Task
    cq pre(activate(T)(state(C)) = true
       if pre(ActivateTask(T)(C) .
    cq (isISR(current(state(C))) or isTask(current(state(C)))) = true
       if pre(ActivateTask(T)(C) .
    cq state(ActivateTask(T)(C)) = activate(T)(state(C))
       if pre(ActivateTask(T)(C) .
    cq status(ActivateTask(T)(C)) = E-OK
       if pre(ActivateTask(T)(C) .
    cq status(ActivateTask(T)(C)) = E-OS-LIMIT
       if occur(enable(state(C)),T) >= multiplicity(T)(C) .
    cq status(ActivateTask(T)(C)) = E-OS-ID
       if occurrence(T(state(C)) == 0 .
  }
}

タスク終了：

#!python

module TERMINATE-TASK
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(TERMINATE)
    pr(ISR)
    pr(CURRENT)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op TerminateTask : -> SystemService
  }
  axioms {
    vars C : System
    vars T : Task
    eq pre(terminate(current(state(C)))(state(C)) = true
       if pre(TerminateTask(C) .
    cq isTask(current(state(C)))
       if pre(TerminateTask(C) .
    cq state(TerminateTask(C)) = terminate(current(state(C)))(state(C))
       if pre(TerminateTask(C) .
    cq status(TerminateTask(C)) = E-OK
       if pre(TerminateTask(C) .
    cq status(TerminateTask(C)) = E-OS-CALLEVEL
       if isISR(current(state(C))) .
  }
}

タスクのチェイン：

#!python

module CHAIN-TASK
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(EXCHANGE)
    pr(ISR)
    pr(CURRENT)
    pr(OCCURRENCE)
    pr(MULTIPLICITY)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op ChainTask : Task -> SystemService
  }
  axioms {
    vars C : System
    vars T : Task
    cq pre(exchange(current(state(C)),T)(state(C)) = true
       if pre(ChainTask(T)(C) .
    cq pre(activate(T)(state(C)) = true
       if pre(ChainTask(T)(C) .
    cq isTask(current(state(C))) = true
       if pre(ChainTask(T)(C) .
    cq state(ChainTask(T)(C)) = exchange(current(state(C)),T)(state(C))
       if pre(ChainTask(T)(C) .
    cq status(ChainTask(T)(C)) = E-OK
       if pre(ChainTask(T)(C) .
    cq status(ChainTask(T)(C)) = E-OS-LIMIT
       if occur(enable(state(C),T) >= multiplicity(T) .
    cq status(ChainTask(T)(C)) = E-OS-ID if  occurrence(T(state(C)) == 0 .
    cq status(ChainTask(T)(C)) =  E-OS-CALLEVEL
       if isISR(current(state(C))) .
  }
}

スケジューラ呼出：

#!python


module SCHEDULE
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(PAUSE)
    pr(ISR)
    pr(CURRENT)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op Schedule : -> SystemService
  }
  axioms {
    vars C : System
    vars T : Task
    cq isTask(current(state(C))) = true
       if pre(Schedule(C)) .
    cq pre(pause(current(state(C)))(state(C)) = true
       if pre(Schedule(C)) .
    cq state(Schedule(C)) = pause(current(state(C)))(state(C))
       if pre(Schedule(C)) .
    cq status(Schedule(C)) = E-OK
       if pre(Schedule(C) .
    cq status(Schedule(C)) = E-OS-CALLEVEL
       if isISR(current(state(C))) .
    cq status(Schedule(C)) = E-OS-RESOURCE
       if occupied(current(state(C)))(state(C)) =/= nil .
  }
}

タスク検索：

#!python

module GET-TASK
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    ex(RESULT-TASK-ID)
    pr(RUNNING)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op GetTask : -> SystemService
  }
  axioms {
    vars C : System
    vars F : Interface
    vars T : Task
    eq state(GetTask(C)) = state(C) .
    cq taskId(result(GetTask(C))) = id(current(state(C))) 
       if isTask(current(state(C))) .
    cq taskId(result(GetTask,F(C)))) = taskId(result(GetTask(C)))
       if not(isTask(current(state(F(C))))) .
  }
}

タスク状態検索：

#!python

module GET-TASK-STATE
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(RESULT-TASK-STATE)
    pr(RUNNING)
    pr(SUSPENDED)
    pr(READY)
    pr(WAITING)
    pr(OCCURRENCE)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op GetTaskState : Task -> SystemService
  }
  axioms {
    vars C : System
    vars T : Task
    cq occurrence(T(state(C)) > 0 = true
       if pre(GetTaskState(T)(C) .
    eq state(GetTaskState(T)(C)) = state(C) .
    cq taskState,result(GetTaskState(T)(C))) = RUNNING
       if running(T(state(C)) .
    cq taskState,result(GetTaskState(T)(C))) = SUSPENDED
       if suspended(T)(state(C)) .
    cq taskState,result(GetTaskState(T)(C))) = READY
       if not(running(T(state(C))) and ready(T)(state(C)) .
    cq taskState,result(GetTaskState(T)(C))) = WAITING
       if waiting(T)(state(C)) .
    cq status(GetTaskState(T)(C)) = E-OK
       if pre(GetTaskState(T)(C) .
    cq status(GetTaskState(T)(C)) =  E-OS-ID
       if occurrence(T(state(C)) == 0 .
  }
}