From a5b7fa569a12d524b93ae9852dc5531f98ceb20e Mon Sep 17 00:00:00 2001 From: Alex Gabriel Date: Tue, 6 May 2025 16:52:49 +0200 Subject: [PATCH 1/6] adding reStructuredText documentation, converted by pandoc --- {docs => docs-md}/README.md | 0 .../assets/images/EU_funded_en.jpg | Bin {docs => docs-md}/assets/images/FHG-logo.png | Bin {docs => docs-md}/assets/images/IMR-logo.png | Bin {docs => docs-md}/assets/images/PAL-logo.png | Bin {docs => docs-md}/assets/images/TUD-logo.png | Bin {docs => docs-md}/assets/images/UPM-logo.png | Bin {docs => docs-md}/assets/images/URJC-logo.png | Bin .../assets/images/coresense-logo-reverse.png | Bin .../assets/images/coresense-logo.png | Bin .../cropped-Coresense-Site-Logo-32x32.png | Bin .../assets/images/tudelft-logo.png | Bin {docs => docs-md}/concepts/agent.md | 0 {docs => docs-md}/concepts/concept.md | 0 {docs => docs-md}/concepts/datatype.md | 0 {docs => docs-md}/concepts/engine.md | 0 {docs => docs-md}/concepts/exertion.md | 0 {docs => docs-md}/concepts/extent.md | 0 {docs => docs-md}/concepts/formalism.md | 0 {docs => docs-md}/concepts/index.md | 0 {docs => docs-md}/concepts/modelet.md | 0 {docs => docs-md}/concepts/origin.md | 0 {docs => docs-md}/concepts/phenomenon.md | 0 {docs => docs-md}/concepts/property.md | 0 .../concepts/representation_class.md | 0 {docs => docs-md}/concepts/requirement.md | 0 {docs => docs-md}/concepts/spacetime_point.md | 0 {docs => docs-md}/concepts/strategy.md | 0 {docs => docs-md}/concepts/template.md | 0 .../documentation-instructions.md | 0 {docs => docs-md}/index.md | 0 .../overrides/partials/footer.html | 0 {docs => docs-md}/packages/index.md | 0 {docs => docs-md}/requirements.txt | 0 {docs => docs-md}/stylesheets/extra.css | 0 {docs => docs-md}/usage/index.md | 0 docs-rst/concepts/agent.rst | 16 ++ docs-rst/concepts/concept.rst | 16 ++ docs-rst/concepts/datatype.rst | 191 ++++++++++++++++++ docs-rst/concepts/engine.rst | 82 ++++++++ docs-rst/concepts/exertion.rst | 68 +++++++ docs-rst/concepts/extent.rst | 46 +++++ docs-rst/concepts/formalism.rst | 22 ++ docs-rst/concepts/index.rst | 106 ++++++++++ docs-rst/concepts/modelet.rst | 106 ++++++++++ docs-rst/concepts/origin.rst | 21 ++ docs-rst/concepts/phenomenon.rst | 17 ++ docs-rst/concepts/property.rst | 49 +++++ docs-rst/concepts/representation_class.rst | 11 + docs-rst/concepts/requirement.rst | 36 ++++ docs-rst/concepts/spacetime_point.rst | 50 +++++ docs-rst/concepts/strategy.rst | 20 ++ docs-rst/concepts/template.rst | 81 ++++++++ docs-rst/index.rst | 1 + docs-rst/packages/index.rst | 2 + docs-rst/usage/index.rst | 13 ++ 56 files changed, 954 insertions(+) rename {docs => docs-md}/README.md (100%) rename {docs => docs-md}/assets/images/EU_funded_en.jpg (100%) rename {docs => docs-md}/assets/images/FHG-logo.png (100%) rename {docs => docs-md}/assets/images/IMR-logo.png (100%) rename {docs => docs-md}/assets/images/PAL-logo.png (100%) rename {docs => docs-md}/assets/images/TUD-logo.png (100%) rename {docs => docs-md}/assets/images/UPM-logo.png (100%) rename {docs => docs-md}/assets/images/URJC-logo.png (100%) rename {docs => docs-md}/assets/images/coresense-logo-reverse.png (100%) rename {docs => docs-md}/assets/images/coresense-logo.png (100%) rename {docs => docs-md}/assets/images/cropped-Coresense-Site-Logo-32x32.png (100%) rename {docs => docs-md}/assets/images/tudelft-logo.png (100%) rename {docs => docs-md}/concepts/agent.md (100%) rename {docs => docs-md}/concepts/concept.md (100%) rename {docs => docs-md}/concepts/datatype.md (100%) rename {docs => docs-md}/concepts/engine.md (100%) rename {docs => docs-md}/concepts/exertion.md (100%) rename {docs => docs-md}/concepts/extent.md (100%) rename {docs => docs-md}/concepts/formalism.md (100%) rename {docs => docs-md}/concepts/index.md (100%) rename {docs => docs-md}/concepts/modelet.md (100%) rename {docs => docs-md}/concepts/origin.md (100%) rename {docs => docs-md}/concepts/phenomenon.md (100%) rename {docs => docs-md}/concepts/property.md (100%) rename {docs => docs-md}/concepts/representation_class.md (100%) rename {docs => docs-md}/concepts/requirement.md (100%) rename {docs => docs-md}/concepts/spacetime_point.md (100%) rename {docs => docs-md}/concepts/strategy.md (100%) rename {docs => docs-md}/concepts/template.md (100%) rename {docs => docs-md}/documentation-instructions.md (100%) rename {docs => docs-md}/index.md (100%) rename {docs => docs-md}/overrides/partials/footer.html (100%) rename {docs => docs-md}/packages/index.md (100%) rename {docs => docs-md}/requirements.txt (100%) rename {docs => docs-md}/stylesheets/extra.css (100%) rename {docs => docs-md}/usage/index.md (100%) create mode 100644 docs-rst/concepts/agent.rst create mode 100644 docs-rst/concepts/concept.rst create mode 100644 docs-rst/concepts/datatype.rst create mode 100644 docs-rst/concepts/engine.rst create mode 100644 docs-rst/concepts/exertion.rst create mode 100644 docs-rst/concepts/extent.rst create mode 100644 docs-rst/concepts/formalism.rst create mode 100644 docs-rst/concepts/index.rst create mode 100644 docs-rst/concepts/modelet.rst create mode 100644 docs-rst/concepts/origin.rst create mode 100644 docs-rst/concepts/phenomenon.rst create mode 100644 docs-rst/concepts/property.rst create mode 100644 docs-rst/concepts/representation_class.rst create mode 100644 docs-rst/concepts/requirement.rst create mode 100644 docs-rst/concepts/spacetime_point.rst create mode 100644 docs-rst/concepts/strategy.rst create mode 100644 docs-rst/concepts/template.rst create mode 100644 docs-rst/index.rst create mode 100644 docs-rst/packages/index.rst create mode 100644 docs-rst/usage/index.rst diff --git a/docs/README.md b/docs-md/README.md similarity index 100% rename from docs/README.md rename to docs-md/README.md diff --git a/docs/assets/images/EU_funded_en.jpg b/docs-md/assets/images/EU_funded_en.jpg similarity index 100% rename from docs/assets/images/EU_funded_en.jpg rename to docs-md/assets/images/EU_funded_en.jpg diff --git a/docs/assets/images/FHG-logo.png b/docs-md/assets/images/FHG-logo.png similarity index 100% rename from docs/assets/images/FHG-logo.png rename to docs-md/assets/images/FHG-logo.png diff --git a/docs/assets/images/IMR-logo.png b/docs-md/assets/images/IMR-logo.png similarity index 100% rename from docs/assets/images/IMR-logo.png rename to docs-md/assets/images/IMR-logo.png diff --git a/docs/assets/images/PAL-logo.png b/docs-md/assets/images/PAL-logo.png similarity index 100% rename from docs/assets/images/PAL-logo.png rename to docs-md/assets/images/PAL-logo.png diff --git a/docs/assets/images/TUD-logo.png b/docs-md/assets/images/TUD-logo.png similarity index 100% rename from docs/assets/images/TUD-logo.png rename to docs-md/assets/images/TUD-logo.png diff --git a/docs/assets/images/UPM-logo.png b/docs-md/assets/images/UPM-logo.png similarity index 100% rename from docs/assets/images/UPM-logo.png rename to docs-md/assets/images/UPM-logo.png diff --git a/docs/assets/images/URJC-logo.png b/docs-md/assets/images/URJC-logo.png similarity index 100% rename from docs/assets/images/URJC-logo.png rename to docs-md/assets/images/URJC-logo.png diff --git a/docs/assets/images/coresense-logo-reverse.png b/docs-md/assets/images/coresense-logo-reverse.png similarity index 100% rename from docs/assets/images/coresense-logo-reverse.png rename to docs-md/assets/images/coresense-logo-reverse.png diff --git a/docs/assets/images/coresense-logo.png b/docs-md/assets/images/coresense-logo.png similarity index 100% rename from docs/assets/images/coresense-logo.png rename to docs-md/assets/images/coresense-logo.png diff --git a/docs/assets/images/cropped-Coresense-Site-Logo-32x32.png b/docs-md/assets/images/cropped-Coresense-Site-Logo-32x32.png similarity index 100% rename from docs/assets/images/cropped-Coresense-Site-Logo-32x32.png rename to docs-md/assets/images/cropped-Coresense-Site-Logo-32x32.png diff --git a/docs/assets/images/tudelft-logo.png b/docs-md/assets/images/tudelft-logo.png similarity index 100% rename from docs/assets/images/tudelft-logo.png rename to docs-md/assets/images/tudelft-logo.png diff --git a/docs/concepts/agent.md b/docs-md/concepts/agent.md similarity index 100% rename from docs/concepts/agent.md rename to docs-md/concepts/agent.md diff --git a/docs/concepts/concept.md b/docs-md/concepts/concept.md similarity index 100% rename from docs/concepts/concept.md rename to docs-md/concepts/concept.md diff --git a/docs/concepts/datatype.md b/docs-md/concepts/datatype.md similarity index 100% rename from docs/concepts/datatype.md rename to docs-md/concepts/datatype.md diff --git a/docs/concepts/engine.md b/docs-md/concepts/engine.md similarity index 100% rename from docs/concepts/engine.md rename to docs-md/concepts/engine.md diff --git a/docs/concepts/exertion.md b/docs-md/concepts/exertion.md similarity index 100% rename from docs/concepts/exertion.md rename to docs-md/concepts/exertion.md diff --git a/docs/concepts/extent.md b/docs-md/concepts/extent.md similarity index 100% rename from docs/concepts/extent.md rename to docs-md/concepts/extent.md diff --git a/docs/concepts/formalism.md b/docs-md/concepts/formalism.md similarity index 100% rename from docs/concepts/formalism.md rename to docs-md/concepts/formalism.md diff --git a/docs/concepts/index.md b/docs-md/concepts/index.md similarity index 100% rename from docs/concepts/index.md rename to docs-md/concepts/index.md diff --git a/docs/concepts/modelet.md b/docs-md/concepts/modelet.md similarity index 100% rename from docs/concepts/modelet.md rename to docs-md/concepts/modelet.md diff --git a/docs/concepts/origin.md b/docs-md/concepts/origin.md similarity index 100% rename from docs/concepts/origin.md rename to docs-md/concepts/origin.md diff --git a/docs/concepts/phenomenon.md b/docs-md/concepts/phenomenon.md similarity index 100% rename from docs/concepts/phenomenon.md rename to docs-md/concepts/phenomenon.md diff --git a/docs/concepts/property.md b/docs-md/concepts/property.md similarity index 100% rename from docs/concepts/property.md rename to docs-md/concepts/property.md diff --git a/docs/concepts/representation_class.md b/docs-md/concepts/representation_class.md similarity index 100% rename from docs/concepts/representation_class.md rename to docs-md/concepts/representation_class.md diff --git a/docs/concepts/requirement.md b/docs-md/concepts/requirement.md similarity index 100% rename from docs/concepts/requirement.md rename to docs-md/concepts/requirement.md diff --git a/docs/concepts/spacetime_point.md b/docs-md/concepts/spacetime_point.md similarity index 100% rename from docs/concepts/spacetime_point.md rename to docs-md/concepts/spacetime_point.md diff --git a/docs/concepts/strategy.md b/docs-md/concepts/strategy.md similarity index 100% rename from docs/concepts/strategy.md rename to docs-md/concepts/strategy.md diff --git a/docs/concepts/template.md b/docs-md/concepts/template.md similarity index 100% rename from docs/concepts/template.md rename to docs-md/concepts/template.md diff --git a/docs/documentation-instructions.md b/docs-md/documentation-instructions.md similarity index 100% rename from docs/documentation-instructions.md rename to docs-md/documentation-instructions.md diff --git a/docs/index.md b/docs-md/index.md similarity index 100% rename from docs/index.md rename to docs-md/index.md diff --git a/docs/overrides/partials/footer.html b/docs-md/overrides/partials/footer.html similarity index 100% rename from docs/overrides/partials/footer.html rename to docs-md/overrides/partials/footer.html diff --git a/docs/packages/index.md b/docs-md/packages/index.md similarity index 100% rename from docs/packages/index.md rename to docs-md/packages/index.md diff --git a/docs/requirements.txt b/docs-md/requirements.txt similarity index 100% rename from docs/requirements.txt rename to docs-md/requirements.txt diff --git a/docs/stylesheets/extra.css b/docs-md/stylesheets/extra.css similarity index 100% rename from docs/stylesheets/extra.css rename to docs-md/stylesheets/extra.css diff --git a/docs/usage/index.md b/docs-md/usage/index.md similarity index 100% rename from docs/usage/index.md rename to docs-md/usage/index.md diff --git a/docs-rst/concepts/agent.rst b/docs-rst/concepts/agent.rst new file mode 100644 index 0000000..73949c6 --- /dev/null +++ b/docs-rst/concepts/agent.rst @@ -0,0 +1,16 @@ +Types +===== + +.. _agent: + +**agent** ``$tType`` +-------------------- + +A **CoreSense** agent which may posess `engines `__ and +`modelets `__. + +!!! warning “Unimplemented” To be introduced later, as collective +awareness is considered. + +Source: ``fundamental-concepts.tff`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/docs-rst/concepts/concept.rst b/docs-rst/concepts/concept.rst new file mode 100644 index 0000000..0a50989 --- /dev/null +++ b/docs-rst/concepts/concept.rst @@ -0,0 +1,16 @@ +Types +===== + +.. _concept: + +**concept** ``$tType`` +---------------------- + +An instance of a class of `phenomenon `__ in the agent’s +world model. + +A `concept <#concept>`__ is a `property `__ of a +`modelet `__. + +!!! example - chair - dog - the color pink - sunrise ###### Source: +``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/datatype.rst b/docs-rst/concepts/datatype.rst new file mode 100644 index 0000000..9c1c75d --- /dev/null +++ b/docs-rst/concepts/datatype.rst @@ -0,0 +1,191 @@ +Types +===== + +.. _datatype: + +**datatype** ``$tType`` +----------------------- + +A precise information encoding that is taken as granted. As the name +suggests, the fundamental types of data considered. + +!!! example - real number - uint8 - pixel ###### Source: +``fundamental-concepts.tff`` + +ROS 2 Interface builtins +======================== + +ROS 2 interfaces (messages, services, and actions) are +`formalisms `__ constructed from semantically named +builtin `datatypes <#datatype>`__ and arrays of these builtins. See the +ROS 2 +`documentation `__ +for more details. + +!!! important These individuals are not associated with a particular +semantic label. The intention (WIP) is to match a particular +`datatype <#datatype>`__ (the ``fieldtype``) and a +`concept `__ (the ``fieldname``) in some +`formalism `__ representing the ROS 2 interface. + +.. _ros2-msg-bool: + +**‘ROS2.msg.Bool’** ```datatype`` <#datatype>`__ +------------------------------------------------ + +The builtin ``bool`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-byte: + +**‘ROS2.msg.Byte’** ```datatype`` <#datatype>`__ +------------------------------------------------ + +The builtin ``byte`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-char: + +**‘ROS2.msg.Char’** ```datatype`` <#datatype>`__ +------------------------------------------------ + +The builtin ``char`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-float32: + +**‘ROS2.msg.Float32’** ```datatype`` <#datatype>`__ +--------------------------------------------------- + +The builtin ``float32`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-float64: + +**‘ROS2.msg.Float64’** ```datatype`` <#datatype>`__ +--------------------------------------------------- + +The builtin ``float64`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-int8: + +**‘ROS2.msg.Int8’** ```datatype`` <#datatype>`__ +------------------------------------------------ + +The builtin ``int8`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-uint8: + +**‘ROS2.msg.Uint8’** ```datatype`` <#datatype>`__ +------------------------------------------------- + +The builtin ``uint8`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-int16: + +**‘ROS2.msg.Int16’** ```datatype`` <#datatype>`__ +------------------------------------------------- + +The builtin ``int16`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-uint16: + +**‘ROS2.msg.Uint16’** ```datatype`` <#datatype>`__ +-------------------------------------------------- + +The builtin ``uin16`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-int32: + +**‘ROS2.msg.Int32’** ```datatype`` <#datatype>`__ +------------------------------------------------- + +The builtin ``int32`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-uint32: + +**‘ROS2.msg.Uint32’** ```datatype`` <#datatype>`__ +-------------------------------------------------- + +The builtin ``uint32`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-int64: + +**‘ROS2.msg.Int64’** ```datatype`` <#datatype>`__ +------------------------------------------------- + +The builtin ``int64`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-uint64: + +**‘ROS2.msg.Uint64’** ```datatype`` <#datatype>`__ +-------------------------------------------------- + +The builtin ``uint64`` field type of a ROS 2 interface. ###### Source: +``datatypes.tff`` + +.. _ros2-msg-string: + +**‘ROS2.msg.String’** ```datatype`` <#datatype>`__ +-------------------------------------------------- + +The builtin (unbounded) ``string`` field type of a ROS 2 interface. +These strings use 8-bit characters. ###### Source: ``datatypes.tff`` + +.. _ros2-msg-wstring: + +**‘ROS2.msg.Wstring’** ```datatype`` <#datatype>`__ +--------------------------------------------------- + +The builtin ``wstring`` field type of a ROS 2 interface. These strings +use 16-bit characters. ###### Source: ``datatypes.tff`` + +ROS 2 Interface arrays +====================== + +ROS 2 interfaces support arrays of builtins, optionally with a fixed or +bounded size. !!! warning Sizes of array datatypes are assumed to be +natural numbers. This is **NOT** enforced by the type checker or logic. + +.. _ros2-msg-bounded-string: + +**‘ROS2.msg.BoundedString’** ``(``\ **``$int``**\ ``>``\ ```datatype`` <#datatype>`__\ ``)`` +-------------------------------------------------------------------------------------------- + +A bounded ``string<=n`` field type of a ROS 2 interface. ``n`` is a +natural number. ###### Source: ``datatypes.tff`` + +.. _ros2-msg-unbounded-dynamic-array: + +**‘ROS2.msg.UnboundedDynamicArray’** ``(``\ ```datatype`` <#datatype>`__\ ``>``\ ```datatype`` <#datatype>`__\ ``)`` +-------------------------------------------------------------------------------------------------------------------- + +An array of any builtin with an unbouned size field type in a ROS 2 +interface. !!! example - ``char[]`` - ``float32[]`` ###### Source: +``datatypes.tff`` + +.. _ros2-msg-bounded-dynamic-array: + +**‘ROS2.msg.BoundedDynamicArray’** ``((``\ ```datatype`` <#datatype>`__\ ``*``\ **``$int``**\ ``) >``\ ```datatype`` <#datatype>`__\ ``)`` +------------------------------------------------------------------------------------------------------------------------------------------ + +A dynamic array of any builtin with a bounded size field type in a ROS 2 +interface. The size must be a natural number. !!! example - +``char[<=5]`` - ``float32[<=4]`` ###### Source: ``datatypes.tff`` + +.. _ros2-msg-static-array: + +**‘ROS2.msg.StaticArray’** ``((``\ ```datatype`` <#datatype>`__\ ``*``\ **``$int``**\ ``) >``\ ```datatype`` <#datatype>`__\ ``)`` +---------------------------------------------------------------------------------------------------------------------------------- + +A static array of any builtin with a fixed size field type in a ROS 2 +interface. The size must be a natural number. !!! example - ``char[5]`` +- ``float32[4]`` ###### Source: ``datatypes.tff`` diff --git a/docs-rst/concepts/engine.rst b/docs-rst/concepts/engine.rst new file mode 100644 index 0000000..fb3e8b9 --- /dev/null +++ b/docs-rst/concepts/engine.rst @@ -0,0 +1,82 @@ +Types +===== + +.. _engine: + +**engine** ``$tType`` +--------------------- + +Does work within a **CoreSense** `agent `__ to produce +`modelets `__. + +- Takes multiple `modelets `__ as an input + `modelet_set `__ +- Uses semantic information to identify valid input modelet + `formalisms `__ + + - semantics could be external (part of the type definition) or + internal (modeled within the `modelet `__ itself) + +- Produces one output `modelet `__ + + - May or may not impart semantic meaning to the output + `modelet `__ + - May (re)define the output modelet `origin `__, + `concept `__, or characteristics + +- Has `exertion `__ characteristics + + - e.g. time delay, resource usage, power consumption + +!!! example - DroneStateEngine (see tff/tests/test-wind-estimation.tff) +- Input Model: - Modelet - formalism: IMU.msg - modelled concept: +inertia - Modelet - formalism: NavSatFix.msg - modelled concept: +geolocation - Output Modelet: - modelet - formalism: DroneState.msg - +modelled concept: drone_state ###### Source: +``engines-and-modelets.tff`` + +Relations +========= + +.. _interface_of: + +**interface_of** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```template_set`` `__\ ``)`` +--------------------------------------------------------------------------------------------------------------- + +An `engine <#engine>`__ requires a set of input +`modelets `__ which matches the +`template_set `__. ###### Source: +``engines-and-modelets.tff`` + +.. _output_modelet_formalism: + +**output_modelet_formalism** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```formalism`` `__\ ``)`` +------------------------------------------------------------------------------------------------------------ + +The `formalism `__ of an `engine <#engine>`__ output +`modelet `__. ###### Source: ``engines-and-modelets.tff`` + +.. _is_output_modelet_concept: + +**is_output_modelet_concept** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```phenomenon`` `__\ ``)`` +--------------------------------------------------------------------------------------------------------------- + +The `concept `__ of an `engine <#engine>`__ output +`modelet `__. ###### Source: ``engines-and-modelets.tff`` + +.. _output_property_of_e: + +**output_property_of_engine** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```property`` `__\ ``)`` +----------------------------------------------------------------------------------------------------------- + +The `property `__ an `engine <#engine>`__ imparts on its +output `modelet `__. ###### Source: ``properties.tff`` + +.. _engine_imparts_representation_class: + +**engine_imparts_representation_class** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```representation_class`` `__\ ``)`` +--------------------------------------------------------------------------------------------------------------------------------------------- + +The `representation_class `__ an +`engine <#engine>`__ imparts on its output `modelet `__. +###### Source: ``engines-and-modelets.tff`` diff --git a/docs-rst/concepts/exertion.rst b/docs-rst/concepts/exertion.rst new file mode 100644 index 0000000..cc5637c --- /dev/null +++ b/docs-rst/concepts/exertion.rst @@ -0,0 +1,68 @@ +Relations +========= + +**inputs_match** ``((``\ ```modelet`` `__\ ``*``\ ```template`` `__\ ``) >``\ \*\*\ ``$o``\ \*\ ``)`` { #inputs_match data-toc-label=‘inputs_match’ } +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ + +Check if a `modelet `__ matches a +`template `__. + +- Check if they are `formally equivalent <#formally_equivalent>`__ +- Check if the `modelet `__ contains *permissible* values + for each of the `properties `__ of + `requirements `__ of the `template `__. + ###### Source: ``engines-and-modelets.tff``, ``properties.tff`` + +.. _formally_equivalent: + +**formally_equivalent** ``((``\ ```template`` `__\ ``*``\ ```modelet`` `__\ ``) >``\ **``$o``**\ ``)`` +------------------------------------------------------------------------------------------------------------------------------- + +A `template `__ and a `modelet `__ share the +same *phenomenon* and `formalism `__. ###### Source: +``properties.tff`` + +.. _interfaces_match: + +**interfaces_match** ``((``\ ```modelet_set`` `__\ ``*``\ ```template_set`` `__\ ``) >``\ **``$o``**\ ``)`` +------------------------------------------------------------------------------------------------------------------------------------------------------------- + +Check if all of the `templates `__ in the +`template_set `__ have a corresponding +`modelet `__ in the `modelet_set `__ +with matching profile. + +- Check if they are `formally equivalent <#formally_equivalent>`__ +- Check if their `inputs match <#inputs_match>`__ ###### Source: + ``engines-and-modelets.tff``, ``properties.tff`` + +.. _exert: + +**exert** ``((``\ ```engine`` `__\ ``*``\ ```modelet_set`` `__\ ``*``\ ```modelet`` `__\ ``) >``\ **``$o``**\ ``)`` +------------------------------------------------------------------------------------------------------------------------------------------------------------------ + +Exert an `engine `__ on a +`modelet_set `__ to produce an output +`modelet `__. ###### Source: ``engines-and-modelets.tff`` + +.. _exertable: + +**exertable** ``((``\ ```modelet_set`` `__\ ``*``\ ```engine`` `__\ ``) >``\ **``$o``**\ ``)`` +--------------------------------------------------------------------------------------------------------------------------------- + +A `modelet_set `__ can be exerted by an +`engine `__ iff their `interfaces +match <#interfaces_match>`__. ###### Source: +``engines-and-modelets.tff`` + +.. raw:: html + + diff --git a/docs-rst/concepts/extent.rst b/docs-rst/concepts/extent.rst new file mode 100644 index 0000000..e0ce89f --- /dev/null +++ b/docs-rst/concepts/extent.rst @@ -0,0 +1,46 @@ +Types +===== + +.. _extent: + +**extent** ``$tType`` +--------------------- + +A 4-dimensional size (3 space, 1 time). !!! note Not to be confused with +a 4-dimentional ```spacetime_point`` `__. ###### +Source: ``fundamental-concepts.tff`` + +Relations +========= + +.. _extent_width: + +**extent_width** ``(``\ ```extent`` <#extent>`__\ ``>``\ **``$real``**\ ``)`` +----------------------------------------------------------------------------- + +The width of an (```extent`` <#extent>`__). ###### Source: +``fundamental-concepts.tff`` + +.. _extent_height: + +**extent_height** ``(``\ ```extent`` <#extent>`__\ ``>``\ **``$real``**\ ``)`` +------------------------------------------------------------------------------ + +The height of an (```extent`` <#extent>`__). ###### Source: +``fundamental-concepts.tff`` + +.. _extent_depth: + +**extent_depth** ``(``\ ```extent`` <#extent>`__\ ``>``\ **``$real``**\ ``)`` +----------------------------------------------------------------------------- + +The depth of an (```extent`` <#extent>`__). ###### Source: +``fundamental-concepts.tff`` + +.. _extent_duration: + +**extent_duration** ``(``\ ```extent`` <#extent>`__\ ``>``\ **``$real``**\ ``)`` +-------------------------------------------------------------------------------- + +The duration of an (```extent`` <#extent>`__). ###### Source: +``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/formalism.rst b/docs-rst/concepts/formalism.rst new file mode 100644 index 0000000..6f91001 --- /dev/null +++ b/docs-rst/concepts/formalism.rst @@ -0,0 +1,22 @@ +Types +===== + +.. _formalism: + +**formalism** ``$tType`` +------------------------ + +The language and structure in which a `phenomenon `__ +could be described. Methods used to express `modelets `__; +class in the *Data Model*. + +- The information structure used to capture the + `concept `__ and `origin `__ +- Highlights some aspects of the *phenomenon* while hiding others +- Defines `engine `__ I/O compatibility and usability with + other models + +New `formalism <#formalism>`__ could be defined or old ones modified. + +!!! example - ROS message - Image format - Language grammar ###### +Source: Understanding presentation diff --git a/docs-rst/concepts/index.rst b/docs-rst/concepts/index.rst new file mode 100644 index 0000000..35944af --- /dev/null +++ b/docs-rst/concepts/index.rst @@ -0,0 +1,106 @@ +Concepts +======== + +!!! danger These concepts are still in development and high susceptible +to change. Use the provided terms, definitions, and types with caution. + +The **Understanding System** (a.k.a Understanding Core) is a CoreSense +module for generating understanding within a *CoreSense* agent. The main +idea is to: !!! quote “Intuition” Find *strategies* of **Engine** +*exertions* to **create** required **Modelets**. + +!!! question “TODO” Add a map of the concepts or something more elegant +here… We should also include the triangle of meaning. + +Types +----- + +`agent `__ +~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/agent.rst:3:3” + +`datatype `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/datatype.rst:3:3” + +`engine `__ +~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/engine.rst:3:3” + +`exertion `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/exertion.rst:3:3” + +`extent `__ +~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/extent.rst:3:3” + +`formalism `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/formalism.rst:3:3” + +`modelet `__ +~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/modelet.rst:3:3” + +`modelet_set `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/modelet.rst:13:13” + +`origin `__ +~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/origin.rst:3:3” + +`phenomenon `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/phenomenon.rst:3:4” + +`property `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/property.rst:3:3” + +`requirement `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/requirement.rst:3:3” + +`representation_class `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/representation_class.rst:3:3” + +`spacetime_point `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/spacetime_point.rst:3:3” + +`strategy `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/strategy.rst:3:3” + +`template `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/template.rst:3:4” + +`template_set `__ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/template.rst:11:11” + +`concept `__ +~~~~~~~~~~~~~~~~~~~~~~~~ + +–8<– “docs/concepts/concept.rst:3:3” diff --git a/docs-rst/concepts/modelet.rst b/docs-rst/concepts/modelet.rst new file mode 100644 index 0000000..4307c55 --- /dev/null +++ b/docs-rst/concepts/modelet.rst @@ -0,0 +1,106 @@ +Types +===== + +.. _modelet: + +**modelet** ``$tType`` +---------------------- + +Models a `phenomenon `__ as the *thought* in the triangle +of meaning. All modelets describe an instance of a +`concept `__, have an `origin `__, and are +modeled in a specific `formalism `__. + +- `Concept `__: the *phenomenon* of the + `modelet <#modelet>`__, an instance of a class in the world model. +- `Origin `__: the agent’s perspective on the *phenomenon* +- `Formalism `__: the representation of the *phenomenon* + ###### Source: ``engines-and-modelets.tff`` + +.. _modelet_set: + +**modelet_set** ``$tType`` +-------------------------- + +Some particular set of `modelets <#modelet>`__ which the has reasoner +assembled. Used to collect the inputs to an `engine `__. !!! +example - {m1, m2, m3} - {m2} - {} ###### Source: +``engines-and-modelets.tff`` + +Relations +========= + +.. _modelet_models_concept: + +**modelet_models_concept** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```phenomenon`` `__\ ``)`` +-------------------------------------------------------------------------------------------------------------- + +The `phenomenon `__ symbolizing the *phenomenon* of a +`modelet `__. !!! question “TODO” rename from ‘concept’ to +something else. ###### Source: ``engines-and-modelets.tff`` + +.. _formalism_of_modelet: + +**formalism_of_modelet** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```formalism`` `__\ ``)`` +---------------------------------------------------------------------------------------------------------- + +The `formalism `__ used by a `modelet <#modelet>`__ to +describe the *phenomenon*. ###### Source: ``engines-and-modelets.tff`` + +.. _modelet_creation_date: + +**modelet_creation_date** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ **``$real``**\ ``)`` +---------------------------------------------------------------------------------------- + +The date a `modelet <#modelet>`__ was created. !!! question “TODO” The +date is represented as a ``$real`` but we don’t make any assumptions +about what that number represents. Unix time? time since last restart? +seconds? This may be solved by integration with ``spacetime_point``. +###### Source: ``engines-and-modelets.tff`` + +.. _modelet_has_location: + +**modelet_has_location** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```spacetime_point`` `__\ ``)`` +---------------------------------------------------------------------------------------------------------------------- + +The time and spatial location a `modelet <#modelet>`__ refers to. +`Modelets `__ may have a specific temporal scope or make an +observation at a specific ```spacetime_point`` `__. +###### Source: ``engines-and-modelets.tff`` + +.. _modelet_has_extent: + +**modelet_has_extent** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```extent`` `__\ ``)`` +-------------------------------------------------------------------------------------------------- + +The time and spatial `extent `__ a `modelet <#modelet>`__ +refers to. `Modelets <#modelet>`__ may have an area/volume/duration of +reference. ###### Source: ``engines-and-modelets.tff`` + +.. _modelet_has_representation_class: + +**modelet_has_representation_class** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```representation_class`` `__\ ``)`` +-------------------------------------------------------------------------------------------------------------------------------------------- + +The `representation_class `__ a +`modelet <#modelet>`__\ ’s relation to its parents has after being +created by an `engine `__. !!! question “TODO” This looks +like it will turn out to be HOL. ###### Source: +``engines-and-modelets.tff`` + +.. _modelet_has_creator: + +**modelet_has_creator** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```engine`` `__\ ``)`` +--------------------------------------------------------------------------------------------------- + +The `engine `__ that created the `modelet <#modelet>`__. +###### Source: ``engines-and-modelets.tff`` + +.. _is_in_modelet_set: + +**is_in_modelet_set** ``((``\ ```modelet`` <#modelet>`__\ ``*``\ ```modelet_set`` <#modelet_set>`__\ ``) >``\ **``$o``**\ ``)`` +------------------------------------------------------------------------------------------------------------------------------- + +Check if a `modelet <#modelet>`__ is a member of a +`modelet_set <#modelet_set>`__. ###### Source: +``engines-and-modelets.tff`` diff --git a/docs-rst/concepts/origin.rst b/docs-rst/concepts/origin.rst new file mode 100644 index 0000000..5f78220 --- /dev/null +++ b/docs-rst/concepts/origin.rst @@ -0,0 +1,21 @@ +Types +===== + +.. _origin: + +**origin** ``$tType`` +--------------------- + +An agent’s perspective on the *phenomenon* captured in a particular +`modelet `__. + +- Observation is *situated* in time and space +- Measured with sensors that have certain characteristics and + limitations + + - (inferred) physical quality (e.g. distance inferred from delay) + - resolution and frame rate + - reflections and transparencies could be misinterpreted + +Source: Understanding presentation +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/docs-rst/concepts/phenomenon.rst b/docs-rst/concepts/phenomenon.rst new file mode 100644 index 0000000..561b4a3 --- /dev/null +++ b/docs-rst/concepts/phenomenon.rst @@ -0,0 +1,17 @@ +Types +===== + +.. _phenomenon: + +**phenomenon** ``$tType`` +------------------------- + +Some space or object or being or process in the real world that the +system represents using `modelets `__. + +- *Situated* in time and space +- May change over time +- Associated with a mission-dependent *meaning* + +!!! example - you - your office - your tea - your tea approaching room +temperature ###### Source: ``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/property.rst b/docs-rst/concepts/property.rst new file mode 100644 index 0000000..f780f9b --- /dev/null +++ b/docs-rst/concepts/property.rst @@ -0,0 +1,49 @@ +Types +===== + +.. _property: + +**property** ``$tType`` +----------------------- + +A specific characteristic of a `modelet `__ or +`engine `__. Multiple things can exhibit the same +`property <#property>`__. + +!!! example - color: red - age: 14 years ###### Source: +``properties.tff`` + +Relations +========= + +.. _has_value: + +**has_value** ``(``\ ```property`` <#property>`__\ ``>``\ **``$real``**\ ``)`` +------------------------------------------------------------------------------ + +The value of a certain `property <#property>`__. ###### Source: +``properties.tff`` + +.. _datatype_of_p: + +**datatype_of_property** ``(``\ ```property`` <#property>`__\ ``>``\ ```datatype`` `__\ ``)`` +---------------------------------------------------------------------------------------------------------- + +The `datatype `__ of a certain `property <#property>`__. +###### Source: ``properties.tff`` + +.. _is_property_of_m: + +**is_property_of_modelet** ``((``\ ```property`` <#property>`__\ ``*``\ ```modelet`` `__\ ``) >``\ **``$o``**\ ``)`` +-------------------------------------------------------------------------------------------------------------------------------- + +Check if a `modelet `__ is described by a certain +`property <#property>`__. ###### Source: ``properties.tff`` + +.. _is_property_of_e: + +**is_property_of_engine** ``((``\ ```property`` <#property>`__\ ``*``\ ```engine`` `__\ ``) >``\ **``$o``**\ ``)`` +----------------------------------------------------------------------------------------------------------------------------- + +Check if an `engine `__ is described by a certain +`property <#property>`__. ###### Source: ``properties.tff`` diff --git a/docs-rst/concepts/representation_class.rst b/docs-rst/concepts/representation_class.rst new file mode 100644 index 0000000..d307ed7 --- /dev/null +++ b/docs-rst/concepts/representation_class.rst @@ -0,0 +1,11 @@ +Types +===== + +.. _representation_class: + +**representation_class** ``$tType`` +----------------------------------- + +The purpose of a `modelet `__ (extrinsic to itself) when +used by an `engine `__. Class in the *Processing/Modelling +Model*. ###### Source: ``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/requirement.rst b/docs-rst/concepts/requirement.rst new file mode 100644 index 0000000..d382163 --- /dev/null +++ b/docs-rst/concepts/requirement.rst @@ -0,0 +1,36 @@ +Types +===== + +.. _requirement: + +**requirement** ``$tType`` +-------------------------- + +A restriction on the `property `__ values that a +`template `__ may enforce on a `modelet `__. +###### Source: ``properties.tff`` + +Relations +========= + +.. _datatype_of_p: + +**datatype_of_requirement** ``(``\ ```requirement`` <#requirement>`__\ ``>``\ ```datatype`` `__\ ``)`` +------------------------------------------------------------------------------------------------------------------- + +The `datatype `__ of a certain +`requirement <#requirement>`__. ###### Source: ``properties.tff`` + +.. _is_permissible: + +**is_permissible** ``((``\ ```requirement`` <#requirement>`__\ ``*``\ **``$real``**\ ``) >``\ **``$o``**\ ``)`` +--------------------------------------------------------------------------------------------------------------- + +Check if a value is *permissible* under a certain +`requirement <#requirement>`__. ###### Source: ``properties.tff`` + +**is_part_of** ``((``\ ```requirement`` <#requirement>`__\ ``*``\ ```template`` `__\ ``) >``\ **``$o``**\ ``)`` { $is_part_of data-toc-label=‘is_part_of’ } +------------------------------------------------------------------------------------------------------------------------------------------------------------------------ + +Check if a `requirement <#requirement>`__ is part of a +`template `__. ###### Source: ``properties.tff`` diff --git a/docs-rst/concepts/spacetime_point.rst b/docs-rst/concepts/spacetime_point.rst new file mode 100644 index 0000000..dcc76d0 --- /dev/null +++ b/docs-rst/concepts/spacetime_point.rst @@ -0,0 +1,50 @@ +Types +===== + +.. _spacetime_point: + +**spacetime_point** ``$tType`` +------------------------------ + +4-dimensional coordinates (3 space, 1 time). !!! note Not to be confused +with a 4-dimentional ```extent`` `__. ###### Source: +``fundamental-concepts.tff`` + +Relations +========= + +.. _point_x: + +**point_x** ``(``\ ```spacetime_point`` <#spacetime_point>`__\ ``>``\ **``$real``**\ ``)`` +------------------------------------------------------------------------------------------ + +The spatial ``x`` coordinate of a point in space and time +(```spacetime_point`` <#spacetime_point>`__). ###### Source: +``fundamental-concepts.tff`` + +.. _point_y: + +**point_y** ``(``\ ```spacetime_point`` <#spacetime_point>`__\ ``>``\ **``$real``**\ ``)`` +------------------------------------------------------------------------------------------ + +The spatial ``y`` coordinate of a point in space and time +(```spacetime_point`` <#spacetime_point>`__). ###### Source: +``fundamental-concepts.tff`` + +.. _point_z: + +**point_z** ``(``\ ```spacetime_point`` <#spacetime_point>`__\ ``>``\ **``$real``**\ ``)`` +------------------------------------------------------------------------------------------ + +The spatial ``z`` coordinate of a point in space and time +(```spacetime_point`` <#spacetime_point>`__). ###### Source: +``fundamental-concepts.tff`` + +.. _point_t: + +**point_t** ``(``\ ```spacetime_point`` <#spacetime_point>`__\ ``>``\ **``$real``**\ ``)`` +------------------------------------------------------------------------------------------ + +The time ``t`` coordinate of a point in space and time +(```spacetime_point`` <#spacetime_point>`__). ###### Source: +``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/strategy.rst b/docs-rst/concepts/strategy.rst new file mode 100644 index 0000000..8208c6d --- /dev/null +++ b/docs-rst/concepts/strategy.rst @@ -0,0 +1,20 @@ +Types +===== + +.. _strategy: + +**strategy** ``((``\ ```modelet_set`` `__\ ``*``\ `modelet `__\ ``) >``\ **``$o``**\ ``)`` +-------------------------------------------------------------------------------------------------------------------------------------- + +A succession of `exertions `__ of `engines `__ +connects `modelets `__. `Strategies <#strategy>`__ +are transitive. + +- Must respect engine `requirements `__ +- Matches `modelet `__ *phenomenon* semantics to physical + reality + + - e.g. “on the living room table” to coordinates + +Source: ``transitive-strategies.tff`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/docs-rst/concepts/template.rst b/docs-rst/concepts/template.rst new file mode 100644 index 0000000..5c7d2b8 --- /dev/null +++ b/docs-rst/concepts/template.rst @@ -0,0 +1,81 @@ +Types +===== + +.. _template: + +**template** ``$tType`` +----------------------- + +Describes the features that a single `modelet `__ should +have for an `engine `__ to accept it as input. + +- a semantic function signature +- `properties `__ and `requirements `__ of + `modelets `__ ###### Source: ``engines-and-modelets.tff`` + +.. _template_set: + +**template_set** ``$tType`` +--------------------------- + +Some particular set of `templates <#template>`__ which describe the +inputs to an `engine `__. !!! example - {t1, t2, t3} - {t2} - +{} ###### Source: ``engines-and-modelets.tff`` + +Relations +========= + +.. _template_has_concept_requirement: + +**template_has_concept_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```concept`` `__\ ``)`` +-------------------------------------------------------------------------------------------------------------------- + +The `concept `__ symbolizing the *phenomenon class* of a +`template `__. ###### Source: ``engines-and-modelets.tff`` + +.. _template_formalism_requirement: + +**template_formalism_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```formalism`` `__\ ``)`` +---------------------------------------------------------------------------------------------------------------------- + +The `formalism `__ this `template <#template>`__ expects +the *phenomenon* to be described by. ###### Source: +``engines-and-templates.tff`` + +.. _template_has_location_requirement: + +**template_has_location_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```spacetime_point`` `__\ ``)`` +------------------------------------------------------------------------------------------------------------------------------------- + +The time and spatial location a `template <#template>`__ refers to. A +`template `__ may have a specific temporal scope or expect +an observation at a specific +```spacetime_point`` `__. ###### Source: +``engines-and-modelets.tff`` + +.. _template_has_extent_requirement: + +**template_has_extent_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```extent`` `__\ ``)`` +----------------------------------------------------------------------------------------------------------------- + +The time and spatial `extent `__ a `template <#template>`__ +covers. A `template <#template>`__ may expect an area/volume/duration of +reference. ###### Source: ``engines-and-modelets.tff`` + +.. _template_has_creator_requirement: + +**template_has_creator_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```engine`` `__\ ``)`` +------------------------------------------------------------------------------------------------------------------ + +The `engine `__ a `template <#template>`__ requires a +`modelet `__ to have been created by. ###### Source: +``engines-and-modelets.tff`` + +.. _is_in_template_set: + +**is_in_template_set** ``((``\ ```template`` <#template>`__\ ``*``\ ```template_set`` <#template_set>`__\ ``) >``\ **``$o``**\ ``)`` +------------------------------------------------------------------------------------------------------------------------------------ + +Check if a `template <#template>`__ is a member of a +`template_set <#template_set>`__. ###### Source: +``engines-and-modelets.tff`` diff --git a/docs-rst/index.rst b/docs-rst/index.rst new file mode 100644 index 0000000..6542de7 --- /dev/null +++ b/docs-rst/index.rst @@ -0,0 +1 @@ +–8<– “README.rst” diff --git a/docs-rst/packages/index.rst b/docs-rst/packages/index.rst new file mode 100644 index 0000000..1c81451 --- /dev/null +++ b/docs-rst/packages/index.rst @@ -0,0 +1,2 @@ +Understanding Packages +====================== diff --git a/docs-rst/usage/index.rst b/docs-rst/usage/index.rst new file mode 100644 index 0000000..1ea03f5 --- /dev/null +++ b/docs-rst/usage/index.rst @@ -0,0 +1,13 @@ +Usage and Installation +====================== + +The ``TFF`` models and tests can be run using the `latest +release `__ +or ``master`` branch of the +`Vampire `__ theorem prover. + +If you want to run the ``THF`` models, you need to either install the +`LEO-III `__ theorem prover or +build the Vampire ``hol`` branch from source using these +`instructions `__. +Make sure to add the ``-DCMAKE_BUILD_HOL=ON`` flag. From 5486b009cbe9e5deb9651d7230f5060331a75c7c Mon Sep 17 00:00:00 2001 From: Rockjack00 Date: Tue, 1 Jul 2025 17:26:12 +0200 Subject: [PATCH 2/6] Added back axioms for properties being exerted by engines --- tff/model/properties.tff | 141 +++++++++++++++++++++++++++++---------- 1 file changed, 105 insertions(+), 36 deletions(-) diff --git a/tff/model/properties.tff b/tff/model/properties.tff index e2682b7..e2dc5dd 100644 --- a/tff/model/properties.tff +++ b/tff/model/properties.tff @@ -34,8 +34,8 @@ tff(decl_property_of_e, type, engine_has_property: (engine * property) > $o). % Engine outputs have properties -tff(decl_engine_output_properties, type, - output_property_of_engine: engine > property). +tff(decl_engine_imparts_output_properties, type, + engine_imparts_output_property: (engine * property) > $o). % Templates have requirements in terms of properties tff(decl_templates_have_requirements, type, @@ -94,25 +94,83 @@ tff(formally_equivalent, axiom, ) ). +% % Modelets and Templates can have matching profiles +% tff(axiom_modelet_matches_template, axiom, +% ! [M: modelet, T: template]: +% ( +% ( +% formally_equivalent(T, M) +% & +% ! [R: requirement]: +% ( +% is_part_of(R, T) +% => +% ? [P: property]: +% ( +% modelet_has_property(M, P) % match modelet to property +% & +% (datatype_of_requirement(R) = datatype_of_property(P)) % property has correct correct data format/type for requirement +% & +% is_permissible(R, has_value(P)) % ensure that the property's value is permissible +% ) +% ) +% ) +% => +% inputs_match(M, T) +% ) +% ). + + + +tff(property_meets_requirement_decl, type, + property_meets_requirement : (property * requirement) > $o +). + +tff(axiom_property_meets_requirement, axiom, + ! [P: property, R: requirement]: + ( + ( + (datatype_of_requirement(R) = datatype_of_property(P)) % property has correct correct data format/type for requirement + & + is_permissible(R, has_value(P)) % ensure that the property's value is permissible + ) + => + property_meets_requirement(P, R) + ) +). + + +tff(modelet_meets_requirement_decl, type, + modelet_meets_requirement : (modelet * requirement) > $o +). + +tff(axiom_modelet_meets_requirement, axiom, + ! [M : modelet, R : requirement, P: property]: + ( + ( + modelet_has_property(M, P) % match modelet to property + & + property_meets_requirement(P, R) + ) + => + modelet_meets_requirement(M, R) + ) +). + + + % Modelets and Templates can have matching profiles -tff(axiom_modelet_matches_template, axiom, +tff(new_axiom_modelet_matches_template, axiom, ! [M: modelet, T: template]: ( ( formally_equivalent(T, M) & - ! [R: requirement]: + ![R: requirement] : ( is_part_of(R, T) => - ? [P: property]: - ( - modelet_has_property(M, P) % match modelet to property - & - (datatype_of_requirement(R) = datatype_of_property(P)) % property has correct correct data format/type for requirement - & - is_permissible(R, has_value(P)) % ensure that the property's value is permissible - ) + modelet_meets_requirement(M, R) ) ) => @@ -120,6 +178,21 @@ tff(axiom_modelet_matches_template, axiom, ) ). + + + + + + + + + + + + + + + % Modelet sets match template sets if all their templates have a corresponding modelet with matching inputs inputs_match(M, T) %interfaces_match(MS, TS) @@ -146,27 +219,23 @@ tff(axiom_modelet_sets_matches_template_sets, axiom, % Engine outputs have properties -%tff(exert_creates, axiom, -% ! [Minput: modelet_set, E: engine]: -% ( -% exertable(E, Minput) -% => -% ? [Moutput: modelet]: -% ( -% exert(E, Minput, Moutput) -% & -% ! [P: property]: -% ( -% ( -% ~engine_has_property(E, P) -% | -% ( -% engine_has_property(E, P) -% & -% modelet_has_property(Moutput, P) -% ) -% ) -% ) -% ) -% ) -%). +tff(exert_creates, axiom, + ! [E: engine, MS: modelet_set, M: modelet, P: property]: + ( + ( + exertable(E, MS) + & + exert(E, MS) = M + & + engine_imparts_output_property(E, P) + ) + => + modelet_has_property(M, P) + ) +). + + + +% Modelets that are output from engines only have the properties imparted by +% their engines +% TODO: this is a strong assumption, do we really want it? From 71eaf5da618ee234f554a9c2f92f7bcac732bd26 Mon Sep 17 00:00:00 2001 From: Alex Gabriel Date: Tue, 16 Sep 2025 13:01:16 +0200 Subject: [PATCH 3/6] renamed docs folder again --- {docs-md => docs}/README.md | 0 {docs-md => docs}/assets/images/EU_funded_en.jpg | Bin {docs-md => docs}/assets/images/FHG-logo.png | Bin {docs-md => docs}/assets/images/IMR-logo.png | Bin {docs-md => docs}/assets/images/PAL-logo.png | Bin {docs-md => docs}/assets/images/TUD-logo.png | Bin {docs-md => docs}/assets/images/UPM-logo.png | Bin {docs-md => docs}/assets/images/URJC-logo.png | Bin .../assets/images/coresense-logo-reverse.png | Bin {docs-md => docs}/assets/images/coresense-logo.png | Bin .../images/cropped-Coresense-Site-Logo-32x32.png | Bin {docs-md => docs}/assets/images/tudelft-logo.png | Bin {docs-md => docs}/concepts/agent.md | 0 {docs-md => docs}/concepts/concept.md | 0 {docs-md => docs}/concepts/datatype.md | 0 {docs-md => docs}/concepts/engine.md | 0 {docs-md => docs}/concepts/exertion.md | 0 {docs-md => docs}/concepts/extent.md | 0 {docs-md => docs}/concepts/formalism.md | 0 {docs-md => docs}/concepts/index.md | 0 {docs-md => docs}/concepts/modelet.md | 0 {docs-md => docs}/concepts/origin.md | 0 {docs-md => docs}/concepts/phenomenon.md | 0 {docs-md => docs}/concepts/property.md | 0 {docs-md => docs}/concepts/representation_class.md | 0 {docs-md => docs}/concepts/requirement.md | 0 {docs-md => docs}/concepts/spacetime_point.md | 0 {docs-md => docs}/concepts/strategy.md | 0 {docs-md => docs}/concepts/template.md | 0 {docs-md => docs}/documentation-instructions.md | 0 {docs-md => docs}/index.md | 0 {docs-md => docs}/overrides/partials/footer.html | 0 {docs-md => docs}/packages/index.md | 0 {docs-md => docs}/requirements.txt | 0 {docs-md => docs}/stylesheets/extra.css | 0 {docs-md => docs}/usage/index.md | 0 36 files changed, 0 insertions(+), 0 deletions(-) rename {docs-md => docs}/README.md (100%) rename {docs-md => docs}/assets/images/EU_funded_en.jpg (100%) rename {docs-md => docs}/assets/images/FHG-logo.png (100%) rename {docs-md => docs}/assets/images/IMR-logo.png (100%) rename {docs-md => docs}/assets/images/PAL-logo.png (100%) rename {docs-md => docs}/assets/images/TUD-logo.png (100%) rename {docs-md => docs}/assets/images/UPM-logo.png (100%) rename {docs-md => docs}/assets/images/URJC-logo.png (100%) rename {docs-md => docs}/assets/images/coresense-logo-reverse.png (100%) rename {docs-md => docs}/assets/images/coresense-logo.png (100%) rename {docs-md => docs}/assets/images/cropped-Coresense-Site-Logo-32x32.png (100%) rename {docs-md => docs}/assets/images/tudelft-logo.png (100%) rename {docs-md => docs}/concepts/agent.md (100%) rename {docs-md => docs}/concepts/concept.md (100%) rename {docs-md => docs}/concepts/datatype.md (100%) rename {docs-md => docs}/concepts/engine.md (100%) rename {docs-md => docs}/concepts/exertion.md (100%) rename {docs-md => docs}/concepts/extent.md (100%) rename {docs-md => docs}/concepts/formalism.md (100%) rename {docs-md => docs}/concepts/index.md (100%) rename {docs-md => docs}/concepts/modelet.md (100%) rename {docs-md => docs}/concepts/origin.md (100%) rename {docs-md => docs}/concepts/phenomenon.md (100%) rename {docs-md => docs}/concepts/property.md (100%) rename {docs-md => docs}/concepts/representation_class.md (100%) rename {docs-md => docs}/concepts/requirement.md (100%) rename {docs-md => docs}/concepts/spacetime_point.md (100%) rename {docs-md => docs}/concepts/strategy.md (100%) rename {docs-md => docs}/concepts/template.md (100%) rename {docs-md => docs}/documentation-instructions.md (100%) rename {docs-md => docs}/index.md (100%) rename {docs-md => docs}/overrides/partials/footer.html (100%) rename {docs-md => docs}/packages/index.md (100%) rename {docs-md => docs}/requirements.txt (100%) rename {docs-md => docs}/stylesheets/extra.css (100%) rename {docs-md => docs}/usage/index.md (100%) diff --git a/docs-md/README.md b/docs/README.md similarity index 100% rename from docs-md/README.md rename to docs/README.md diff --git a/docs-md/assets/images/EU_funded_en.jpg b/docs/assets/images/EU_funded_en.jpg similarity index 100% rename from docs-md/assets/images/EU_funded_en.jpg rename to docs/assets/images/EU_funded_en.jpg diff --git a/docs-md/assets/images/FHG-logo.png b/docs/assets/images/FHG-logo.png similarity index 100% rename from docs-md/assets/images/FHG-logo.png rename to docs/assets/images/FHG-logo.png diff --git a/docs-md/assets/images/IMR-logo.png b/docs/assets/images/IMR-logo.png similarity index 100% rename from docs-md/assets/images/IMR-logo.png rename to docs/assets/images/IMR-logo.png diff --git a/docs-md/assets/images/PAL-logo.png b/docs/assets/images/PAL-logo.png similarity index 100% rename from docs-md/assets/images/PAL-logo.png rename to docs/assets/images/PAL-logo.png diff --git a/docs-md/assets/images/TUD-logo.png b/docs/assets/images/TUD-logo.png similarity index 100% rename from docs-md/assets/images/TUD-logo.png rename to docs/assets/images/TUD-logo.png diff --git a/docs-md/assets/images/UPM-logo.png b/docs/assets/images/UPM-logo.png similarity index 100% rename from docs-md/assets/images/UPM-logo.png rename to docs/assets/images/UPM-logo.png diff --git a/docs-md/assets/images/URJC-logo.png b/docs/assets/images/URJC-logo.png similarity index 100% rename from docs-md/assets/images/URJC-logo.png rename to docs/assets/images/URJC-logo.png diff --git a/docs-md/assets/images/coresense-logo-reverse.png b/docs/assets/images/coresense-logo-reverse.png similarity index 100% rename from docs-md/assets/images/coresense-logo-reverse.png rename to docs/assets/images/coresense-logo-reverse.png diff --git a/docs-md/assets/images/coresense-logo.png b/docs/assets/images/coresense-logo.png similarity index 100% rename from docs-md/assets/images/coresense-logo.png rename to docs/assets/images/coresense-logo.png diff --git a/docs-md/assets/images/cropped-Coresense-Site-Logo-32x32.png b/docs/assets/images/cropped-Coresense-Site-Logo-32x32.png similarity index 100% rename from docs-md/assets/images/cropped-Coresense-Site-Logo-32x32.png rename to docs/assets/images/cropped-Coresense-Site-Logo-32x32.png diff --git a/docs-md/assets/images/tudelft-logo.png b/docs/assets/images/tudelft-logo.png similarity index 100% rename from docs-md/assets/images/tudelft-logo.png rename to docs/assets/images/tudelft-logo.png diff --git a/docs-md/concepts/agent.md b/docs/concepts/agent.md similarity index 100% rename from docs-md/concepts/agent.md rename to docs/concepts/agent.md diff --git a/docs-md/concepts/concept.md b/docs/concepts/concept.md similarity index 100% rename from docs-md/concepts/concept.md rename to docs/concepts/concept.md diff --git a/docs-md/concepts/datatype.md b/docs/concepts/datatype.md similarity index 100% rename from docs-md/concepts/datatype.md rename to docs/concepts/datatype.md diff --git a/docs-md/concepts/engine.md b/docs/concepts/engine.md similarity index 100% rename from docs-md/concepts/engine.md rename to docs/concepts/engine.md diff --git a/docs-md/concepts/exertion.md b/docs/concepts/exertion.md similarity index 100% rename from docs-md/concepts/exertion.md rename to docs/concepts/exertion.md diff --git a/docs-md/concepts/extent.md b/docs/concepts/extent.md similarity index 100% rename from docs-md/concepts/extent.md rename to docs/concepts/extent.md diff --git a/docs-md/concepts/formalism.md b/docs/concepts/formalism.md similarity index 100% rename from docs-md/concepts/formalism.md rename to docs/concepts/formalism.md diff --git a/docs-md/concepts/index.md b/docs/concepts/index.md similarity index 100% rename from docs-md/concepts/index.md rename to docs/concepts/index.md diff --git a/docs-md/concepts/modelet.md b/docs/concepts/modelet.md similarity index 100% rename from docs-md/concepts/modelet.md rename to docs/concepts/modelet.md diff --git a/docs-md/concepts/origin.md b/docs/concepts/origin.md similarity index 100% rename from docs-md/concepts/origin.md rename to docs/concepts/origin.md diff --git a/docs-md/concepts/phenomenon.md b/docs/concepts/phenomenon.md similarity index 100% rename from docs-md/concepts/phenomenon.md rename to docs/concepts/phenomenon.md diff --git a/docs-md/concepts/property.md b/docs/concepts/property.md similarity index 100% rename from docs-md/concepts/property.md rename to docs/concepts/property.md diff --git a/docs-md/concepts/representation_class.md b/docs/concepts/representation_class.md similarity index 100% rename from docs-md/concepts/representation_class.md rename to docs/concepts/representation_class.md diff --git a/docs-md/concepts/requirement.md b/docs/concepts/requirement.md similarity index 100% rename from docs-md/concepts/requirement.md rename to docs/concepts/requirement.md diff --git a/docs-md/concepts/spacetime_point.md b/docs/concepts/spacetime_point.md similarity index 100% rename from docs-md/concepts/spacetime_point.md rename to docs/concepts/spacetime_point.md diff --git a/docs-md/concepts/strategy.md b/docs/concepts/strategy.md similarity index 100% rename from docs-md/concepts/strategy.md rename to docs/concepts/strategy.md diff --git a/docs-md/concepts/template.md b/docs/concepts/template.md similarity index 100% rename from docs-md/concepts/template.md rename to docs/concepts/template.md diff --git a/docs-md/documentation-instructions.md b/docs/documentation-instructions.md similarity index 100% rename from docs-md/documentation-instructions.md rename to docs/documentation-instructions.md diff --git a/docs-md/index.md b/docs/index.md similarity index 100% rename from docs-md/index.md rename to docs/index.md diff --git a/docs-md/overrides/partials/footer.html b/docs/overrides/partials/footer.html similarity index 100% rename from docs-md/overrides/partials/footer.html rename to docs/overrides/partials/footer.html diff --git a/docs-md/packages/index.md b/docs/packages/index.md similarity index 100% rename from docs-md/packages/index.md rename to docs/packages/index.md diff --git a/docs-md/requirements.txt b/docs/requirements.txt similarity index 100% rename from docs-md/requirements.txt rename to docs/requirements.txt diff --git a/docs-md/stylesheets/extra.css b/docs/stylesheets/extra.css similarity index 100% rename from docs-md/stylesheets/extra.css rename to docs/stylesheets/extra.css diff --git a/docs-md/usage/index.md b/docs/usage/index.md similarity index 100% rename from docs-md/usage/index.md rename to docs/usage/index.md From f0d90b655c4cc96b3bb5bfe1be5efdd7a953798e Mon Sep 17 00:00:00 2001 From: Alex Gabriel Date: Tue, 16 Sep 2025 13:32:52 +0200 Subject: [PATCH 4/6] removed rst docs --- docs-rst/concepts/agent.rst | 16 -- docs-rst/concepts/concept.rst | 16 -- docs-rst/concepts/datatype.rst | 191 --------------------- docs-rst/concepts/engine.rst | 82 --------- docs-rst/concepts/exertion.rst | 68 -------- docs-rst/concepts/extent.rst | 46 ----- docs-rst/concepts/formalism.rst | 22 --- docs-rst/concepts/index.rst | 106 ------------ docs-rst/concepts/modelet.rst | 106 ------------ docs-rst/concepts/origin.rst | 21 --- docs-rst/concepts/phenomenon.rst | 17 -- docs-rst/concepts/property.rst | 49 ------ docs-rst/concepts/representation_class.rst | 11 -- docs-rst/concepts/requirement.rst | 36 ---- docs-rst/concepts/spacetime_point.rst | 50 ------ docs-rst/concepts/strategy.rst | 20 --- docs-rst/concepts/template.rst | 81 --------- docs-rst/index.rst | 1 - docs-rst/packages/index.rst | 2 - docs-rst/usage/index.rst | 13 -- 20 files changed, 954 deletions(-) delete mode 100644 docs-rst/concepts/agent.rst delete mode 100644 docs-rst/concepts/concept.rst delete mode 100644 docs-rst/concepts/datatype.rst delete mode 100644 docs-rst/concepts/engine.rst delete mode 100644 docs-rst/concepts/exertion.rst delete mode 100644 docs-rst/concepts/extent.rst delete mode 100644 docs-rst/concepts/formalism.rst delete mode 100644 docs-rst/concepts/index.rst delete mode 100644 docs-rst/concepts/modelet.rst delete mode 100644 docs-rst/concepts/origin.rst delete mode 100644 docs-rst/concepts/phenomenon.rst delete mode 100644 docs-rst/concepts/property.rst delete mode 100644 docs-rst/concepts/representation_class.rst delete mode 100644 docs-rst/concepts/requirement.rst delete mode 100644 docs-rst/concepts/spacetime_point.rst delete mode 100644 docs-rst/concepts/strategy.rst delete mode 100644 docs-rst/concepts/template.rst delete mode 100644 docs-rst/index.rst delete mode 100644 docs-rst/packages/index.rst delete mode 100644 docs-rst/usage/index.rst diff --git a/docs-rst/concepts/agent.rst b/docs-rst/concepts/agent.rst deleted file mode 100644 index 73949c6..0000000 --- a/docs-rst/concepts/agent.rst +++ /dev/null @@ -1,16 +0,0 @@ -Types -===== - -.. _agent: - -**agent** ``$tType`` --------------------- - -A **CoreSense** agent which may posess `engines `__ and -`modelets `__. - -!!! warning “Unimplemented” To be introduced later, as collective -awareness is considered. - -Source: ``fundamental-concepts.tff`` -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/docs-rst/concepts/concept.rst b/docs-rst/concepts/concept.rst deleted file mode 100644 index 0a50989..0000000 --- a/docs-rst/concepts/concept.rst +++ /dev/null @@ -1,16 +0,0 @@ -Types -===== - -.. _concept: - -**concept** ``$tType`` ----------------------- - -An instance of a class of `phenomenon `__ in the agent’s -world model. - -A `concept <#concept>`__ is a `property `__ of a -`modelet `__. - -!!! example - chair - dog - the color pink - sunrise ###### Source: -``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/datatype.rst b/docs-rst/concepts/datatype.rst deleted file mode 100644 index 9c1c75d..0000000 --- a/docs-rst/concepts/datatype.rst +++ /dev/null @@ -1,191 +0,0 @@ -Types -===== - -.. _datatype: - -**datatype** ``$tType`` ------------------------ - -A precise information encoding that is taken as granted. As the name -suggests, the fundamental types of data considered. - -!!! example - real number - uint8 - pixel ###### Source: -``fundamental-concepts.tff`` - -ROS 2 Interface builtins -======================== - -ROS 2 interfaces (messages, services, and actions) are -`formalisms `__ constructed from semantically named -builtin `datatypes <#datatype>`__ and arrays of these builtins. See the -ROS 2 -`documentation `__ -for more details. - -!!! important These individuals are not associated with a particular -semantic label. The intention (WIP) is to match a particular -`datatype <#datatype>`__ (the ``fieldtype``) and a -`concept `__ (the ``fieldname``) in some -`formalism `__ representing the ROS 2 interface. - -.. _ros2-msg-bool: - -**‘ROS2.msg.Bool’** ```datatype`` <#datatype>`__ ------------------------------------------------- - -The builtin ``bool`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-byte: - -**‘ROS2.msg.Byte’** ```datatype`` <#datatype>`__ ------------------------------------------------- - -The builtin ``byte`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-char: - -**‘ROS2.msg.Char’** ```datatype`` <#datatype>`__ ------------------------------------------------- - -The builtin ``char`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-float32: - -**‘ROS2.msg.Float32’** ```datatype`` <#datatype>`__ ---------------------------------------------------- - -The builtin ``float32`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-float64: - -**‘ROS2.msg.Float64’** ```datatype`` <#datatype>`__ ---------------------------------------------------- - -The builtin ``float64`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-int8: - -**‘ROS2.msg.Int8’** ```datatype`` <#datatype>`__ ------------------------------------------------- - -The builtin ``int8`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-uint8: - -**‘ROS2.msg.Uint8’** ```datatype`` <#datatype>`__ -------------------------------------------------- - -The builtin ``uint8`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-int16: - -**‘ROS2.msg.Int16’** ```datatype`` <#datatype>`__ -------------------------------------------------- - -The builtin ``int16`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-uint16: - -**‘ROS2.msg.Uint16’** ```datatype`` <#datatype>`__ --------------------------------------------------- - -The builtin ``uin16`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-int32: - -**‘ROS2.msg.Int32’** ```datatype`` <#datatype>`__ -------------------------------------------------- - -The builtin ``int32`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-uint32: - -**‘ROS2.msg.Uint32’** ```datatype`` <#datatype>`__ --------------------------------------------------- - -The builtin ``uint32`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-int64: - -**‘ROS2.msg.Int64’** ```datatype`` <#datatype>`__ -------------------------------------------------- - -The builtin ``int64`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-uint64: - -**‘ROS2.msg.Uint64’** ```datatype`` <#datatype>`__ --------------------------------------------------- - -The builtin ``uint64`` field type of a ROS 2 interface. ###### Source: -``datatypes.tff`` - -.. _ros2-msg-string: - -**‘ROS2.msg.String’** ```datatype`` <#datatype>`__ --------------------------------------------------- - -The builtin (unbounded) ``string`` field type of a ROS 2 interface. -These strings use 8-bit characters. ###### Source: ``datatypes.tff`` - -.. _ros2-msg-wstring: - -**‘ROS2.msg.Wstring’** ```datatype`` <#datatype>`__ ---------------------------------------------------- - -The builtin ``wstring`` field type of a ROS 2 interface. These strings -use 16-bit characters. ###### Source: ``datatypes.tff`` - -ROS 2 Interface arrays -====================== - -ROS 2 interfaces support arrays of builtins, optionally with a fixed or -bounded size. !!! warning Sizes of array datatypes are assumed to be -natural numbers. This is **NOT** enforced by the type checker or logic. - -.. _ros2-msg-bounded-string: - -**‘ROS2.msg.BoundedString’** ``(``\ **``$int``**\ ``>``\ ```datatype`` <#datatype>`__\ ``)`` --------------------------------------------------------------------------------------------- - -A bounded ``string<=n`` field type of a ROS 2 interface. ``n`` is a -natural number. ###### Source: ``datatypes.tff`` - -.. _ros2-msg-unbounded-dynamic-array: - -**‘ROS2.msg.UnboundedDynamicArray’** ``(``\ ```datatype`` <#datatype>`__\ ``>``\ ```datatype`` <#datatype>`__\ ``)`` --------------------------------------------------------------------------------------------------------------------- - -An array of any builtin with an unbouned size field type in a ROS 2 -interface. !!! example - ``char[]`` - ``float32[]`` ###### Source: -``datatypes.tff`` - -.. _ros2-msg-bounded-dynamic-array: - -**‘ROS2.msg.BoundedDynamicArray’** ``((``\ ```datatype`` <#datatype>`__\ ``*``\ **``$int``**\ ``) >``\ ```datatype`` <#datatype>`__\ ``)`` ------------------------------------------------------------------------------------------------------------------------------------------- - -A dynamic array of any builtin with a bounded size field type in a ROS 2 -interface. The size must be a natural number. !!! example - -``char[<=5]`` - ``float32[<=4]`` ###### Source: ``datatypes.tff`` - -.. _ros2-msg-static-array: - -**‘ROS2.msg.StaticArray’** ``((``\ ```datatype`` <#datatype>`__\ ``*``\ **``$int``**\ ``) >``\ ```datatype`` <#datatype>`__\ ``)`` ----------------------------------------------------------------------------------------------------------------------------------- - -A static array of any builtin with a fixed size field type in a ROS 2 -interface. The size must be a natural number. !!! example - ``char[5]`` -- ``float32[4]`` ###### Source: ``datatypes.tff`` diff --git a/docs-rst/concepts/engine.rst b/docs-rst/concepts/engine.rst deleted file mode 100644 index fb3e8b9..0000000 --- a/docs-rst/concepts/engine.rst +++ /dev/null @@ -1,82 +0,0 @@ -Types -===== - -.. _engine: - -**engine** ``$tType`` ---------------------- - -Does work within a **CoreSense** `agent `__ to produce -`modelets `__. - -- Takes multiple `modelets `__ as an input - `modelet_set `__ -- Uses semantic information to identify valid input modelet - `formalisms `__ - - - semantics could be external (part of the type definition) or - internal (modeled within the `modelet `__ itself) - -- Produces one output `modelet `__ - - - May or may not impart semantic meaning to the output - `modelet `__ - - May (re)define the output modelet `origin `__, - `concept `__, or characteristics - -- Has `exertion `__ characteristics - - - e.g. time delay, resource usage, power consumption - -!!! example - DroneStateEngine (see tff/tests/test-wind-estimation.tff) -- Input Model: - Modelet - formalism: IMU.msg - modelled concept: -inertia - Modelet - formalism: NavSatFix.msg - modelled concept: -geolocation - Output Modelet: - modelet - formalism: DroneState.msg - -modelled concept: drone_state ###### Source: -``engines-and-modelets.tff`` - -Relations -========= - -.. _interface_of: - -**interface_of** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```template_set`` `__\ ``)`` ---------------------------------------------------------------------------------------------------------------- - -An `engine <#engine>`__ requires a set of input -`modelets `__ which matches the -`template_set `__. ###### Source: -``engines-and-modelets.tff`` - -.. _output_modelet_formalism: - -**output_modelet_formalism** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```formalism`` `__\ ``)`` ------------------------------------------------------------------------------------------------------------- - -The `formalism `__ of an `engine <#engine>`__ output -`modelet `__. ###### Source: ``engines-and-modelets.tff`` - -.. _is_output_modelet_concept: - -**is_output_modelet_concept** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```phenomenon`` `__\ ``)`` ---------------------------------------------------------------------------------------------------------------- - -The `concept `__ of an `engine <#engine>`__ output -`modelet `__. ###### Source: ``engines-and-modelets.tff`` - -.. _output_property_of_e: - -**output_property_of_engine** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```property`` `__\ ``)`` ------------------------------------------------------------------------------------------------------------ - -The `property `__ an `engine <#engine>`__ imparts on its -output `modelet `__. ###### Source: ``properties.tff`` - -.. _engine_imparts_representation_class: - -**engine_imparts_representation_class** ``(``\ ```engine`` <#engine>`__\ ``>``\ ```representation_class`` `__\ ``)`` ---------------------------------------------------------------------------------------------------------------------------------------------- - -The `representation_class `__ an -`engine <#engine>`__ imparts on its output `modelet `__. -###### Source: ``engines-and-modelets.tff`` diff --git a/docs-rst/concepts/exertion.rst b/docs-rst/concepts/exertion.rst deleted file mode 100644 index cc5637c..0000000 --- a/docs-rst/concepts/exertion.rst +++ /dev/null @@ -1,68 +0,0 @@ -Relations -========= - -**inputs_match** ``((``\ ```modelet`` `__\ ``*``\ ```template`` `__\ ``) >``\ \*\*\ ``$o``\ \*\ ``)`` { #inputs_match data-toc-label=‘inputs_match’ } ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - -Check if a `modelet `__ matches a -`template `__. - -- Check if they are `formally equivalent <#formally_equivalent>`__ -- Check if the `modelet `__ contains *permissible* values - for each of the `properties `__ of - `requirements `__ of the `template `__. - ###### Source: ``engines-and-modelets.tff``, ``properties.tff`` - -.. _formally_equivalent: - -**formally_equivalent** ``((``\ ```template`` `__\ ``*``\ ```modelet`` `__\ ``) >``\ **``$o``**\ ``)`` -------------------------------------------------------------------------------------------------------------------------------- - -A `template `__ and a `modelet `__ share the -same *phenomenon* and `formalism `__. ###### Source: -``properties.tff`` - -.. _interfaces_match: - -**interfaces_match** ``((``\ ```modelet_set`` `__\ ``*``\ ```template_set`` `__\ ``) >``\ **``$o``**\ ``)`` -------------------------------------------------------------------------------------------------------------------------------------------------------------- - -Check if all of the `templates `__ in the -`template_set `__ have a corresponding -`modelet `__ in the `modelet_set `__ -with matching profile. - -- Check if they are `formally equivalent <#formally_equivalent>`__ -- Check if their `inputs match <#inputs_match>`__ ###### Source: - ``engines-and-modelets.tff``, ``properties.tff`` - -.. _exert: - -**exert** ``((``\ ```engine`` `__\ ``*``\ ```modelet_set`` `__\ ``*``\ ```modelet`` `__\ ``) >``\ **``$o``**\ ``)`` ------------------------------------------------------------------------------------------------------------------------------------------------------------------- - -Exert an `engine `__ on a -`modelet_set `__ to produce an output -`modelet `__. ###### Source: ``engines-and-modelets.tff`` - -.. _exertable: - -**exertable** ``((``\ ```modelet_set`` `__\ ``*``\ ```engine`` `__\ ``) >``\ **``$o``**\ ``)`` ---------------------------------------------------------------------------------------------------------------------------------- - -A `modelet_set `__ can be exerted by an -`engine `__ iff their `interfaces -match <#interfaces_match>`__. ###### Source: -``engines-and-modelets.tff`` - -.. raw:: html - - diff --git a/docs-rst/concepts/extent.rst b/docs-rst/concepts/extent.rst deleted file mode 100644 index e0ce89f..0000000 --- a/docs-rst/concepts/extent.rst +++ /dev/null @@ -1,46 +0,0 @@ -Types -===== - -.. _extent: - -**extent** ``$tType`` ---------------------- - -A 4-dimensional size (3 space, 1 time). !!! note Not to be confused with -a 4-dimentional ```spacetime_point`` `__. ###### -Source: ``fundamental-concepts.tff`` - -Relations -========= - -.. _extent_width: - -**extent_width** ``(``\ ```extent`` <#extent>`__\ ``>``\ **``$real``**\ ``)`` ------------------------------------------------------------------------------ - -The width of an (```extent`` <#extent>`__). ###### Source: -``fundamental-concepts.tff`` - -.. _extent_height: - -**extent_height** ``(``\ ```extent`` <#extent>`__\ ``>``\ **``$real``**\ ``)`` ------------------------------------------------------------------------------- - -The height of an (```extent`` <#extent>`__). ###### Source: -``fundamental-concepts.tff`` - -.. _extent_depth: - -**extent_depth** ``(``\ ```extent`` <#extent>`__\ ``>``\ **``$real``**\ ``)`` ------------------------------------------------------------------------------ - -The depth of an (```extent`` <#extent>`__). ###### Source: -``fundamental-concepts.tff`` - -.. _extent_duration: - -**extent_duration** ``(``\ ```extent`` <#extent>`__\ ``>``\ **``$real``**\ ``)`` --------------------------------------------------------------------------------- - -The duration of an (```extent`` <#extent>`__). ###### Source: -``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/formalism.rst b/docs-rst/concepts/formalism.rst deleted file mode 100644 index 6f91001..0000000 --- a/docs-rst/concepts/formalism.rst +++ /dev/null @@ -1,22 +0,0 @@ -Types -===== - -.. _formalism: - -**formalism** ``$tType`` ------------------------- - -The language and structure in which a `phenomenon `__ -could be described. Methods used to express `modelets `__; -class in the *Data Model*. - -- The information structure used to capture the - `concept `__ and `origin `__ -- Highlights some aspects of the *phenomenon* while hiding others -- Defines `engine `__ I/O compatibility and usability with - other models - -New `formalism <#formalism>`__ could be defined or old ones modified. - -!!! example - ROS message - Image format - Language grammar ###### -Source: Understanding presentation diff --git a/docs-rst/concepts/index.rst b/docs-rst/concepts/index.rst deleted file mode 100644 index 35944af..0000000 --- a/docs-rst/concepts/index.rst +++ /dev/null @@ -1,106 +0,0 @@ -Concepts -======== - -!!! danger These concepts are still in development and high susceptible -to change. Use the provided terms, definitions, and types with caution. - -The **Understanding System** (a.k.a Understanding Core) is a CoreSense -module for generating understanding within a *CoreSense* agent. The main -idea is to: !!! quote “Intuition” Find *strategies* of **Engine** -*exertions* to **create** required **Modelets**. - -!!! question “TODO” Add a map of the concepts or something more elegant -here… We should also include the triangle of meaning. - -Types ------ - -`agent `__ -~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/agent.rst:3:3” - -`datatype `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/datatype.rst:3:3” - -`engine `__ -~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/engine.rst:3:3” - -`exertion `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/exertion.rst:3:3” - -`extent `__ -~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/extent.rst:3:3” - -`formalism `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/formalism.rst:3:3” - -`modelet `__ -~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/modelet.rst:3:3” - -`modelet_set `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/modelet.rst:13:13” - -`origin `__ -~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/origin.rst:3:3” - -`phenomenon `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/phenomenon.rst:3:4” - -`property `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/property.rst:3:3” - -`requirement `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/requirement.rst:3:3” - -`representation_class `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/representation_class.rst:3:3” - -`spacetime_point `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/spacetime_point.rst:3:3” - -`strategy `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/strategy.rst:3:3” - -`template `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/template.rst:3:4” - -`template_set `__ -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/template.rst:11:11” - -`concept `__ -~~~~~~~~~~~~~~~~~~~~~~~~ - -–8<– “docs/concepts/concept.rst:3:3” diff --git a/docs-rst/concepts/modelet.rst b/docs-rst/concepts/modelet.rst deleted file mode 100644 index 4307c55..0000000 --- a/docs-rst/concepts/modelet.rst +++ /dev/null @@ -1,106 +0,0 @@ -Types -===== - -.. _modelet: - -**modelet** ``$tType`` ----------------------- - -Models a `phenomenon `__ as the *thought* in the triangle -of meaning. All modelets describe an instance of a -`concept `__, have an `origin `__, and are -modeled in a specific `formalism `__. - -- `Concept `__: the *phenomenon* of the - `modelet <#modelet>`__, an instance of a class in the world model. -- `Origin `__: the agent’s perspective on the *phenomenon* -- `Formalism `__: the representation of the *phenomenon* - ###### Source: ``engines-and-modelets.tff`` - -.. _modelet_set: - -**modelet_set** ``$tType`` --------------------------- - -Some particular set of `modelets <#modelet>`__ which the has reasoner -assembled. Used to collect the inputs to an `engine `__. !!! -example - {m1, m2, m3} - {m2} - {} ###### Source: -``engines-and-modelets.tff`` - -Relations -========= - -.. _modelet_models_concept: - -**modelet_models_concept** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```phenomenon`` `__\ ``)`` --------------------------------------------------------------------------------------------------------------- - -The `phenomenon `__ symbolizing the *phenomenon* of a -`modelet `__. !!! question “TODO” rename from ‘concept’ to -something else. ###### Source: ``engines-and-modelets.tff`` - -.. _formalism_of_modelet: - -**formalism_of_modelet** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```formalism`` `__\ ``)`` ----------------------------------------------------------------------------------------------------------- - -The `formalism `__ used by a `modelet <#modelet>`__ to -describe the *phenomenon*. ###### Source: ``engines-and-modelets.tff`` - -.. _modelet_creation_date: - -**modelet_creation_date** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ **``$real``**\ ``)`` ----------------------------------------------------------------------------------------- - -The date a `modelet <#modelet>`__ was created. !!! question “TODO” The -date is represented as a ``$real`` but we don’t make any assumptions -about what that number represents. Unix time? time since last restart? -seconds? This may be solved by integration with ``spacetime_point``. -###### Source: ``engines-and-modelets.tff`` - -.. _modelet_has_location: - -**modelet_has_location** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```spacetime_point`` `__\ ``)`` ----------------------------------------------------------------------------------------------------------------------- - -The time and spatial location a `modelet <#modelet>`__ refers to. -`Modelets `__ may have a specific temporal scope or make an -observation at a specific ```spacetime_point`` `__. -###### Source: ``engines-and-modelets.tff`` - -.. _modelet_has_extent: - -**modelet_has_extent** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```extent`` `__\ ``)`` --------------------------------------------------------------------------------------------------- - -The time and spatial `extent `__ a `modelet <#modelet>`__ -refers to. `Modelets <#modelet>`__ may have an area/volume/duration of -reference. ###### Source: ``engines-and-modelets.tff`` - -.. _modelet_has_representation_class: - -**modelet_has_representation_class** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```representation_class`` `__\ ``)`` --------------------------------------------------------------------------------------------------------------------------------------------- - -The `representation_class `__ a -`modelet <#modelet>`__\ ’s relation to its parents has after being -created by an `engine `__. !!! question “TODO” This looks -like it will turn out to be HOL. ###### Source: -``engines-and-modelets.tff`` - -.. _modelet_has_creator: - -**modelet_has_creator** ``(``\ ```modelet`` <#modelet>`__\ ``>``\ ```engine`` `__\ ``)`` ---------------------------------------------------------------------------------------------------- - -The `engine `__ that created the `modelet <#modelet>`__. -###### Source: ``engines-and-modelets.tff`` - -.. _is_in_modelet_set: - -**is_in_modelet_set** ``((``\ ```modelet`` <#modelet>`__\ ``*``\ ```modelet_set`` <#modelet_set>`__\ ``) >``\ **``$o``**\ ``)`` -------------------------------------------------------------------------------------------------------------------------------- - -Check if a `modelet <#modelet>`__ is a member of a -`modelet_set <#modelet_set>`__. ###### Source: -``engines-and-modelets.tff`` diff --git a/docs-rst/concepts/origin.rst b/docs-rst/concepts/origin.rst deleted file mode 100644 index 5f78220..0000000 --- a/docs-rst/concepts/origin.rst +++ /dev/null @@ -1,21 +0,0 @@ -Types -===== - -.. _origin: - -**origin** ``$tType`` ---------------------- - -An agent’s perspective on the *phenomenon* captured in a particular -`modelet `__. - -- Observation is *situated* in time and space -- Measured with sensors that have certain characteristics and - limitations - - - (inferred) physical quality (e.g. distance inferred from delay) - - resolution and frame rate - - reflections and transparencies could be misinterpreted - -Source: Understanding presentation -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/docs-rst/concepts/phenomenon.rst b/docs-rst/concepts/phenomenon.rst deleted file mode 100644 index 561b4a3..0000000 --- a/docs-rst/concepts/phenomenon.rst +++ /dev/null @@ -1,17 +0,0 @@ -Types -===== - -.. _phenomenon: - -**phenomenon** ``$tType`` -------------------------- - -Some space or object or being or process in the real world that the -system represents using `modelets `__. - -- *Situated* in time and space -- May change over time -- Associated with a mission-dependent *meaning* - -!!! example - you - your office - your tea - your tea approaching room -temperature ###### Source: ``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/property.rst b/docs-rst/concepts/property.rst deleted file mode 100644 index f780f9b..0000000 --- a/docs-rst/concepts/property.rst +++ /dev/null @@ -1,49 +0,0 @@ -Types -===== - -.. _property: - -**property** ``$tType`` ------------------------ - -A specific characteristic of a `modelet `__ or -`engine `__. Multiple things can exhibit the same -`property <#property>`__. - -!!! example - color: red - age: 14 years ###### Source: -``properties.tff`` - -Relations -========= - -.. _has_value: - -**has_value** ``(``\ ```property`` <#property>`__\ ``>``\ **``$real``**\ ``)`` ------------------------------------------------------------------------------- - -The value of a certain `property <#property>`__. ###### Source: -``properties.tff`` - -.. _datatype_of_p: - -**datatype_of_property** ``(``\ ```property`` <#property>`__\ ``>``\ ```datatype`` `__\ ``)`` ----------------------------------------------------------------------------------------------------------- - -The `datatype `__ of a certain `property <#property>`__. -###### Source: ``properties.tff`` - -.. _is_property_of_m: - -**is_property_of_modelet** ``((``\ ```property`` <#property>`__\ ``*``\ ```modelet`` `__\ ``) >``\ **``$o``**\ ``)`` --------------------------------------------------------------------------------------------------------------------------------- - -Check if a `modelet `__ is described by a certain -`property <#property>`__. ###### Source: ``properties.tff`` - -.. _is_property_of_e: - -**is_property_of_engine** ``((``\ ```property`` <#property>`__\ ``*``\ ```engine`` `__\ ``) >``\ **``$o``**\ ``)`` ------------------------------------------------------------------------------------------------------------------------------ - -Check if an `engine `__ is described by a certain -`property <#property>`__. ###### Source: ``properties.tff`` diff --git a/docs-rst/concepts/representation_class.rst b/docs-rst/concepts/representation_class.rst deleted file mode 100644 index d307ed7..0000000 --- a/docs-rst/concepts/representation_class.rst +++ /dev/null @@ -1,11 +0,0 @@ -Types -===== - -.. _representation_class: - -**representation_class** ``$tType`` ------------------------------------ - -The purpose of a `modelet `__ (extrinsic to itself) when -used by an `engine `__. Class in the *Processing/Modelling -Model*. ###### Source: ``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/requirement.rst b/docs-rst/concepts/requirement.rst deleted file mode 100644 index d382163..0000000 --- a/docs-rst/concepts/requirement.rst +++ /dev/null @@ -1,36 +0,0 @@ -Types -===== - -.. _requirement: - -**requirement** ``$tType`` --------------------------- - -A restriction on the `property `__ values that a -`template `__ may enforce on a `modelet `__. -###### Source: ``properties.tff`` - -Relations -========= - -.. _datatype_of_p: - -**datatype_of_requirement** ``(``\ ```requirement`` <#requirement>`__\ ``>``\ ```datatype`` `__\ ``)`` -------------------------------------------------------------------------------------------------------------------- - -The `datatype `__ of a certain -`requirement <#requirement>`__. ###### Source: ``properties.tff`` - -.. _is_permissible: - -**is_permissible** ``((``\ ```requirement`` <#requirement>`__\ ``*``\ **``$real``**\ ``) >``\ **``$o``**\ ``)`` ---------------------------------------------------------------------------------------------------------------- - -Check if a value is *permissible* under a certain -`requirement <#requirement>`__. ###### Source: ``properties.tff`` - -**is_part_of** ``((``\ ```requirement`` <#requirement>`__\ ``*``\ ```template`` `__\ ``) >``\ **``$o``**\ ``)`` { $is_part_of data-toc-label=‘is_part_of’ } ------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - -Check if a `requirement <#requirement>`__ is part of a -`template `__. ###### Source: ``properties.tff`` diff --git a/docs-rst/concepts/spacetime_point.rst b/docs-rst/concepts/spacetime_point.rst deleted file mode 100644 index dcc76d0..0000000 --- a/docs-rst/concepts/spacetime_point.rst +++ /dev/null @@ -1,50 +0,0 @@ -Types -===== - -.. _spacetime_point: - -**spacetime_point** ``$tType`` ------------------------------- - -4-dimensional coordinates (3 space, 1 time). !!! note Not to be confused -with a 4-dimentional ```extent`` `__. ###### Source: -``fundamental-concepts.tff`` - -Relations -========= - -.. _point_x: - -**point_x** ``(``\ ```spacetime_point`` <#spacetime_point>`__\ ``>``\ **``$real``**\ ``)`` ------------------------------------------------------------------------------------------- - -The spatial ``x`` coordinate of a point in space and time -(```spacetime_point`` <#spacetime_point>`__). ###### Source: -``fundamental-concepts.tff`` - -.. _point_y: - -**point_y** ``(``\ ```spacetime_point`` <#spacetime_point>`__\ ``>``\ **``$real``**\ ``)`` ------------------------------------------------------------------------------------------- - -The spatial ``y`` coordinate of a point in space and time -(```spacetime_point`` <#spacetime_point>`__). ###### Source: -``fundamental-concepts.tff`` - -.. _point_z: - -**point_z** ``(``\ ```spacetime_point`` <#spacetime_point>`__\ ``>``\ **``$real``**\ ``)`` ------------------------------------------------------------------------------------------- - -The spatial ``z`` coordinate of a point in space and time -(```spacetime_point`` <#spacetime_point>`__). ###### Source: -``fundamental-concepts.tff`` - -.. _point_t: - -**point_t** ``(``\ ```spacetime_point`` <#spacetime_point>`__\ ``>``\ **``$real``**\ ``)`` ------------------------------------------------------------------------------------------- - -The time ``t`` coordinate of a point in space and time -(```spacetime_point`` <#spacetime_point>`__). ###### Source: -``fundamental-concepts.tff`` diff --git a/docs-rst/concepts/strategy.rst b/docs-rst/concepts/strategy.rst deleted file mode 100644 index 8208c6d..0000000 --- a/docs-rst/concepts/strategy.rst +++ /dev/null @@ -1,20 +0,0 @@ -Types -===== - -.. _strategy: - -**strategy** ``((``\ ```modelet_set`` `__\ ``*``\ `modelet `__\ ``) >``\ **``$o``**\ ``)`` --------------------------------------------------------------------------------------------------------------------------------------- - -A succession of `exertions `__ of `engines `__ -connects `modelets `__. `Strategies <#strategy>`__ -are transitive. - -- Must respect engine `requirements `__ -- Matches `modelet `__ *phenomenon* semantics to physical - reality - - - e.g. “on the living room table” to coordinates - -Source: ``transitive-strategies.tff`` -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/docs-rst/concepts/template.rst b/docs-rst/concepts/template.rst deleted file mode 100644 index 5c7d2b8..0000000 --- a/docs-rst/concepts/template.rst +++ /dev/null @@ -1,81 +0,0 @@ -Types -===== - -.. _template: - -**template** ``$tType`` ------------------------ - -Describes the features that a single `modelet `__ should -have for an `engine `__ to accept it as input. - -- a semantic function signature -- `properties `__ and `requirements `__ of - `modelets `__ ###### Source: ``engines-and-modelets.tff`` - -.. _template_set: - -**template_set** ``$tType`` ---------------------------- - -Some particular set of `templates <#template>`__ which describe the -inputs to an `engine `__. !!! example - {t1, t2, t3} - {t2} - -{} ###### Source: ``engines-and-modelets.tff`` - -Relations -========= - -.. _template_has_concept_requirement: - -**template_has_concept_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```concept`` `__\ ``)`` --------------------------------------------------------------------------------------------------------------------- - -The `concept `__ symbolizing the *phenomenon class* of a -`template `__. ###### Source: ``engines-and-modelets.tff`` - -.. _template_formalism_requirement: - -**template_formalism_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```formalism`` `__\ ``)`` ----------------------------------------------------------------------------------------------------------------------- - -The `formalism `__ this `template <#template>`__ expects -the *phenomenon* to be described by. ###### Source: -``engines-and-templates.tff`` - -.. _template_has_location_requirement: - -**template_has_location_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```spacetime_point`` `__\ ``)`` -------------------------------------------------------------------------------------------------------------------------------------- - -The time and spatial location a `template <#template>`__ refers to. A -`template `__ may have a specific temporal scope or expect -an observation at a specific -```spacetime_point`` `__. ###### Source: -``engines-and-modelets.tff`` - -.. _template_has_extent_requirement: - -**template_has_extent_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```extent`` `__\ ``)`` ------------------------------------------------------------------------------------------------------------------ - -The time and spatial `extent `__ a `template <#template>`__ -covers. A `template <#template>`__ may expect an area/volume/duration of -reference. ###### Source: ``engines-and-modelets.tff`` - -.. _template_has_creator_requirement: - -**template_has_creator_requirement** ``(``\ ```template`` <#template>`__\ ``>``\ ```engine`` `__\ ``)`` ------------------------------------------------------------------------------------------------------------------- - -The `engine `__ a `template <#template>`__ requires a -`modelet `__ to have been created by. ###### Source: -``engines-and-modelets.tff`` - -.. _is_in_template_set: - -**is_in_template_set** ``((``\ ```template`` <#template>`__\ ``*``\ ```template_set`` <#template_set>`__\ ``) >``\ **``$o``**\ ``)`` ------------------------------------------------------------------------------------------------------------------------------------- - -Check if a `template <#template>`__ is a member of a -`template_set <#template_set>`__. ###### Source: -``engines-and-modelets.tff`` diff --git a/docs-rst/index.rst b/docs-rst/index.rst deleted file mode 100644 index 6542de7..0000000 --- a/docs-rst/index.rst +++ /dev/null @@ -1 +0,0 @@ -–8<– “README.rst” diff --git a/docs-rst/packages/index.rst b/docs-rst/packages/index.rst deleted file mode 100644 index 1c81451..0000000 --- a/docs-rst/packages/index.rst +++ /dev/null @@ -1,2 +0,0 @@ -Understanding Packages -====================== diff --git a/docs-rst/usage/index.rst b/docs-rst/usage/index.rst deleted file mode 100644 index 1ea03f5..0000000 --- a/docs-rst/usage/index.rst +++ /dev/null @@ -1,13 +0,0 @@ -Usage and Installation -====================== - -The ``TFF`` models and tests can be run using the `latest -release `__ -or ``master`` branch of the -`Vampire `__ theorem prover. - -If you want to run the ``THF`` models, you need to either install the -`LEO-III `__ theorem prover or -build the Vampire ``hol`` branch from source using these -`instructions `__. -Make sure to add the ``-DCMAKE_BUILD_HOL=ON`` flag. From 1a62e51cccec7356e67e500fec223a46067052da Mon Sep 17 00:00:00 2001 From: Alex Gabriel Date: Tue, 16 Sep 2025 13:38:55 +0200 Subject: [PATCH 5/6] removed commented older formulation --- tff/model/properties.tff | 26 -------------------------- 1 file changed, 26 deletions(-) diff --git a/tff/model/properties.tff b/tff/model/properties.tff index e2dc5dd..ded61dc 100644 --- a/tff/model/properties.tff +++ b/tff/model/properties.tff @@ -94,32 +94,6 @@ tff(formally_equivalent, axiom, ) ). -% % Modelets and Templates can have matching profiles -% tff(axiom_modelet_matches_template, axiom, -% ! [M: modelet, T: template]: -% ( -% ( -% formally_equivalent(T, M) -% & -% ! [R: requirement]: -% ( -% is_part_of(R, T) -% => -% ? [P: property]: -% ( -% modelet_has_property(M, P) % match modelet to property -% & -% (datatype_of_requirement(R) = datatype_of_property(P)) % property has correct correct data format/type for requirement -% & -% is_permissible(R, has_value(P)) % ensure that the property's value is permissible -% ) -% ) -% ) -% => -% inputs_match(M, T) -% ) -% ). - tff(property_meets_requirement_decl, type, From b61cfcdf34d34fbcc7592098169c8057e127bc5e Mon Sep 17 00:00:00 2001 From: Alex Gabriel Date: Tue, 16 Sep 2025 13:45:18 +0200 Subject: [PATCH 6/6] changed inputs_match label --- tff/model/properties.tff | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/tff/model/properties.tff b/tff/model/properties.tff index ded61dc..7f6f117 100644 --- a/tff/model/properties.tff +++ b/tff/model/properties.tff @@ -134,7 +134,7 @@ tff(axiom_modelet_meets_requirement, axiom, % Modelets and Templates can have matching profiles -tff(new_axiom_modelet_matches_template, axiom, +tff(axiom_modelet_matches_template, axiom, ! [M: modelet, T: template]: ( ( @@ -153,20 +153,6 @@ tff(new_axiom_modelet_matches_template, axiom, ). - - - - - - - - - - - - - - % Modelet sets match template sets if all their templates have a corresponding modelet with matching inputs inputs_match(M, T) %interfaces_match(MS, TS)