
\begin{flushright}
\sort{The Triptych Dogma}\\[2mm]
\sf In order to \textsl{specify} \sort{$\mathbb{S}$}\textsl{oftware},
\sf we must understand its \sort{$\mathbb{R}$}\textsl{equirements.}\\[0.5mm]
\sf In order to \textsl{prescribe} \sort{$\mathbb{R}$}\textsl{equirements}
we must understand the \sort{$\mathbb{D}$}\textsl{omain}.\\[0.5mm]
\sf So we must \textsf{study, analyze} and \textsf{describe} \sort{$\mathbb{D}$}\textsl{omains.}\\[0.5mm]
\sort{{$\mathbb{D}$,$\mathbb{S}$ $\models$ $\mathbb{R}$:}}

\cacm{{In proofs of $\mathbb{S}$\textsl{oftware} correctness,\\ with respect to
$\mathbb{R}$\textsl{equirements},\\ assumptions are made with respect to the
$\mathbb{D}$\textsl{omain.}}}

\end{flushright}\rm%

\mnewfoil
 
\noindent
We present a systematic \sfsl{method}, its
      \sfsl{principles}, 
      \sfsl{procedures}, 
      \sfsl{techniques} 
      and 
      \sfsl{tools}, 
      for efficiently \sfsl{analyzing} \&\ \sfsl{describing} domains.
      This paper is based on \cite{BjornerFAoC2015MDAAD,BjornerTOSEM2018,BjornerMonograph2020}.
      It simplifies the methodology of these considerably -- as well as introduces
      some novel presentation and description language concepts.

   %%%   \tableofcontents

\pmlp{\treprikker
 
\noindent
\sort{Alert:} Before You start reading this paper, You are kindly informed of the following:

\highlight{What The Paper is All About}{The \sfsl{Triptych Dogma},
  above, says it all: this paper is about a new area of computing
  science -- that of \sfsl{domains}. It is about what domains are. How
  to model them. And their role in software development. There are
  many ``domain things'' it is not about: it is not about `derived' properties of
  domains -- beyond, for example, \sfsl{intentional pull}
  [Sect.\,\vref{Intentional Pull}]. Such are
  left for studies of domains based on the kind of formal domain
  descriptions such as those advocated by this paper\dbsquare}


\highlight{A Radically New Approach to Software Development}{The \sfsl{Triptych Approach to Software
  Development}, calls for \sfsl{software} to be developed on the basis of
  \sfsl{requirements prescriptions}, themselves developed on the basis
  of \sfsl{domain descriptions}. We furthermore advocate these
  specifications and their development be formal. That is: there are
  formal methods for the development of either of these three kinds of
  specifications:
\begin{itemize}
\item Development of domain descriptions is outlined in
      this paper.
  
\item Development of requirements, from domain descriptions, is outlined in
  \cite[\sfsl{Chapter 9}]{BjornerMonograph2020}.
  
\item Development of software, from  requirements prescriptions, is treated,
  extensively, in \cite{TheSEBook123}.
\end{itemize}

\noindent
The reader should understand that the current paper, with its 
insistence of strictly following a method, formally, is at odds with
current `software engineering'  practices.\dbsquare}


\highlight{Characterizations rather than Definitions}{The object of
  domain study, analysis and description, i.e., the domains, are,
  necessarily, informal. A resulting domain description is formal. So
  the domain items being studied and analyzed cannot be given a formal
  definition.
  Conventionally [so-called theoretical] computer scientists expect and
  can seemingly only operate in a world of clearly defined
  concepts. Not so here. It is not possible. Hence we use the term
  `characterization' in lieu of `definition'\dbsquare}


\highlight{Seemingly Fragmented Texts}{The text of this paper is a
  sequence of enumerated sections, subsections, sub-subsections and paragraphs,
  with short {\sc Highlights, Characterizations, Examples,} {\sc Ontological
  Choices, Prompts, Schemas} and ordinary short texts. The brevity is intentional. Each
  and all of these units outline important concepts. Each contain a
  meaning and can be read ``in isolation''\dbsquare}
}

\nbbbbb{Domains}\HHHH

\begynd
\pind We start by delineating the informal concept of
domain,\footnote{Our use of the term `domain' should not be confused
  with that of \textsf{Dana Scott}'s Domain Theory:
  \texttt{https://\-en.\-wi\-ki\-pe\-di\-a.\-org/\-wi\-ki/\-Scott\_\-do\-main}.} 
\afslut

\nbbbb{What are They\,?}\HHHH

\begynd
\pind What do we mean by `domain'\,?
\afslut

\characterization{Domain}{
\begynd
\pind By a \sfsl{domain} we shall understand
\begynd
\pind a \sfsl{rationally describable} segment of
\pind a \sfsl{discrete dynamics} fragment of
\pind a \sfsl{human assisted} reality: the world that we
      daily observe -- in which we work and act, a reality made
      significant by human-created entities.
\afslut
\pind The domain embody
\begynd
\pind \sfsl{endurants}
\pind and \sfsl{perdurants} \dbsquare
\afslut
}

\illustration{Some Domain Examples}{A few, more-or-less self-explanatory examples:
\begin{itemize}
\item \sort{Rivers} -- with their natural sources, deltas, tributaries,
  waterfalls, etc., and their man-made dams, harbours, locks, etc. --
  and their conveyage of materials (ships etc.) \cite[\sfsl{Chapter B}]{Bjorner2024:DomainModelsACompendium}.
\item \sort{Road nets} -- with street segments and intersections, traffic
  lights and automobiles -- and the flow of these \cite[\sfsl{Chapter E}]{Bjorner2024:DomainModelsACompendium}.
\item \sort{Pipelines} -- with their liquids (oil, or gas, or water), wells, pipes, valves, pumps, forks,
  joins and wells and the flow of fluids \cite[\sfsl{Chapter I}]{Bjorner2024:DomainModelsACompendium}.
\item \sort{Container terminals} -- with their container vessels, containers,
  cranes, trucks, etc. -- and the movement of all of these\cite[\sfsl{Chapter K}]{Bjorner2024:DomainModelsACompendium}\dbsquare
\end{itemize}}

\noindent
\mnewfoil%\LLLL
\begynd
\pind Characterization\,\vref{def:Domain} relies on the understanding of the terms
      \sfsl{`rationally describable'}, \sfsl{`discrete dynamics'}, \nyl \sfsl{`human
      assisted'}, \nyl \sfsl{`solid'} and \sfsl{`fluid'}.
 The last two will be explained later.
\pind By \sort{\sfsl{rationally describable}} we mean that what is described
      can be understood, including reasoned about, in a rational,  that is,
      logical manner -- {in other words  \sort{\sfsl{logically
            tractable}}.}\footnote{Another, ``upside--down'' -- after
        the fact -- [perhaps `cheating'] way of
        defining `describable' is: is it describable in terms of the
        method of this paper\,!}
\pind By \sort{\sfsl{discrete dynamics}} we imply that we shall basically
      rule out such domain phenomena which have
      properties which are continuous with
      respect to their time-wise\pos{, i.e., dynamic,}{} behaviour.
\pind By \sort{\sfsl{human-assisted}} we mean that the domains -- that we are
      interested in modeling -- have, as an important property, that
      they possess man-made entities.
\afslut

\nbbbb{Some Introductory Remarks}

\bbb{A Discussion of Our Characterization of a Concept of Domain}

\begynd
\pind Characterization\,\vref{def:Domain} is our attempt to delineate
      the subject area.
\begynd
\pind That is, ``our'' concept of \sfsl{`domain'} is `novel':
\begynd
\pind \sfsl{new and not resembling something formerly known or used}. 
\afslut 
\pind As such it may be unfamiliar to most readers.
\afslut
\pind So it takes time to digest that characterization.
\pind So the reader may have to return to the page, Page\,\pageref{def:Domain},
\pind to be reminded of the definition.
\afslut

\nbbb{Formal Methods and Description Language}

The reader is assumed to have a reasonable grasp of formal methods --
such as espoused in \cite{e:db:Bj78bwo,e:db:Bj82b,TheSEBook123,m:z:jd+jcppw96}.

The descriptions evolving from the modeling approach of
  this paper are in the abstract, model-oriented specification
  language \texttt{RSL} \cite{RSL} of the
  \sort{R}aise\footnote{\sort{RAISE} stands for \sort{R}igorous
    \sort{A}pproach to \sort{I}ndustrial \sort{S}oftware
    \sort{E}ngineering \cite{RaiseMethod}.}
  \sort{S}pecification \sort{L}anguage. But other abstract
  specification languages could be used: \texttt{VDM} \citevdm,
  \texttt{Z} \citez, \texttt{Alloy} \citealloy, \texttt{CafeOBJ}
  \citecafeobj, etc.
\pind We have chosen \texttt{RSL} since it embodies a variant of
\texttt{CSP} \citecsp\ -- being used to express domain behaviours.
\afslut

\nbbb{Programming Languages versus Domain Semantics}

\begynd
\pind From around the late 1960s, 
\begynd
\pind spurred on by the works of
      \textsf{John McCarthy, Peter Landin, Christopher
      Strachey, Dana Scott} and others,
\pind it was not unusual to see publications of entire formal
      definitions of programming language semantics.
\pind Widespread technical reports were \cite[1969, 1974]{ULD69,Bek74-old}
\pind Notably so was \cite[1976]{MilR76}.
\pind There was the 1978 publication \cite[\sfsl{Chapter 5, Algol 60}, 1978]{e:db:Bj78bwo}. 
\pind Others were \cite[\sfsl{Chapters 6--7, Algol 60 and Pascal}, 1982]{e:db:Bj82b}
\pind As late as into the 1980s there were such publications \cite[1980]{LNCS98}.
\afslut

\pind Formal descriptions of domains, such as we shall unravel a method
      for their study, analysis and description,
\begynd
\pind likewise amount to semantics
\pind for the terms of the professional languages  
\pind spoken by stakeholders of domains.
\afslut
\pind So perhaps it is time to take the topic serious.
\afslut

\nbbb{A New Universe}\label{sss:A New Universe}

\begynd
\pind The concept of domain -- such as we shall delineate and treat it
      -- is novel.
\begynd
\pind That is: new and not treated in this way before.
\pind Its presentation, therefore, necessarily involves the
      introduction of a new universe of concepts.
\pind Not the neat, well-defined concepts of neither ``classical'' computer
      science nor software engineering.
\afslut
\pind It may take some concentration on the part of the reader
\pind to get used to this\,!

\pind You will therefore be introduced to quite a universe of
      new concepts.
\begynd
\pind You will find these concepts named in most display
      lines\footnote{-- that is, section, subsection, sub-subsection, paragraph and
      sub-paragraph lines} and in
      Figs.\,\vref{onto.fig0} and \vref{MAJlexicon}.
\afslut
\afslut

\nbbbbb{Six  Languages}

\input{Nlanguages}

\nbbbbb{Endurants and Perdurants, I}

\begynd
\pind The above characterization hinges on the  characterizations of
\begynd
\pind endurants and
\pind perdurants.
\afslut
\afslut
    
\characterization{Endurants}{ Endurants are \pdefindex{endurant}\ 
      those quantities of domains that we can
      observe (see and touch), in \sfsl{space}, as ``complete''
      entities at no matter 
      which point in \sfsl{time} -- ``material'' entities that
      persists, endures -- capable of enduring adversity, severity, or
      hardship {[Merriam Webster]}\dbsquare}%%%%

\pind \sfsl{Endurants} are
\begynd
\pind either \sfsl{natural} [``God-given''] 
\pind or \sfsl{artefactual} [``man-made''].
\afslut
Endurants may be either solid (discrete) or fluid, and solid
endurants, called parts, may be considered
\begynd
\pind \sfsl{atomic} or  \sfsl{compound} parts;
\pind or, as in \pos{this \compendium}{this talk} solid endurants may be further unanalysed  \sfsl{living
      species:}
\begynd
\pind \sfsl{plants} and \sfsl{animals} -- including \sfsl{humans}.
\afslut
\afslut

\characterization{Perdurants}{ Perdurants are \pdefindex{perdurant}\   
      those quantities of domains for which only a
      fragment exists, in \sfsl{space}, if we look at or touch them at
      any given snapshot in
      \sfsl{time} \nycacm{[Merriam Webster]}\dbsquare}%%%%

\noindent
\pind \sfsl{Perdurants} are here considered to be
\begynd
\pind \sfsl{actions}, 
\pind \sfsl{events} and 
\pind \sfsl{behaviours}.
\afslut
\afslut
\treprikker
\noindent
We exclude, from our treatment of domains, issues of living species, ethics, biology and
psychology.

\nbbbbb{A Domain Analysis \& Description Ontology}\label{sec:Ontology}\label{An Upper Ontology}

\bbbb{The Chosen Ontology}

\begynd
\pind Figure\,\ref{onto.fig0} expresses an
      ontology\footnote{An ontology is the
        philosophical study of being. It investigates what types of
        entities exist, how they are grouped into categories, and how
        they are related to one another on the most fundamental level
        (and whether there even is a fundamental level) \wiki.} for our
      analysis  of domains.
\pind Not a taxonomy\footnote{A taxonomy (or taxonomic
      classification) is a scheme of classification, especially a
      hierarchical classification, in which things are organized into
      groups or types \wiki.}  for any one specific domain.
\afslut

\begin{figure}[ht]
  \begin{center}
    \epsfig{file=onto.eps,height=10.4cm}
    \caption{{A Domain Analysis \& Description Ontology}}
    \label{onto.fig0}
  \end{center}
\end{figure}
  
\noindent
\begynd
\pind The idea of Fig.\,\vref{onto.fig0} is the following:
\begin{itemize}
\item It presents a recipe for how to \sort{analyze} a domain.
\item You, the \sfsl{domain \sort{analyzer} cum describer}, are
      \sfsl{`confronted'}\footnote{By `confronted' we mean: You are reading about it,
      in papers, in books, in postings on the \texttt{Internet}, visiting
      it, talking with domain stakeholders: professional people working
      ``in'' the domain; You may, yourself, ``be an entity'' of that domain\,!} with, or by a domain.
\item You have Fig.\,\vref{onto.fig0} in front of you, on a piece of
      paper, or in Your mind, or both.
\item You are then asked, by the domain \sort{analysis} \& description method
      of this paper, to ``start'' at the uppermost $\bullet$, just
      below and between the `\sort{r}'
      and the first `\sort{s}' in the main title, \textsf{Phenomena of Natural and
      Artefactual Unive\underline{\sort{rs}}es of Discourse}.
\item The \sort{analysis} \& description ontology of Fig.\,\ref{onto.fig0}
      then \sfsl{directs} You to inquire as to whether the phenomenon
      -- whichever You are ''looking at/reading about/...'' -- is either
      \sfsl{rationally describable}, i.e., is 
      an \sfsl{entity} (\texttt{is\_entity}) or is \sfsl{indescribable}.
\item That is, You are, in general, ``positioned'' at a bullet,
       $\bullet$, labeled $\alpha$,
       ``below'' which there may be two alternative bullets,
      one, $\beta$, to the right and one to the left, $\gamma$. 
\item It is Your decision whether the answer to the ``query'' that
      each such situation warrants, is yes, \texttt{is\_}$\beta$, or
      no, \texttt{is\_}$\gamma$. 
\item The characterizations of the concepts whose names,
      $\alpha,\beta,\gamma$ etc., are attached to the
      $\bullet$s of Fig.\,\ref{onto.fig0} are given in the following sections.
\item Whether they are precise enough to guide You in Your obtaining
      reasonable answers, ``yes'' or ``no'', to the $\bullet$ed queries is, of
      course, a problem. I hope they are.
\item If Your answer is ``yes'', then Your \sort{analysis} is to
      proceed ``down the tree'', usually indicated 
      by ``yes'' or ``no'' answers. 
\item If one, or the other is a ``leaf'' of the
      ontology tree, then You have finished examining the phenomena You set
      out to \sort{analyze}.
\item If it is not a leaf, then further \sort{analysis} is required.
\item (We shall, in this \compendium, leave out the analysis and hence
      description of \sfsl{living species}.)
\item If an \sort{analysis} of a phenomenon has reached one of the (only) two
      \dbsquare's, then the \sort{analysis} at that $\bullet$ results in the
      domain describer \sort{describing} some of the properties of
      that phenomenon. 
\item That \sort{analysis} involves ``setting aside'', for subsequent
      \sort{analysis \& description}, one or more [thus \sort{analysis}
      etc.-pending] phenomena (which are subsequently to be tackled
      from the ``root'' of the ontology).
\end{itemize}
\noindent
\pind We do  not [need to] prescribe in which order You analyze \& describe
      the phenomena that has been ``set aside''.
\afslut

\treprikker

\noindent
\begynd
\pind In Fig.\,\vref{onto.fig0} You will have noticed the positioning
of the concepts of $\mathbb{TIME}$ and $\mathbb{SPACE}$ ``right
under'' the \textsl{Phenomena} bullet $\bullet$.
These two concepts are neither endurants not perdurants. And they are
not attributes of either. They can, however, as shown by S{\o}rlander
\cite{kaisorlander2023}, be transcendentally deduced by rational reasoning.
\afslut

\nbbbb{Discussion of The Chosen Ontology}

\begynd
\pind We shall in the following motivate the choice of the
      \sfsl{ontological classification} reflected in Fig\,\vref{onto.fig0}.
\begynd
\pind We shall argue that this classification is not ``an accidental choice''.
\pind In fact, we shall try justify  the classification 
\pind with reference to the philosophy of \textsf{Kai S{\o}rlander}
\cite{kaisorlander1994,kaisorlander2016,kaisorlander2022,kaisorlander2023}%
\footnote{The
      2022 book, \cite{kaisorlander2022}, is presently a latest in \textsf{Kai
        S{\o}rlander}'s work. It refines and further develops the
      theme of the earlier, 1994--2016 books. \cite{kaisorlander2023} is an English
      translation of \cite{kaisorlander2022}}. 
\pind \textsf{Kai S{\o}rlander}'s aim in these books is to examine
\pind \sfsl{that which is absolutely necessary, inevitable, in any description of the world.}
\afslut 
\pind In \cite[\sfsl{Chapter\,2}]{BjornerMonograph2020} we present a
      summary of  \textsf{S{\o}rlander}'s philosophy.
\pind In paragraphs, in the rest of this paper, marked
      \sort{{\sc Ontological Choice}}, we shall relate
      \textsf{S{\o}rlander}'s philosophy's ``inevitability'' to the
      ontology for studying domains.   
\afslut

\nbbbbb{The Name, Type and Value Concepts}\label{The Name, Type and Value Concepts}

\begynd
\pind Domain \sfsl{modeling}, as well as \sfsl{programming},
\begynd
\pind depends, in their \sfsl{specification},
\pind on \sfsl{separation of concerns:}
\begynd
\pind which kind of \sfsl{values} are subjectable to which kinds of \sfsl{operations},
\pind etc., 
\afslut
\pind in order to achieve
\begynd
\pind ease of \sfsl{understanding} a model or a program,
\pind ease of \sfsl{proving properties} of a model, 
\pind or \sfsl{correctness} of a program.
\afslut
\afslut
\afslut

\nbbbb{Names}\label{DomainsINames}

\begynd
\pind We name things in order to refer to them in our speech, models
      and programs.
\pind Names of types and values in models and programs are usually not
      so-called ``first-citizens'', i.e., values that can be arguments
      in functions, etc.
\pind The ``science of names'' is interesting.\footnote{The study of
  names is called \sfsl{onomastics} or \sfsl{onomatology}. \sfsl{Onomastics} covers the
  naming of all things, including place names (toponyms) and personal
  names (\sfsl{anthroponyms}).} 
\pind In
\texttt{bo\-tan\-i\-cal\-so\-ci\-e\-ty.\-org.\-za/\-the-\-science-\-of-\-names-\-an-\-in\-tro\-duct\-ion-\-to-\-plant-\-tax\-o\-no\-my}
the authors actually speak of a ``science of names'' in connection with
plant taxonomy: the ``art'' of choosing such names that reflect some
possible classification of what they name.
\afslut

%\mtc

\nbbbb{Types}\label{DomainsIValues}
\begynd
\pind The type concept is crucial to programming and modeling.
\afslut

\characterization{Type}{A \sfsl{type} is a class, i.e., a further
  undefined set, of values (``of the same kind'') \dbsquare} 

\noindent
\begynd
\pind We name types.
\afslut

\illustration{Type Names}{Some examples of type names are:
\begin{itemize}
\item \textsf{RT} -- the class of all road transport instances: the
  \sfsl{Metropolitan London Road Transport}, the \sfsl{US Federal
  Freeway System}, etc.
\item \textsf{RN} -- the class of all road net instances (within a road transport).
\item \textsf{SA} -- the class of all automobiles (within a road
  transport) \dbsquare
\end{itemize}
}
\noindent
\begynd
\pind You, the domain describer, choose type names.
\begynd
\pind Choosing type names is a ``serious affair''.
\pind It must be done carefully.
\pind You can choose short (as above) or long names: \textsf{Road\_Transport},
      \textsf{Road\_Net}, etc.
\pind We prefer short, but not cryptic names, like \textsf{X, Y, Z,
      ...} .
\pind Names that are easy to \sfsl{memorize}, i.e., \sfsl{mnemonics}.
\afslut
\afslut

\nbbbb{Values}

\begynd
\pind Values are what  programming and modeling, in a sense,
      is all about''.
\pind In  programming, values are the \sfsl{data} ``upon'' which the
      program code specifies computations.
\pind In modeling values are, for example, what we observe: the entities in front of
      our eyes.
\afslut


\nbbbbb{Phenomena and Entities}\HHHH

\begynd
\pind \characterization{Phenomena}{ {\pdefindex{phenomenon} By a
\sfsl{phenomenon} we shall understand a fact that is
     observed to exist or happen\dbsquare}}

\noindent
\begynd
\pind Some phenomena are rationally describable -- to some
      degree\footnote{That is: It is up to the domain analyzer cum describer
      to decide as to how many rationally describable phenomena to select
      for analysis \& description. Also in this sense one practices
      abstraction by ``abstracting
      away'' [the analysis \& description of] phenomena that are irrelevant
      for the ``current'' (!) domain description.} -- others are not. 
\afslut

\noindent
\pind \characterization{Entities}{By an entity \pdefindex{entity} By
      an \sfsl{entity} 
      we shall understand a more-or-less rationally describable
      phenomenon\dbsquare} 

\noindent
\prompt{\texttt{is\_entity}}{\label{dal:entity}We introduce the informal presentation language predicate
\texttt{is\_entity}. It holds for phenomena {$\phi$} if {$\phi$} is describable\dbsquare}

A \sfsl{prompt}\dbeat{, i.e., a \sfsl{cue}}\footnote{French:
  \sfsl{mot-cl{\'e}}, German: \sfsl{stichwort}, Spanish:
  \sfsl{palabra clave}} is an informal ``advice'' to the domain
  analyzer to ``perform'' a mental inquiry wrt.\ the real-life domain
  being studied.

\noindent
\illustration{Phenomena and Entities}{Some, but not necessarily
  all aspects of a river can
  be rationally described, hence can be still be considered
  entities. Similarly, many aspects of a
  road net can be rationally described, hence will be considered
  entities\dbsquare}

\noindent
{If You are not happy with this `characterization', then substitute
  ``rationally describable'' with: \sl describable in terms of the
  endurants and perdurants brought forward in this paper: their
  external and internal qualities, unique identifiers, mereologies amd
  attributes, channels and  behaviours\,!\rm}

\scsort{Phenomena}{We choose to ``initialize'' our ontological
``search'' to a question of whether a phenomenon is rationally
describable -- based on the tenet of \textsf{Kai S{\o}rlander}'s
philosophy, namely that ``whatever'' we postulate is either
\sfsl{true} or \sfsl{false} and that \sfsl{a principle of
contradiction} holds: \sfsl{whatever we so express can not both hold and
not hold}\dbsquare}

\textsf{Kai S{\o}rlander} then develops his inquiry -- \sfsl{as to what is
absolutely necessary in any description of the world} -- into the
rationality of such descriptions necessarily be based on time and
space and, from there, by a series of transcendental deductions, into
a base in \sfsl{Newton}'s physics. We shall, in a sense, stop there. That is,
in the domain concept, such as we have delineated it, we shall not
need to go into \sfsl{Einsteinian} physics.

\nbbbbb{Endurants and Perdurants, II}

We repeat our characterizations of endurants and perdurants.

\nbbbb{Endurants}

\begynd
\pind We repeat characterization\,\vref{def:Endurants}.

\pind \characterization{Endurant}{ Endurants are \pdefindex{endurant}\ 
      those quantities of domains that we can
      observe (see and touch), in \sfsl{space}, as ``complete''
      entities at no matter 
      which point in \sfsl{time} -- ``material'' entities that
      persists, endures -- capable of enduring adversity, severity, or
      hardship \nycacm{[Merriam Webster]}\dbsquare}%%%%
      
\noindent
\illustration{Endurants}{ Examples of endurants are: a street segment
      [link], a street intersection [hub], an 
      automobile\dbsquare}

\noindent
\prompt{\texttt{is\_endurant}}{ \label{dal:endurant}We introduce the
  informal presentation language predicate 
\texttt{is\_endurant} to hold for entity \textsf{e} if
\texttt{is\_endurant(e)} holds\dbsquare}

\nbbbb{Perdurants}

We repeat characterization\,\vref{def:Perdurants}.
\begynd
\pind \characterization{Perdurant}{ Perdurants are \pdefindex{perdurant}\   
      those quantities of domains for which only a
      fragment exists, in \sfsl{space}, if we look at or touch them at
      any given snapshot in
      \sfsl{time} \nycacm{[Merriam Webster]}\dbsquare}%%%%
  
\noindent
\illustration{Perdurant}{ A moving automobile is an example of a
  perdurant\dbsquare} 
        
\dbeat{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\noindent
\pind Domain perdurants, when eventually modeled in software, typically
      become processes. Hence the careful analysis of domain perdurants is a
      prerequisite for subsequent careful conception and analyses of
      functions (procedures).
\afslut}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%
    
\noindent
\prompt{\texttt{is\_perdurant}}{ \label{dal:perdurant}We introduce the
  informal presentation language predicate 
\texttt{is\_perdurant} to hold for entity \textsf{e} if
\texttt{is\_perdurant(e)} holds\dbsquare}

\nbbbb{Ontological Choice}

\begynd
\pind The \sort{ontological choice} of entities being ``viewed'' as either endurants or
      perdurants is motivated as follows:
\begynd
\pind The concept of endurants 
\begynd
\pind can be justified in terms of Newton's physics 
\pind without going into kinematics, i.e., without including time considerations.
\afslut
\pind The concept of perdurants  
\begynd
\pind can then, on one hand, be justified in terms of Newton's physics
\pind now taking time into consideration, 
\pind hence kinematics, and from there causality, etc.;
\pind and, on the other hand, and as we shall see,
\pind by transcendentally deducing perdurants from solid endurants\dbsquare
\afslut
\afslut
\afslut
 
\nbbbbb{External and Internal Endurant Qualities}\label{sec:External
  and Internal Endurant Qualities}
 
\begynd
\pind The main contribution of this section is that of a calculus of
      domain analysis and description prompts.
\pind Two facets are being presented.
\begynd
\pind Aspects of a domain science: of how we suggest domains can, and should, be
      viewed -- ontologically.
\pind And aspects of a domain engineering:  of how we suggest domains
      can, and should, be analyzed and described.
\afslut
      
\pind We begin by characterizing the two concepts: \textsf{external}
and  \textsf{internal qualities}.
\afslut

\characterization{External Qualities}{ \pdefindex{external quality}\
     External qualities of endurants of a manifest domain 
\begynd
\pind are, in a simplifying sense, those we can
\begynd
\pind {see,}
\pind touch and
\pind have spatial extent.
\afslut
\pind They, so to speak, take form.
\afslut}

\characterization{Internal Qualities}{ Internal qualities are
  \pdefindex{internal quality} 
\begynd
\pind those properties [of endurants]
\pind that do not occupy \sfsl{space}
\pind but can be measured or spoken about\dbsquare
\afslut}%%%%

\noindent
\begynd
\pind Perhaps we should instead label these two qualities \textsf{tangible}
      and  \textsf{intangible qualities}.
\afslut

\scsort{Rationality}{The rational, analytic philosophy issues
  of the inevitability of these qualities is this: (i) can they be
  justified as inevitable, and (ii) can they be suitably
  ``separated'', i.e., both disjoint and exhaustive\,? Or are they
  merely of empirical nature\,?
  The choice here is also that we separate our
  inquiry into examining \sfsl{both external and internal
  qualities} of endurants [not `either or']\dbsquare}

\nbbbb{External Qualities -- Tangibles}\label{sec:ExternalQualities}


\noindent
\illustration{External Qualities}{ An example of external qualities of
  a domains is:
\begynd
\pind the Cartesian\footnote{\LLLL Cartesian
      after the French philosopher, mathematician, scientist Ren{\'e}
      Descartes (1596--1650)} 
\begynd
\pind of sets of solid atomic street intersections, and
\pind of sets  of solid atomic street segments, and 
\pind of sets  of solid automobiles
\afslut of a road transport system
\pind  where  
\begynd
\pind \sl Cartesian, 
\pind \pind sets, 
\pind atomicity\rm, and 
\pind \pind \sl solidity \rm
\afslut
reflect external qualities\dbsquare
\afslut}
%%%%%%%
    
\nbbb{The Universe of Discourse}

\begynd
\pind The most immediate external quality of a domain is the
      ``entire'' domain -- ``itself''\,!
\begynd
\pind So any domain analysis starts by identifying that ``entire'' domain\,!
\pind By giving it a name, say \textsf{UoD}, for \sfsl{universe of discourse},
\pind Then describing it, in \sfsl{narrative} form, that is, in natural
      language containing terms of professional/technical nature, the domain.
\pind And, finally, \sfsl{formalizing} just the name: giving the name
      ``status'' of being a type name, that is, of the type of a class of
      domains whose further properties will be described subsequently.
\afslut
\afslut

\skema{The Universe of Discourse}{\label{su:uod}%
%\RSLatex
%   &\sort{Narration:}&
%        &\rm The name, and hence the type, of the domain is\sf\ & UoD
%        &The& UoD &domain can be briefly characterized by ...&
%   &\sort{Formalization:}&
%        type UoD &\dbsquare&
%\endRSLatex
\bp
\>\ \sort{Narration:}\\
\>\>\>\>\rm The name, and hence the type, of the domain is\sf\  UoD\\
\>\>\>\>The UoD domain can be briefly characterized by ...\\
\>\ \sort{Formalization:}\\
\>\>\>\>\kw{type} UoD \dbsquare
\ep
}

\nbbb{Solid and Fluid Endurants}

\begynd
\pind Given then that there are endurants
\begynd
\pind we now postulate that they are either [mutually exclusive] \sfsl{solid} (i.e., discrete) or \sfsl{fluid.}
\afslut
\afslut

\scsort{Solids vs. Fluids}{Here we [seem to] make a practical choice,
not one based on a philosophical argument, one of logical necessity,
but one based on empirical evidence. It is possible for endurants to
either be solid or fluid; and here we shall not consider the case
where solid [fluid] endurants, due to being heated [cooled], enters a fluid state [or
vice versa]\dbsquare}

\bb{Solid cum Discrete Endurants.}

\characterization{Discrete cum Solid Endurants}{By a
      \sfsl{solid} cum \sfsl{discrete} endurant we shall understand
      an endurant  which is  separate,  individual or distinct in form or concept,
      or, rephrasing, have body (or magnitude)
      of three-dimensions: length (or height), breadth and depth
      \cite[\sfsl{OED, Vol.\,II, pg.\,2046}]{OED}\dbsquare}%

\noindent
\illustration{Solid Endurants}{Pipeline system examples of solid endurants are
\sl
\begynd 
\pind wells,
\pind pipes,
\pind valves,
\pind pumps, 
\pind forks, 
\pind joins \rm and \sl
\pind sinks \rm
\afslut
of pipelines.  (These
  units may, however, and usually will, contain fluids, e.g., oil, gas
  or water.)\dbsquare
\afslut}

\prompt{\texttt{is\_solid}}{\label{dal:solid}%
We introduce the informal presentation language predicate
\texttt{is\_solid} to hold for endurant \textsf{e} if
\texttt{is\_solid(e)} holds\dbsquare}

\bb{Fluids.}

\characterization{Fluid Endurants}{
\begynd
\pind By a \sfsl{fluid endurant} we shall understand  an endurant \nyl which is 
\begynd
\pind prolonged, without interruption, \nyl in an unbroken series or pattern;
\pind or, rephrasing:  a substance (liquid,
  gas or plasma) having the property of flowing, consisting of
  particles that move  among themselves \cite[\sfsl{OED, Vol.\,I, pg.\,774}]{OED}
  \dbsquare
\afslut}
%%%%%%% ****
\afslut

\noindent
\illustration{Fluid Endurants}{ Examples of fluid endurants are:
  \pos{}{\begin{multicols}{3}} \sl
\begynd
\pind water, \pind oil, \pind gas,
  \pind compressed air, \pind smoke\dbsquare
  \afslut \rm
\pos{}{\end{multicols}}}


\mnewfoil

\noindent
\begynd
\pind Fluids are otherwise
\begynd
\pind liquid, or
\pind gaseous, or
\pind plasmatic, or
\pind granular\footnote{\label{fn.granular} This is a purely
  pragmatic decision. ``Of course'' sand, gravel, soil, etc., are not
  fluids, but for our modeling purposes it is convenient to
  ``compartmentalise'' them as fluids\,!}, or
\pind plant products, i.e., chopped sugar cane, threshed, or
otherwise\footnote{See footnote \ref{fn.granular}.},
\pind et cetera.
\afslut
\pind Fluid endurants will be analyzed and described \nyl in relation to
      solid endurants, viz.\ their ``containers''.
\afslut

\prompt{\texttt{is\_fluid}}{\label{dal:fluid}%
We introduce the informal presentation language predicate
\texttt{is\_fluid} to hold for endurant \textsf{e} if
\texttt{is\_fluid(e)} holds\dbsquare}

\nbbb{Parts and Living Species Endurants}

\begynd
\pind Given then that there are solid endurants
\begynd
\pind we now postulate that they are either [mutually exclusive]
\sfsl{parts} or \sfsl{living species.}
\afslut
\afslut

\scsort{Parts and Living Species}{With S{\o}rlander,
\cite[\sfsl{Sect.\,5.7.1, pages\,71--72}]{kaisorlander2023}
we reason
that one can distinguish between parts and living species\dbsquare}

\nbb{Parts}\label{chapDomainsI:Parts}
  
\begynd
\pind \characterization{Parts}{ \pdefindex{parts}\
\begynd
\pind The non-living species solids are what we shall call parts\dbsquare
\afslut}

\noindent
\pind Parts are the ``work-horses'' of man-made domains.
\pind That is, we shall mostly be concerned  \nyl with the analysis and
      description of endurants into parts.
\afslut

\illustration{Parts}{Example\,\ref{eks:Solid Endurants}, of solids,
  is an example of parts\dbsquare}

\noindent
\prompt{\texttt{is\_part}}{\label{dal:part}%
We introduce the informal presentation language predicate
\texttt{is\_part} to hold for solid endurants \textsf{e} if
\texttt{is\_part(e)} holds\dbsquare}

\noindent
\begynd
\pind We distinguish between atomic and compound parts.
\afslut

\scsort{Atomic and Compound Parts}{It is an empirical fact that parts can be
composed from parts. That possibility exists. Hence we can
[philosophy-wise] reason likewise\dbsquare}

\subparagraph{Atomic Parts.}

\dbeat{%%%%%%%%%%%%%%%%%%
\begin{definition}{\rm\label{def:Atomic Part}
      By an \textsl{atomic part} we shall understand a part
      which the domain analyzer considers to be indivisible
      in the sense of not meaningfully consist of sub-parts \dbsquare}
\end{definition}
}%%%%%%%%%%%%%%%%%%%%%%%%%
    
\characterization{Atomic Part}{By an \textsl{atomic part} we shall understand a part
which the domain analyzer considers to be indivisible
in the sense of not meaningfully consist of sub-parts \dbsquare}

\illustration{Atomic Parts}{ Examples of atomic parts are:
\begynd 
\pind hubs, \textsf{H}, i.e.,  street intersections;
\pind links, \textsf{L}, i.e., the stretches of roads between two neighbouring hubs; and
\pind automobiles, \textsf{A}:
\afslut
%\RSLatex
%   type H, L, A & \dbsquare&
%\endRSLatex 
\bp
\>\ \kw{type} H, L, A  \dbsquare
\ep
}

\noindent
\prompt{\texttt{is\_atomic}}{\label{dal:atomic}%
We introduce the informal presentation language predicate
\texttt{is\_atomic} to hold for parts \textsf{p} if
\texttt{is\_atomic(p)} holds\dbsquare}

\subparagraph{Compound Parts.}
  
\characterization{Compound Part}{ %
\begynd
\pind {Compound} {part}s are those which are observed to
[potentially] consist of several parts \eod
\afslut
}

\illustration{Compound Parts}{ An example of a compound parts is: a road net consisting of
\begynd
\pind  a set of hubs,
  i.e., street intersections or ``end-of-streets'',  and
\pind a set of
  links, i.e., street segments (with no contained hubs),
\afslut
 is a Cartesian compound;
\begynd
\pind and the sets of hubs and the sets of links
\afslut are part set compounds\dbsquare}

\noindent
\prompt{\texttt{is\_compound}}{\label{dal:compound}%
We introduce the informal presentation language predicate
\texttt{is\_compound} to hold for parts \textsf{p} if
\texttt{is\_compound(p)} holds\dbsquare}

\noindent
\begynd
\pind We, pragmatically, distinguish between
\begynd
\pind Cartesian product- and set-oriented parts.
\afslut
\afslut

\scsort{Cartesians}{The Cartesian versus set parts is an
empirical choice. It is not justified in terms of philosophy, but in
terms of mathematics -- of mathematical expediency\,!\dbsquare}


\subparagraph{Cartesians.}\label{Cartesians}   
Cartesians are product-like types -- and are named after the French
philosopher, scientist and mathematician Ren{\'e} Descartes
(1596--1640) \wiki.

\characterization{Cartesians}{ %
\begynd
\pind {Cartesian} {part}s are  those compound parts  which are
\begynd
\pind observed to consist  of two or more
      distinctly sort-named endurants (solids or fluids) \eod
\afslut
\afslut
}

\illustration{Cartesians: Road Transport}{A road transport, \textsf{rt:RT}, is observed to consist of an
  aggregate of a road net, \textsf{rn:RN}, and a set of automobiles, \textsf{SA}, where the road net
  is observed, i.e., abstracted, as a Cartesian of a set of hubs, \textsf{ah:AH},
  i.e., street intersections (or specifically designated points
  segmenting an otherwise ``straight'' street into two such), and a
  set of links, \textsf{al:AL}, i.e., street segments between two ``neighbouring''
  hubs.
%\RSLatex
%type
%   RT, RN, SA, AH = H-set, AL = L-set 
%value
%   &{\obs}&RN: RT -> RN, &{\obs}&SA: RT -> SA,, &{\obs}&AH: RN -> AH, &{\obs}&AL: RN -> AL  &\dbsquare&
%\endRSLatex 
\bp
\kw{type}\\
\>\ RT, RN, SA, AH {\EQ} H\kw{-set}, AL {\EQ} L\kw{-set} \\
\kw{value}\\
\>\ {\obs}RN: RT {\RIGHTARROW} RN, {\obs}SA: RT {\RIGHTARROW} SA,, {\obs}AH: RN {\RIGHTARROW} AH, {\obs}AL: RN {\RIGHTARROW} AL\ \ \dbsquare
\ep
}

\noindent
\prompt{\texttt{is\_Cartesian}}{\label{dal:Cartesian}%
We introduce the informal presentation language predicate
\texttt{is\_Cartesian} to hold for compound parts \textsf{p} if
\texttt{is\_Cartesian(p)} holds\dbsquare}

\noindent
\begynd
\pind Once a part, say \textsf{p:P}, has been analyzed into a Cartesian, we inquire
      as to the type names of the endurants\footnote{We emphasize that
      the observed elements of a Cartesian part may be both solids, at
      least one, and fluids.} of which it consists.
\pind The inquiry: \texttt{{record\_Cartesian\_part\_type\_names}(p:P)}, we decide, then
      yields the type of the constituent endurants.   
\afslut

\prompt{record-Cartesian-part-type-names}{\label{skema:record-Cartesian-part-type-names}%%%
%\RSLatex
%value
%   &\texttt{record\_Cartesian\_part\_type\_names}&: P -> &$\mathbb{T}$&-set
%   &\texttt{record\_Cartesian\_part\_type\_names}&(p) as {&${\eta}$&E1,&${\eta}$&E2,...,&${\eta}$&En} &\dbsquare&
%\endRSLatex 
\bp
\kw{value}\\
\>\ \texttt{record\_Cartesian\_part\_type\_names}: P {\RIGHTARROW} $\mathbb{T}$\kw{-set}\\
\>\ \texttt{record\_Cartesian\_part\_type\_names}(p) \kw{as} {\LBRACE}${\eta}$E1,${\eta}$E2,{\DOTDOTDOT},${\eta}$En{\RBRACE} \dbsquare
\ep
}%%%
\noindent
\begynd
\pind Here 
\pind \textsf{$\mathbb{T}$} is the \sort{name} of the type of all type names, and
\pind \textsf{$\eta$Ei} is the \sort{name} of type \textsf{Ei}.
\afslut

\begynd
\pind Please note the novel introduction of type names as values.
\begynd
\pind Where a type identifier, say  \textsf{T}, stands for, denotes, a
      class of values of that type,
\pind \textsf{$\eta$T} denotes the name of type \textsf{T}.
\afslut

\pind Please also note that
      \texttt{record\_Cartesian\_part\_type\_names} is not a description
      language construct.
\begynd
\pind It is an analysis language, i.e., an informal natural language,
      here English, construct.
\pind As such it is being used by the domain analyzer cum describer
\pind who ``applies'' it to an observed endurant and 
\pind notes down, in her mind or jots it on a scratch of paper,
\pind her decision as to appropriate [new] type names.
\afslut
\afslut

\illustration{Cartesian Parts}{The  {Cartesian} {part}s of a road
                     transport, \textsf{rt:RT}, is thus observed to consists of
\begin{itemize}
\item an aggregate of a road net, \textsf{rn:RN}, and
\item an aggregate set of automobiles, \textsf{sa:SA}:
\end{itemize}
\noindent
that is:
\begin{itemize}
\item \texttt{{record\_Cartesian\_part\_type\_names}(rt:RT)} = $\{$\textsf{$\eta$RN,$\eta$SA}$\}$
\end{itemize}

\noindent
where the type name \textsf{$\eta$RT} was -- and the type names \textsf{$\eta$RN}
and \textsf{$\eta$SA} are -- coined,
i.e., more-or-less freely chosen, by the domain analyzer cum
describer \dbsquare}%\footnote{Cf.\,Sect.\,\ref{The Type and Value Concepts}} \dbsquare

\subparagraph{Part Sets.}\label{Part Sets.}

\characterization{Part Sets}{{Part} {set}s
      are  those compound parts  which are  observed to consist of an indefinite number of  \nyl zero,
      one or more parts \eod}

\noindent
\prompt{\texttt{is\_part\_set} }{\label{dal:part-set}%
We introduce the informal presentation language predicate
\texttt{is\_part\_set} to hold for compound parts \textsf{e} if
\texttt{is\_part\_set(e)} holds\dbsquare}

\noindent
\begynd
\pind Once a part, say \textsf{e:E}, has been analyzed into a part set we inquire
      as to the set of parts and their type of which it consists.
\pind The inquiry: \texttt{record\_part\_set\_part\_type\_names}, we decide, then
      yields the (single) type of the constituent parts.
\afslut

\prompt{record-part-set-part-type-names}{\label{skema:record-part-set-part-type-names}%%%%
%\RSLatex
%value
%   &\texttt{record\_part\_set\_part\_type\_names}&: E -> &$\mathbb{T}$&Ps><&$\mathbb{T}$&P
%   &\texttt{record\_part\_set\_part\_type\_names}&(e:E) as (&$\eta$\,&Ps,&$\eta$\,&P) &\dbsquare&
%\endRSLatex 
\bp
\kw{value}\\
\>\ \texttt{record\_part\_set\_part\_type\_names}: E {\RIGHTARROW} $\mathbb{T}$Ps{\TIMES}$\mathbb{T}$P\\
\>\ \texttt{record\_part\_set\_part\_type\_names}(e:E) \kw{as} ($\eta$\,Ps,$\eta$\,P) \dbsquare
\ep
\noindent
Here the name of the value, \textsf{e}, and the type names
\textsf{$\eta$\,Ps} and \textsf{$\eta$\,P} are coined, 
i.e., more-or-less freely chosen, by the domain analyzer cum
describer \dbsquare
}%%%%%%%%%

\noindent
 Please also note that
      \texttt{record\_part\_set\_part\_type\_names} is not a description
      language construct.
\begynd
\pind It is an analysis language, i.e., an informal natural language,
      here English, construct.
\pind As such it is being used by the domain analyzer cum describer
\pind who ``applies'' in to an observed endurant and 
\pind notes down, in her mind or jots it on a scratch of paper,
\pind her decision as to appropriate [new] type names.
\afslut
\afslut
      
\illustration{Part Sets: Road Transport}{The road transport contains a set of
     automobiles.
\begynd
\pind The part set type name has been chosen to be \textsf{SA}.
\begynd
\pind It is then determined (i.e., analyzed) that \textsf{SA} is a set
      of \textsf{A}utomobile of type \textsf{A}
\begin{itemize}
\item \texttt{record\_part\_set\_part\_type\_names(sa:SA)} = ($\eta$\,\textsf{As},$\eta$\,\textsf{A}) \dbsquare
\end{itemize}
\afslut
\afslut
}

\subparagraph{Compound Observers.}\label{obs-Observer Functions:Part Sets}
%\label{Compound Observers}
\begynd
\pind Once the domain analyzer cum describer has decided upon the
      names of atomic and compound parts, 
\pind {\obs}erver functions can be applied to Cartesian
      and part set, \textsf{e:E}, parts:
\afslut

\describes{Describe Cartesians and Part Set Parts}\label{dal:record-Cartesians}\label{su:pt}\label{skema:Describe Cartesians and Part Set Parts}
%\RSLatex
%value
%   let {&$\eta$\,&P1,&$\eta$\,&P2,...,&$\eta$\,&Pn} = &\texttt{record\_Cartesian\_part\_type\_names(e:E)}& in
%   &\bq&type 
%      P1, P2, ..., Pn; 
%   value 
%      &{\obs}&P1: E->P1, &{\obs}&P2: E->P2,...n &{\obs}&Pn: E->Pn &\eq&
%                                                                                       & [respectively:]&
%   let (&$\eta$\,&Ps,&$\eta$\,&P) = &\texttt{record\_part\_set\_part\_type\_names(e:E)}& in
%   &\bq&type 
%      P, Ps = P-set, 
%   value
%      &{\obs}&Ps: E->Ps &\eq&
%   end end &\dbsquare&
%\endRSLatex 
\bp
\kw{value}\\
\>\ \kw{let} {\LBRACE}$\eta$\,P1,$\eta$\,P2,{\DOTDOTDOT},$\eta$\,Pn{\RBRACE} {\EQ} \texttt{record\_Cartesian\_part\_type\_names(e:E)} \kw{in}\\
\>\ \bq\kw{type} \\
\>\>\>P1, P2, {\DOTDOTDOT}, Pn; \\
\>\ \kw{value} \\
\>\>\>{\obs}P1: E{\RIGHTARROW}P1, {\obs}P2: E{\RIGHTARROW}P2,{\DOTDOTDOT}n {\obs}Pn: E{\RIGHTARROW}Pn \eq\\
\>\>\>\>\>\>\>\>\>\>\>\>\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  [respectively:]\\
\>\ \kw{let} ($\eta$\,Ps,$\eta$\,P) {\EQ} \texttt{record\_part\_set\_part\_type\_names(e:E)} \kw{in}\\
\>\ \bq\kw{type} \\
\>\>\>P, Ps {\EQ} P\kw{-set}, \\
\>\ \kw{value}\\
\>\>\>{\obs}Ps: E{\RIGHTARROW}Ps \eq\\
\>\ \kw{end} \kw{end} \dbsquare
\ep

\noindent
\begynd
\pind The \bq...\eq\ texts are the \texttt{RSL} texts ``generated'',
       i.e., written down, by the domain describer.
\pind They are \sfsl{domain model specification units}.
\begynd
\pind The ``surrounding'' \texttt{RSL}-like texts are not written down as
      phrases, elements, of the domain description.
\pind They are elements of the domain describers' ``notice board'',
\pind and, as such, elements of the development of domain models.
\afslut
\pind We have introduced a core domain modeling tool
\begynd
\pind the \textsf{{\obs}... observer function},
\pind one to be ``applied'' mentally by the domain describer,
\pind and one that appears in (\amol) domain descriptions 
\afslut
\pind The {\obs}... observer function is ``applied'' by the domain describer,
\pind it is not a computable function. 
\afslut

 Please also note that
      \texttt{Describe Cartesians and Part Set Parts} schema,
      \ref{skema:Describe Cartesians and Part Set Parts}, is not a
      description   language construct.
\begynd
\pind It is an analysis language, i.e., an informal natural language,
      here English, construct.
\pind As such it is being used by the domain analyzer cum describer
\pind who ``applies'' in to an observed endurant and 
\pind notes down, but now in a final form, elements, that is
      \sfsl{domain description units}.
\afslut
\afslut
      
\treprikker

\noindent
A major step of the development of domain models has now been
presented: that of the analysis \& description of the external
qualities of domains.

Schema\,\vref{skema:Describe Cartesians and Part Set Parts} is the
first manifestation of the domain analysis \& description method
leading to actual domain description elements.

From unveiling a \sfsl{science of domains} we have ``arrived'' at an
\sfsl{engineering of domain descriptions.}

\nbbb{States}\label{ss:ExInternalQualities:States}\label{part-states}

\characterization{States}{By a \sfsl{state} we shall mean any subset of the parts
  of a domain \dbsquare}

\illustration{Road Transport State}{%
%\RSLatex
%variable
%   &$hs$&:AH := &{\obs}&AH(&{\obs}&RN(rt)), 
%   &$ls$&:AL := &{\obs}&AL(&{\obs}&RN(rt)),
%   &$as$&:SA := &{\obs}&SA(rt), 
%   `sigma:(H|L|A)-set := &$hs$&union&$ls$&union&$as$& &\dbsquare&
%\endRSLatex 
\bp
\kw{variable}\\
\>\ $hs$:AH :{\EQ} {\obs}AH({\obs}RN(rt)), \\
\>\ $ls$:AL :{\EQ} {\obs}AL({\obs}RN(rt)),\\
\>\ $as$:SA :{\EQ} {\obs}SA(rt), \\
\>\ $\sigma$:(H{\BAR}L{\BAR}A)\kw{-set} :{\EQ} $hs${\UNION}$ls${\UNION}$as$ \dbsquare
\ep
}

\noindent
\begynd
\pind We have chosen to model domain states as \sort{variable}s rather than
      as \sort{value}s.
\pind The reason for this is
\begynd
\pind that the values of monitorable, including biddable part
      attributes\footnote{The concepts of monitorable, including biddable
      part attributes is treated in
      Sect.\,\ref{MichaelAJacksonsAttributeCategories}.} can change, and 
\pind that domains are often extended and ``shrunk'' by the addition,
      respectively removal of parts:
\illustration{Road Transport Development}{
\begynd
\pind adding or removing hubs, links
      and  automobiles  \dbsquare
\afslut}
\afslut
\noindent
We omit coverage of the aspect of bidding changes to monitorable part attributes.
\afslut

\nbbb{Validity of Endurant Observations}

\begynd
\pind We remind the reader that the {\obs}erver functions, as all
      later such functions: \mbox{{\uid-},} {\mereo}- and {\attr}-functions,
      are applied by humans
\begynd
\pind and that the outcome of these ``applications'' 
\pind is the result of human choices,
\pind and possibly biased by inexperience, taste, preference, bias, etc.
\afslut
\pind How do we know whether a domain analyzer \& describer's
      description of domain parts is valid\,?
\begynd
\pind Whether relevantly identified parts are modeled
      reasonably wrt.\ being atomic, Cartesians or part sets 
\pind Whether all relevant endurants have been identified\,?
\pind Etc.
\afslut
\pind The short answer is: we never know.
\pind Our models are conjectures and may be refuted \cite{popper-car-tgask63}.
\pind A social process of peer reviews, by domain stakeholders and
      other domain modelers is needed --
\pind as may a process of verifying\footnote{testing, model checking
  and theorem proving} properties of the domain
description held up against claimed properties of the (real) domain.
\afslut

\nbbb{Summary of Endurant Analysis Predicates}

Characterizations \ref{def:Entities}--\ref{def:Part Sets} imply the following 
 analysis predicates (Char.:\,$\delta$, Page\,$\pi$):

\begin{multicols}{2}
\begin{itemize} 
  \item {\textsf{is\_entity}}, {\rm\dfpg{Entities}}
  \item {\textsf{is\_endurant}}, {\rm\dfpg{Endurant}}
  \item {\textsf{is\_perdurant}}, {\rm\dfpg{Perdurant}}
  \item {\textsf{is\_solid}}, {\rm\dfpg{Discrete cum Solid Endurants}}
  \item {\textsf{is\_fluid}}, {\rm\dfpg{Fluid Endurants}}
  \item {\textsf{is\_part}}, {\rm\dfpg{Parts}}
  \item {\textsf{is\_atomic}}, {\rm\dfpg{Atomic Part}}
  \item {\textsf{is\_compound}}, {\rm\dfpg{Compound Part}}
  \item {\textsf{is\_Cartesian}}, {\rm\dfpg{Cartesians}}
  \item {\textsf{is\_part\_set}}, {\rm\dfpg{Part Sets}}
\end{itemize}
\end{multicols}

\noindent
\begynd
\pind We remind the \pos{reader}{student} that the above predicates
\begynd
\pind represent ``formulas'' in the presentation, \sort{not} the
      description, language.
\pind They are not \amol\ clauses.
\pind They are in the mind of the domain analyzers cum describers.
\pind They are ``executed'' by such persons.
\pind Their result, whether \sort{true}, \sort{false} or
\sort{chaos}\footnote{The outcome of applying an analysis predicate
  of the prescribed kind may be \sort{chaos} if the prerequisites for
  its application does not hold.},
\pind are noted by these persons 
\pind and determine their next step of domain analysis.
\afslut
\afslut
\label{sec:ExternalQualities.n} 
%\illustration{Road Transport}{Automobiles are \bbcolor{\textsf{mobile}}, hubs
%  and links are \bbcolor{\textsf{stationary}}, only Automobiles, hubs
%  and links are \bbcolor{\textsf{manifest}}, the rest are
%  \bbcolor{\textsf{structures}}, i.e., conceptual \dbsquare}

\nbbb{``Trees are Not Recursive''}

\begynd
\pind A `fact', that seems to surprise many, is that parts are not ``recursive''.
\begynd
\pind Yes, in all our domain modeling experiments, \cite{Bjorner2024:DomainModelsACompendium},
\pind we have not come across the need for recursively observing
      compound parts.
\pind Trees, for example, are not recursive in this sense.
\begynd
\pind Trees have roots.
\pind Sub-trees not.
\pind Banyan trees\footnote{https://www.britannica.com/plant/banyan} have several ``intertwined trees''.
\afslut
\pind But it would be `twisting' the modeling to try fit
      a description of such trees to a `recursion wim'\,!
\afslut
\pind Instead, trees are defined as nets, such as are road nets,
\pind where these nets then satisfy certain constraints 
      \cite[\sfsl{Chapter B}]{Bjorner2024:DomainModelsACompendium} --
      usually modeled by a mereology, see Sect.\,\vref{dom:Mereology}.
\afslut

\nbbbb{Internal Qualities -- Intangibles}\label{sec:InternalQualities}

\begynd
\pind The previous section has unveiled an ontology of the external qualities of endurants.
\begynd
\pind The unveiling consisted of two elements:
\begynd
\pind a set of analysis predicates, predicates \ref{def:Entities}--\ref{def:Part Sets}, and analysis functions,
      schemas \ref{skema:record-Cartesian-part-type-names}--\ref{skema:record-part-set-part-type-names}, and
      \pind a pair of description functions,
      schema\,\vref{skema:Describe Cartesians and Part Set Parts}.
\afslut

\pind The application of  description functions result in \amol\ text.

\pind That text conveys certain properties of domains:
\begynd
\pind that they consists of such-and-such endurants, 
\pind notably parts,
\pind and that these endurants ``derive'' from other endurants. 
\afslut
\pind But the \amol\ description texts do not \sfsl{``give flesh \&
      blood''} to these endurants.
\pind Questions like:
\begynd
\pind \sfsl{`what are their spatial extents\,?'},
\pind \sfsl{`how much do the weigh\,?'},
\pind \sfsl{`what colour do they have\,?'},
\pind et cetera,
\afslut are left unanswered.
\afslut
\pind In the present section we shall address such issues.
\pind We call them \sfsl{internal qualities}.
\afslut

\characterization{{Internal Qualities}}{ Internal qualities are \pdefindex{internal quality}
\begynd
\pind those properties [of endurants]
\pind that do not occupy \sfsl{space}
\pind but can be measured or spoken about\dbsquare
\afslut}%%%%
      
\illustration{Internal qualities}{ Examples of internal qualities are %%%%
\begynd
\pind the \sfsl{unique identity} of a part, 
\pind the \sfsl{mereological relation} of parts to other parts, and 
\pind the endurant \sfsl{attributes} such as temperature, length,
      colour, etc.\dbsquare
\afslut} 

\noindent
\begynd
\pind This section therefore introduces a number of domain description tools:
\begin{itemize}
\item {\uid}: the unique identifier observer of parts;
\item {\mereo}: the mereology observer of parts; 
\item {\attr}: (zero,) one or more attribute observers of endurants; and
\item {\sort{attributes\_}}: the attribute query of endurants.%; %%% 14AUGUST2023
%\item {}: .
\end{itemize}
\afslut
  
\nbbb{Unique Identity}\label{ss:InternalQualities:UniqueIdentity}\label{dom:Unique Identification}

\scsort{Unique Identity}{%
\begynd
\pind We postulate that separately discernible parts have unique
      identify.
\pind The issue, really, is a philosophical one.
\pind We refer to
\cite[\sfsl{Sects.\,2.2.2.3--2.2.2.4, pages\,14--15}]{BjornerMonograph2020}
   for a discussion of the
      existence and uniqueness of entities\dbsquare
\afslut}

\begynd
\pind \characterization{Unique Identity}{ A unique identity is
\begynd
\pind an immaterial property
\pind that distinguishes any two \sfsl{spatially}
      distinct solids\footnotemark\dbsquare
\afslut}\footnotetext{For pragmatic reasons we do not have to
speculate as to whether ``bodies'' of fluids can be ascribed unique
identity. The pragmatics is that we, in our extensive modeling
experiments have not found a need for such ascription\,!}
\noindent
\pind The unique identity of a part \textsf{p} of type \textsf{P} is
      obtained by the postulated observer {\uid}P: 
\afslut

\describe{Describe-Unique-Identity-Part-Observer}\label{su:ui}
%\RSLatex
%   &\bq&type
%       P,PI
%    value
%       &{\uid}&P: P -> PI&\eq \dbsquare&
%\endRSLatex 
\bp
\>\ \bq\kw{type}\\
\>\>\>\ P,PI\\
\>\>\kw{value}\\
\>\>\>\ {\uid}P: P {\RIGHTARROW} PI\eq \dbsquare
\ep
\eacm
\noindent
\begynd
\pind Here \textsf{PI} is the type of the unique identifiers of parts of type \textsf{P}.
\afslut
\dbeat{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\characterization{Unique Identifiers}{%
\begynd
\pind  {\texttt{record\_unique\_identifiers}(p:P)} records
       the names of the unique identifier types of parts \textsf{p:P}:
\begin{itemize}
\item {\texttt{record\_unique\_identifiers}(p:P)} \sort{as}
  \textsf{$\{\eta$PI,$\eta$Pi1,$\eta$Pi2,...,$\eta$Pin$\}$} \dbsquare
\end{itemize}
\afslut
}}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\illustration{Unique Road Transport Identifiers}{The  {unique} {identifiers}s of a road
                     transport, \textsf{rt:RT}, 
                     consists of the unique identifiers of the 
\begin{multicols}{2}
\begin{itemize}
\item road transport -- \textsf{rti:RTI},
\item (Cartesian) road net -- \textsf{rni:RNI},
\item (set of) automobiles -- \textsf{sa:SAI},
\item automobile, \textsf{ai:AI},
\item (set of) hubs, \textsf{hai:AHI},
\item (set of) links, \textsf{lai:LAI},
\item hub, \textsf{hi:HI}, and
\item link, \textsf{li:LI}, 
\end{itemize}
\end{multicols}
\dbeat{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\noindent
that is:

\begin{itemize}
\item \texttt{{record\_unique\_identifiers}(rt:RT)} = $\{$\textsf{RNI,SAI,AI,AHI,LAI,HI,LI}$\}$
\end{itemize}}}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\noindent
where the type names\dbeat{\footnote{Cf.\,Sect.\,\ref{The Type and Value Concepts}}} are all coined,
i.e., more-or-less freely chosen, by the domain analyzer cum
describer -- though, as You can see, these names were here formed by
``suffixing'' \textsf{I}s to relevant part names \dbsquare

\dbeat{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\nbb{Unique Identity Observer Functions}\label{uid:Observer Functions}

\noindent
\begynd
\pind Once a domain has been analyzed into all its parts, we can
ascertain these by an informal function.

\pind The inquiry \textsf{\sort{record\_domain\_part\_type\_names}(rts:RTS)}\footnote{We leave it to
        the reader to describe the general \textsf{\sort{record\_domain\_part\_type\_names}(p:P)}.}
      yields the type names of their unique identifiers --
\pind and hence of their observer functions,
      \textsf{{\uid}P}\footnote{Cf.\,Sects.\,\ref{Cartesians}--\ref{obs-Observer Functions:Part Sets}}: 
\afslut

\describe{Describe-Unique-Identifiers}
%\RSLatex
%   let {&$\eta$\,&P1,&$\eta$\,&P2,...,&$\eta$\,&Pn} = &\textsf{\sort{record\_domain\_part\_type\_names}(p:P)}& in
%   &\bq&type 
%      P1I, P2I, ..., PnI; 
%    value 
%      &{\uid}&P1: P1->P1I, &{\uid}&P2: P2->P2I,..., &{\uid}&Pn: Pn->PnI &\eq&
%   end  &\dbsquare&
%\endRSLatex
\bp
\>\ \kw{let} {\LBRACE}$\eta$\,P1,$\eta$\,P2,{\DOTDOTDOT},$\eta$\,Pn{\RBRACE} {\EQ} \textsf{\sort{record\_domain\_part\_type\_names}(p:P)} \kw{in}\\
\>\ \bq\kw{type} \\
\>\>\>P1I, P2I, {\DOTDOTDOT}, PnI; \\
\>\>\kw{value} \\
\>\>\>{\uid}P1: P1{\RIGHTARROW}P1I, {\uid}P2: P2{\RIGHTARROW}P2I,{\DOTDOTDOT}, {\uid}Pn: Pn{\RIGHTARROW}PnI \eq\\
\>\ \kw{end}\ \ \dbsquare
\ep
\eacm   
\noindent
\begynd
\pind The \bq...\eq\ texts are the \mola\ texts ``generated'',
       i.e., written down, by the domain describer.
\pind They are \sfsl{domain model specification
  units}.\indexcon{domain!model!specification
  units}\indexcon{specification!unit!domain model}
\afslut
}%%%%%%%%%%%%%%%%%%%%%%%%%%

\begynd
\pind We have thus introduced a core domain modeling tool
\begynd
\pind the \textsf{{\uid}... observer function},
\pind one to be ``applied'' mentally by the domain describer,
\pind and one that appears in (\mola) domain descriptions 
\afslut
\pind The {\uid}... observer function is ``applied'' by the domain describer,
\pind it is not a computable function. 
\afslut

\nbb{Uniqueness of Parts}\label{ss:Uniqueness of Parts}
\begynd
\pind No two parts have the same unique identifier.
\afslut

\illustration{Road Transport Uniqueness}{
%\RSLatex
%variable
%   &$hs_{uids}$&:HI-set := { &{\uid}&H(h) | h:H:-&u\,&isin&\,&`sigma }  
%   &$ls_{uids}$&:LI-set := { &{\uid}&L(l) | l:L:-&u\,&isin&\,&`sigma } 
%   &$as_{uids}$&:AI-set := { &{\uid}&A(a) | a:A:-&u\,&isin&\,&`sigma } 
%   `sigma&$_{uids}$&:(HI|LI|AI)-set := { &{\uid}&(H|L|A)(u) | u:(H|L|A):-&u\,&isin&\,&`sigma }
%axiom
%   always card `sigma = card `sigma&$_{uids}$&   &\dbsquare\ For $\sigma$ see Sect.\,\vref{part-states}.&
%\endRSLatex 
\bp
\kw{variable}\\
\>\ $hs_{uids}$:HI\kw{-set} :{\EQ} {\LBRACE} {\uid}H(h) {\BAR} h:H{\RDOT}u\,{\ISIN}\,$\sigma$ {\RBRACE}\ \ \\
\>\ $ls_{uids}$:LI\kw{-set} :{\EQ} {\LBRACE} {\uid}L(l) {\BAR} l:L{\RDOT}u\,{\ISIN}\,$\sigma$ {\RBRACE} \\
\>\ $as_{uids}$:AI\kw{-set} :{\EQ} {\LBRACE} {\uid}A(a) {\BAR} a:A{\RDOT}u\,{\ISIN}\,$\sigma$ {\RBRACE} \\
\>\ $\sigma$$_{uids}$:(HI{\BAR}LI{\BAR}AI)\kw{-set} :{\EQ} {\LBRACE} {\uid}(H{\BAR}L{\BAR}A)(u) {\BAR} u:(H{\BAR}L{\BAR}A){\RDOT}u\,{\ISIN}\,$\sigma$ {\RBRACE}\\
\kw{axiom}\\
\>\ {\ALWAYS} \kw{card} $\sigma$ {\EQ} \kw{card} $\sigma$$_{uids}$\ \ \ \dbsquare\ For $\sigma$ see Sect.\,\vref{part-states}.
\ep
}

\noindent
We have chosen, for the same reason as given in Sect.\,\ref{part-states}, to
model a unique identifier state. The {\ALWAYS} [\textsl{always}] prefix in the
\sort{axiom} then expresses that changes of parts or addition of parts to and deletions of
parts from the domain shall maintain their uniqueness over time (i.e.,
always).

\nbbb{Mereology}\label{ss:InternalQualities:Mereology}\label{dom:Mereology}

\begynd
\pind The concept of mereology is due to the Polish mathematician,
logician and philosopher
Stanis{\l}aw Le{\'{s}}niewski (1886--1939)
  \cite{Varzi1994,BjornerMereology2013}.
\afslut

\begynd 
\pind \characterization{Mereology}{ Mereology is \pdefindex{mereology}\  
      a theory of [endurant] part-hood relations: 
\begynd 
\pind of the relations of an [endurant]
      parts to a whole 
\pind and the
      relations of [endurant] parts to [endurant] parts within that
      whole\dbsquare
\afslut}%%%%
\afslut

\scsort{Mereology}{Stanis{\l}aw Le{\'{s}}niewski was not
  satisfied with Bertrand Russell's ``repair'' of Gottlob Frege's
  axiom systems for set theory. Instead he put forward his axiom
  system for, as he called it, mereology. Both as a mathematical
  theory and as a philosophical reasoning\dbsquare}

\illustration{Mereology}{ Examples of mereologies are %%%%
\begynd 
\pind that a link is topologically \sl connected \rm to \nyl
      exactly one or, usually, two specific hubs, 
\pind that hubs are \sl connected \rm to \nyl zero, one or
      more specific links, 
\pind and that links and hubs are   \sl  open  \rm to \nyl
      the traffic of specific subsets of automobiles \dbsquare
\afslut
}
\noindent
\begynd
\pind Mereologies can be expressed in terms of unique identifiers.
\afslut
%%%%%%%

\illustration{Mereology Representation}{%
\begynd
\pind For our `running road transport example'  the mereologies of
      links, hubs and automobiles can thus be expressed as follows:
\begin{itemize}
\item \textsf{{\mereo}L(l) = $\{$hi$'$,hi$''\}$} where
  \textsf{hi,hi$'$,hi$''$} are the unique identifiers of the hubs that
  the link connects, i.e., are in $hs_{uids}$;
\item \textsf{{\mereo}H(h) = $\{$li$_1$,li$_2$,...,li$_n\}$} where
  \textsf{li$_1$,li$_2$,...,li$_n$} are the unique identifiers of the
  links that are imminent upon (i.e., emanates from) the hub, i.e., are in $ls_{uids}$; and 
\item \textsf{{\mereo}A(a) = $\{$ri$_1$,ri$_2$,...,ri$_m\}$} where
  \textsf{ri$_1$,ri$_2$,...,ri$_m$} are unique identifiers of the road
  (hub and link) elements that make up the road net, i.e., are in $hs_{uids}{\cup}ls_{uids}$ \dbsquare
\end{itemize}
\afslut}

\noindent
\begynd
\pind Once the unique identifiers of all parts of a domain has been
      described we can analyses and describe their mereologies.
\pind The inquiry: \textsf{\sort{{\mereo}P}(p)}
      yields a mereology type (name), say \textsf{PMer}, and its
      description%
\footnote{Cf.\,Sect.\,\ref{obs-Observer Functions:Part Sets}}: 
\afslut

\describe{Describe-Mereology}\label{su:me}
%\RSLatex
%    &\bq&type
%       PMer = &$\mathcal{M}$&(PI1,PI2,...,PIm)
%    value
%       &{\mereo}&P: P -> PMer
%    axiom
%      &$\mathcal{A}$&(pm:PMer)&\eq& &\dbsquare&   
%\endRSLatex 
\bp
\>\>\bq\kw{type}\\
\>\>\>\ PMer {\EQ} $\mathcal{M}$(PI1,PI2,{\DOTDOTDOT},PIm)\\
\>\>\kw{value}\\
\>\>\>\ {\mereo}P: P {\RIGHTARROW} PMer\\
\>\>\kw{axiom}\\
\>\>\>$\mathcal{A}$(pm:PMer)\eq \dbsquare\ \ \ 
\ep
\eacm
\noindent
where
\begynd
\pind \textsf{$\mathcal{M}$(PI1,PI2,...,PIm)} is a type expression over unique
      identifier types of the domain;
\pind \textsf{{\mereo}P} is the mereology observer function for parts
      \textsf{p:P}; and
\pind \textsf{$\mathcal{A}$(pm:PMer)} is an axiom that secures that the
      unique identifiers of any part are indeed of parts of the domain.
\afslut

\nbbb{Attributes}\label{ss:InternalQualities:Attributes}\label{dom:Attributes}

\begynd
\pind Attributes are what finally gives ``life'' to endurants:
\begynd
\pind The external qualities ``only'' named 
\pind and gave structure to their atomic or compound types.
\pind The internal qualities of uniqueness and mereology are
      intangible quantities.
\pind The internal quality of attributes gives ``flesh \& blood'' to
      endurants:
\begynd
\pind they let us express endurant properties 
\pind that we can more easily,
\pind i.e., concretely, relate to.
\afslut
\afslut
\afslut

\nbb{General}

\characterization{Attributes}{ Attributes are \pdefindex{attribute}\
      properties of  endurants
\begynd 
\pind that can be measured  either physically 
\pind (by means of length (ruler) and spatial quantity
      measuring equipment, electronically, chemically, or otherwise) 
\pind or can be objectively spoken about\dbsquare
\afslut}%%%%

\scsort{Attributes}{First some empirical observation: in
    reasoning about ``the world around us'' 
    we express its properties in terms of predicates. These predicates,
    for example: \sfsl{``that building's wall is red''}, \sfsl{building}
    refers to an endurant part whereas  \sfsl{wall} and \sfsl{red} refers
    to attributes. Now the ``rub'': endurant attributes is what give
    \sfsl{``flesh \& blood''} to
    domains\dbsquare}\dbeat{\footnote{\bbcolor{Editorial remark:} I am not yet
    satisfied with this reasoning. The issue is: to force the concept
    of attributes to be justified philosophically, as an inevitable
    element of any world description, and not being forced upon us
    solely from empirical evidence.}}

%\vspace{2mm}
 
\noindent
\begynd
\pind Attributes are of types and, accordingly have values.

\pind We postulate an informal domain analysis function,
      \texttt{record\_attribute\_type\_names}:
\begynd
\pind The domain analyzer, in observing a part, $p$:$P$,
\pind analyzes it into the set of attribute names
\pind of parts $p$:$P$
\afslut
\afslut
 
\describe{record-attribute-type-names}\label{dal:record-Attributes}
%\RSLatex
%value
%   &\texttt{record\_attribute\_type\_names}: \textsf{P {\RIGHTARROW} ${\eta}\mathbb{T}$\sort{-set}}&
%   &\texttt{record\_attribute\_type\_names(p:P)} \sort{as} \textsf{${\eta}$T\sort{-set}}  \dbsquare&
%\endRSLatex 
\bp
\kw{value}\\
\>\ \texttt{record\_attribute\_type\_names}: \textsf{P {\RIGHTARROW} ${\eta}\mathbb{T}$\sort{-set}}\\
\>\ \texttt{record\_attribute\_type\_names(p:P)} \sort{as} \textsf{${\eta}$T\sort{-set}}  \dbsquare
\ep
\eacm

\illustration{Road Net Attributes, I}{ Examples of attributes are: 
\begynd 
\pind hubs have states, \textsf{h$\sigma$:H$\Sigma$}: the set of pairs of link
      identifiers, \textsf{($f$li,$t$li)}, of the \textsf{li}nks $f$rom and
      $t$o  which automobiles may enter, respectively leave the hub; and
\pind hubs have state spaces, \textsf{h$\omega$:H$\Omega$}: the set of hub states ``signaling''
      which states are open/closed, i.e., \bgcolor{green}\sort{/}\brcolor{red};
\pind links that have lengths, \textsf{LEN}; and
\pind automobiles have road net positions, \textsf{APos},
\pind either \sfsl{at a hub}, \textsf{atH}, or \sfsl{on a link},
      \textsf{onL}, some fraction,
      \textsf{f:\sort{Real}}, down a \textsf{l}ink, identified by
      \textsf{li}, from a hub, identified by \textsf{fhi}, 
      towards a hub, identified by \textsf{thi}.
\pind Hubs and links have \textsl{histories:}
      time-stamped, chronologically ordered sequences of automobiles
      entering and leaving links and hubs, with automobile histories
      similarly recording hubs and links entered and left.
\pind 
\pind 
\afslut
\begin{multicols}{2}
%\RSLatex
%type
%   H`Sigma = (LI><LI)-set
%   H`Omega = H`Sigma-set
%   LEN = Nat &\sort{m}&
%   APos = atH | onL
%   atH :: HI
%   onL :: LI >< (fhi:HI >< f:Real >< thi:HI)
%   HHis,LHis = (&$\mathbb{TIME}$&><AI)-list
%   AHis =  (&$\mathbb{TIME}$&><(HI|LI))-list
%value
%   attr_H`Sigma: H -> H`Sigma
%   attr_H`Omega: H -> H`Omega
%   attr_LEN: L -> LEN
%   attr_APos: A -> APos
%   attr_HHis: H -> HHis
%   attr_LHis: L -> LHis
%   attr_AHis: A -> AHis
%axiom
%   all (li,(fhi,f,thi)):onL :- 0<f<1
%      /\&li&isin&$ls_{uids}$&/\{fhi,thi}<<=&$hs_{uids}$&/\...&\dbsquare&
%\endRSLatex
\bp
\kw{type}\\
\>\ H$\Sigma$ {\EQ} (LI{\TIMES}LI)\kw{-set}\\
\>\ H$\Omega$ {\EQ} H$\Sigma$\kw{-set}\\
\>\ LEN {\EQ} \kw{Nat} \sort{m}\\
\>\ APos {\EQ} atH {\BAR} onL\\
\>\ atH :: HI\\
\>\ onL :: LI {\TIMES} (fhi:HI {\TIMES} f:\kw{Real} {\TIMES} thi:HI)\\
\>\ HHis,LHis {\EQ} ($\mathbb{TIME}${\TIMES}AI)$^{\ast}$\\
\>\ AHis {\EQ}\ \ ($\mathbb{TIME}${\TIMES}(HI{\BAR}LI))$^{\ast}$\\
\kw{value}\\
\>\ attr\_H$\Sigma$: H {\RIGHTARROW} H$\Sigma$\\
\>\ attr\_H$\Omega$: H {\RIGHTARROW} H$\Omega$\\
\>\ attr\_LEN: L {\RIGHTARROW} LEN\\
\>\ attr\_APos: A {\RIGHTARROW} APos\\
\>\ attr\_HHis: H {\RIGHTARROW} HHis\\
\>\ attr\_LHis: L {\RIGHTARROW} LHis\\
\>\ attr\_AHis: A {\RIGHTARROW} AHis\\
\kw{axiom}\\
\>\ {\ALL} (li,(fhi,f,thi)):onL {\RDOT} 0{\LT}f{\LT}1\\
\>\>\>{\WEDGE}li{\ISIN}$ls_{uids}${\WEDGE}{\LBRACE}fhi,thi{\RBRACE}{\SUBSETEQ}$hs_{uids}${\WEDGE}{\DOTDOTDOT}\dbsquare
\ep
\end{multicols}
}

\describe{Describe-endurant-attributes(e:E)}\label{su:at}
%\RSLatex
%   let {&${\eta}\,$&A1,&${\eta}$&A2,...,&${\eta}$&An}  = &\texttt{record\_attribute\_type\_names}&(e:E) in 
%   &\bq\,&type 
%       A1, A2, ..., An
%    value
%       &{\attr}\_&A1: E -> A1, &{\attr}\_&A2: E -> A2, ..., &{\attr}\_&An: E -> An
%    axiom
%       all a1:A1, a2:A2, ..., an:An: &$\mathcal{A}$&(a1,a2,...,an) &\eq&  
%   end &\dbsquare&
%\endRSLatex 
\bp
\>\ \kw{let} {\LBRACE}${\eta}\,$A1,${\eta}$A2,{\DOTDOTDOT},${\eta}$An{\RBRACE}\ \ {\EQ} \texttt{record\_attribute\_type\_names}(e:E) \kw{in} \\
\>\ \bq\,\kw{type} \\
\>\>\>\ A1, A2, {\DOTDOTDOT}, An\\
\>\>\kw{value}\\
\>\>\>\ {\attr}\_A1: E {\RIGHTARROW} A1, {\attr}\_A2: E {\RIGHTARROW} A2, {\DOTDOTDOT}, {\attr}\_An: E {\RIGHTARROW} An\\
\>\>\kw{axiom}\\
\>\>\>\ {\ALL} a1:A1, a2:A2, {\DOTDOTDOT}, an:An: $\mathcal{A}$(a1,a2,{\DOTDOTDOT},an) \eq\ \ \\
\>\ \kw{end} \dbsquare
\ep
\eacm

\nbb{Michael A. Jackson's Attribute Categories}\label{MichaelAJacksonsAttributeCategories}

\begynd
\pind Michael A.\ Jackson \cite{lexicon} has suggested a hierarchy of
      attribute categories:\LLLL
\begynd
\pind from \sfsl{static} (\texttt{is\_static}\footnote{\texttt{static:} values are
  constants, cannot change})
\pind to \sfsl{dynamic} (\texttt{is\_dynamic}\footnote{\texttt{dynamic:} values are
  variable, can change}) values -- and within the dynamic value category:
\begynd
\pind \sfsl{inert} values (\texttt{is\_inert}\footnote{\texttt{inert:} values can only
  change as the result of external stimuli where these stimuli prescribe new values}),
\pind \sfsl{reactive} values  (\texttt{is\_reactive}\footnote{\texttt{reactive:} values,
  if they vary, change  in response to external stimuli,  where these
  stimuli  either come from outside the domain of interest or from
  other endurants.}), 
\pind \sfsl{active} values  (\texttt{is\_active}\footnote{\texttt{active:} values can
  change (also) on their own volition}) -- and within the dynamic active value category:
\begynd
\pind \sfsl{autonomous} values
      (\texttt{is\_\-au\-to\-no\-mous}\footnote{\texttt{autonomous:} values change only ``on their own
      volition''; the values
      of an autonomous attributes are a ``law onto 
      themselves and their surroundings''.}), 
\pind \sfsl{biddable} values (\texttt{is\_biddable}\footnote{\texttt{biddable:} values are prescribed
     but may fail to be observed as such}),  and
\pind \sfsl{programmable} values (\texttt{is\_programmable}\footnote{\texttt{programmable:} values can be prescribed}) .
\afslut
\afslut
\mnewfoil
\noindent
\pind We postulate informal domain analysis predicates, ``performed''
      by the domain analyzer:
\afslut%

%\RSLatex
%value 
%   is_static,is_autonomous,is_biddable,is_programmable &[etc.]&: `eta&\,T&->Bool
%\endRSLatex 
\bp
\kw{value} \\
\>\ is\_static,is\_autonomous,is\_biddable,is\_programmable [etc.]: $\eta$\,T{\RIGHTARROW}\kw{Bool}
\ep

\noindent
\pind We refer to \cite{lexicon} and
     \cite{BjornerMonograph2020} [\sfsl{Chapter\,5, Sect.\,5.4.2.3}] for details.
\afslut%
\mnewfoil%
\begynd
\pind We suggest a minor revision of Michael A.\ Jackson's attribute
      categorization, see left side of Fig.\,\vref{MAJlexicon}.
\begynd
\pind We single out the inert from the ontology of
      Fig.\,\vref{MAJlexicon}, left side.
\pind Inert attributes seem to be ``set externally'' to the endurant.
\pind So we now distinguish between \texttt{is\_external} and
      \texttt{is\_internal} dynamic attributes.
\afslut
\pind We summarize Jackson's attribute and our revised categorization in Fig.\,\ref{MAJlexicon}.
\afslut
\mnewfoil

 \begin{figure}[ht]
  \begin{center}
    \epsfig{file=attributes.eps,height=4cm}  
    \epsfig{file=rev-attributes.eps,height=4cm}
    \caption{Michael Jackson's [Revised] Attribute Categories}\label{MAJlexicon}
  \end{center}
\end{figure}

This distinction has [pragmatic] consequences for how we treat
arguments of the behaviours of parts, cf.\ Sect.\,\ref{sss:Behaviour
  Signature} (page\,\pageref{sss:Behaviour Signature.inert}).
%%  LocalWords:  Bool MAJlexicon endurant behaviours endurants au tes
%%  LocalWords:  mous tns stichwort palabra clave ben dibj rlander's


%%% 
\mnewfoil%
\illustration{Road Net Attributes, II}{The link length and hub state space attributes are
  static,  hub states and automobile positions
  programmable. Automobile speed and acceleration attributes, which
  we do not model, are monitorable \dbsquare}

\mnewfoil%

\noindent
\begynd
\pind The attributes categorization determines, in the next major
section on perdurants, the treatment of hub, link and automobile behaviours.
\afslut

\label{pre-primer.Prompts}

\nbb{Analytic Attribute Extraction Functions:}\LLll
\pos{
\begynd
\pind For later purpose we
need characterize three specific attribute category extraction functions:
\begynd
\pind \texttt{static\_attributes}, 
\pind \texttt{monitorable\_at\-tri\-bu\-tes}, and
\pind \texttt{programmable\_attributes}:\LLll
\afslut
\afslut
}{}

%\RSLatex
%value
%   p:P
%   tns = &\texttt{record\_attribute\_type\_names}&(p)
%   
%   &\texttt{static\_attributes}&: &${\eta}T$&-set -> &${\eta}T$&-set
%   &\texttt{static\_attributes}&(tns) is { &${\eta}$&tn | &${\eta}$&tn:&${\eta}T$& :- &${\eta}$&tn isin tns /\ is_static(tn) }
%
%   &\texttt{inert\_attributes}&: &${\eta}T$&-set -> &${\eta}T$&-set
%   &\texttt{inert\_attributes}&(tns) is { &${\eta}$&tn | &${\eta}$&tn:&${\eta}T$& :- &${\eta}$&tn isin tns /\ is_inert(tn) }
%
%   &\texttt{monitorable\_attributes}& &${\eta}T$&-set -> &${\eta}T$&-set
%   &\texttt{monitorable\_attributes}&(tns) is { &${\eta}$&tn | &${\eta}$&tn:&${\eta}T$& :- &${\eta}$&tn isin tns /\ is_monitorable(tn) }
%
%   &\texttt{programmable\_attributes}& &${\eta}T$&-set -> &${\eta}T$&-set
%   &\texttt{programmable\_attributes}&(tns) is { &${\eta}$&tn | &${\eta}$&tn:&${\eta}T$& :- &${\eta}$&tn isin tns /\ is_programmable(tn) }
%
%   &\texttt{is\_monitorable}&: T -> Bool
%   &\texttt{is\_monitorable}&(t) is ~is_static(t) /\ ~is_inert(t) /\ ~is_programmble(t)
%\endRSLatex 
\bp
\kw{value}\\
\>\ p:P\\
\>\ tns {\EQ} \texttt{record\_attribute\_type\_names}(p)\\
\>\ \\
\>\ \texttt{static\_attributes}: ${\eta}T$\kw{-set} {\RIGHTARROW} ${\eta}T$\kw{-set}\\
\>\ \texttt{static\_attributes}(tns) {\IS} {\LBRACE} ${\eta}$tn {\BAR} ${\eta}$tn:${\eta}T$ {\RDOT} ${\eta}$tn {\ISIN} tns {\WEDGE} is\_static(tn) {\RBRACE}\\
\\
\>\ \texttt{inert\_attributes}: ${\eta}T$\kw{-set} {\RIGHTARROW} ${\eta}T$\kw{-set}\\
\>\ \texttt{inert\_attributes}(tns) {\IS} {\LBRACE} ${\eta}$tn {\BAR} ${\eta}$tn:${\eta}T$ {\RDOT} ${\eta}$tn {\ISIN} tns {\WEDGE} is\_inert(tn) {\RBRACE}\\
\\
\>\ \texttt{monitorable\_attributes} ${\eta}T$\kw{-set} {\RIGHTARROW} ${\eta}T$\kw{-set}\\
\>\ \texttt{monitorable\_attributes}(tns) {\IS} {\LBRACE} ${\eta}$tn {\BAR} ${\eta}$tn:${\eta}T$ {\RDOT} ${\eta}$tn {\ISIN} tns {\WEDGE} is\_monitorable(tn) {\RBRACE}\\
\\
\>\ \texttt{programmable\_attributes} ${\eta}T$\kw{-set} {\RIGHTARROW} ${\eta}T$\kw{-set}\\
\>\ \texttt{programmable\_attributes}(tns) {\IS} {\LBRACE} ${\eta}$tn {\BAR} ${\eta}$tn:${\eta}T$ {\RDOT} ${\eta}$tn {\ISIN} tns {\WEDGE} is\_programmable(tn) {\RBRACE}\\
\\
\>\ \texttt{is\_monitorable}: T {\RIGHTARROW} \kw{Bool}\\
\>\ \texttt{is\_monitorable}(t) {\IS} {\SIM}is\_static(t) {\WEDGE} {\SIM}is\_inert(t) {\WEDGE} {\SIM}is\_programmable(t)
\ep

\pos{
\noindent\large
\begynd
\pind Please be reminded that these functions are informal.
\begynd
\pind They are part of the presentation language.
\pind Do not be confused by their \amol-like appearance.
\afslut
\afslut
\HHHH
}{}
\nbbbb{Intentional Pull}\label{Intentional Pull}

\scsort{Intentional Pull}{In \cite[\sfsl{pages 167--168}]{kaisorlander2016}
    S{\o}rlander argues wrt.\ \sfsl{``how can entities be the source of
    forces ?''} and thus reasons for \sfsl{gravitational pull}. That
    same kind of reasoning, with proper substitution of terms, leads us
    to the concept of \sfsl{intentional pull}\dbsquare}

%\vspace{2mm}
 
\noindent
\begynd
\pind Two or more parts
\begynd
\pind of different sorts, but with overlapping sets of
intents\footnote{Intent: purpose; God-given or human-imposed\,!}
\pind may excert an \textsf{intentional ``pull''} on one another.
\afslut
\pind This \sfsl{intentional ``pull''} may take many forms.
\begynd
\pind Let $p_x:X$ and $p_y:Y$ 
\pind be two parts of \sfsl{different sorts} ($X,Y$), 
\pind and with \sfsl{common intent}, $\iota$.
\pind \sfsl{Manifestations} of these, their common intent
\pind must somehow be \sfsl{subject to constraints},
\pind and these must be \sfsl{expressed predicatively}.
\afslut
\afslut

\begynd
\pind When a compound artifact
\begynd
\pind models ``itself'' as put together
      with a number of other endurants
\pind then it does have an intentionality and
\pind the components' individual intentionalities does, \nyl i.e.,
      shall relate to that.
\afslut
\afslut

\illustration{Road Transport Intentionality}{%%%%%%%%%
\begynd
\pind \sfsl{Automobiles} include the \sfsl{intent:} \texttt{trans\-port}, 
\pind  and so do \sfsl{hubs} and \sfsl{links}.
\pind \sfsl{Manifestations} of \texttt{transport} are reflected in
\begynd
\pind \sfsl{hubs, links} and \sfsl{automobiles} 
\pind having the \sfsl{history} attribute.
\afslut
\pind The \sfsl{intentional ``pull''} of these manifestations is this:
\begynd
\pind For every automobile, if it records being in some hub or on some link
      at time $\tau$,
\pind then the designated hub, respectively link, records exactly that
      automobile; and vice versa:
\pind for every hub [link], if it records the visit of some automobile
      at time $\tau$,
\pind then the designated automobile records exactly that hub [link].
\afslut
\pind We leave the formalization of the above 
      to the \pos{reader}{listener} \dbsquare
    }
    
\illustration{Double-entry Bookkeeping}{
\begynd
\pind Another example of intentional ``pull'' is that of double-entry bookkeeping.
\begynd
\pind Here the income/expense ledger
\pind must balance
\pind the actives/passives ledger \dbsquare
\afslut
\afslut
}

{\illustration{The Henry George Theorem.}{The Henry George theorem states that 
  under certain conditions, aggregate spending by government on public
  goods will increase aggregate rent based on land value (land rent)
  more than that amount, with the benefit of the last marginal
  investment equaling its cost \dbsquare\footnote{Stiglitz, Joseph
  (1977). ``The Theory of Local Public Goods''. In Feldstein, M.S.;
  Inman, R.P. (eds.). The Economics of Public Services. Palgrave
  Macmillan,
  London. pp. 274–333. doi:10.1007/978-1-349-02917-4\_12. ISBN
  978-1-349-02919-8.}$^{,}$\footnote{Henry
  George (September 2, 1839 -- October 29, 1897) was an American
  political economist and journalist. His writing was immensely
  popular in 19th-century America and sparked several reform movements
  of the Progressive Era. He inspired the economic philosophy known as
  Georgism, the belief that people should own the value they produce
  themselves, but that the economic value of land (including natural
  resources) should belong equally to all members of society. George
  famously argued that a single tax on land values would create a more
  productive and just society.}}}
\label{sec:InternalQualities.n}

\nbbbb{Summary of Endurants}

\begynd
\pind We have completed our treatment of endurants.
\begynd
\pind That treatment was based on an ontology for the observable
      phenomena of domains -- 
\pind such as we have delineated the concept of domains.
\afslut
\pind The treatment was crucially based on an ontology for the
      structure of domain phenomena, and, in a sense, ``alternated'' between
\begynd
\pind analysis predicates,
\pind analysis functions, and
\pind description functions.
\afslut
\pind We have carefully justified this ontology in \sort{`Ontological
      Choice'} paragraphs
\afslut

\nbbbbb{Perdurant Concepts}\label{sec:Perdurant Concepts}
 
\begynd
\pind The main contribution of this section is that of
      \sfsl{transcendentally deducing} perdurants from endurant parts, 
\begynd
\pind in particular \sfsl{behaviours} ``of'' parts.
\afslut

\pind Major perdurants are those of actions, events and behaviours
\pind with behaviours generally being sets of sequences of \bbcolor{actions,
      events} and \bbcolor{behaviours.}
\afslut

\nbbbb{``Morphing'' Parts into Behaviours}

\begynd
\pind As already indicated we shall
\begynd
\pind transcendentally deduce
\pind (perdurant) behaviours from
\pind those (endurant) parts
\begynd
\pind which we, as domain analyzers cum describers,
\pind have endowed with all three kinds of internal qualities:
\pind unique identifiers, mereologies and attributes.
\afslut
\afslut
\pind We shall use the \texttt{CSP} \cite{Hoare85+2004}\
constructs of
\amol\ (derived from   \texttt{RSL} \cite{RSL})
to model concurrent behaviours.
\afslut

\nbbbb{Transcendental Deduction}\label{sss:Transcendental Deduction}

\characterization{Transcendental}{By \brcolor{transcendental}  \nyl we shall
    understand the philosophical
    notion:  \nyl \bbcolor{the a priori or intuitive basis of knowledge,  \nyl
      independent of experience \eod}}
  
\noindent
\begynd
\pind A priori knowledge or intuition is central:
\begynd
\pind By \sfsl{a priori} we mean that it not only precedes,
\pind but also determines rational thought.
\afslut
\afslut

\characterization{Transcendental Deduction}{ \nyl
By a \brcolor{transcendental deduction} \nyl
    we shall 
    understand the philosophical
    notion: \nyl \bbcolor{a 
    \textsf{transcendental} ``conversion'' \nyl of one kind of 
    knowledge \nyl into a seemingly different kind of knowledge \eod}}

\illustration{Transcendental Deductions -- Informal Examples}{\HHHH\label{exs-of-td-some}%
\begynd
\pind We give some intuitive examples of transcendental deductions.
\pind They are from the ``domain'' of programming languages.
\begynd
\pind There is the syntax of a programming language, \nyl
      and there are the programs that supposedly adhere to this syntax.
\pind Given that, the following are now transcendental deductions.

%\pos{\psno}{\mnewfoil}
      
\begynd
\pind The software tool, \bbcolor{\textsl{a syntax checker}}\pos{, that takes a program and
      checks whether it satisfies the syntax, including the statically
      decidable context conditions, i.e., the \textsl{statics
        semantics} -- such a tool is one of several forms of
      transcendental deductions}{}.
    
\pind The software tools, \bbcolor{\textsl{an automatic theorem
      prover}} and  \nyl \bbcolor{\textsl{a  model checker}}\pos{, for example
    \texttt{SPIN}  \cite{Holzmann03},
    that takes a program 
      and some \texttt{theorem}, 
      respectively a \texttt{Promela} statement, and proves,
      respectively checks, the program correct with respect the
      theorem, or the statement}{}.
      
\pind A \bbcolor{\textsl{compiler}} and an \bbcolor{\textsl{interpreter}}\pos{ for any programming language}{}.
\afslut
 
\pind Yes, indeed, any \bbcolor{\textsl{abstract interpretation}}
      \cite{PatrickCousot2021}
\nyl reflects a transcendental
      deduction:
\begynd
\pind firstly, these examples show that  there are many
      transcendental deductions; 
\pind secondly, they show that there is no single-most preferred
      transcendental deduction\dbsquare
\afslut
\afslut
\afslut
}%

\scsort{Transcendental Deduction of Behaviours from Parts}{So this, then, is, in a sense, our
``final'' ontological choice: that of transcendentally deducing
behaviours from parts\dbsquare}

\nbbbb{Actors -- A Synopsis}

This section provides a summary overview.

\characterization{Actors}{ \pdefindex{actor}\ 
\begynd
\pind An actor is anything
      that can initiate an \sort{action}, \sort{event} or
      \sort{behaviour} \dbsquare
\afslut}
%%%%%%%
 
\nbbb{Action}
   
\characterization{Actions}{ \pdefindex{action}\
\begynd
\pind  An action is a
      function that can purposefully change a state\dbsquare
\afslut}
\illustration{Road Net Actions}{ These are some road transport actions:
\begynd
\pind an automobile 
\begynd
\pind leaving a hub, entering a link;
\pind leaving a link, entering a hubs;
\pind entering the road net; and
\pind leaving the road net \dbsquare
\afslut
\afslut}

%%%%%%%

\nbbb{Event}

\characterization{Events}{ \pdefindex{event}\
\begynd
\pind  An event is a function
      that surreptitiously changes a state\dbsquare
\afslut}
\illustration{Road Net Events}{ These are some road net events:
\begynd
\pind The blocking of a link due to a mud slide;
\pind the failing of a hub traffic signal due to power outage;
\pind an automobile failing to drive; and
\pind the blocking of a link due to an automobile accident\dbsquare
\afslut}
\noindent
We shall not formalize events.

%%%%%%%
    
\nbbb{Behaviour}

\characterization{Behaviours}{ \pdefindex{behaviour}
\begynd
\pind Behaviours are sets 
\pind of sequences of 
\pind actions, events and behaviours\dbsquare
\afslut}
\noindent
\begynd
\pind Concurrency is modeled by the \sfsl{sets} of sequences.
\pind Synchronization and communication of behaviours are effected
\pind by \texttt{CSP} \sfsl{output/inputs}: \textsf{ch[$\{$i,j$\}$]\,!value/ch[$\{$i,j$\}$]\,?}.
\afslut
%%%%%%%
\mnewfoil\LLll
\illustration{Road Net Traffic}{ %
\begynd
\pind Road net traffic can be seen as a behaviour
\begynd
\pind of all the behaviours of automobiles,
\begynd
\pind where each automobile behaviour is seen as sequence of \nyl start, stop,
      turn right, turn left, etc., actions;
\afslut
\pind of all the behaviours of links
\begynd
\pind where each link behaviour is seen \nyl as a set of sequences (i.e., behaviours) of ``following'' the
\begynd
\pind link entering, link leaving, and movement
\afslut of automobiles on the link;
\afslut
\pind of all the behaviours of hubs (etc.);
\pind of the behaviour of the aggregate of roads, \nyl viz.\ \sfsl{The Department of Roads}, and
\pind of the behaviour of the aggregate of automobiles, \nyl viz,\
      \sfsl{The Department of Vehicles}.
\afslut
\afslut}\HHHH

%%%% \noindent
%%%% We shall, in this \acmorbook{paper}{\compendium}, consider aggregates
%%%% as purely conceptual structures. That is, structures have no behaviour (counterparts).

\nbbbb{Channel}

\begynd
\pind \characterization{Channel}{ \pdefindex{channel}\
\begynd
\pind A channel is anything 
\pind that allows synchronization and communication
\pind of values
\pind between behaviours\dbsquare
\afslut}
\afslut

\describe{Channel}\label{su:ch} We suggest the following schema for describing
                      channels:
%\RSLatex
%   &\bq&channel { ch[{ui,uj}] | ui,ij:UI :- ... } M
%\endRSLatex 
\bp
\>\ \bq\kw{channel} {\LBRACE} ch{\LBRACKET}{\LBRACE}ui,uj{\RBRACE}{\RBRACKET} {\BAR} ui,ij:UI {\RDOT} {\DOTDOTDOT} {\RBRACE} M
\ep
\noindent
where \textsf{ch} is the describer-chosen name for an array of
channels, \textsf{ui,uj} are channel array indices of the unique
identifiers, \textsf{UI}, of the chosen domain\dbsquare

\illustration{Road Transport Interaction Channel}{%
%\RSLatex
%   channel { ch[{ui,uj}] | {ui,ij}:(HI|LI|AI)-set :- ui~=uj/\{ui,uj}<<=`sigma&$_{uids}$& } M  
%\endRSLatex
\bp
\>\ \kw{channel} {\LBRACE} ch{\LBRACKET}{\LBRACE}ui,uj{\RBRACE}{\RBRACKET} {\BAR} {\LBRACE}ui,ij{\RBRACE}:(HI{\BAR}LI{\BAR}AI)\kw{-set} {\RDOT} ui{\NOTEQ}uj{\WEDGE}{\LBRACE}ui,uj{\RBRACE}{\SUBSETEQ}$\sigma$$_{uids}$ {\RBRACE} M\ \ 
\ep
\noindent
Channel array \textsf{ch} is indexed by a ``pair'' of distinct unique
part identifiers of the domain. We shall later
outline \textsf{M}, the type of the ``messages'' communicated between behaviours \dbsquare
}

\nbbbb{Behaviours \& Actions}\label{ss:Behaviours}

We single out the perdurants of behaviours -- as they relate directly
to the parts of Sect.\,\ref{sec:External and Internal Endurant Qualities}.
The treatment is ``divided'' into three sections.

\nbbb{Behaviour Signature}\label{sss:Behaviour Signature}

\describe{Behaviour Signature}{\indent\label{su:be1}By the
  \sfsl{behaviour signature}, for a part 
  $p$, we shall
  understand a pair: the name of the behaviour, \textsf{B$_{p}$}, and a function type
  expression as indicated:\rm \\[2mm] \small%[2mm]
\sort{value}\\
\hspace*{6mm} \textsf{B$_{p}$:} \textsf{Uid$_p${\RIGHTARROW}}\footnote{We
  have \textsf{Sch{\"{o}}nfinckel'ed}
  \texttt{https://en.wikipedia.org/wiki/Moses\_Sch{\"{o}}nfinkel\#Further\_reading}
  (Curried \texttt{https://\-en.\-wi\-ki\-pe\-di\-a.\-org/\-wi\-ki/\-Cur\-ry\-ing}) the function type}
  \textsf{Mereo$_p${\RIGHTARROW}Sta\_Vals$_p${\RIGHTARROW}Inert\_Vals$_p${\RIGHTARROW}Mon\_Refs$_p${\RIGHTARROW}Prgr\_Vals$_p$}
  {\RIGHTARROW} $\{$ ch[$\{$i,j$\}$] $\mid$ ... $\}$
  \sort{Unit}\\ \normalsize%[2mm]
 
\noindent
We explain:

\begin{itemize}
\item \textsf{Uid$_p$} is the type of unique identifiers of part $p$,
  {\textsf{{\uid}P(p)} = \textsf{Uid$_p$};}
  
\item  \textsf{Mereo$_p$} is the type of the mereology of part $p$,
  {\textsf{{\mereo}P(p)}  = \textsf{Mereo$_p$};}
  
\item \textsf{Sta\_Vals$_p$} is a Cartesian of the type of inert attributes  of part
      $p$. Given \texttt{record\_attribu\-te\_\-ty\-pe\_\-names(p)}
      \texttt{static\_attributes(record\_attribute\_\-type\_\-na\-mes(p))}
    yields \textsf{Sta\_Vals$_p$};

\item \textsf{Inert\_Vals$_p$} is a Cartesian of the type of static attributes  of part
      $p$.\label{sss:Behaviour Signature.inert} Given \texttt{record\_attribu\-te\_\-ty\-pe\_\-names(p)}
      \texttt{inert\_attributes(record\_attri\-bute\_\-ty\-pe\_\-na\-mes\-(p))}
    yields \textsf{Inert\_Vals$_p$};
    
\item  \textsf{Mon\_Refs$_p$}  is a Cartesian of the
      {\attr}ibute observer functions
      of the types of monitorable attributes  of part
      $p$. Given \texttt{record\_attri\-bute\_\-ty\-pe\_names(p)}
      analysis function \texttt{monitorable\_\-attributes(re\-cord\_attribute\_type\_names(p))}
    yields \textsf{Mon\_Vals$_p$};
    
\item \textsf{Prgr\_Vals$_p$} is a Cartesian of the type of
      programmable attributes  of part $p$.  Given
      \texttt{record\_at\-tri\-bu\-te\_type\_names(p)}
      analysis function \texttt{programmable\_\-at\-tributes(re\-cord\_at\-tri\-bu\-te\_\-ty\-pe\_\-names(p))}.
    yields \textsf{Prgr\_Vals$_p$};
    
\item  $\{$ ch[$\{$i,j$\}$] $\mid$ ... $\}$ specifies the channels over
  which part $p$ behaviours, \textsf{B$_{p}$}, may communicate; and
  
\item \sort{Unit} is the type name for the () value\footnote{-- You
      may ``read' () as the value yielded by a statement, including a
      never-terminating function} \dbsquare 
\end{itemize}
\afslut}
\noindent
The Cartesian arguments may ``degenerate'' to the non-Cartesian of no, or just one
      type identifier, In none, i.e., (), then () may be skipped. If
      one, e.g., ($a$), then  $(a)$ is listed.

\illustration{Road Transport Behaviour Signatures}{%
%\RSLatex
%value
%   hub: HI->MereoH->(H`Omega><...)->(...)->(HHist><...)
%                 ->{ch[{&{\uid}&H(&$p$&),ai}]|ai:AI:-a&i&isin&$as_{uid}$&} Unit
%   link: LI->MereoL->(LEN><...)->(...)->(LHist><...)
%                 ->{ch[{&{\uid}&L(&$p$&),ai}]|ai:AI:-a&i&isin&$as_{uid}$&} Unit
%   automobile: AI->MereoA->(...)->(&{\attr}&AVel><&{\attr}&HAcc><...)->(APos><AHist><...)
%                 ->{ch[{&{\uid}&H(&$p$&),ri}]|ri:(HI|LI):-r&i&isin&$hs_{uid}$&union&$ls_{uid}$&} Unit 
%\endRSLatex 
\bp
\kw{value}\\
\>\ hub: HI{\RIGHTARROW}MereoH{\RIGHTARROW}(H$\Omega${\TIMES}{\DOTDOTDOT}){\RIGHTARROW}({\DOTDOTDOT}){\RIGHTARROW}(HHist{\TIMES}{\DOTDOTDOT})\\
\>\>\>\>\>\>\>\>\ {\RIGHTARROW}{\LBRACE}ch{\LBRACKET}{\LBRACE}{\uid}H($p$),ai{\RBRACE}{\RBRACKET}{\BAR}ai:AI{\RDOT}ai{\ISIN}$as_{uid}${\RBRACE} \kw{Unit}\\
\>\ link: LI{\RIGHTARROW}MereoL{\RIGHTARROW}(LEN{\TIMES}{\DOTDOTDOT}){\RIGHTARROW}({\DOTDOTDOT}){\RIGHTARROW}(LHist{\TIMES}{\DOTDOTDOT})\\
\>\>\>\>\>\>\>\>\ {\RIGHTARROW}{\LBRACE}ch{\LBRACKET}{\LBRACE}{\uid}L($p$),ai{\RBRACE}{\RBRACKET}{\BAR}ai:AI{\RDOT}ai{\ISIN}$as_{uid}${\RBRACE} \kw{Unit}\\
\>\ automobile: AI{\RIGHTARROW}MereoA{\RIGHTARROW}({\DOTDOTDOT}){\RIGHTARROW}({\attr}AVel{\TIMES}{\attr}HAcc{\TIMES}{\DOTDOTDOT}){\RIGHTARROW}(APos{\TIMES}AHist{\TIMES}{\DOTDOTDOT})\\
\>\>\>\>\>\>\>\>\ {\RIGHTARROW}{\LBRACE}ch{\LBRACKET}{\LBRACE}{\uid}H($p$),ri{\RBRACE}{\RBRACKET}{\BAR}ri:(HI{\BAR}LI){\RDOT}ri{\ISIN}$hs_{uid}${\UNION}$ls_{uid}${\RBRACE} \kw{Unit} 
\ep
\noindent
\begynd
\pind Here we have suggested additional part attributes:
\begynd
\pind monitorable automobile velocity and acceleration,  \textsf{AVel, AAcc},
\afslut
\pind and omitted other attributes \dbsquare
\afslut
}

\nbbb{Inert Arguments: Some Examples}\label{sss:Inert Arguments}

\begynd
\pind Let us give some examples of inert attributes of automobiles.
\begynd
\pind (i) Driving uphill, one a level road, or downhill, excert some \texttt{inert}
      ``drag'' or ``pull''.
\pind (ii) Velocity can be treated as a reactive attribute -- but it
can be [approximately] calculated on the basis of, for example, these
\texttt{inert} attributes: drag/pull and accelerator pedal pressure,
and the \texttt{static} engine power attribute.
\afslut
\afslut

%\nbbb{Behaviour Definitions}
%\nbbb{Action Definitions}

\input{defs}

\nbbb{Behaviour Invocation}\label{sss:Behaviour Invocation1}

\describe{Behaviour Invocation}\label{su:be2}
\noindent
\begynd
\pind Behaviours are invoked as follows:
\afslut

%\RSLatex
%   &{\bq}&B&$_p$&(&{\uid}$_p$&(p))&\footnotemark&
%       (&{\mereo}&P(p))     
%           (&{\attr}&staA&$_1$&(p),...,&{\attr}&staA&$_s$&(p))
%                (&{\attr}&inertA&$_1$&(p),...,&{\attr}&inertA&$_i$&(p))
%                     (&{\attr}&monA&$_1$&,...,&{\attr}&monA&$_m$&) 
%                          (&{\attr}&prgA&$_1$&(p),...,&{\attr}&prgA&$_p$&(p))&{\eq}&
%\endRSLatex 
\bp
\>\ {\bq}B$_p$({\uid}$_p$(p))\footnotemark\\
\>\>\>\ ({\mereo}P(p))\ \ \ \ \ \\
\>\>\>\>\>\ ({\attr}staA$_1$(p),{\DOTDOTDOT},{\attr}staA$_s$(p))\\
\>\>\>\>\>\>\>\>({\attr}inertA$_1$(p),{\DOTDOTDOT},{\attr}inertA$_i$(p))\\
\>\>\>\>\>\>\>\>\>\>\ ({\attr}monA$_1$,{\DOTDOTDOT},{\attr}monA$_m$) \\
\>\>\>\>\>\>\>\>\>\>\>\>\ \ ({\attr}prgA$_1$(p),{\DOTDOTDOT},{\attr}prgA$_p$(p)){\eq}
\ep
\footnotetext{We show the arguments of the
  invocation on separate lines only for readability. That is: normally
we show the invocation arguments as \textsf{B(...)(...)(...)(...)(...)}.}
\begin{itemize}
\item All arguments are passed \sfsl{by value}. 
\item  The \sfsl{uid} value is never changed.
\item  The \sfsl{mereology} value is usually not changed.
\item  The  \sfsl{static attribute} values are fixed, never changed.
\item  The  \sfsl{inert attribute} values are fixed, but can be
       updated by receiving explicit input communications.
\item The  \sfsl{monitorable attribute} values are functions, i.e., it
is as if the ``actual'' monitorable values are passed \sfsl{by name}\,!
\item  The  \sfsl{programmable attribute} values are usually changed,
  ``updated'', by actions described in the behaviour definition \dbsquare
\end{itemize}

\nbbb{Argument References}\label{sss:Argument References}

\begynd
\pind Within behaviour descriptions, see next section, references are
      made to the behaviour arguments.
\begynd
\pind References, $a$, to  \sfsl{unique identifier, mereology, static} and
      \sfsl{pro\-gam\-mab\-le attribute} arguments yield their value. 
\pind References, $a$, to  \sfsl{monitorable attribute} arguments
      also yield  their value. This value is an {\attr}\textsf{A}
      observer function.
\begynd
\pind To yield, i.e., \textsf{read}, the monitorable attribute value this function is
      applied to that behaviour's uniquely identified part, $p_{uid}$, in the
      global part state, $\sigma$.
\pind To update,, i.e., \textsf{write}, say, to a value $v$, for the case of a \sfsl{biddable, monitorable}
      attribute, that behaviour's uniquely identified part, $p_{uid}$, in the
      global part state, $\sigma$, shall have part $p_{uid}$'s
      \textsf{A} attribute changed to $v$ -- with all other attribute
      values of $p_{uid}$ unchanged.
\afslut
\afslut
\pind Common to both the read and write functions is the
\sfsl{retrieve part} function:
\begin{enumerate}\setei
\item[*] \label{re-pt-000} Given a unique part identifier, \textsf{pi}, assumed to be
                        that of an existing domain part,
\item[*] \label{re-pt-010} \textsf{retr\_part}  \sfsl{read}s the global [all parts] variable
                        $\sigma$ to retrieve that part \textsf{p} whose unique part
                        identifier is \textsf{pi}.
\savei\end{enumerate}
\afslut

%\RSLatex
%value
%[*]   &\,\,&retr_part: PI -> P  read &\label{retrieve part}&
%[*]   &\,\,&retr_part(pi) is let p:P :- p isin &\sort{c}\,&`sigma /\ uid_P(p)=pi in p end
%[*]   &\,\,&pre: exists p:P :- p isin &\sort{c}\,&`sigma /\ uid_P(p)=pi
%\endRSLatex 
\bp
\kw{value}\\
{\LBRACKET}{\AST}{\RBRACKET}\ \ \ \,\,retr\_part: PI {\RIGHTARROW} P\ \ \kw{read} \label{retrieve part}\\
{\LBRACKET}{\AST}{\RBRACKET}\ \ \ \,\,retr\_part(pi) {\IS} \kw{let} p:P {\RDOT} p {\ISIN} \sort{c}\,$\sigma$ {\WEDGE} uid\_P(p){\EQ}pi \kw{in} p \kw{end}\\
{\LBRACKET}{\AST}{\RBRACKET}\ \ \ \,\,\kw{pre}: {\EXISTS} p:P {\RDOT} p {\ISIN} \sort{c}\,$\sigma$ {\WEDGE} uid\_P(p){\EQ}pi
\ep

\noindent
\begynd
\pind You may think of the functions being illustrated in this
      section, Sect.\,\ref{sss:Argument References}, 
\begynd
\pind \textsf{retr\_part}, \textsf{read\_A\_from\_P} and \textsf{update\_P\_with\_A}, 
\pind as ``belonging'' to the description language,
\pind but here suitably expressed for any domain,
\pind that is, with suitable substitutions for \textsf{A} and \textsf{P}.
\afslut
\afslut

\bb{Evaluation of Monitorable Attributes.}\label{Evaluation of Monitorable Attributes}

\begin{enumerate}\setei
\item \label{us000} Let \textsf{pi:PI} be the unique identifier of any
  part, $p$, with monitorable attributes, let \textsf{A} be a
  monitorable attribute of $p$, and let \textsf{$\eta$A} be the name
  of attribute \textsf{A}.
\item \label{us010} Evaluation of the [current] attribute  \textsf{A}
  value of $p$ is defined by function \textsf{read\_A\_\-from\_\-P}.
\savei\end{enumerate}

%\RSLatex
%value
%&\ref{us000}.&    pi:PI, a:A, `eta&A&:`eta&$\mathbb{T}$&
%&\ref{us010}.&    read_A_from_P: PI >< &$\mathbb{T}$& -> read `sigma A &\label{readA}&
%&\ref{us010}.&    read_A(pi,`eta&A&) is attr_A(retr_part(pi))
%\endRSLatex 
\bp
\kw{value}\\
\ref{us000}.\ \ \ \ pi:PI, a:A, $\eta$A:$\eta$$\mathbb{T}$\\
\ref{us010}.\ \ \ \ read\_A\_from\_P: PI {\TIMES} $\mathbb{T}$ {\RIGHTARROW} \kw{read} $\sigma$ A \label{readA}\\
\ref{us010}.\ \ \ \ read\_A(pi,$\eta$A) {\IS} attr\_A(retr\_part(pi))
\ep

\nbb{Update of Biddable Attributes}\label{Update of Biddable Attributes}

\begin{enumerate}\setei
\item \label{us040} The update of a monitorable attribute \textsf{A},
  with attribute name \textsf{$\eta$A}
  of part $p$, identified by \textsf{pi}, to a new value \kw{write}s
  to the global part state $\sigma$. 
\item \label{us060} Part $p$ is retrieved from the global state.
\item \label{us070} A new part, \textsf{p$'$} is formed such that
  \textsf{p$'$} is like part \textsf{p}:
\begin{enumerate}
\item \label{us080} same unique identifier, 
\item \label{us081} same mereology,
\item \label{us082} same attributes values,
\item \label{us083} except for \textsf{A}.
\end{enumerate}
\item \label{us100} That new $p'$ replaces $p$ in $\sigma$.
\savei\end{enumerate}

\mnewfoil\LLLL\HHHH

%\RSLatex
%value
%&\ref{us040}.&    `sigma, a:A, pi:PI, `eta&A&:`eta&$\mathbb{T}$&
%
%&\ref{us040}.&    update_P_with_A: PI >< A >< &$\eta\mathbb{T}$& -> write `sigma &\label{updatePwithA}&  
%&\ref{us040}.&    update_P_with_A(pi,a,`eta&A&) is
%&\ref{us060}.&        let p = retr_part(pi) in
%&\ref{us070}.&        let p&$'$&:P :-  
%&\ref{us080}.&            uid_P(p&$'$&)=pi 
%&\ref{us081}.&            /\ mereo_P(p)=mereo_P(p&$'$&)
%&\ref{us082}.&            /\ all `eta&A$'$& isin &\texttt{record\_attribute\_type\_names}&(p)\{`eta&A&} 
%&\ref{us082}.&                 => attr_A&$'$&(p)=attr_A&$'$&(p&$'$&)
%&\ref{us083}.&            /\ attr_A(p')=a in
%&\ref{us100}.&        `sigma := &\sort{c}\,&`sigma \ {p} union {p'}
%&\ref{us040}.&        end end
%&\ref{us060}.&     pre: exists p:P :- p isin &\sort{c}\,&`sigma /\ uid_P(p)=pi
%\endRSLatex 
\bp
\kw{value}\\
\ref{us040}.\ \ \ \ $\sigma$, a:A, pi:PI, $\eta$A:$\eta$$\mathbb{T}$\\
\\
\ref{us040}.\ \ \ \ update\_P\_with\_A: PI {\TIMES} A {\TIMES} $\eta\mathbb{T}$ {\RIGHTARROW} \kw{write} $\sigma$ \label{updatePwithA}\ \ \\
\ref{us040}.\ \ \ \ update\_P\_with\_A(pi,a,$\eta$A) {\IS}\\
\ref{us060}.\ \ \ \ \ \ \ \ \kw{let} p {\EQ} retr\_part(pi) \kw{in}\\
\ref{us070}.\ \ \ \ \ \ \ \ \kw{let} p$'$:P {\RDOT}\ \ \\
\ref{us080}.\ \ \ \ \ \ \ \ \ \ \ \ uid\_P(p$'$){\EQ}pi \\
\ref{us081}.\ \ \ \ \ \ \ \ \ \ \ \ {\WEDGE} mereo\_P(p){\EQ}mereo\_P(p$'$)\\
\ref{us082}.\ \ \ \ \ \ \ \ \ \ \ \ {\WEDGE} {\ALL} $\eta$A$'$ {\ISIN} \texttt{record\_attribute\_type\_names}(p){\SETMINUS}{\LBRACE}$\eta$A{\RBRACE} \\
\ref{us082}.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\DBLRIGHTARROW} attr\_A$'$(p){\EQ}attr\_A$'$(p$'$)\\
\ref{us083}.\ \ \ \ \ \ \ \ \ \ \ \ {\WEDGE} attr\_A(p{\PRIM}){\EQ}a \kw{in}\\
\ref{us100}.\ \ \ \ \ \ \ \ $\sigma$ :{\EQ} \sort{c}\,$\sigma$ {\SETMINUS} {\LBRACE}p{\RBRACE} {\UNION} {\LBRACE}p{\PRIM}{\RBRACE}\\
\ref{us040}.\ \ \ \ \ \ \ \ \kw{end} \kw{end}\\
\ref{us060}.\ \ \ \ \ \kw{pre}: {\EXISTS} p:P {\RDOT} p {\ISIN} \sort{c}\,$\sigma$ {\WEDGE} uid\_P(p){\EQ}pi
\ep
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\nbbb{Behaviour Description -- Examples}\label{sss:Behaviour Description}

\begynd
\pind Behaviour descriptions rely strongly on \texttt{CSP}s'
\cite{Hoare85+2004}
expressivity.
\pind Leaving out some details (\_, `...'), and \sfsl{without ``further ado''}, we exemplify.
\afslut

\illustration{Automobile Behaviour at Hub}{%
\begin{enumerate}\setei
\item \label{habff1y} We abstract automobile  behaviour \textsf{at} a 
                    \textsf{H}{ub} (\textsf{hi}).
\begin{enumerate}
\item \label{habff1ay} Either the automobile remains in the hub,
\item \label{habff1bby} or, internally non-deterministically, 
\item \label{habff1by} leaves the hub entering a link, 
\item \label{habff1ccy} or, internally non-deterministically, 
\item \label{habff1cy} stops.
\end{enumerate}
\savei\end{enumerate}

%\RSLatex
%&\ref{habff1y}&  automobile(ai)(ris)(...)(atH(hi),ahis,_) is
%&\ref{habff1ay}&      automobile_remains_in_hub(ai)(ris)(...)(atH(hi),ahis,_)
%&\ref{habff1bby}&     |^|
%&\ref{habff1by}&      automobile_leaving_hub(ai)(ris)(...)(atH(hi),ahis,_)
%&\ref{habff1ccy}&     |^|
%&\ref{habff1cy}&      automobile_stop(ai)(ris)(...)(atH(hi),ahis,_)
%\endRSLatex 
\bp
\ref{habff1y}\ \ automobile(ai)(ris)({\DOTDOTDOT})(atH(hi),ahis,{\UNDERLINE}) {\IS}\\
\ref{habff1ay}\ \ \ \ \ \ automobile\_remains\_in\_hub(ai)(ris)({\DOTDOTDOT})(atH(hi),ahis,{\UNDERLINE})\\
\ref{habff1bby}\ \ \ \ \ {\NONDETCHOICE}\\
\ref{habff1by}\ \ \ \ \ \ automobile\_leaving\_hub(ai)(ris)({\DOTDOTDOT})(atH(hi),ahis,{\UNDERLINE})\\
\ref{habff1ccy}\ \ \ \ \ {\NONDETCHOICE}\\
\ref{habff1cy}\ \ \ \ \ \ automobile\_stop(ai)(ris)({\DOTDOTDOT})(atH(hi),ahis,{\UNDERLINE})
\ep

\mnewfoil
\begin{enumerate}\setei
\item \label{habff-10} {[\ref{habff1ay}]} The automobile remains in the hub:
\begin{enumerate}
\item \label{habff-15} time is recorded,
\item \label{habff-20} the automobile remains at that hub, ``idling'', 
\item \label{habff-30} informing (``first'') the hub behaviour.
\end{enumerate}
\savei\end{enumerate}

%\RSLatex
%&\ref{habff-10}&  automobile_remains_in_hub(ai)(ris)(...)(atH(hi),ahis,_) is
%&\ref{habff-15}&     let `tau = &\recordtime\ & in
%&\ref{habff-30}&     ch[{ai,hi}] ! `tau ;
%&\ref{habff-20}&     automobile(ai)(ris)(...)(atH(hi),<.(`tau,hi).>^ahis,_) end
%\endRSLatex 
\bp
\ref{habff-10}\ \ automobile\_remains\_in\_hub(ai)(ris)({\DOTDOTDOT})(atH(hi),ahis,{\UNDERLINE}) {\IS}\\
\ref{habff-15}\ \ \ \ \ \kw{let} $\tau$ {\EQ} \recordtime\  \kw{in}\\
\ref{habff-30}\ \ \ \ \ ch{\LBRACKET}{\LBRACE}ai,hi{\RBRACE}{\RBRACKET} ! $\tau$ ;\\
\ref{habff-20}\ \ \ \ \ automobile(ai)(ris)({\DOTDOTDOT})(atH(hi),{\LANGLE}($\tau$,hi){\RANGLE}{\CONCAT}ahis,{\UNDERLINE}) \kw{end}
\ep

\begin{enumerate}\setei
\item \label{habff49x} {[\ref{habff1by}]} The automobile leaves the hub
                      entering  link \textsf{li}:
\begin{enumerate} 
\item \label{habff6x} time is recorded;
\item \label{habff7x} hub is informed of automobile leaving and link
                     that it is entering;
\item \label{habff8x} ``whereupon'' the vehicle resumes (i.e., ``while
                     at the same time'' resuming) the vehicle
                     behaviour positioned at the very beginning
                     (\textsf{0}) of that link.
\end{enumerate}
\savei\end{enumerate}
%\RSLatex
%&\ref{habff49x}&  automobile_leaving_hub(ai)({li}union&ris&)(...)(atH(hi),ahis,_) is
%&\ref{habff6x}&      let `tau = &\recordtime\, \, & in
%&\ref{habff7x}&      (ch[{ai,hi}] ! `tau || ch[{ai,li}] ! `tau) ;
%&\ref{habff8x}&      automobile(ai)(ris)(...)(onL(li,(hi,0,_)),<.(`tau,li).>^ahis,_) end
%&\ref{habff49x}&       pre: &[hub is not isolated]&
%\endRSLatex 
\bp
\ref{habff49x}\ \ automobile\_leaving\_hub(ai)({\LBRACE}li{\RBRACE}{\UNION}ris)({\DOTDOTDOT})(atH(hi),ahis,{\UNDERLINE}) {\IS}\\
\ref{habff6x}\ \ \ \ \ \ \kw{let} $\tau$ {\EQ} \recordtime\, \,  \kw{in}\\
\ref{habff7x}\ \ \ \ \ \ (ch{\LBRACKET}{\LBRACE}ai,hi{\RBRACE}{\RBRACKET} ! $\tau$ {\PARL} ch{\LBRACKET}{\LBRACE}ai,li{\RBRACE}{\RBRACKET} ! $\tau$) ;\\
\ref{habff8x}\ \ \ \ \ \ automobile(ai)(ris)({\DOTDOTDOT})(onL(li,(hi,0,{\UNDERLINE})),{\LANGLE}($\tau$,li){\RANGLE}{\CONCAT}ahis,{\UNDERLINE}) \kw{end}\\
\ref{habff49x}\ \ \ \ \ \ \ \kw{pre}: [hub is not isolated]
\ep

\noindent
\begynd
\pind The choice of link entered is here expressed (\ref{habff49x}) as a
      non-deterministic choice\footnote{-- as indicated by the
        \sort{pre-} condition: the hub mereology must specify that it
        is not isolated. Automobiles can never leave isolated hubs.}. 
\pind One can model the leave hub/enter link otherwise. 
\afslut
\mnewfoil

\begin{enumerate}\setei
\item \label{xxxxx} {[\ref{habff1cy}]}  Or the  automobile ``disappears --- off the radar''~!
\savei\end{enumerate}

%\RSLatex
%&\ref{xxxxx}&  automobile_stop(ai)(ris),(...)(atH(hi),ahis,_) is stop &\dbsquare&
%\endRSLatex 
\bp
\ref{xxxxx}\ \ automobile\_stop(ai)(ris),({\DOTDOTDOT})(atH(hi),ahis,{\UNDERLINE}) {\IS} \kw{stop} \dbsquare
\ep
}rm\pos{\normalsize}{\HHHH}

\nbbbb{Behaviour Initialization.}\label{sss:Behaviour Initialization}\label{su:in}

\begynd
\pind For every manifest part it must be described how its behaviour
      is initialized.
\afslut

\illustration{Road Transport Initialization}{We ``wrap up''
             the main example of this \acmorbook{paper}{\compendium}:
\begynd
\pind We omit treatment of monitorable attributes.
\afslut
\begin{enumerate}\setei
\item \label{rtsi000} Let us refer to the system initialization as an action.
\item \label{rtsi010} All hubs are initialized,
\item \label{rtsi020} all links are initialized, and
\item \label{rtsi030} all automobiles are initialized.
\savei\end{enumerate}

\mnewfoil\LLLL\HHHH

%\RSLatex
%value
%&\ref{rtsi000}.&  rts_initialisation: Unit -> Unit
%&\ref{rtsi000}.&  rts_initialisation() is
%&\ref{rtsi010}.&     || { hub(&{\uid}&H(l))(&{\mereo}&H(l))(&{\attr}&H`Omega(l),...)(&{\attr}&H`Sigma(l),...)| h:H :- h isin &$hs$& }
%&\ref{rtsi020}.&     || || { link(&{\uid}&L(l))(&{\mereo}&L(l))(&{\attr}&LEN(l),...)(&{\attr}&L`Sigma(l),...)| l:L :- l isin &$ls$& }
%&\ref{rtsi030}.&     || || { automobile(&{\uid}&A(a))(&{\mereo}&A(a))(&{\attr}&APos(a)&{\attr}&AHis(a),...) | a:A :- a isin &$as$& }
%\endRSLatex 
\bp
\kw{value}\\
\ref{rtsi000}.\ \ rts\_initialisation: \kw{Unit} {\RIGHTARROW} \kw{Unit}\\
\ref{rtsi000}.\ \ rts\_initialisation() {\IS}\\
\ref{rtsi010}.\ \ \ \ \ {\PARL} {\LBRACE} hub({\uid}H(l))({\mereo}H(l))({\attr}H$\Omega$(l),{\DOTDOTDOT})({\attr}H$\Sigma$(l),{\DOTDOTDOT}){\BAR} h:H {\RDOT} h {\ISIN} $hs$ {\RBRACE}\\
\ref{rtsi020}.\ \ \ \ \ {\PARL} {\PARL} {\LBRACE} link({\uid}L(l))({\mereo}L(l))({\attr}LEN(l),{\DOTDOTDOT})({\attr}L$\Sigma$(l),{\DOTDOTDOT}){\BAR} l:L {\RDOT} l {\ISIN} $ls$ {\RBRACE}\\
\ref{rtsi030}.\ \ \ \ \ {\PARL} {\PARL} {\LBRACE} automobile({\uid}A(a))({\mereo}A(a))({\attr}APos(a){\attr}AHis(a),{\DOTDOTDOT}) {\BAR} a:A {\RDOT} a {\ISIN} $as$ {\RBRACE}
\ep

\noindent
\begynd 
\pind We have here omitted possible monitorable attributes.
\pind For  $hs, ls, as$ we refer to
Sect.\,\ref{ss:ExInternalQualities:States} \dbsquare
\afslut}\label{sec:Perdurant Concepts.n}

\label{sec:Facets}
\input{facets}
 
\nbbbbb{Conclusion}


\begynd
\pind We have summarized a method 
\begynd
\pind to be used by [human] domain analyzers cum describers
\pind in studying and modeling domains.
\pind Our previous  publications
      \cite{BjornerFAoC2015MDAAD,BjornerTOSEM2018,BjornerMonograph2020}
      have, with this paper, found its most recent, we risk to say,
      for us, final form.
      
\pind Of course, domain models can be developed without the calculi
      presented in this paper.
\pind And was for many years.
\pind From the early 1990s a number of formal models of railways were
      worked out
      \cite{RaiseCaseBook2001,db00:p:ifac,db03:forms2003,dines-idpt-02,db03:ifac-cts2003}.
\pind The problem, though, was still, between 1992 and 2016, 
\pind \sfsl{``where to
      begin, how to proceed and when to end''}.
\pind The domain analysis \& description ontology and, hence calculus,
      of this paper shows how.
\pind The systematic approach to domain modeling of this ontology and
      calculus has stood its test of time.
\pind The \texttt{Internet}  \url{http://www.imm.dtu.dk/~dibj/2024/models/domain-models.pdf} `publication'
      \cite{Bjorner2024:DomainModelsACompendium} include several domain models\footnote{%
\begin{multicols}{4}
\begin{itemize}
\item \sfsl{Graphs},
\item \sfsl{Rivers},
\item \sfsl{Canals},
\item \sfsl{Railways},
\item \sfsl{Road Transport},
\item \sfsl{The ``7 Seas''},
\item \sfsl{The ``Blue Skies''},
\item \sfsl{Credit Cards},
\item \sfsl{Weather Information},
\item \sfsl{Documents},
\item \sfsl{Urban Planning},
\item \sfsl{Swarms of Drones},
\item \sfsl{Container Terminals},
\item \sfsl{A Retailer Market},
\item \sfsl{Assembly Lines},
\item \sfsl{Bookkeeping},
\item \sfsl{Shipping},
\item \sfsl{Stock Exchanges},
\item \sfsl{Web Transactions}, etc.
\end{itemize}
\end{multicols}}
      from the 2007--2024 period.
\pind Their development has helped hone the method of the present paper.
\pind Most recent domain modeling \cite{2025:transport,2025:banking} were not carried out to
``stress-test'' the modeling approach, but for reasons outlined in the
introductory section of those reports\,!
\afslut

\nbbbb{Previous Literature}

\begynd
\pind To the best of my knowledge there is no prior, comparable
      publications in the field of domain science and engineering.
\begynd
\pind Closest would be \textsf{Michael A.\ Jackson}'s
      \cite{MichaelJackson2010}.
\pind Well, most computer scientists working in the field of
      correctness of programs, from somewhat ``early on'', stressed
      the importance of making proper assumptions about the domain,
\pind They would then express these ``in-line'', as appropriate
      predicates, with their proofs.
\pind Michael A.\ Jackson, lifted this, to a systematic treatment of
      the domain in his triplet `Problem Frame Approach':
      \sfsl{program, machine, domain} \cite{mja2001a}. 
\pind But Jackson did not lift his problem frame concern into a proper
      study of domains.
\afslut
\afslut

\nbbbb{The Method}\label{ss:The Method}

\begynd
\pind So the method procedure is this:
\begynd
\pind (1) First analyze and describe the \sfsl{external qualities} of the chosen domain.
\pind (2) For each of the so-described endurants You then analyze and
      describe their \sfsl{internal qualities.}
\begynd
\pind (2.1) First their \sfsl{unique identification.}
\pind (2.2) Then their \sfsl{mereology.}
\pind (2.3) Then their \sfsl{attributes.}
\pind (2.4) And finally possible \sfsl{intentional pulls.}
\afslut
\pind (3) First then are You ready to tackle the issue of perdurants.
\begynd
\pind (3.1) Decide upon the \sfsl{state.} (That may already have been done in
            connection with (1).)
\pind (3.2) Then describe the \sfsl{channels.}
\pind (3.3) Then analyze and describe [part] \sfsl{behaviour signatures.}
\pind (3.4) Then describe \sfsl{behaviour invocation.}
\pind (3.5) Then \sfsl{behaviour (body) definitions.}
\afslut
\pind (4) Finally describe \sfsl{domain initialization.}
\afslut
\afslut

\nbbbb{Specification Units}\label{ss:Specification Units}

\begynd
\pind The method thus focuses, step-by-step, on the development of the
      following \sfsl{specification units:}
\begynd
\pind \sort{type} specification units,
\pind \sort{value} specification units,
\pind \sort{axiom} specification units,
\pind \sort{variable} declaration units, and
\pind \sort{channel} declaration units.
\afslut

\pind There are two forms of \sfsl{type} specifications:
\begynd
\pind ($\alpha$) introduction of sorts, i.e., type names, and
\pind ($\beta$) specification of types: pairs of new type names and type
      expressions -- as atomic, alternate or composite types: set,
      Cartesian, list, map or function types.
      \afslut
      
\pind There are basically three forms of value specification units:
\begynd
\pind (i)   (``simple'') naming of values, 
\pind (ii)  signature of functions: function name and function type, and
\pind (iii) signature of (endurant \sort{obs\_}, unique identifier \sort{uid\_}, mereology, \sort{mereo\_}, and
            attribute \sort{attr\_}) observer functions.
\afslut            
\afslut

\nbbbb{Object Orientation}\label{ss:Object Orientation}

\begynd
\pind So far we have not used the term `object'\,!

\pind We shall now venture the following:

\begynd
\pind \sfsl{The combined description of endurant parts and their
      perdurant behaviour form an object definition.}

\pind You can then, for yourself, develop a way of graphically
      presenting these object definitions such
\begynd
\pind that each part type
      is represented by a box that contains the specification units
      for [all] external and internal endurant qualities as well as
      for the perdurant [part] behaviour signatures and definitions;
\pind and such that the mereologies of these parts is represented by
      [possibly directed] lines connecting relevant boxes.
\afslut
\afslut

\pind That is, an object concept solely based on essentially
      inescapable world description facts -- as justified by
      S{\o}rlander's Philosophy
      \cite{kaisorlander1994,kaisorlander2016,kaisorlander2022,kaisorlander2023}\,! 
\pind No ``finicky'' programming language ``tricks''\,!

\pind We leave it to the reader to compare this definition to those of
      so-called object-oriented programming languages.
\afslut

\nbbbb{Other Domain Modeling Approaches}\label{sss:Other Domain Modeling Approaches}

\begynd
\pind \cite{caseUNUIIST} shows fragments of a number of expertly
      expressed domain models.
\begynd
\pind They are all expressed in \texttt{RAISE}.\footnote{Other
  approaches could also be used: \texttt{VDM} \citevdm,  \texttt{Z}
  \citez,  \texttt{Alloy} \citealloy,  \texttt{CafeOBJ} \citecafeobj, etc.}
\pind But they are not following the method of this paper.
\pind In other words, it is possible to develop domain models not using the method\,!
\afslut
\pind This author has found, however, that following the method --
\begynd
\pind developed after the projects reported in \cite{caseUNUIIST} --
\pind leads to far less problematic situations --
\pind in contrast to my \sort{not} adhering strictly to the method.
\afslut
\pind In other words, based on this subjective observation, 
\pind we advice using the method. 
\afslut

\begynd
\pind There is thus no proof that following the method does result in
      simpler, straightforward developments.

\pind But we do take the fact that we can justify the method, 
\pind cf.\,Fig.\,\vref{onto.fig0},
\pind on the basis on the inevitability of describing the world as per
      philosophy of Kai S{\o}rlander
      \cite{kaisorlander1994,kaisorlander2016,kaisorlander2022,kaisorlander2023},
\pind and that that may have a bearing on the experienced shorter
      domain description development efforts.
\afslut

\nbbbb{How Much\,? How Little\,?}

\begynd
\pind How wide must we \sfsl{cast the net} when studying a domain\,?
\begynd
\pind The answer to that question depends, we suggest, on whether our
      quest
\begynd
\pind is for studying a domain in general, to see what might come out,
\pind or whether it is a study aiming at a specific model for a
      specific software development.
\afslut
\pind In the former case \sfsl{we cast the net} as we please -- we
      suggest: as wide as possible, wider that for specific quests. 
\pind In the latter case \sfsl{we should cast the net} as ``narrowly''
      as is reasonable: to fit those parts of a domain that we expect
      the requirements 
      and software to deal with\,!
\pind In this latter case we should assume that someone, perhaps the
      same developers, has first ``tried their hand'' on a wider domain.
\afslut
\afslut

\nbbbb{Correctness}

\begynd
\pind Today, 2024, software correctness appears focused on
\begynd
\pind the correctness of algorithms, possibly involving concurrency.
\afslut
\pind Correctness, of software, in the context of a specific domain,
\begynd
\pind means that the software requirements are ``correctly'' derived
      from a domain description, and
\pind that the software design is correctly derived from the domain
      requirements,  
\pind that is: \sort{{$\mathbb{D}$,$\mathbb{S}$ $\models$ $\mathbb{R}$.}}
\afslut
\pind Advances in program proofs helps little if not including proper
      domain and requirements specifications.
\afslut

\nbbbb{Domain Facets}

\begynd
\pind There is more to \sfsl{domain modeling} than covered in this paper.
\pind In \cite{dines:facs:2008} and in \cite[\sfsl{Chapter
      8}]{BjornerMonograph2020} we cover the concept of \sfsl{domain facets}.
\pind General examples of domain facets are \sfsl{support technologies,
  rules \& regulations, scripts, license languages, management \&
  organization,} and \sfsl{human behaviour}. 
\afslut

\bbbb{Perspectives}

\begynd
\pind Domain models can be developed for either of a number of reasons:
\begin{itemize}
\item (i)   in order to \sfsl{understand} a human-artifact domain;
\item (ii ) in order to \sfsl{re-engineer the business processes} of a
            human-artifact domain; or
\item (iii) in order to develop \sfsl{requirements prescriptions} and,
            subsequently \sfsl{software} \sfsl{application} ``within''
            that domain.
\end{itemize}
\noindent
\pind [(ii)]  We refer to \cite{m.hammer93,m.hammer95}
and
\cite[\sfsl{Vol.\,3, Chapter\,19, pages\,404--412}]{TheSEBook123}
for the
              concept of \sfsl{business process engineering}.
              \pind [(iii)] We refer to
              \cite[\sfsl{Chapter 9}]{BjornerMonograph2020}
              for the
              concept of \sfsl{requirements engineering}.
\afslut

\subsection{The Semantics of Domain Models}

\begynd
\pind The meaning of domain models, such as we describe them in this
      paper, is, ``of course'', the actual, real domain ``out there''\,!
\begynd
\pind One could, and, perhaps one should, formulate a mathematical
      semantics of the models, that is, of the \sort{is\_..., obs\_...,
      uid\_..., mereo\_...} and \sort{attr\_...} analysis and description
      functions and what they entail (e.g., the type name labels:
      $\eta\mathbb{T}$'s; etc.).   
\pind An early such semantics description is given in \cite{bjorner-jaist-2014}.
\afslut
\afslut

\subsection{Further on Domain Modeling}

\begynd
\pind Additional facets of domain modeling are covered in 
\begynd
\pind  \cite{dines:ugo65:2008}
and
\pind  \cite[\sfsl{Chapter 8: \textsf{Domain Facets.}}]{BjornerMonograph2020} 
\afslut
\afslut

\subsection{Software Development}
 
\begynd
\pind \cite{dines:ugo65:2008} and
      \cite[\sfsl{Chapter 9 \textsf{Requirements}}]{BjornerMonograph2020}
\begynd
\pind show how to develop $\mathcal{R}$equirements prescriptions from
      $\mathcal{D}$omain descriptions.
\afslut
\pind \cite{TheSEBook123}
shows how to develop $\mathcal{S}$oftware designs
      from $\mathcal{R}$equirements prescriptions.
      \afslut

 
\subsection{Modeling}

\begynd
\pind Domain descriptions, such as outlined in this paper,
\begynd
\pind are models of domains, that is, of some reality.
\pind They need not necessarily lead to or be motivated by possible
      development of software for such domains.
\pind They can be experimentally researched and developed just for the
      sake of understanding domains in which man has had an
      significantly influence.
\pind They are models.
\pind We refer to \cite{FettkeReisig2023}
for complementary modeling
      based on Petri nets.
\afslut
\pind The current author is fascinated by the interplay between
      graphical and textual descriptions of \texttt{HERAKLIT}, well,
      in general \texttt{Petri Nets}.
\afslut
          
    
\subsection{Philosophy of Computing}

\begynd
\pind The Danish philosopher Kai S{\o}rlander
\cite{kaisorlander1994,kaisorlander2016,kaisorlander2022,kaisorlander2023}  
\begynd
\pind has shown that there is a foundation in philosophy
\pind for domain analysis and description. 
\afslut
\pind We refer to \cite[\sfsl{Chapter\,2}]{NewPrimer2023}
for a summary of his findings.
\afslut

%\dbeat
{ 
\subsection{A Manifesto}

\begynd
\pind So there is no excuse, anymore\,!
\begynd
\pind Of course we have developed interpreters and compilers for
      programming languages by first developing formal semantics for
      those languages \cite{e:db:Bj80f,Clem84}.
\pind Likewise we must now do for the languages of domain stakeholders, at
      least for the domains covered by this paper.
\pind There really is no excuse\,!
\afslut
\afslut
}

\bibliographystyle{plain}

\newcommand{\dbcite}[1]{\cite{#1}}
\newcommand{\dbkey}[1]{}
\newcommand{\BREAK}{}
\newcommand{\dbabstract}[1]{}
\newcommand{\dbbibpth}{/home/db/bib}
\input{ictac.bbl}
\dbeat
{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\sf
\bibliography{% 
\dbbibpth/strings,%
\dbbibpth/infra,%
\dbbibpth/ada,%
\dbbibpth/alle,%
\dbbibpth/allrail,%
\dbbibpth/annals,%% 
\dbbibpth/arch,%
\dbbibpth/asm,%
\dbbibpth/asger-specification,%%
\dbbibpth/asger-philosophy,%
\dbbibpth/b-method,%
\dbbibpth/bib,%
\dbbibpth/dsae,%% 
\dbbibpth/cacm,%
\dbbibpth/cofi,%
\dbbibpth/concept,%
\dbbibpth/darcsa,%
\dbbibpth/dcia,%%
\dbbibpth/ddc,%
\dbbibpth/des,%
\dbbibpth/art-dines,%%%%%%%%%%%%%%%%%%%%%%%%%%%
\dbbibpth/book-dines,%
\dbbibpth/rept-dines,%%
\dbbibpth/adm-dines,%
\dbbibpth/notes-dines,%
\dbbibpth/ckm,%
\dbbibpth/dines99,%
\dbbibpth/domain,%
\dbbibpth/doreso,%%
\dbbibpth/filosofi,%
\dbbibpth/chriswgeorge,%
\dbbibpth/havelund,%
\dbbibpth/HaxthausenReferences,%
\dbbibpth/heraklit,%
\dbbibpth/icse,%%
\dbbibpth/internet,%
\dbbibpth/jackson,%
\dbbibpth/klaus,%
\dbbibpth/ks,%
\dbbibpth/languages,%
\dbbibpth/larch,%
\dbbibpth/ll,%%
\dbbibpth/logics,%
\dbbibpth/method,%
\dbbibpth/nikolaj,%
\dbbibpth/nraisepap,%
\dbbibpth/1999,%
\dbbibpth/ontology,%%
\dbbibpth/pe,%
\dbbibpth/pipelines,%
\dbbibpth/raisepap,%
\dbbibpth/s2000,%
\dbbibpth/s2000-1,%
\dbbibpth/swarms,%%
\dbbibpth/seeduc,%
\dbbibpth/train,%
\dbbibpth/tlt,%
\dbbibpth/unuiist,%
\dbbibpth/vienna,%
\dbbibpth/vdm,%
\dbbibpth/vdmfme,%
\dbbibpth/zall}
\rm
}%%%%%%%%%%%%%%%%%%

\end{document}

%%  LocalWords:  modeling defind endurants perdurants endurant RSL le
%%  LocalWords:  artefactual unanalysed perdurant behaviours harbours
%%  LocalWords:  conveyage behaviour aise igorous pproach ndustrial
%%  LocalWords:  oftware ngineering pecification VDM CafeOBJ CSP vref
%%  LocalWords:  Unive ra nal ly de scrib subjectable onomastics bo
%%  LocalWords:  onomatology Onomastics toponyms anthroponyms ci ty
%%  LocalWords:  za tro mereologies amd modelled Ren atomicity et rn
%%  LocalWords:  plasmatic compartmentalise cetera neighbouring al Ei
%%  LocalWords:  Cartesians sa Ps utomobile erver ps Pn computable hs
%%  LocalWords:  monitorable wrt Defn mereological colour mereology
%%  LocalWords:  rts RTS rtsi RTSI rni RNI SAI ai hai AHI lai LAI li
%%  LocalWords:  PnI uids Stanis niewski ri PMer PIm nks rom APos atH
%%  LocalWords:  onL fhi thi HHis LHis AHis attr excert Stiglitz th
%%  LocalWords:  intentionality intentionalities Feldstein Inman ui
%%  LocalWords:  Palgrave Georgism uj ij Uid nfinckel'ed nfinkel wi
%%  LocalWords:  ki pe di ry ing Mereo Vals Prgr MereoH HHist uid ub
%%  LocalWords:  MereoL LHist MereoA AVel HAcc AHist AAcc ris ahis te
%%  LocalWords:  expressivity deterministically pre initialisation na
%%  LocalWords:  Bool priori prover Promela attribu ibute attri bute
%%  LocalWords:  tri staA monA prgA progammable behaviour's retr UoD
%%  LocalWords:  mereo equirements omain omains ontologically skema
%%  LocalWords:  schemas rti RTI Kai rlander Einsteinian inertA Petri
%%  LocalWords:  Gottlob Frege's HERAKLIT Manifasto ada alle allrail
%%  LocalWords:  asm asger dsae cacm cofi darcsa dcia ddc des rept
%%  LocalWords:  adm ckm doreso filosofi chriswgeorge havelund icse
%%  LocalWords:  HaxthausenReferences heraklit jackson klaus logics
%%  LocalWords:  nikolaj raisepap seeduc tlt unuiist vienna vdm zall
%%  LocalWords:  vdmfme nraisepap Landin Strachey wim MAJlexicon gam
%%  LocalWords:  ShaoFa anguage mab pdf dom
