From 7524b11ef5f24d40d43156e2437260c55e507ceb Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Tue, 4 Oct 2022 09:02:58 +0200 Subject: [PATCH 01/26] Initial commit of ReadMe.md for MCP-0027 --- RationaleMCP/0027/ReadMe.md | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 RationaleMCP/0027/ReadMe.md diff --git a/RationaleMCP/0027/ReadMe.md b/RationaleMCP/0027/ReadMe.md new file mode 100644 index 000000000..6d604d515 --- /dev/null +++ b/RationaleMCP/0027/ReadMe.md @@ -0,0 +1,34 @@ +# Modelica Change Proposal MCP-0027
Units of Literal Constants +Francesco Casella, Henrik Tidefelt + +**(In Development)** + +## Summary +The purpose of this MCP is to allow more unit errors to be detected by giving more expressions the unit `"1"` instead of having an undefined unit. +The problem with undefined unit is that it gets in the way of carrying out checking of units (which tools tend to deal with by not checking units at all where this happens). + +## Revisions +| Date | Description | +| --- | --- | +| 2022-10-04 | Henrik Tidefelt. Filling this document with initial content. | + +## Contributor License Agreement +All authors of this MCP or their organizations have signed the "Modelica Contributor License Agreement". + +## Rationale +FIXME + +## Backwards Compatibility +As current Modelica doesn't clearly reject some models with non-sensical combination of units, this MCP will break backwards compatibility by turning at least some of these invalid. + +## Tool Implementation +None, so far. + +### Experience with Prototype +N/A + +## Required Patents +To the best of our knowledge, there are no patents that would conflict with the incorporation of this MCP. + +## References +(None.) From 1309d1056809f54513657891058e415133e7fcf1 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Tue, 4 Oct 2022 13:28:08 +0200 Subject: [PATCH 02/26] Handle units of literal constants by means of rules for the empty unit --- chapters/unitexpressions.tex | 130 +++++++++++++++++++++++++++++++++++ 1 file changed, 130 insertions(+) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index d40b9cd4b..8360607ab 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -89,3 +89,133 @@ \section{The Syntax of Unit Expressions}\label{the-syntax-of-unit-expressions} The unit expression \lstinline!"T"! means tesla, but note that the letter \lstinline!T! is also the symbol for the prefix tera which has a multiplier value of 10\textsuperscript{12}. \end{example} + + +\section{Unit Checking}\label{unit-checking} + +How to verify that units are used in compatible ways is current not fully determined by the specification. +This section gives rules for certain situations, but in general tools are expected to reason based on common sense. + + +\subsection{Empty and Undefined Units}\label{empty-and-undefined-units} + +In situations where the specification does not prescribe how to determine the unit of an expression, the unit of that expression is said to be \firstuse[undefined unit]{undefined}. +It is then not possible for a tool to reject the equation (or other construct) with support in the specification, and options for the tool include silently not performing unit checking, or applying checks based on common sense. + +The unit of an expression can also be defined as being \firstuse[empty unit]{empty}, see below. +In certain places (see below), expressions with empty unit can be implicitly cast to suitable units. +When an expression with empty unit is implicitly cast to some unit, that unit is referred to as the \firstuse{inferred unit} of the expression. + + +\subsection{Unit Inference}\label{unit-inference} + +Where the empty unit has no other defined meaning, it can be implicitly cast to unit \lstinline!"1"!. + +In some cases the empty unit can be implicitly cast to an inferred unit: +\begin{itemize} +\item + In binding equations and modifications: + \begin{itemize} + \item The entire expression of the binding or modification. + \item When the entire expression is an array construction, array concatenation and array range, then apply rules recursively for the direct subexpressions. + \end{itemize} +\item + The entire argument expression in a function call. +% To keep the design close to the bare minimum, this part is currently excluded: +%\item +% For a translation-time constant with value 0.0: +% \begin{itemize} +% \item Expressions constituting the entire side of an equality or relation. +% \item The right hand side of an assignment. +% \item The direct subexpressions of array construction, array concatenation, and array range. +% \end{itemize} +\end{itemize} + + +\subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} + +This section describes conditions under which an expression has empty unit. +Conditions not given here must not be interpreted as definitely not implying empty unit; instead, the unit may be currently undefined for some expressions, allowing the unit to be properly defined in future versions of the specification. + +Basic expressions defined to have empty unit: +\begin{itemize} +\item + \lstinline!Real! literals. +\item + \lstinline!Integer! expressions implicitly cast to \lstinline!Real!. +\end{itemize} + +Expressions defined to \emph{not} propagate the empty unit, thereby forcing inference of unit \lstinline!"1"!: +\begin{itemize} +\item + Addition, subtraction, multiplication and division operators when either operand has non-empty unit. +\item + Right operand of binary exponentiation. +\item + Component references outside functions where the declared \lstinline!unit!-attribute is \lstinline!""! (possibly by not being specified). + (Unit checking involving user-defined functions with empty unit on inputs and outputs is currently not defined.) +\end{itemize} + +Built-in non-array operators, functions, and special expressions that propagate any unit (including empty): +\begin{itemize} +\item + Negation, addition, subtraction (scalar or element-wise) +\end{itemize} + +Special situations in which the empty unit can be propagated up the expression tree: +\begin{itemize} +\item + Multiplication and division when both operands have empty unit. +\end{itemize} + +\begin{example} +Consider unit checking of the following declaration equation: +\begin{lstlisting}[language=modelica] +Real y(unit = "m") = 1 + 2.5 * 3; +\end{lstlisting} +The unit of the declaration equation right-hand side is determined as follows: +\begin{itemize} +\item The \lstinline!Real! literal \lstinline!2.5! has empty unit. +\item The \lstinline!Integer! literals \lstinline!1! and \lstinline!3! are implicitly cast to \lstinline!Real!, and therefore have empty unit. +\item The multiplication \lstinline!2.5 * 3! has empty unit, as multiplication can propagate the empty unit of both operands. +\item The addition \lstinline!1 + (2.5 * 3)! has empty unit, as addition can propagate any unit as long as both operands have the same unit. +\item The entire right-hand side expression gets inferred unit \lstinline!"m"! in order to be compatible with the component's declared \lstinline!unit!. +\end{itemize} +\end{example} + +\begin{example} +Consider unit checking of the following erroneous declaration equation for \lstinline!y!: +\begin{lstlisting}[language=modelica] +Real x(unit = "m") = 1.0; +Real y(unit = "m") = x^2 / 2; +\end{lstlisting} +The unit of the declaration equation right-hand side is determined as follows: +\begin{itemize} +\item The unit of \lstinline!x! is \lstinline!"m"!, and common sense gives that \lstinline!x^2! has unit \lstinline!"m2"! +\item The \lstinline!Integer! literal \lstinline!1! is implicitly cast to \lstinline!Real!, and therefore has empty unit. +\item As the left operand of \lstinline!x^2 / 2! is non-empty, the right operand cannot be empty, and hence empty unit of \lstinline!2! is implicitly cast to \lstinline!"1"!. +\item Common sense then gives that the unit of \lstinline!x^2 / 2! is \lstinline!"m2"!, which is an error due to the required unit being \lstinline!"m"!. +\end{itemize} +\end{example} + +\begin{example} +Consider the potential consequences of an undefined unit in the following declaration equation: +\begin{lstlisting}[language=modelica] +Real y(unit = "m") = sin(1.57); +\end{lstlisting} +To see that the unit of the declaration equation right-hand side is undefined, note that: +\begin{itemize} +\item The \lstinline!Real! literal \lstinline!1.57! has empty unit. +\item The expression \lstinline!sin(1.57)! is not covered by the specification, and hence has undefined unit. +\end{itemize} +If a tool wants to proceed according to ``common sense'', alternatives include: +\begin{itemize} +\item + Assume that \lstinline!sin! is a mapping from unit \lstinline!"1"! to unit \lstinline!"1"!. + The unit of \lstinline!1.57! then defaults to \lstinline!"1"! (alternatively, the same unit could be obtained by inference). + The unit of \lstinline!sin(1.57)! is then found to be \lstinline!"1"!, which is an error due to the required unit being \lstinline!"m"!. +\item + Assume that \lstinline!sin! preserves both the unit \lstinline!"1"! and the empty unit. + The empty unit of \lstinline!1.57! gets propagated to \lstinline!sin(1.57)!, which in turn gets inferred unit \lstinline!"m"!. +\end{itemize} +\end{example} From 2dfb4e86323a5b5480ec0a9dd0eaff03cb0774fd Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 5 Oct 2022 14:38:12 +0200 Subject: [PATCH 03/26] Clarify that all operands of additive operators need to have the same unit --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 8360607ab..74da56701 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -159,7 +159,7 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} Built-in non-array operators, functions, and special expressions that propagate any unit (including empty): \begin{itemize} \item - Negation, addition, subtraction (scalar or element-wise) + When all operands have the same unit: negation, addition, and subtraction (scalar or element-wise). \end{itemize} Special situations in which the empty unit can be propagated up the expression tree: From 0c62f41ec87fd2d5b481a1576365fbb03627ea9b Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 5 Oct 2022 14:42:11 +0200 Subject: [PATCH 04/26] Clarify "component references outside functions" --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 74da56701..91baed572 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -152,7 +152,7 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} \item Right operand of binary exponentiation. \item - Component references outside functions where the declared \lstinline!unit!-attribute is \lstinline!""! (possibly by not being specified). + Component references outside of functions, where the component's declared \lstinline!unit!-attribute is \lstinline!""! (possibly by not being specified). (Unit checking involving user-defined functions with empty unit on inputs and outputs is currently not defined.) \end{itemize} From 203c16ec4671c59bec7304432e42d8d167e2cff6 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 5 Oct 2022 14:45:43 +0200 Subject: [PATCH 05/26] Fix small mistake in example --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 91baed572..b8a342e4a 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -192,7 +192,7 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} The unit of the declaration equation right-hand side is determined as follows: \begin{itemize} \item The unit of \lstinline!x! is \lstinline!"m"!, and common sense gives that \lstinline!x^2! has unit \lstinline!"m2"! -\item The \lstinline!Integer! literal \lstinline!1! is implicitly cast to \lstinline!Real!, and therefore has empty unit. +\item The \lstinline!Real! literal \lstinline!1.0! has empty unit, and gets inferred unit \lstinline!"m"!. \item As the left operand of \lstinline!x^2 / 2! is non-empty, the right operand cannot be empty, and hence empty unit of \lstinline!2! is implicitly cast to \lstinline!"1"!. \item Common sense then gives that the unit of \lstinline!x^2 / 2! is \lstinline!"m2"!, which is an error due to the required unit being \lstinline!"m"!. \end{itemize} From 5d420650f3feefc3ae4f901fad0cae72db83f545 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 5 Oct 2022 15:00:08 +0200 Subject: [PATCH 06/26] Change "common sense" -> "(standard) dimensional analysis" --- chapters/unitexpressions.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index b8a342e4a..e696737ec 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -94,13 +94,13 @@ \section{The Syntax of Unit Expressions}\label{the-syntax-of-unit-expressions} \section{Unit Checking}\label{unit-checking} How to verify that units are used in compatible ways is current not fully determined by the specification. -This section gives rules for certain situations, but in general tools are expected to reason based on common sense. +This section gives rules for certain situations, but in general tools are expected to reason according to standard dimensional analysis (from here on referred to as just \firstuse{dimensional analysis}). \subsection{Empty and Undefined Units}\label{empty-and-undefined-units} In situations where the specification does not prescribe how to determine the unit of an expression, the unit of that expression is said to be \firstuse[undefined unit]{undefined}. -It is then not possible for a tool to reject the equation (or other construct) with support in the specification, and options for the tool include silently not performing unit checking, or applying checks based on common sense. +It is then not possible for a tool to reject the equation (or other construct) with support in the specification, and options for the tool include silently not performing unit checking, or applying checks based dimensional analysis. The unit of an expression can also be defined as being \firstuse[empty unit]{empty}, see below. In certain places (see below), expressions with empty unit can be implicitly cast to suitable units. @@ -191,10 +191,10 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} \end{lstlisting} The unit of the declaration equation right-hand side is determined as follows: \begin{itemize} -\item The unit of \lstinline!x! is \lstinline!"m"!, and common sense gives that \lstinline!x^2! has unit \lstinline!"m2"! +\item The unit of \lstinline!x! is \lstinline!"m"!, and dimensional analysis gives that \lstinline!x^2! has unit \lstinline!"m2"! \item The \lstinline!Real! literal \lstinline!1.0! has empty unit, and gets inferred unit \lstinline!"m"!. \item As the left operand of \lstinline!x^2 / 2! is non-empty, the right operand cannot be empty, and hence empty unit of \lstinline!2! is implicitly cast to \lstinline!"1"!. -\item Common sense then gives that the unit of \lstinline!x^2 / 2! is \lstinline!"m2"!, which is an error due to the required unit being \lstinline!"m"!. +\item Dimensional analysis then gives that the unit of \lstinline!x^2 / 2! is \lstinline!"m2"!, which is an error due to the required unit being \lstinline!"m"!. \end{itemize} \end{example} @@ -208,7 +208,7 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} \item The \lstinline!Real! literal \lstinline!1.57! has empty unit. \item The expression \lstinline!sin(1.57)! is not covered by the specification, and hence has undefined unit. \end{itemize} -If a tool wants to proceed according to ``common sense'', alternatives include: +If a tool wants to proceed according to ``standard dimensional analysis'', alternatives include: \begin{itemize} \item Assume that \lstinline!sin! is a mapping from unit \lstinline!"1"! to unit \lstinline!"1"!. From fc4abde0686ca2f604e75c0faa594e6efcae9f52 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 5 Oct 2022 16:20:35 +0200 Subject: [PATCH 07/26] Add section with examples of "standard dimensional analysis" --- chapters/unitexpressions.tex | 40 +++++++++++++++++++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index e696737ec..a31fd4657 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -94,7 +94,45 @@ \section{The Syntax of Unit Expressions}\label{the-syntax-of-unit-expressions} \section{Unit Checking}\label{unit-checking} How to verify that units are used in compatible ways is current not fully determined by the specification. -This section gives rules for certain situations, but in general tools are expected to reason according to standard dimensional analysis (from here on referred to as just \firstuse{dimensional analysis}). +This section gives rules for certain situations, but in general tools are expected to reason according to standard dimensional analysis.. + + +\subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} + +This section gives an incomplete characterization of \emph{standard dimensional analysis}, also referred to as just \firstuse{dimensional analysis}. +What is described below applies to unit checking in Modelica -- \emph{standard dimensional analysis} could have additional meanings in other contexts. +While Modelica has a concept of \willintroduce{empty units} (described in later sections), standard dimensional analysis only deals with non-empty units such as \lstinline!"m"!, \lstinline!"m/s"!, or \lstinline!"1"!. +It consists of two parts: +\begin{itemize} +\item + Unit compatibility requirements. +\item + Rules for deriving the unit of an expression. +\end{itemize} + +Examples of unit compatibility requirements that must be met in Modelica: +\begin{itemize} +\item + The expression of a declaration equation must have the same unit as the component to which it belongs. +\item + The two sides of an equation or assignment statement must have the same unit. +\item + The two operands of the additive operators \lstinline!+! and \lstinline!-! must have the same unit. +\item + In a function call, the unit of an argument expression must match the unit (unless empty, see below) of the corresponding function input component. +\end{itemize} + +% TODO: Replace these examples by giving unit semantics where operators and built-in functions are defined in the specification, +% and just include some likes to places where such semantics are given. +Examples of unit derivation in Modelica: +\begin{itemize} +\item + The result of additive operators has the same unit as the operands. +\item + The result of multiplication has a unit obtained by adding the exponents of the operands' units. +\item + Built-in operators such as \lstinline!pre! and \lstinline!previous! preserve units, while \lstinline!der! changes the unit by dividing it by \lstinline!"s"!. +\end{itemize} \subsection{Empty and Undefined Units}\label{empty-and-undefined-units} From b86567b0271204c21ee75aacfbf054bb649392c9 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 5 Oct 2022 16:33:15 +0200 Subject: [PATCH 08/26] Fix minor typo --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index a31fd4657..cc0f04a43 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -94,7 +94,7 @@ \section{The Syntax of Unit Expressions}\label{the-syntax-of-unit-expressions} \section{Unit Checking}\label{unit-checking} How to verify that units are used in compatible ways is current not fully determined by the specification. -This section gives rules for certain situations, but in general tools are expected to reason according to standard dimensional analysis.. +This section gives rules for certain situations, but in general tools are expected to reason according to standard dimensional analysis. \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} From 1f5131cab2bd8e009ee24523d599abfc2323e293 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 5 Oct 2022 20:25:00 +0200 Subject: [PATCH 09/26] Put quotes around 'standard dimensional analysis' --- chapters/unitexpressions.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index cc0f04a43..3cd615db6 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -99,8 +99,8 @@ \section{Unit Checking}\label{unit-checking} \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} -This section gives an incomplete characterization of \emph{standard dimensional analysis}, also referred to as just \firstuse{dimensional analysis}. -What is described below applies to unit checking in Modelica -- \emph{standard dimensional analysis} could have additional meanings in other contexts. +This section gives an incomplete characterization of ``standard dimensional analysis'', also referred to as just \firstuse{dimensional analysis}. +What is described below applies to unit checking in Modelica -- \emph{dimensional analysis} could have additional meanings in other contexts. While Modelica has a concept of \willintroduce{empty units} (described in later sections), standard dimensional analysis only deals with non-empty units such as \lstinline!"m"!, \lstinline!"m/s"!, or \lstinline!"1"!. It consists of two parts: \begin{itemize} From 3291a7300c0a5bab47ffedfbb6fb32c09892583d Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 5 Oct 2022 20:26:11 +0200 Subject: [PATCH 10/26] Say "multiplying the operands' units" --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 3cd615db6..60680b9d4 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -129,7 +129,7 @@ \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} \item The result of additive operators has the same unit as the operands. \item - The result of multiplication has a unit obtained by adding the exponents of the operands' units. + The result of multiplication has a unit obtained by multiplying the operands' units. \item Built-in operators such as \lstinline!pre! and \lstinline!previous! preserve units, while \lstinline!der! changes the unit by dividing it by \lstinline!"s"!. \end{itemize} From f639afcd9cdd694e47fc4db6b639b3225ba5b9a5 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 5 Oct 2022 20:35:12 +0200 Subject: [PATCH 11/26] Make use of terminology 'dimensional homogenity' --- chapters/unitexpressions.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 60680b9d4..77d5be481 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -113,9 +113,9 @@ \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} Examples of unit compatibility requirements that must be met in Modelica: \begin{itemize} \item - The expression of a declaration equation must have the same unit as the component to which it belongs. + Dimensional homogeneity: The two sides of an equation or assignment statement must have the same unit. \item - The two sides of an equation or assignment statement must have the same unit. + The expression of a declaration equation must have the same unit as the component to which it belongs (special case of dimensional homogeneity). \item The two operands of the additive operators \lstinline!+! and \lstinline!-! must have the same unit. \item From 3a3b1f0bf8320c1d76d17451882b5ea9b64032c9 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 26 Oct 2022 09:09:46 +0200 Subject: [PATCH 12/26] Don't present lists as "Examples of...", but add "other" item at the end As suggested by @bilderbuchi. --- chapters/unitexpressions.tex | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 77d5be481..11d7db5e0 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -110,7 +110,7 @@ \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} Rules for deriving the unit of an expression. \end{itemize} -Examples of unit compatibility requirements that must be met in Modelica: +Unit compatibility requirements that must be met in Modelica: \begin{itemize} \item Dimensional homogeneity: The two sides of an equation or assignment statement must have the same unit. @@ -120,11 +120,13 @@ \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} The two operands of the additive operators \lstinline!+! and \lstinline!-! must have the same unit. \item In a function call, the unit of an argument expression must match the unit (unless empty, see below) of the corresponding function input component. +\item + Other situations where unit compatibility might seem natural are currently not covered by the specification, but could become additional unit compatibility requirements in the future. \end{itemize} % TODO: Replace these examples by giving unit semantics where operators and built-in functions are defined in the specification, % and just include some likes to places where such semantics are given. -Examples of unit derivation in Modelica: +Unit derivation in Modelica: \begin{itemize} \item The result of additive operators has the same unit as the operands. @@ -132,6 +134,8 @@ \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} The result of multiplication has a unit obtained by multiplying the operands' units. \item Built-in operators such as \lstinline!pre! and \lstinline!previous! preserve units, while \lstinline!der! changes the unit by dividing it by \lstinline!"s"!. +\item + Other expressions are not yet covered by the specification. \end{itemize} From e411347e1109671c70539b4678ab06ceb74a10df Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 26 Oct 2022 09:11:42 +0200 Subject: [PATCH 13/26] Say "reject or approve" As suggested by @bilderbuchi. --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 11d7db5e0..3d4b5c0fc 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -142,7 +142,7 @@ \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} \subsection{Empty and Undefined Units}\label{empty-and-undefined-units} In situations where the specification does not prescribe how to determine the unit of an expression, the unit of that expression is said to be \firstuse[undefined unit]{undefined}. -It is then not possible for a tool to reject the equation (or other construct) with support in the specification, and options for the tool include silently not performing unit checking, or applying checks based dimensional analysis. +It is then not possible for a tool to reject or approve the equation (or other construct) with support in the specification, and options for the tool include silently not performing unit checking, or applying checks based dimensional analysis. The unit of an expression can also be defined as being \firstuse[empty unit]{empty}, see below. In certain places (see below), expressions with empty unit can be implicitly cast to suitable units. From f3755a2c1a52f0a7efd0b65cd8acaa468ef104cc Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 26 Oct 2022 09:13:43 +0200 Subject: [PATCH 14/26] Add missing "on" --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 3d4b5c0fc..939f8ad76 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -142,7 +142,7 @@ \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} \subsection{Empty and Undefined Units}\label{empty-and-undefined-units} In situations where the specification does not prescribe how to determine the unit of an expression, the unit of that expression is said to be \firstuse[undefined unit]{undefined}. -It is then not possible for a tool to reject or approve the equation (or other construct) with support in the specification, and options for the tool include silently not performing unit checking, or applying checks based dimensional analysis. +It is then not possible for a tool to reject or approve the equation (or other construct) with support in the specification, and options for the tool include silently not performing unit checking, or applying checks based on dimensional analysis. The unit of an expression can also be defined as being \firstuse[empty unit]{empty}, see below. In certain places (see below), expressions with empty unit can be implicitly cast to suitable units. From fccda32d5cd01c1ce6564b999e4783cf667eec59 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 26 Oct 2022 09:46:04 +0200 Subject: [PATCH 15/26] Reformulate "In some cases" Trying to address comment by @bilderbuchi. --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 939f8ad76..eda00c9b3 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -153,7 +153,7 @@ \subsection{Unit Inference}\label{unit-inference} Where the empty unit has no other defined meaning, it can be implicitly cast to unit \lstinline!"1"!. -In some cases the empty unit can be implicitly cast to an inferred unit: +In the following cases, the empty unit can be implicitly cast to an inferred unit: \begin{itemize} \item In binding equations and modifications: From 89092bad649eb3fa85e5112103a9c0ab9b81a322 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 26 Oct 2022 10:59:56 +0200 Subject: [PATCH 16/26] Change 'can be' -> 'is' Trying to address comment by @bilderbuchi. --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index eda00c9b3..e41284f83 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -204,7 +204,7 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} When all operands have the same unit: negation, addition, and subtraction (scalar or element-wise). \end{itemize} -Special situations in which the empty unit can be propagated up the expression tree: +Special situations in which the empty unit is propagated up the expression tree: \begin{itemize} \item Multiplication and division when both operands have empty unit. From 82bb062b070dd54b46d4d88a913131bc06c69fa4 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 26 Oct 2022 22:42:13 +0200 Subject: [PATCH 17/26] Fix typo in comment --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index e41284f83..2d89c032d 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -125,7 +125,7 @@ \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} \end{itemize} % TODO: Replace these examples by giving unit semantics where operators and built-in functions are defined in the specification, -% and just include some likes to places where such semantics are given. +% and just include some links to places where such semantics are given. Unit derivation in Modelica: \begin{itemize} \item From 99ff3c9cc92a02f49a3d7b7ad46d64a38f6da49e Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 26 Oct 2022 23:33:26 +0200 Subject: [PATCH 18/26] Describe unit propagation and elaborate bottom-up nature of unit derivation --- chapters/unitexpressions.tex | 114 +++++++++++++++++++++++++++++++---- 1 file changed, 102 insertions(+), 12 deletions(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 2d89c032d..9b961a6d7 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -115,14 +115,17 @@ \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} \item Dimensional homogeneity: The two sides of an equation or assignment statement must have the same unit. \item - The expression of a declaration equation must have the same unit as the component to which it belongs (special case of dimensional homogeneity). + The expression of a binding equation must have the same unit as the component to which it belongs (special case of dimensional homogeneity). \item The two operands of the additive operators \lstinline!+! and \lstinline!-! must have the same unit. \item - In a function call, the unit of an argument expression must match the unit (unless empty, see below) of the corresponding function input component. + The two connectors in a \lstinline!connect!-equation must agree on all units inside the connectors (follows from dimensional homogeneity and additive operator rule). +\item + In a function call, the unit of an argument expression must match the unit of the corresponding function input component. \item Other situations where unit compatibility might seem natural are currently not covered by the specification, but could become additional unit compatibility requirements in the future. \end{itemize} +The requirements above apply to non-empty as well as empty units, but both \willintroduce{unit propagation} and \willintroduce{unit inference} (described below) need to be considered when verifying the requirements. % TODO: Replace these examples by giving unit semantics where operators and built-in functions are defined in the specification, % and just include some links to places where such semantics are given. @@ -149,11 +152,81 @@ \subsection{Empty and Undefined Units}\label{empty-and-undefined-units} When an expression with empty unit is implicitly cast to some unit, that unit is referred to as the \firstuse{inferred unit} of the expression. +\subsection{Unit Propagation}\label{unit-propagation} + +The main work of unit checking is performed on the flattened model, with the exception that \lstinline!connect!-equations need to be considered for \firstuse{unit propagation}. + +Unit propagation is the act of replacing the empty unit of an instantiated component by some other unit in order to fulfill some of the most obvious unit compatibility requirements. +It is the first step of the unit checking procedure, being independent of both unit derivation and unit inference. +Unit propagation takes place in the following situations: +\begin{itemize} +\item + Simple binding equations (\cref{equation-categories}): + When a component is declared with empty \lstinline!unit!-attribute and has a binding equation with just a component reference on the right-hand side, the unit of the right-hand side replaces the empty unit. +\item + \lstinline!connect!-equations: + Units can be propagated in both directions of a \lstinline!connect!-equation. +\end{itemize} + +Notation: The \emph{\lstinline!unit!-attribute of a component} refers to the attribute as given in the model. +The \emph{unit of a component} refers to the component's unit after unit propagation has been carried out. + +\begin{nonnormative} +The reason to not propagate units of non-simple binding equations is to avoid bootstrapping problems where unit propagation depends on unit derivation, and unit derivation depends on unit propagation. +If the restrictions on unit propagation would be relaxed in the future, this would be a backwards compatible change as it only means that there would be less need to write out units explicitly. +\end{nonnormative} + +\begin{nonnormative} +For unit propagation in \lstinline!connect!-equations, it is recommended to perform the propagation on the connection sets to avoid diagnostics involving two connectors where neither is declared with a non-empty unit. +By considering a connection set, a diagnostic message can omit all the connectors where the unit is empty, and only report examples of connectors in the set with mismatched non-empty units. +\end{nonnormative} + +\begin{example} +The following illustrates unit propagation and its limitations: +\begin{lstlisting}[language=modelica] +Real x(unit = "m") = 1.0; // OK: No unit propagation. +Real y = x; // OK: Unit propagation assigns y the unit "m". +Real z = y; // OK: Unit propagation assigns z the unit "m". +Real w = 2 * z; // Error: No unit propagation as 2 * z isn't simple. +\end{lstlisting} +(The rules making the binding equation for \lstinline!x! OK will be given in the sections below.) +\end{example} + + +\subsection{Bottom-Up Unit Derivation}\label{bottom-up-unit-derivation} + +After completed unit propagation, the unit of every expression shall be determined in order to be able to verify unit compatibility requirements. +The derivation is a bottom-up analysis of the expression tree, involving expression-specific rules and a simple form of unit inference. +Separate rules assign units to all expression tree leaves (such as variables and literals). +For a general non-leaf expression $\mathit{op}(e_{1},\, e_{2},\, \ldots, e_{n})$ where $\mathit{op}$ symolizes the kind of expression and the $e_{i}$ represent the immediate children in the expression tree, unit derivation follows these steps: +\begin{enumerate} +\item + Derive the unit of each subexpression $e_{i}$. + The so obtained unit of the expression might be empty as well as non-empty. +\item + If there is a unit derivation rule for $\mathit{op}$ matching the units of the $e_{i}$, apply that rule. + Note that some expressions can handle subexpressions with empty unit, often assigning the empty unit to the entire $\mathit{op}$-expression as well. +\item + Otherwise: + \begin{enumerate} + \def\labelenumii{\alph{enumii}.} + \item + Infer a non-empty unit for each $e_{i}$ that has empty unit, and let $e'_{i}$ denote the subexpressions after unit inference. + How the unit is inferred depends on the kind of expression, and is described in \cref{unit-inference}. + \item + If there is a unit derivation rule for $\mathit{op}(e'_{1},\, e'_{2},\, \ldots, e'_{n})$, apply that rule. + \item + Otherwise, the $\mathit{op}$-expression has a unit error. + \end{enumerate} +\end{enumerate} + + \subsection{Unit Inference}\label{unit-inference} -Where the empty unit has no other defined meaning, it can be implicitly cast to unit \lstinline!"1"!. +In Modelica unit checking, \firstuse{unit inference} refers to the implicit casting of an expression with empty unit to a corresponding expression with non-empty unit. +An expression can only get an inferred unit when appearing in a context where the empty unit is not allowed. -In the following cases, the empty unit can be implicitly cast to an inferred unit: +When encountering the empty unit in the following situations, the inferred unit is (uniquely) determined by ensuring that unit compatibility requirements are fulfilled: \begin{itemize} \item In binding equations and modifications: @@ -173,6 +246,8 @@ \subsection{Unit Inference}\label{unit-inference} % \end{itemize} \end{itemize} +Otherwise, the inferred unit is \lstinline!"1"!. + \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} @@ -194,7 +269,7 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} \item Right operand of binary exponentiation. \item - Component references outside of functions, where the component's declared \lstinline!unit!-attribute is \lstinline!""! (possibly by not being specified). + Component references outside of functions, where the component's unit (after unit propagation has been carried out) is empty (possibly by not being specified). (Unit checking involving user-defined functions with empty unit on inputs and outputs is currently not defined.) \end{itemize} @@ -211,27 +286,27 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} \end{itemize} \begin{example} -Consider unit checking of the following declaration equation: +Consider unit checking of the following binding equation: \begin{lstlisting}[language=modelica] Real y(unit = "m") = 1 + 2.5 * 3; \end{lstlisting} -The unit of the declaration equation right-hand side is determined as follows: +The unit of the binding equation right-hand side is determined as follows: \begin{itemize} \item The \lstinline!Real! literal \lstinline!2.5! has empty unit. \item The \lstinline!Integer! literals \lstinline!1! and \lstinline!3! are implicitly cast to \lstinline!Real!, and therefore have empty unit. \item The multiplication \lstinline!2.5 * 3! has empty unit, as multiplication can propagate the empty unit of both operands. \item The addition \lstinline!1 + (2.5 * 3)! has empty unit, as addition can propagate any unit as long as both operands have the same unit. -\item The entire right-hand side expression gets inferred unit \lstinline!"m"! in order to be compatible with the component's declared \lstinline!unit!. +\item The entire right-hand side expression gets inferred unit \lstinline!"m"! in order to be compatible with the component's declared \lstinline!unit!-attribute. \end{itemize} \end{example} \begin{example} -Consider unit checking of the following erroneous declaration equation for \lstinline!y!: +Consider unit checking of the following erroneous binding equation for \lstinline!y!: \begin{lstlisting}[language=modelica] Real x(unit = "m") = 1.0; Real y(unit = "m") = x^2 / 2; \end{lstlisting} -The unit of the declaration equation right-hand side is determined as follows: +The unit of the binding equation right-hand side is determined as follows: \begin{itemize} \item The unit of \lstinline!x! is \lstinline!"m"!, and dimensional analysis gives that \lstinline!x^2! has unit \lstinline!"m2"! \item The \lstinline!Real! literal \lstinline!1.0! has empty unit, and gets inferred unit \lstinline!"m"!. @@ -241,11 +316,26 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} \end{example} \begin{example} -Consider the potential consequences of an undefined unit in the following declaration equation: +Difference between using a literal and a constant: +\begin{lstlisting}[language=modelica] +function f + input Real u(unit = "m"); + output Real y(unit = "m") = u; +end f; +constant Real pi = 3.14; +Real x(unit = "m") = f(3.14); // OK. +Real y(unit = "m") = f(pi); // Error. +\end{lstlisting} +The first call to \lstinline!f! is OK due to unit inference making \lstinline!"m"! the inferred unit of \lstinline!3.14!. +The second call to \lstinline!f! is an error because the component reference \lstinline!pi! has an inferred unit of \lstinline!"1"! by itself, which prevents inference of the unit required by the function call. +\end{example} + +\begin{example} +Consider the potential consequences of an undefined unit in the following binding equation: \begin{lstlisting}[language=modelica] Real y(unit = "m") = sin(1.57); \end{lstlisting} -To see that the unit of the declaration equation right-hand side is undefined, note that: +To see that the unit of the binding equation right-hand side is undefined, note that: \begin{itemize} \item The \lstinline!Real! literal \lstinline!1.57! has empty unit. \item The expression \lstinline!sin(1.57)! is not covered by the specification, and hence has undefined unit. From 13529f794c91a1f800081cdbe1689b361183bad8 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Mon, 31 Oct 2022 22:34:59 +0100 Subject: [PATCH 19/26] Also describe unit mappings of transcendental functions to match other proposal --- chapters/unitexpressions.tex | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 9b961a6d7..4e77f2cbb 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -262,7 +262,7 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} \lstinline!Integer! expressions implicitly cast to \lstinline!Real!. \end{itemize} -Expressions defined to \emph{not} propagate the empty unit, thereby forcing inference of unit \lstinline!"1"!: +Expressions defined to \emph{not} propagate the empty unit up the expression tree, thereby forcing inference of unit \lstinline!"1"!: \begin{itemize} \item Addition, subtraction, multiplication and division operators when either operand has non-empty unit. @@ -273,10 +273,22 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} (Unit checking involving user-defined functions with empty unit on inputs and outputs is currently not defined.) \end{itemize} -Built-in non-array operators, functions, and special expressions that propagate any unit (including empty): +Built-in non-array operators, functions, and special expressions that propagate any unit (including empty) up the expression tree: \begin{itemize} \item - When all operands have the same unit: negation, addition, and subtraction (scalar or element-wise). + When all operands have the same unit: negation, addition, and subtraction (scalar or element-wise), see {array-element-wise-addition-subtraction-and-string-concatenation}. +\item + The \lstinline!abs! function, see \cref{modelica:abs}. +\end{itemize} + +Transcendental functions that propagate both unit \lstinline!"1"! and the empty unit up the expression tree: +\begin{itemize} +\item + All of the elementary mathematical functions listed in \cref{built-in-mathematical-functions-and-external-built-in-functions}. + (Whether some of these also accept other dimensionless units such as \lstinline!"rad"! for the input argument is currently not defined.) +\item + The only binary of these functions, \lstinline!atan2!, requires both arguments to have the same unit, and accepts any unit. + The result of \lstinline!atan2! has empty unit only when both arguments have empty unit; otherwise the unit of the result is \lstinline!"1"!. \end{itemize} Special situations in which the empty unit is propagated up the expression tree: From 847e6458fe79bc9ab863ab924095ddf30e7710ef Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Tue, 1 Nov 2022 14:06:39 +0100 Subject: [PATCH 20/26] Change 'are expected to' -> 'should' Ad discussed with @bilderbuchi. --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 4e77f2cbb..bb61b6fcd 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -94,7 +94,7 @@ \section{The Syntax of Unit Expressions}\label{the-syntax-of-unit-expressions} \section{Unit Checking}\label{unit-checking} How to verify that units are used in compatible ways is current not fully determined by the specification. -This section gives rules for certain situations, but in general tools are expected to reason according to standard dimensional analysis. +This section gives rules for certain situations, but in general tools should reason according to standard dimensional analysis. \subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis} From ebfc229fa0b73b2e6b03c8b0c821bb8e9f154d39 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Tue, 1 Nov 2022 14:57:02 +0100 Subject: [PATCH 21/26] Add example illustrating bottom-up nature of unit inference --- chapters/unitexpressions.tex | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index bb61b6fcd..84f48bd06 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -248,6 +248,18 @@ \subsection{Unit Inference}\label{unit-inference} Otherwise, the inferred unit is \lstinline!"1"!. +\begin{example} +Consider unit inference in the binding equation below: +\begin{lstlisting}[language=modelica] +Real y(unit = "m") = 1.5; +\end{lstlisting} +With the pseudo-code form \lstinline!unit($e$, $u$)! representing the expression $e$ having empty unit being cast to unit $u$, the binding equation after unit inference could be expressed explicitly as: +\begin{lstlisting}[language=modelica] +Real y(unit = "m") = unit(1.5, "m"); // Using pseudo-code operator 'unit'. +\end{lstlisting} +Note that unit inference has not changed the empty unit of \lstinline!1.5! itself, but that it has introduced an implicit unit cast \emph{around} \lstinline!1.5! in order to fulfill the unit compatibility requirement. +\end{example} + \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} From 232c4fa6918b4ebe5a3059c41bd3330903d3fc4e Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Tue, 1 Nov 2022 14:58:00 +0100 Subject: [PATCH 22/26] Make stronger statement about when unit inference takes place --- chapters/unitexpressions.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 84f48bd06..3b9694f2f 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -224,7 +224,7 @@ \subsection{Bottom-Up Unit Derivation}\label{bottom-up-unit-derivation} \subsection{Unit Inference}\label{unit-inference} In Modelica unit checking, \firstuse{unit inference} refers to the implicit casting of an expression with empty unit to a corresponding expression with non-empty unit. -An expression can only get an inferred unit when appearing in a context where the empty unit is not allowed. +An expression having empty unit always gets an inferred non-empty unit when appearing in a context where the empty unit is not allowed. When encountering the empty unit in the following situations, the inferred unit is (uniquely) determined by ensuring that unit compatibility requirements are fulfilled: \begin{itemize} From 9aeb15f8f0e96475184de4a96c9d381f7488ef8c Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 2 Nov 2022 21:22:31 +0100 Subject: [PATCH 23/26] Change example on undefined unit to user-defined function instead of 'sin' --- chapters/unitexpressions.tex | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 3b9694f2f..4210879a6 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -355,23 +355,23 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} \end{example} \begin{example} -Consider the potential consequences of an undefined unit in the following binding equation: +Consider the potential consequences of an undefined unit in the following binding equation for \lstinline!y!: \begin{lstlisting}[language=modelica] -Real y(unit = "m") = sin(1.57); +function f + input Real u; + output Real y = u; +end f; +Real x(unit = "m2") = 1.57; +Real y(unit = "m") = f(x); \end{lstlisting} -To see that the unit of the binding equation right-hand side is undefined, note that: -\begin{itemize} -\item The \lstinline!Real! literal \lstinline!1.57! has empty unit. -\item The expression \lstinline!sin(1.57)! is not covered by the specification, and hence has undefined unit. -\end{itemize} +To see that the unit of the binding equation right-hand side is undefined, note that the unit of the function call \lstinline!f(x)! is not covered by the specification, and hence has undefined unit. If a tool wants to proceed according to ``standard dimensional analysis'', alternatives include: \begin{itemize} \item - Assume that \lstinline!sin! is a mapping from unit \lstinline!"1"! to unit \lstinline!"1"!. - The unit of \lstinline!1.57! then defaults to \lstinline!"1"! (alternatively, the same unit could be obtained by inference). - The unit of \lstinline!sin(1.57)! is then found to be \lstinline!"1"!, which is an error due to the required unit being \lstinline!"m"!. + Ingore the unit of the input passed to \lstinline!f!, and assume that the call expression always gets the declared unit of the output, namely the empty unit. + As the unit of \lstinline!f(x)! is assumed empty, it gets inferred unit \lstinline!"m"!. \item - Assume that \lstinline!sin! preserves both the unit \lstinline!"1"! and the empty unit. - The empty unit of \lstinline!1.57! gets propagated to \lstinline!sin(1.57)!, which in turn gets inferred unit \lstinline!"m"!. + Analyze \lstinline!f! and conclude that it preserves any unit. + The unit of \lstinline!f(x)! then becomes \lstinline!"m2"!, which is a unit error for the binding equation. \end{itemize} \end{example} From a28b795680a85a0171c41ec0d9e3f228cad56f2f Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 2 Nov 2022 22:08:28 +0100 Subject: [PATCH 24/26] Simplify proposal by not omitting rules concerning non-empty units --- chapters/unitexpressions.tex | 77 ++++++++++-------------------------- 1 file changed, 21 insertions(+), 56 deletions(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index 4210879a6..cc029365b 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -266,47 +266,27 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} This section describes conditions under which an expression has empty unit. Conditions not given here must not be interpreted as definitely not implying empty unit; instead, the unit may be currently undefined for some expressions, allowing the unit to be properly defined in future versions of the specification. -Basic expressions defined to have empty unit: +The following expressions are the only ones having empty unit: \begin{itemize} \item \lstinline!Real! literals. \item - \lstinline!Integer! expressions implicitly cast to \lstinline!Real!. -\end{itemize} - -Expressions defined to \emph{not} propagate the empty unit up the expression tree, thereby forcing inference of unit \lstinline!"1"!: -\begin{itemize} -\item - Addition, subtraction, multiplication and division operators when either operand has non-empty unit. -\item - Right operand of binary exponentiation. -\item - Component references outside of functions, where the component's unit (after unit propagation has been carried out) is empty (possibly by not being specified). - (Unit checking involving user-defined functions with empty unit on inputs and outputs is currently not defined.) -\end{itemize} - -Built-in non-array operators, functions, and special expressions that propagate any unit (including empty) up the expression tree: -\begin{itemize} -\item - When all operands have the same unit: negation, addition, and subtraction (scalar or element-wise), see {array-element-wise-addition-subtraction-and-string-concatenation}. -\item - The \lstinline!abs! function, see \cref{modelica:abs}. -\end{itemize} - -Transcendental functions that propagate both unit \lstinline!"1"! and the empty unit up the expression tree: -\begin{itemize} + \lstinline!Real! component references where the component's unit (after unit propagation has been carried out) is empty (possibly by not being specified). \item - All of the elementary mathematical functions listed in \cref{built-in-mathematical-functions-and-external-built-in-functions}. - (Whether some of these also accept other dimensionless units such as \lstinline!"rad"! for the input argument is currently not defined.) + \lstinline!Integer! expressions implicitly cast to \lstinline!Real!. \item - The only binary of these functions, \lstinline!atan2!, requires both arguments to have the same unit, and accepts any unit. - The result of \lstinline!atan2! has empty unit only when both arguments have empty unit; otherwise the unit of the result is \lstinline!"1"!. -\end{itemize} - -Special situations in which the empty unit is propagated up the expression tree: -\begin{itemize} + The following compound expressions result in the empty unit if and only if all operands have empty unit: + \begin{itemize} + \item \lstinline!Real!-valued numeric operator expressions. + \item Function calls to \lstinline!Real!-valued built-in functions (see \cref{built-in-mathematical-functions-and-external-built-in-functions}, \cref{modelica:der}, \cref{modelica:pre}, \cref{modelica:abs}, \cref{modelica:sqrt}, \cref{modelica:floor}, etc.). + \end{itemize} + If one of the operands has non-empty unit, all operands must have non-empty unit, meaning that operands with empty unit get inferred unit \lstinline!"1"!. \item - Multiplication and division when both operands have empty unit. + Function calls to \lstinline!Real!-valued user-defined functions where: + \begin{itemize} + \item All \lstinline!Real! function inputs and outputs have empty declared unit (possibly by not being specified). + \item All \lstinline!Real! argument expressions have empty unit. + \end{itemize} \end{itemize} \begin{example} @@ -318,8 +298,8 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} \begin{itemize} \item The \lstinline!Real! literal \lstinline!2.5! has empty unit. \item The \lstinline!Integer! literals \lstinline!1! and \lstinline!3! are implicitly cast to \lstinline!Real!, and therefore have empty unit. -\item The multiplication \lstinline!2.5 * 3! has empty unit, as multiplication can propagate the empty unit of both operands. -\item The addition \lstinline!1 + (2.5 * 3)! has empty unit, as addition can propagate any unit as long as both operands have the same unit. +\item The multiplication \lstinline!2.5 * 3! has empty unit, as both multiplication operands have empty unit. +\item The addition \lstinline!1 + (2.5 * 3)! has empty unit, as both addition operands have empty unit. \item The entire right-hand side expression gets inferred unit \lstinline!"m"! in order to be compatible with the component's declared \lstinline!unit!-attribute. \end{itemize} \end{example} @@ -328,32 +308,17 @@ \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit} Consider unit checking of the following erroneous binding equation for \lstinline!y!: \begin{lstlisting}[language=modelica] Real x(unit = "m") = 1.0; -Real y(unit = "m") = x^2 / 2; +Real y(unit = "m") = (x * x) / 2; \end{lstlisting} The unit of the binding equation right-hand side is determined as follows: \begin{itemize} -\item The unit of \lstinline!x! is \lstinline!"m"!, and dimensional analysis gives that \lstinline!x^2! has unit \lstinline!"m2"! -\item The \lstinline!Real! literal \lstinline!1.0! has empty unit, and gets inferred unit \lstinline!"m"!. -\item As the left operand of \lstinline!x^2 / 2! is non-empty, the right operand cannot be empty, and hence empty unit of \lstinline!2! is implicitly cast to \lstinline!"1"!. -\item Dimensional analysis then gives that the unit of \lstinline!x^2 / 2! is \lstinline!"m2"!, which is an error due to the required unit being \lstinline!"m"!. +\item The unit of \lstinline!x! is \lstinline!"m"!, and dimensional analysis gives that \lstinline!x * x! has unit \lstinline!"m2"! +\item The \lstinline!Integer! literal \lstinline!2! is implicitly cast to \lstinline!Real!, and therefore has empty unit. +\item As the left operand of \lstinline!(x * x) / 2! has non-empty unit, the right operand is implicitly cast to unit \lstinline!"1"!. +\item Dimensional analysis then gives that the unit of \lstinline!(x * x) / 2! is \lstinline!"m2"!, which is an error due to the required unit being \lstinline!"m"!. \end{itemize} \end{example} -\begin{example} -Difference between using a literal and a constant: -\begin{lstlisting}[language=modelica] -function f - input Real u(unit = "m"); - output Real y(unit = "m") = u; -end f; -constant Real pi = 3.14; -Real x(unit = "m") = f(3.14); // OK. -Real y(unit = "m") = f(pi); // Error. -\end{lstlisting} -The first call to \lstinline!f! is OK due to unit inference making \lstinline!"m"! the inferred unit of \lstinline!3.14!. -The second call to \lstinline!f! is an error because the component reference \lstinline!pi! has an inferred unit of \lstinline!"1"! by itself, which prevents inference of the unit required by the function call. -\end{example} - \begin{example} Consider the potential consequences of an undefined unit in the following binding equation for \lstinline!y!: \begin{lstlisting}[language=modelica] From 089f554a87f8b5b740ce2531111a549d5613dcb4 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Mon, 7 Nov 2022 22:55:58 +0100 Subject: [PATCH 25/26] Move 'Otherwise...' into item list As suggested by @qlambert-pro. --- chapters/unitexpressions.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index cc029365b..e6ad99a5c 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -244,10 +244,10 @@ \subsection{Unit Inference}\label{unit-inference} % \item The right hand side of an assignment. % \item The direct subexpressions of array construction, array concatenation, and array range. % \end{itemize} +\item + Otherwise, the inferred unit is \lstinline!"1"!. \end{itemize} -Otherwise, the inferred unit is \lstinline!"1"!. - \begin{example} Consider unit inference in the binding equation below: \begin{lstlisting}[language=modelica] From 35e4f01ad3fe493f079535ab54206530a7253cd2 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Thu, 10 Nov 2022 16:40:07 +0100 Subject: [PATCH 26/26] Rule out unit inference for components with empty unit-attribute --- chapters/unitexpressions.tex | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/chapters/unitexpressions.tex b/chapters/unitexpressions.tex index e6ad99a5c..7ac00b8af 100644 --- a/chapters/unitexpressions.tex +++ b/chapters/unitexpressions.tex @@ -231,7 +231,7 @@ \subsection{Unit Inference}\label{unit-inference} \item In binding equations and modifications: \begin{itemize} - \item The entire expression of the binding or modification. + \item The entire expression of the binding or modification, provided that the left-hand side component has non-empty \lstinline!unit!-attribute. \item When the entire expression is an array construction, array concatenation and array range, then apply rules recursively for the direct subexpressions. \end{itemize} \item @@ -260,6 +260,19 @@ \subsection{Unit Inference}\label{unit-inference} Note that unit inference has not changed the empty unit of \lstinline!1.5! itself, but that it has introduced an implicit unit cast \emph{around} \lstinline!1.5! in order to fulfill the unit compatibility requirement. \end{example} +\begin{example} +Consider the following unit error: +\begin{lstlisting}[language=modelica] + RealInput u = 1.5; + RealOutput y(unit = "m"); +equation + connect(u, y); +\end{lstlisting} +Here, the \lstinline!unit!-attribute of \lstinline!u! is empty, but the unit of \lstinline!u! is \lstinline!"m"! after unit propagation. +It follows that the binding equation for \lstinline!u! has a unit error since the inferred unit of \lstinline!1.5! is \lstinline!"1"!. +Note that relaxing the unit inference rules so that \lstinline!1.5! would get inferred unit based on the unit (instead of the \lstinline!unit!-attribute) of \lstinline!u! would be dangerous, as the meaning of \lstinline!1.5! could then change due to unit changes in remote parts of the model. +\end{example} + \subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit}