Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / backup / 08_DescriptionFramework_for_StateTransitionSystems
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 } }
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 } }
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 } }
Updated