Mode resolution

Context

This page describes the mode resolution mechanism. Its goal is to compute the computation mode of a block according to its input, outputs, memories and parameters DataTypes, SignalTypes and values.

In order to find the correct mode for an instance of a block, it is mandatory to represent each mode by a different expression (signature). For a BlockType it will not be possible to have two BlockModes having the same signature. If it is the case, it will not be possible to select a mode for this block. This will mean either:

  • The provided block instance is not correct
  • The specification is not correct
  • The specification is not complete

In the BlockLibrary instance verification page we describe how to check that a block’s specification is correct according to the previously exposed conditions. We also provide means to verify if a block specification is complete.

According to this, if we do not manage to find a correct BlockMode for a block instance this means that the provided block instance is not correct.

Precisions on the BlockMode/BlockVariant relations with BlockVariants

BlockModes implements BlockVariants. BlockVariants extends other BlockVariants. These two relations are modeled using VariantSet model elements. See BlockLibrary Meta-model page for documentation. A VariantSet is contained in either a BlockVariant, a BlockMode or an Other VariantSet. Each VariantSet has an attached operator giving him a specific semantics. We distinguish between two operators AND and ALT:

  • AND operator: The AND VariantSet container must implement (or extend if the container is a BlockVariant) all of the BlockVariants and VariantSets refered by this VariantSet.
  • ALT operator: The ALT VariantSet container must implement (or extend if the container is a BlockVariant) one of the BlockVariants and VariantsSets refered by this VariantSet.

It is worth noting that:

  • From one BlockMode/BlockVariant we can have multiple relations. This allows to combine the two kind of relations.
  • A VariantSet has either a reference to BlockVariants or to VariantSets but not combinations of both.

Definitions

The ALT relation

We need here to introduce a new symbol for logical formulas: \(\bigodot\) named ALT for Aternative. This symbol is stating that for a set of logical properties if exactly one of these properties is true (this behavior is close to the one of the binary logical operator XOR but generalized for a set of values). It is ofter refered to as n-ary XOR.

Here is the formal definition of the ALT operator:

\[S = \{a_1, a_2, ..., a_{n}\}, \forall i \in [1..n], a_i \in \mathcal{B}\]\[\bigodot^{n}_{i=1} S(i) = \left( \bigvee^{n}_{i=1} S(i) \right) \wedge \left( \bigwedge^{i,j \leq n, i \not= j}_{i,j =1} \neg(S(i) \wedge S(j)) \right)\]

Operations on specification elements

Let’s assume the following operations definitions:

  • \(SIG(e)\): BlockMode | BlockVariant -> Signature

    The signature of \(e\). Detailed definition is given below.

  • \(SC(e)\): StructuralFeature -> Set(Annotation)

    The collection of structural constraints of \(e\). Structural constraints are the properties expressed in the StructuralFeatures of the element \(e\) and its structural constraints.

    Returns a collection of Annotations.

    Note In the following, \(SC(e)_i\) is the \(i^{th}\) element of this collection.

  • \(BV^{\&}(e)\): BlockMode | BlockVariant -> Set(BlockVariant)

    The collection of BlockVariants implemented (if \(e\) is a BlockMode) or extended (if e is a BlockVariant) by the \(e\) : SpecificationElement related to it by AND relations.

    Returns a collection of BlockVariant.

    Note In the following, \(BV^{\&}(e)_i\) is the \(i^{th}\) element of this collection.

  • \(BV^{\odot}(e)\): BlockMode | BlockVariant -> Set(Set(BlockVariant))

    The collection of collections of BlockVariants implemented (if \(e\) is a BlockMode) or extended (if \(e\) is a BlockVariant) by the \(e\) : SpecificationElement related to \(e\) by ALT relations. Each sub collection in the result contains the elements related in one ALT relation.

    Returns a collection of collections of BlockVariants.

    Note In the following, \(BV^{\odot}(e)_{i,j}\) is the \(j^{th}\) BlockVariant of the \(i^{th}\) collection of BlockVariants.

We will refer in the following with \(|X|\) as the cardinal (number of elements) of the collection \(X\).

BlockMode signature calculus

According to the previous definitions:

  • The signature of an element \(e\) (either a BlockMode or a BlockVariant) is recusively defined by:
\[\begin{split}SIG(e) = \left( \bigwedge^{|SC(e)|}_{i=1} SC(e)_i \right) \land \left( \left( \bigwedge^{|BV^{\&}(e)|}_{i=1} SIG(BV^{\&}(e)_i) \right) \land \left( \bigwedge^{|BV^{\odot}(e)|}_{i=1} \left( \bigodot^{|BV^{\odot}(e)_i|}_{j=1} SIG(BV^{\odot}(e)_{i,j}) \right) \right) \right)\end{split}\]

Example

Example 1:

Let take a BlockMode called \(a\). Let’s imagine a first ALT (\(\odot\)) relation between \(a\) and three BlockVariants (\(v_1, v_2, v_3\)) and a second ALT relation between \(a\) and two BlockVariants (\(v_4, v_5\)). As these two ALT relations needs to be satisfied then a AND VariantSet holds both of them. A compact form for this is:

  • \(a\) implements \(\&(\odot(v_1, v_2, v_3), \odot(v_4, v_5))\)

We give in the following the result for the computation of the set of signatures for \(a\):

\(SIG(a) = \bigodot\{\)

\[\left(\bigwedge^{|SC(a)|}_{i=1} SC(a)_i \right) \land \left(\bigwedge^{|SC(v_1)|}_{i=1} SC(v_1)_i \right) \land \left(\bigwedge^{|SC(v_4)|}_{i=1} SC(v_4)_i \right) \land \left(\bigwedge^{|SC(v_5)|}_{i=1} SC(v_5)_i \right),\]
\[\left(\bigwedge^{|SC(a)|}_{i=1} SC(a)_i \right) \land \left(\bigwedge^{|SC(v_2)|}_{i=1} SC(v_2)_i \right) \land \left(\bigwedge^{|SC(v_4)|}_{i=1} SC(v_4)_i \right) \land \left(\bigwedge^{|SC(v_5)|}_{i=1} SC(v_5)_i \right),\]
\[\left(\bigwedge^{|SC(a)|}_{i=1} SC(a)_i \right) \land \left(\bigwedge^{|SC(v_3)|}_{i=1} SC(v_3)_i \right) \land \left(\bigwedge^{|SC(v_4)|}_{i=1} SC(v_4)_i \right) \land \left(\bigwedge^{|SC(v_5)|}_{i=1} SC(v_5)_i \right)\]

\(\}\)

Termination of the calculus

In the OCL constraints specified on the BlockLibrary metamodel, we specified that no cycle can exists in the BlockVariant hierarchy. Furthermore, there is a finite number of BlockVariants and BlockModes in a BlockLibrary. This make the previous calculus possible to finish and so the calculation always possible.