Wiki

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
  }
)

LIST/TASK

#!python
make LIST/TASK
(
  LIST(
    TASK { sort Elt -> Task }
  ) * {
    sort List -> List/Task
  }
)

BAG/ENTITY

#!python
make BAG/ENTITY
(
  BAG(
    ENTITY { sort Elt -> Entity }
  ) * {
    sort Bag -> Bag/Entity
  }
)

BAG/TASK

#!python
make BAG/TASK
(
  BAG(
    TASK { sort Elt -> Task }
  ) * {
    sort Bag -> Bag/Task
  }
)

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
  }
)

OVERRIDE/ENTITY

#!python
make OVERRIDE/ENTITY
(
  OVERRIDE(
    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
    eq deducible((X @ L),(Y @ L) |- (X former(L) Y),(X = Y),(Y former(L) X)) = true .
    cq deducible(nil |- (X former(L) Y),(X = Y),(Y former(L) X)) = true
       if  (deducible(nil |- X @ L) = true)
       and (deducible(nil |- Y @ L) = true) .
  }
}

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
  }
)

OBSERVER2SET/TASK

#!python
make OBSERVER2SET/TASK
(
  FOCUS(
    SET/TASK { sort Elt -> Set/Task }
  ) * {
    sort Observer2Elt -> Observer2Set/Task
  }
)

OBSERVER2SET/EXTENDEDTASK

#!python
make OBSERVER2SET/EXTENDEDTASK
(
  FOCUS(
    SET/EXTENDEDTASK { sort Elt -> Set/ExtendedTask }
  ) * {
    sort Observer2Elt -> Observer2Set/ExtendedTask
  }
)

OBSERVER2LIST/ENTITY

#!python
make OBSERVER2LIST/ENTITY
(
  FOCUS(
    LIST/ENTITY { sort Elt -> List/Entity }
  ) * {
    sort Observer2Elt -> Observer2List/Entity
  }
)

OBSERVER2LIST/TASK

#!python
make OBSERVER2LIST/TASK
(
  FOCUS(
    LIST/TASK { sort Elt -> List/Task }
  ) * {
    sort Observer2Elt -> Observer2List/Task
  }
)

OBSERVER2BAG/ENTITY

#!python
make OBSERVER2BAG/ENTITY
(
  FOCUS(
    BAG/ENTITY { sort Elt -> Bag/Entity }
  ) * {
    sort Observer2Elt -> Observer2Bag/Entity
  }
)

OBSERVER2BAG/TASK

#!python
make OBSERVER2BAG/TASK
(
  FOCUS(
    BAG/TASK { sort Elt -> Bag/Task }
  ) * {
    sort Observer2Elt -> Observer2Bag/Task
  }
)

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
  }
)