Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / backup / 10_Instantiation_of_ParameterizedModules_to_Use
Instantiation of Parameterized Modules
In this section, we enumerate instantiation of parameterized modules which are used in the description of the OSEK OS.
SET/ENTITY
#!python make SET/ENTITY ( SET( ENTITY { sort Elt -> Entity } ) * { sort Set -> Set/Entity } )
SET/TASK
#!python make SET/TASK ( SET( TASK { sort Elt -> Task } ) * { sort Set -> Set/Task } )
SET/EXTENDEDTASK
#!python make SET/EXTENDEDTASK ( SET( EXTENDEDTASK { sort Elt -> ExtendedTask } ) * { sort Set -> Set/ExtendedTask } )
LIST/ENTITY
#!python make LIST/ENTITY ( LIST( ENTITY { sort Elt -> Entity } ) * { sort List -> List/Entity } )
BAG/ENTITY
#!python make BAG/ENTITY ( BAG( ENTITY { sort Elt -> Entity } ) * { sort Bag -> Bag/Entity } )
RELATION/ENTITY
#!python make RELATION/ENTITY ( RELATION( ENTITY { sort Elt -> Entity } ) * { sort Relation -> Relation/Entity } )
IRREFLEXIVE/ENTITY
#!python make IRREFLEXIVE/ENTITY ( IRREFLEXIVE( ENTITY { sort Elt -> Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity } ) * { sort Irreflexive -> Irreflexive/Entity } )
ASYMMETRIC/ENTITY
#!python make ASYMMETRIC/ENTITY ( ASYMMETRIC( ENTITY { sort Elt -> Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity } ) * { sort Asymmetric -> Asymmetric/Entity } )
TRANSITIVE/ENTITY
#!python make TRANSITIVE/ENTITY ( TRANSITIVE( ENTITY { sort Elt -> Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity } ) * { sort Transitive -> Transitive/Entity } )
PARTIALORDER/ENTITY
#!python make PARTIALORDER/ENTITY ( PARTIALORDER( ENTITY { sort Elt -> Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity }, IRREFLEXIVE/ENTITY { sort Irreflexive -> Irreflexive/Entity }, ASYMMETRIC/ENTITY { sort Asymmetric -> Asymmetric/Entity }, TRANSITIVE/ENTITY { sort Transitive -> Transitive/Entity } ) * { sort PartialOrder -> PartialOrder/Entity } )
TOTALORDER/ENTITY
#!python make TOTALORDER/ENTITY ( TOTALORDER( ENTITY { sort Elt -> Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity }, IRREFLEXIVE/ENTITY { sort Irreflexive -> Irreflexive/Entity }, ASYMMETRIC/ENTITY { sort Asymmetric -> Asymmetric/Entity }, TRANSITIVE/ENTITY { sort Transitive -> Transitive/Entity }, PARTIALORDER/ENTITY { sort PartialOrder -> PartialOrder/Entity } ) * { sort TotalOrder -> TotalOrder/Entity } )
ROOT/ENTITY
#!python make ROOT/ENTITY ( ROOT( ENTITY { sort Elt -> Entity }, SET/ENTITY { sort Set -> Set/Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity }, IRREFLEXIVE/ENTITY { sort Irreflexive -> Irreflexive/Entity }, ASYMMETRIC/ENTITY { sort Asymmetric -> Asymmetric/Entity }, TRANSITIVE/ENTITY { sort Transitive -> Transitive/Entity }, PARTIALORDER/ENTITY { sort PartialOrder -> PartialOrder/Entity } ) )
COMPLEMENT/ENTITY
#!python make COMPLEMENT/ENTITY ( COMPLEMENT( ENTITY { sort Elt -> Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity } ) )
TRANSITIVE'/ENTITY
#!python make TRANSITIVE'/ENTITY ( TRANSITIVE'( ENTITY { sort Elt -> Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity }, TRANSITIVE/ENTITY { sort Transitive -> Transitive/Entity }, COMPLEMENT/ENTITY ) * { sort Transitive' -> Transitive'/Entity } )
PARTIALORDER'/ENTITY
#!python make PARTIALORDER'/ENTITY ( PARTIALORDER'( ENTITY { sort Elt -> Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity }, IRREFLEXIVE/ENTITY { sort Irreflexive -> Irreflexive/Entity }, ASYMMETRIC/ENTITY { sort Asymmetric -> Asymmetric/Entity }, TRANSITIVE/ENTITY { sort Transitive -> Transitive/Entity }, PARTIALORDER/ENTITY { sort PartialOrder -> PartialOrder/Entity } COMPLEMENT/ENTITY, TRANSITIVE'/ENTITY { sort Transitive' -> Transitive'/Entity } ) * { sort PartialOrder' -> PartialOrder'/Entity } )
COMBINE/ENTITY
#!python make COMBINE/ENTITY ( COMBINE( ENTITY { sort Elt -> Entity }, RELATION/ENTITY { sort Relation -> Relation/Entity }, IRREFLEXIVE/ENTITY { sort Irreflexive -> Irreflexive/Entity }, ASYMMETRIC/ENTITY { sort Asymmetric -> Asymmetric/Entity }, TRANSITIVE/ENTITY { sort Transitive -> Transitive/Entity }, PARTIALORDER/ENTITY { sort PartialOrder -> PartialOrder/Entity } COMPLEMENT/ENTITY, TRANSITIVE'/ENTITY { sort Transitive' -> Transitive'/Entity } PARTIALORDER'/ENTITY { sort PartialOrder' -> PartialOrder'/Entity } ) )
FORMER/ENTITY
#!python module FORMER/ENTITY { imports { pr(LIST/ENTITY) ex(PARTIALORDER/ENTITY) } signature { op former : List/Entity -> PartialOrder/Entity } axioms { vars L : List/Entity vars X Y : Entity cq deducible(nil |- (X former(L) Y),(X = Y),(Y former(L) X)) = true if (X ? L)/\(Y ? L) . } }
OBSERVER2NUMBER
#!python make OBSERVER2NUMBER ( FOCUS( NUMBER { sort Elt -> Number } ) * { sort Observer2Elt -> Observer2Number } )
OBSERVER2PROP
#!python make OBSERVER2PROP ( FOCUS( PROP { sort Elt -> Prop } ) * { sort Observer2Elt -> Observer2Prop } )
OBSERVER2ENTITY
#!python make OBSERVER2ENTITY ( FOCUS( ENTITY { sort Elt -> Entity } ) * { sort Observer2Elt -> Observer2Entity } )
OBSERVER2SET/ENTITY
#!python make OBSERVER2SET/ENTITY ( FOCUS( SET/ENTITY { sort Elt -> Set/Entity } ) * { sort Observer2Elt -> Observer2Set/Entity } )
OBSERVER2LIST/ENTITY
#!python make OBSERVER2LIST/ENTITY ( FOCUS( LIST/ENTITY { sort Elt -> List/Entity } ) * { sort Observer2Elt -> Observer2List/Entity } )
OBSERVER2SET/TASK
#!python make OBSERVER2SET/TASK ( FOCUS( SET/TASK { sort Elt -> Set/Task } ) * { sort Observer2Elt -> Observer2Set/Task } )
OBSERVER2BAG/ENTITY
#!python make OBSERVER2BAG/ENTITY ( FOCUS( BAG/ENTITY { sort Elt -> Bag/Entity } ) * { sort Observer2Elt -> Observer2Bag/Entity } )
OBSERVER2SET/EXTENDEDTASK
#!python make OBSERVER2SET/EXTENDEDTASK ( FOCUS( SET/EXTENDEDTASK { sort Elt -> Set/ExtendedTask } ) * { sort Observer2Elt -> Observer2Set/ExtendedTask } )
OBSERVER2RELATION/ENTITY
#!python make OBSERVER2RELATION/ENTITY ( FOCUS( RELATION/ENTITY { sort Elt -> Relation/Entity } ) * { sort Observer2Elt -> Observer2Relation/Entity } )
OBSERVER2IRREFLEXIVE/ENTITY
#!python make OBSERVER2IRREFLEXIVE/ENTITY ( FOCUS( IRREFLEXIVE/ENTITY { sort Elt -> Irreflexive/Entity } ) * { sort Observer2Elt -> Observer2Irreflexive/Entity } )
OBSERVER2PARTIALORDER/ENTITY
#!python make OBSERVER2PARTIALORDER/ENTITY ( FOCUS( PARTIALORDER/ENTITY { sort Elt -> PartialOrder/Entity } ) * { sort Observer2Elt -> Observer2PartialOrder/Entity } )
OBSERVER2PARTIALORDER'/ENTITY
#!python make OBSERVER2PARTIALORDER'/ENTITY ( FOCUS( PARTIALORDER'/ENTITY { sort Elt -> PartialOrder'/Entity } ) * { sort Observer2Elt -> Observer2PartialOrder'/Entity } )
Updated