Skip to content

ST6RI-929 KerML 1.1 Ballot #2 - Model Library #757

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
seidewitz wants to merge 3 commits into
base: master
Choose a base branch
from
+151 −120
Open

ST6RI-929 KerML 1.1 Ballot #2 - Model Library #757

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
89fad96
KERML11-9 Corrected typo in documentation of Transfer::isInstant.
seidewitz May 2, 2026
428e7a4
KERML11-144 Made Collections docs in spec and library file consistent.
seidewitz May 2, 2026
d8c344c
ST6RI-929 Regenerated sysml.library index.
seidewitz May 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion sysml.library/.index.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15387,6 +15387,7 @@
"anyTrue",
"collect",
"dataValues",
"equals",
"exactlyOne",
"exists",
"forAll",
Expand Down Expand Up @@ -280190,5 +280191,5 @@
"withoutOccurrences"
]
},
"checksum": "83ebd85a5305dcef0cc1f3f11c219737ad8f38448d8bc28af253c0a2d8af413e"
"checksum": "e69c541524fc1effc91c174657bf78869a7064934d7a70994d63fd364f44d6ae"
}
266 changes: 148 additions & 118 deletions sysml.library/Kernel Libraries/Kernel Data Type Library/Collections.kerml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,147 +1,177 @@
standard library package Collections {
doc
/*
* This package defines a standard set of Collection data types. Unlike sequences of values
* defined directly using multiplicity, these data types allow for the possibility of collections
* as elements of collections.
*/
doc
/*
* This package defines a standard set of Collection data types. Unlike sequences of values
* defined directly using multiplicity, these data types allow for the possibility of collections
* as elements of collections.
*/

private import Base::*;
private import ScalarValues::*;
private import SequenceFunctions::size;
private import IntegerFunctions::*;
private import ControlFunctions::*;
private import Base::*;
private import ScalarValues::*;
private import SequenceFunctions::size;
private import SequenceFunctions::equals;
private import IntegerFunctions::*;
private import ControlFunctions::*;

abstract datatype Collection {
doc
/*
* Collection is the top level abstract supertype of all collection types.
* The name elements is used to denote the members or contents of the collection.
*/

feature elements[0..*] nonunique;
}
abstract datatype Collection {
doc
/*
* A Collection is a DataValue that represents a collection of elements of a given type.
*/

feature elements[0..*] nonunique {
doc
/*
* The contents of the Collection.
*/
}
}

abstract datatype OrderedCollection :> Collection {
doc
/*
* OrderedCollection is the abstract supertype for all ordered collection types.
*/
feature elements[0..*] ordered nonunique :>> Collection::elements;
doc
/*
* An OrderedCollection is a Collection of which the elements are ordered and not necessarily unique.
*/
feature elements[0..*] ordered nonunique :>> Collection::elements;
}

abstract datatype UniqueCollection :> Collection {
doc
/*
* UniqueCollection is the abstract supertype for all collection types with unique elements.
*/

feature elements[0..*] :>> Collection::elements {
/* Note: Redefinition of 'elements' is unique by default. */
}
doc
/*
* A UniqueCollection is a Collection of which the elements are unique and not necessarily ordered.
*/

feature elements[0..*] :>> Collection::elements {
doc
/* Note: Redefinition of 'elements' is unique by default. */
}
}

datatype Array :> OrderedCollection {
doc
/*
* An Array is a fixed size, multi-dimensional Collection of which the elements are nonunique and ordered.
* Its dimensions specify how many dimensions the array has, and how many elements there are in each dimension.
* The rank is equal to the number of dimensions. The flattenedSize is equal to the total number of elements
* in the array.
*
* Feature elements is a flattened sequence of all elements of an Array and can be accessed by a tuple of indices.
* The number of indices is equal to rank. The elements are packed according to row-major convention, as in the C programming language.
*
* The elements of an Array can be assessed by a tuple of indices. The number of indices in such tuple is equal to rank.
* The packing of the elements, i.e. the flattened representation, follows the row-major convention,
* as in the C programming language.
*
* Note 1. Feature dimensions may be empty, which denotes a zero dimensional array, allowing an Array to collapse to a single element.
* This is useful to allow for specialization of an Array into a type restricted to represent a scalar.
* The flattenedSize of a zero dimensional array is 1.
*
* Note 2: An Array can represent the generalized mathematical concept of an infinite matrix of any rank, i.e. not limited to rank two.
*/

doc
/*
* An Array is a fixed size, multi-dimensional Collection of which the elements are nonunique and ordered.
* Its dimensions specify how many dimensions the array has, and how many elements there are in each dimension.
* The rank is equal to the number of dimensions. The flattenedSize is equal to the total number of elements
* in the array.
*
* Feature elements is a flattened sequence of all elements of an Array and can be accessed by a tuple of indices.
* The number of indices is equal to rank. The elements are packed according to row-major convention.
*
* The elements of an Array can be assessed by a tuple of indices. The number of indices in such tuple is equal to rank.
* The elements are packed according to the row-major convention.
*
* Note 1. Feature dimensions may be empty, which denotes a zero dimensional array, allowing an Array to collapse to a single element.
* This is useful to allow for specialization of an Array into a type restricted to represent a scalar.
* The flattenedSize of a zero dimensional array is 1.
*
* Note 2: An Array can represent the generalized mathematical concept of an infinite matrix of any rank, i.e. not limited to rank two.
*/

feature dimensions: Positive[0..*] ordered nonunique {
doc
/* Feature `dimensions` defines the N-dimensional shape of the Array
* The alternative name `shape` (as used in many programming languages) is not used as it would interfere with a geometric shape feature.
*/
doc
/*
* Defines the N-dimensional shape of the Array.
*/
}

feature rank: Natural[1] = size(dimensions) {
doc
/*
* The number of dimensions.
*/
}
feature rank: Natural[1] = size(dimensions);
feature flattenedSize: Positive[1] = dimensions->reduce '*' ?? 1;

feature flattenedSize: Positive[1] = dimensions->reduce '*' ?? 1 {
doc
/*
* The number of elements in the Array, given as the product of the dimensions,
* or 1 if dimensions is empty.
*/
}

inv { flattenedSize == size(elements) }
}

datatype Bag :> Collection {
doc
/*
* Bag is a variable-size, unordered collection of nonunique elements.
*/
}
datatype Set :> UniqueCollection {
doc
/*
* Set is a variable-size, unordered collection of unique elements.
*/
}
datatype Bag :> Collection {
doc
/*
* A Bag is a variable-size Collection of which the elements are unordered and nonunique.
*/
}
datatype Set :> UniqueCollection {
doc
/*
* A Set is a variable-size Collection of which the elements are unique and unordered.
*/
}

datatype OrderedSet :> OrderedCollection, UniqueCollection
intersects OrderedCollection, UniqueCollection {
doc
/*
* OrderedSet is a variable-size, ordered collection of unique elements.
*/

feature elements[0..*] ordered :>> OrderedCollection::elements, UniqueCollection::elements {
/* Note: Redefinition of `elements` is unique by default. */
}
}

datatype List :> OrderedCollection {
doc
/*
* List is a variable-size, ordered collection of nonunique elements.
*/
}
datatype OrderedSet :> OrderedCollection, UniqueCollection
intersects OrderedCollection, UniqueCollection {
doc
/*
* An OrderedSet is a variable-size Collection of which the elements are unique and ordered.
*/

feature elements[0..*] ordered :>> OrderedCollection::elements, UniqueCollection::elements {
doc
/* Note: Redefinition of elements is unique by default. */
}
}

datatype List :> OrderedCollection {
doc
/*
* A List is a variable-size Collection of which the elements are nonunique and ordered.
*/
}

datatype KeyValuePair {
doc
/*
* KeyValuePair is a tuple of a key and a value for use in Map collections.
* The key must be immutable.
*/
doc
/*
* A KeyValuePair is a DataValue that represents a pair of a key and an associated val,
* primarily for use in Maps.
*/
feature key: Anything[0..*] ordered nonunique;
feature val: Anything[0..*] ordered nonunique;
}

datatype Map :> Collection {
doc
/*
* Map is a variable-size, unordered collection of elements that are key-value pairs.
*/

feature elements: KeyValuePair[0..*] :>> Collection::elements {
/* Note: Redefinition of `elements` is unique by default.
* The `key` of any `KeyValuePair` must be unique over the collection of `KeyValuePair`.
* The `val` does not need to be unique.
*/
}
doc
/*
* Map is a variable-size Collection of which the elements are KeyValuePairs.
* The keys must be unique within the Map. The vals need not be unique.
*/

feature elements: KeyValuePair[0..*] :>> Collection::elements {
doc
/* Note: Redefinition of elements is unique by default.*/
}

inv {
elements->forAll{ in e1 : KeyValuePair;
not elements->exists{ in e2 : KeyValuePair;
e1 != e2 and e1.key->equals(e2.key) }
}
}
}

datatype OrderedMap :> Map {
doc
/*
* OrderedMap is a variable-size, ordered collection of elements that are key-value pairs.
*/
datatype OrderedMap :> Map, OrderedCollection {
doc
/*
* An OrderedMap is a variable-size Map that maintains an ordering of its elements.
*
* The ordering may be by key of the KeyValuePair elements, or by order of construction,
* or any other method. The essential aspect is that ordering is maintained and guaranteed across
* accesses to the OrderedMap.
*/

feature elements: KeyValuePair[0..*] ordered :>> Map::elements {
/* Note: Redefinition of `elements` is unique by default. */
}
feature elements: KeyValuePair[0..*] ordered :>> Map::elements, OrderedCollection::elements {
doc
/* Note: Redefinition of elements is unique by default. */
}
}

}
2 changes: 1 addition & 1 deletion sysml.library/Kernel Libraries/Kernel Semantic Library/Transfers.kerml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ standard library package Transfers {
feature isInstant: Boolean[1] {
doc
/*
* If isInstance is true, then the transfer is instantaneous.
* If isInstant is true, then the transfer is instantaneous.
*/
}

Expand Down
Loading