Wiki

A Framework for Formal Description of State Transition Systems

In this section, we introduce an abstract structure of state transition systems represented by four CafeOBJ modules, named SYSTEM, VALUE, OBSERVER and TRANSITION.

SYSTEM

The module SYSTEM declares the sort System, which represents a universal state space of the target system to be described.

#!python

module SYSTEM
{
  signature
  {
    [ System ]
  }
}

VALUE

A term of the sort State represents a state of the target system. An information extracted from a state is called "observable value". The following module declares a sort of observable values.

#!python

module VALUE
{
  signature
  {
    [ Value ]
  }
}

OBSERVER

The module OBSERVER declares the sort Observer, whose element represents an operation to extract an observable value from a state.

#!python

module OBSERVER
{
  imports
  {
    pr(SYSTEM)
    ex(VALUE)
  }
  signature
  {
    [ Observer ]
    op __ : Observer System -> Value
  }
}

In the module OBSERVER, application of an observer to a state is declared, too. Let f and s be an observer and state, respectively. Then the term f(s) represents an observable value extrected from s with f.

TRANSITION

The module TRANSITION declares the sort Transition whose term represents a state transition.

#!python

module TRANSITION
{
  imports
  {
    ex(SYSTEM)
  }
  signature
  {
    [ Transition ]
    op __ : Transition System -> System
    op complete : System -> Bool
  }
}

Similarly to OBSERVER, this module also declares an operation for application of a transition to a system. Let f and s be a transision and a state, respectively. Then the term f(s) denotes the state modified from s by applying f.

The operation complete returns a some kind of status of applying a transition. A Boolean value complete(f(s)) indicates if the application of f to s was successfully finished or not.

FOCUS

The following module FOCUS is an assistant for refinement.

#!python
module FOCUS
(
  X :: TRIV
)
{
  imports
  {
    ex(OBSERVER)
  }
  signature
  {
    [ Observer2Elt < Observation ]
    [ Elt < Value ]
    op __ : Observer2Elt System -> Elt
  }  
}