diff --git a/doc/1-Kernel_Modeling_Language.pdf b/doc/1-Kernel_Modeling_Language.pdf index fc1caed0..21fcb3a3 100644 Binary files a/doc/1-Kernel_Modeling_Language.pdf and b/doc/1-Kernel_Modeling_Language.pdf differ diff --git a/doc/2-OMG_Systems_Modeling_Language.pdf b/doc/2-OMG_Systems_Modeling_Language.pdf index 67b97824..2fc4fba6 100644 Binary files a/doc/2-OMG_Systems_Modeling_Language.pdf and b/doc/2-OMG_Systems_Modeling_Language.pdf differ diff --git a/doc/3-Systems_Modeling_API_and_Services.pdf b/doc/3-Systems_Modeling_API_and_Services.pdf index 73e55b18..a09f8988 100644 Binary files a/doc/3-Systems_Modeling_API_and_Services.pdf and b/doc/3-Systems_Modeling_API_and_Services.pdf differ diff --git a/doc/Intro to the SysML v2 Language-Textual Notation.pdf b/doc/Intro to the SysML v2 Language-Textual Notation.pdf index 4fa08379..dc9c1d24 100644 Binary files a/doc/Intro to the SysML v2 Language-Textual Notation.pdf and b/doc/Intro to the SysML v2 Language-Textual Notation.pdf differ diff --git a/install/eclipse/org.omg.sysml.site.zip b/install/eclipse/org.omg.sysml.site.zip index 3f4dbfe2..8decc022 100644 Binary files a/install/eclipse/org.omg.sysml.site.zip and b/install/eclipse/org.omg.sysml.site.zip differ diff --git a/install/jupyter/README.pdf b/install/jupyter/README.pdf index 2af07857..92c9b5be 100644 Binary files a/install/jupyter/README.pdf and b/install/jupyter/README.pdf differ diff --git a/install/jupyter/install.bat b/install/jupyter/install.bat index 05bd0474..c0079be7 100755 --- a/install/jupyter/install.bat +++ b/install/jupyter/install.bat @@ -20,7 +20,7 @@ @echo off -set /A SYSML_VERSION="0.20.0" +set /A SYSML_VERSION="0.21.0" echo --- Step 1: Testing Conda installation --- where conda diff --git a/install/jupyter/install.sh b/install/jupyter/install.sh index e2ce6d06..ba2720b9 100755 --- a/install/jupyter/install.sh +++ b/install/jupyter/install.sh @@ -21,7 +21,7 @@ set -e -SYSML_VERSION="0.20.0" +SYSML_VERSION="0.21.0" echo "--- Step 1: Testing Conda installation ---" command -v conda || (echo "Conda is not installed. Please install Conda and re-run." && return 1) diff --git a/kerml/src/examples/Mass Roll-up Example/MassRollup_1.kerml b/kerml/src/examples/Mass Roll-up Example/MassRollup_1.kerml index e5c48526..b2809012 100644 --- a/kerml/src/examples/Mass Roll-up Example/MassRollup_1.kerml +++ b/kerml/src/examples/Mass Roll-up Example/MassRollup_1.kerml @@ -1,5 +1,5 @@ package MassRollup_1 { - import ScalarFunctions::*; + import NumericalFunctions::*; class MassedThing { feature mass subsets ISQ::mass; diff --git a/kerml/src/examples/Mass Roll-up Example/MassRollup_2.kerml b/kerml/src/examples/Mass Roll-up Example/MassRollup_2.kerml index 6d93a52a..4b4dd934 100644 --- a/kerml/src/examples/Mass Roll-up Example/MassRollup_2.kerml +++ b/kerml/src/examples/Mass Roll-up Example/MassRollup_2.kerml @@ -1,5 +1,5 @@ package MassRollup_2 { - import ScalarFunctions::*; + import NumericalFunctions::*; import ISQ::*; class MassedThing { diff --git a/kerml/src/examples/Simple Tests/Associations.kerml b/kerml/src/examples/Simple Tests/Associations.kerml new file mode 100644 index 00000000..8497bb89 --- /dev/null +++ b/kerml/src/examples/Simple Tests/Associations.kerml @@ -0,0 +1,11 @@ +package Associations { + assoc A { + end x; + end y[1..*]; + } + + assoc B specializes A { + end x1; + end y1[0..*] redefines y; + } +} \ No newline at end of file diff --git a/kerml/src/examples/Simple Tests/Expressions.kerml b/kerml/src/examples/Simple Tests/Expressions.kerml index c469897d..83d7e229 100644 --- a/kerml/src/examples/Simple Tests/Expressions.kerml +++ b/kerml/src/examples/Simple Tests/Expressions.kerml @@ -12,7 +12,10 @@ package Expressions { b = x > y? x-y: y-x; c = x->collect {in xx; xx + 1}; - d = x->reduce {in s; in t; s + t}->reduce '+'; + c1 = x.{in xx; xx + 1}; + d = x->select {in xx; xx != null}; + d1 = x.?{in xx; xx != null}; + e = x->reduce {in s; in t; s + t}->reduce '+'; behavior w specializes ControlPerformances::LoopPerformance (inout v: Integer) { in expr redefines whileTest {v > 3} diff --git a/sysml.library/Domain Libraries/Geometry/BasicGeometry.sysml b/sysml.library/Domain Libraries/Geometry/BasicGeometry.sysml deleted file mode 100644 index 28aa0b8a..00000000 --- a/sysml.library/Domain Libraries/Geometry/BasicGeometry.sysml +++ /dev/null @@ -1,34 +0,0 @@ -package BasicGeometry { - private import UnitsAndScales::DimensionOneValue; - private import ISQ::LengthValue; - private import SI::*; - private import RealFunctions::*; - - /** - * Component of Cartesian direction vector with value in interval [-1:1] - */ - attribute def DirectionValue :> DimensionOneValue { - assert constraint { num >= -1.0 & num <= 1.0 } - } - - attribute def CoordinateValue :> LengthValue; - - attribute def Location3DCartesian { - attribute x: CoordinateValue[1]; - attribute y: CoordinateValue[1]; - attribute z: CoordinateValue[1]; - } - - attribute def Direction3DCartesian { - attribute xDir: DirectionValue[1]; - attribute yDir: DirectionValue[1]; - attribute zDir: DirectionValue[1]; - assert constraint { xDir**2 + yDir**2 + zDir**2 == 1.0 } - } - - attribute def AxisPlacement3DCartesian { - attribute location: Location3DCartesian[1]; - attribute zAxisDir: Direction3DCartesian[1]; - attribute xAxisDir: Direction3DCartesian[1]; - } -} \ No newline at end of file diff --git a/sysml.library/Domain Libraries/Geometry/ShapeItems.sysml b/sysml.library/Domain Libraries/Geometry/ShapeItems.sysml new file mode 100644 index 00000000..3540b0cc --- /dev/null +++ b/sysml.library/Domain Libraries/Geometry/ShapeItems.sysml @@ -0,0 +1,266 @@ +/** + * This package provides a model of items that represent basic geometric shapes. + */ +package ShapeItems { + private import ScalarValues::Boolean; + private import ISQ::*; + private import SI::m; + private import Occurrences::WithinBoth; + private import Objects::*; + private import Items::Item; + private import SequenceFunctions::isEmpty; + + /** + * A Line is a Curve that is a straight line of a given length. + */ + item def Line :> Curve { + attribute :>> length; + attribute :>> outerSpaceDimension = 1; + } + + /** + * A PlanarSurface is a flat Surface with a given area. + */ + item def PlanarSurface :> Surface { + attribute :>> area; + attribute :>> outerSpaceDimension = 2; + } + + /** + * Shell is the most general Surface shape. + */ + abstract item def Shell :> Item, StructuredSpaceObject, Surface; + + /** + * Path is the most general Curve shape. + */ + abstract item def Path :> Item, StructuredSpaceObject, Curve; + + /** + * A Circle is a Path in the shape of a circle of a given radius. + */ + item def Circle :> Path { + attribute radius :>> radius; + + item :>> faces [0]; + item :>> edges [1] { + attribute circumference :>> length = Circle::radius * TrigFunctions::pi; + item :>> shape : Item [0]; + item :>> vertices [0]; + } + item :>> vertices [0]; + } + + /** + * A Disc is a Shell bounded by a Circle. + */ + item def Disc :> Shell { + attribute radius :>> radius; + + item :>> shape : Circle [1] { + attribute :>> radius = Disc::radius; + } + + item :>> faces : PlanarSurface [1] { + item :>> edges [1]; + } + item :>> edges : Circle [1] = shape; + item :>> vertices [0]; + + connection :WithinBoth connect faces.edges [1] to edges [0..*]; + } + + /** + * A Sphere is a Shell in the shape of a sphere of a given radius. + */ + item def Sphere :> Shell { + attribute :>> radius; + + item faces : Surface [1] :>> faces; + item :>> edges [0]; + item :>> vertices [0]; + } + + /** + * A Cone is a Shell in the shape of a right circular code, possibly truncated, with given + * baseRadius, apexRadius and height. + */ + item def Cone :> Shell { + attribute baseRadius :> radius; + attribute apexRadius :> radius default 0 [m]; + attribute :>> height; + attribute isTruncated : Boolean [1] = (apexRadius > 0); + + item faces : Surface [2..3] :>> faces; + item bf : Disc [1] :> faces; + item af : Disc [0..1] :> faces; + item cf : Surface [1] :> faces; + constraint { (apexRadius == 0) == isEmpty(af) } + + item edges : Circle [1..2] :>> edges; + item be [1] :> edges { + attribute :>> radius = baseRadius; + } + item ae [0..1] :> edges { + attribute :>> radius = apexRadius; + } + constraint { isEmpty(af) == isEmpty(ae) } + + item vertices : Point [0..1] :>> vertices; + constraint { isEmpty(ae) == isEmpty(vertices) } + + /* Faces to edges */ + connection :WithinBoth connect bf.edges [1] to be [0..*]; + connection :WithinBoth connect af.edges [1] to ae [0..*]; + connection :WithinBoth connect cf.edges [1] to be [0..*]; + connection :WithinBoth connect cf.edges [1] to ae [0..*]; + + /* Faces to vertices */ + connection :WithinBoth connect cf.vertices [1] to vertices [0..*]; + + /* Coincident edges */ + connection :WithinBoth connect be [2] to be [2]; + connection :WithinBoth connect ae [2] to ae [2]; + + } + + /** + * A Cylinder is a Cone whose baseRadius and apexRadius are the same, representing + * a right circular cylinder. + */ + item def Cylinder :> Cone { + attribute :>> radius = baseRadius; + + attribute :>> baseRadius = apexRadius; + } + + /** + * A Cuboid is a Shell in the shape of a six-sided polyhedron with rectangular sides, with + * given length, width and height. + */ + item def Cuboid :> Shell { + attribute :>> length; + attribute :>> width; + attribute :>> height; + + item faces : PlanarSurface [6] :>> faces { + item :>> edges [4]; + } + item tf :> faces [1]; + item bf :> faces [1]; + item ff :> faces [1]; + item rf :> faces [1]; + item slf :> faces [1]; + item srf :> faces [1]; + + item edges : Line [12] :>> edges { + item :>> vertices [2]; + } + item tfe [2] :> edges { attribute :>> length = Cuboid::length; } + item tre [2] :> edges { attribute :>> length = Cuboid::length; } + item tsle [2] :> edges { attribute :>> length = Cuboid::width; } + item tsre [2] :> edges { attribute :>> length = Cuboid::width; } + item bfe [2] :> edges { attribute :>> length = Cuboid::length; } + item bre [2] :> edges { attribute :>> length = Cuboid::length; } + item bsle [2] :> edges { attribute :>> length = Cuboid::width; } + item bsre [2] :> edges { attribute :>> length = Cuboid::width; } + item ufle [2] :> edges { attribute :>> length = Cuboid::height; } + item ufre [2] :> edges { attribute :>> length = Cuboid::height; } + item urle [2] :> edges { attribute :>> length = Cuboid::height; } + item urre [2] :> edges { attribute :>> length = Cuboid::height; } + + item vertices : Point [8] :>> vertices; + item tflv [3] :> vertices; + item tfrv [3] :> vertices; + item trlv [3] :> vertices; + item trrv [3] :> vertices; + item bflv [3] :> vertices; + item bfrv [3] :> vertices; + item brlv [3] :> vertices; + item brrv [3] :> vertices; + + /* Faces to edges */ + connection :WithinBoth connect tf.edges [1] to tfe [0..*]; + connection :WithinBoth connect tf.edges [1] to tre [0..*]; + connection :WithinBoth connect tf.edges [1] to tsle [0..*]; + connection :WithinBoth connect tf.edges [1] to tsre [0..*]; + + connection :WithinBoth connect bf.edges [1] to bfe [0..*]; + connection :WithinBoth connect bf.edges [1] to bre [0..*]; + connection :WithinBoth connect bf.edges [1] to bsle [0..*]; + connection :WithinBoth connect bf.edges [1] to bsre [0..*]; + + connection :WithinBoth connect ff.edges [1] to tfe [0..*]; + connection :WithinBoth connect ff.edges [1] to bfe [0..*]; + connection :WithinBoth connect ff.edges [1] to ufle [0..*]; + connection :WithinBoth connect ff.edges [1] to ufre [0..*]; + + connection :WithinBoth connect rf.edges [1] to tre [0..*]; + connection :WithinBoth connect rf.edges [1] to bre [0..*]; + connection :WithinBoth connect rf.edges [1] to urle [0..*]; + connection :WithinBoth connect rf.edges [1] to urre [0..*]; + + connection :WithinBoth connect slf.edges [1] to tsle [0..*]; + connection :WithinBoth connect slf.edges [1] to bsle [0..*]; + connection :WithinBoth connect slf.edges [1] to ufle [0..*]; + connection :WithinBoth connect slf.edges [1] to urle [0..*]; + + connection :WithinBoth connect srf.edges [1] to tsre [0..*]; + connection :WithinBoth connect srf.edges [1] to bsre [0..*]; + connection :WithinBoth connect srf.edges [1] to ufre [0..*]; + connection :WithinBoth connect srf.edges [1] to urre [0..*]; + + /* Edges to vertices */ + connection :WithinBoth connect tfe.vertices [1] to tflv [0..*]; + connection :WithinBoth connect tfe.vertices [1] to tfrv [0..*]; + connection :WithinBoth connect tre.vertices [1] to trlv [0..*]; + connection :WithinBoth connect tre.vertices [1] to trrv [0..*]; + connection :WithinBoth connect tsle.vertices [1] to tflv [0..*]; + connection :WithinBoth connect tsle.vertices [1] to trlv [0..*]; + connection :WithinBoth connect tsre.vertices [1] to tfrv [0..*]; + connection :WithinBoth connect tsre.vertices [1] to trrv [0..*]; + + connection :WithinBoth connect bfe.vertices [1] to bflv [0..*]; + connection :WithinBoth connect bfe.vertices [1] to bfrv [0..*]; + connection :WithinBoth connect bre.vertices [1] to brlv [0..*]; + connection :WithinBoth connect bre.vertices [1] to brrv [0..*]; + connection :WithinBoth connect bsle.vertices [1] to bflv [0..*]; + connection :WithinBoth connect bsle.vertices [1] to brlv [0..*]; + connection :WithinBoth connect bsre.vertices [1] to bfrv [0..*]; + connection :WithinBoth connect bsre.vertices [1] to brrv [0..*]; + + connection :WithinBoth connect ufle.vertices [1] to tflv [0..*]; + connection :WithinBoth connect ufle.vertices [1] to bflv [0..*]; + connection :WithinBoth connect ufre.vertices [1] to tfrv [0..*]; + connection :WithinBoth connect ufre.vertices [1] to bfrv [0..*]; + connection :WithinBoth connect urle.vertices [1] to trlv [0..*]; + connection :WithinBoth connect urle.vertices [1] to brlv [0..*]; + connection :WithinBoth connect urre.vertices [1] to trrv [0..*]; + connection :WithinBoth connect urre.vertices [1] to brrv [0..*]; + + /* Coincident edges */ + connection :WithinBoth connect tfe [2] to tfe [2]; + connection :WithinBoth connect tre [2] to tre [2]; + connection :WithinBoth connect tsle [2] to tsle [2]; + connection :WithinBoth connect tsre [2] to tsre [2]; + connection :WithinBoth connect bfe [2] to bfe [2]; + connection :WithinBoth connect bre [2] to bre [2]; + connection :WithinBoth connect bsle [2] to bsle [2]; + connection :WithinBoth connect bsre [2] to bsre [2]; + connection :WithinBoth connect ufle [2] to ufle [2]; + connection :WithinBoth connect ufre [2] to ufre [2]; + connection :WithinBoth connect urle [2] to urle [2]; + connection :WithinBoth connect urre [2] to urre [2]; + + /* Coincident vertices */ + connection :WithinBoth connect tflv [3] to tflv [3]; + connection :WithinBoth connect tfrv [3] to tfrv [3]; + connection :WithinBoth connect trlv [3] to trlv [3]; + connection :WithinBoth connect trrv [3] to trrv [3]; + connection :WithinBoth connect bflv [3] to bflv [3]; + connection :WithinBoth connect bfrv [3] to bfrv [3]; + connection :WithinBoth connect brlv [3] to brlv [3]; + connection :WithinBoth connect brrv [3] to brrv [3]; + } + alias Box for Cuboid; +} \ No newline at end of file diff --git a/sysml.library/Domain Libraries/Geometry/SpatialItems.sysml b/sysml.library/Domain Libraries/Geometry/SpatialItems.sysml new file mode 100644 index 00000000..af445449 --- /dev/null +++ b/sysml.library/Domain Libraries/Geometry/SpatialItems.sysml @@ -0,0 +1,144 @@ +/** + * This package models physical items that have a spatial extent and act as a spatial frame of reference + * for obtaining position and displacement vectors of points within them. + */ +package SpatialItems { + private import Objects::Point; + private import SpatialFrames::SpatialFrame; + private import Quantities::VectorQuantityValue; + private import UnitsAndScales::VectorMeasurementReference; + private import Time::Clock; + private import Time::TimeInstantValue; + private import ISQ::Cartesian3dSpatialCoordinateSystem; + private import VectorFunctions::isZeroVector; + private import ControlFunctions::forAll; + + /** + * A SpatialItem is an Item with a three-dimensional spatial extent that also acts as a SpatialFrame of reference. + */ + item def SpatialItem :> SpatialFrame { + ref item :>> self : SpatialItem; + + /** + * A local Clock to be used as the corresponding time reference within this SpatialItem. + * By default this is the global defaultClock. + */ + ref item localClock : Clock[1] default Time::defaultClock; + + /** + * The three-dimensional VectorMeasurementReference to be used as the measurement reference for position + * and displacement vector values relative to this SpatialItem. + */ + attribute coordinateFrame : VectorMeasurementReference[1] default Cartesian3dSpatialCoordinateSystem() { + attribute :>> dimensions = 3; + } + + /** + * The Point at the origin of the coordinateFrame of this SpatialItem. + */ + item originPoint : Point[1] :> spaceShots; + + /** + * The CurrentPositionOf the originPoint must always be a zero vector. + */ + assert constraint originPointConstraint { + isZeroVector(CurrentPositionOf(originPoint, SpatialItem::self)) + } + } + + /** + * A CompoundSpatialItem is a SpatialItem that is a spacial union of a collection of component SpatialItems. + */ + item def CompoundSpatialItem :> SpatialItem { + + /** + * The composite SpatialItems that together make up this CompoundSpatialItem. + * The coordinateFrames of the compositeItems are nested in the coordinateFrame of the CompoundSpatialItem, + * and, by default, they have the same localClock as the CompoundSpacialItem. + */ + item componentItems : SpatialItem[0..*] ordered :> subitems { + item nestedLocalClock :>> localClock default localClock; + attribute nestedBasisDirections : VectorQuantityValue[3]; + attribute nestedOrigin : VectorQuantityValue[0..1]; + attribute nestedCoordinateFrame :>> coordinateFrame { + attribute :>> placement[1] { + attribute :>> source = coordinateFrame; + attribute :>> target = nestedCoordinateFrame; + attribute :>> basisDirections = nestedBasisDirections; + attribute :>> origin = nestedOrigin; + } + } + } + + /** + * A CompoundSpatialItem is a spatial union of its componentItems. + */ + attribute componentUnion[1] :> unionsOf { + item :>> elements = componentItems; + } + + } + + /** + * The PositionOf a Point relative to a SpatialItem, at a specific TimeInstantValue relative to a given Clock, + * is a positionVector that is a VectorQuantityValue in the coordinateFrame of the SpatialItem. + * The default Clock is the localClock of the SpatialItem. + */ + calc def PositionOf :> SpatialFrames::PositionOf { + in point : Point[1]; + in timeInstant : TimeInstantValue[1]; + in enclosingItem :>> 'frame' : SpatialItem[1]; + in clock : Clock[1] default enclosingItem.localClock; + return positionVector : VectorQuantityValue[1] { + attribute :>> mRef = enclosingItem.coordinateFrame; + attribute :>> isBound = true; + } + } + + /** + * The CurrentPositionOf a Point relative to a SpatialItem and a Clock is the PositionOf + * the Point relative to the SpatialItem at the currentTime of the Clock. + */ + calc def CurrentPositionOf :> SpatialFrames::CurrentPositionOf { + in point : Point[1]; + in enclosingItem :>> 'frame' : SpatialItem[1]; + in clock : Clock[1] default enclosingItem.localClock; + return positionVector : VectorQuantityValue[1] { + attribute :>> mRef = enclosingItem.coordinateFrame; + attribute :>> isBound = true; + } + } + + /** + * The DisplacementOf two Points relative to a SpatialItem, at a specific TimeInstantValue relative to a + * given Clock, is the displacementVector computed as the difference between the PositionOf the + * first Point and PositionOf the second Point, relative to that SpatialItem, at that timeInstant. + */ + calc def DisplacementOf :> SpatialFrames::DisplacementOf { + in point1 : Point[1]; + in point2 : Point[1]; + in timeInstant : TimeInstantValue[1]; + in spacialItem :>> 'frame' : SpatialItem[1]; + in clock : Clock[1] default spacialItem.localClock; + return displacementVector : VectorQuantityValue[1] { + attribute :>> mRef = spacialItem.coordinateFrame; + attribute :>> isBound = false; + } + } + + /** + * The CurrentDisplacementOf two Points relative to a SpatialItem and a Clock is the DisplacementOf + * the Points relative to the SpacialItem, at the currentTime of the Clock. + */ + calc def CurrentDisplacementOf :> SpatialFrames::CurrentDisplacementOf { + in point1 : Point[1]; + in point2 : Point[1]; + in spacialItem :>> 'frame' : SpatialItem[1]; + in clock : Clock[1] default spacialItem.localClock; + return displacementVector : VectorQuantityValue[1] { + attribute :>> mRef = spacialItem.coordinateFrame; + attribute :>> isBound = false; + } + } + +} \ No newline at end of file diff --git a/sysml.library/Domain Libraries/Quantities and Units/Quantities.sysml b/sysml.library/Domain Libraries/Quantities and Units/Quantities.sysml index 5706c48b..00ad99a1 100644 --- a/sysml.library/Domain Libraries/Quantities and Units/Quantities.sysml +++ b/sysml.library/Domain Libraries/Quantities and Units/Quantities.sysml @@ -9,6 +9,7 @@ package Quantities { private import ScalarValues::Natural; private import ScalarValues::Boolean; private import ScalarValues::String; + private import VectorValues::NumericalVectorValue; /** * The value of a quantity is a tuple of one or more numbers (i.e. mathematical number values) and a reference to a measurement reference. @@ -31,7 +32,7 @@ package Quantities { assert constraint boundMatch { (isBound == mRef.isBound) || (!isBound && mRef.isBound) } } - abstract attribute def VectorQuantityValue :> TensorQuantityValue { + abstract attribute def VectorQuantityValue :> TensorQuantityValue, NumericalVectorValue { attribute :>> mRef: UnitsAndScales::VectorMeasurementReference; } diff --git a/sysml.library/Domain Libraries/Quantities and Units/QuantityCalculations.sysml b/sysml.library/Domain Libraries/Quantities and Units/QuantityCalculations.sysml index 393590a6..75e57b67 100644 --- a/sysml.library/Domain Libraries/Quantities and Units/QuantityCalculations.sysml +++ b/sysml.library/Domain Libraries/Quantities and Units/QuantityCalculations.sysml @@ -4,9 +4,16 @@ package QuantityCalculations { import UnitsAndScales::ScalarMeasurementReference; import UnitsAndScales::DimensionOneValue; - calc def '[' specializes BaseFunctions::'[' (x: NumericalValue, y: ScalarMeasurementReference): ScalarQuantityValue; + calc def isZero specializes NumericalFunctions::isZero(x: ScalarQuantityValue): Boolean { + NumericalFunctions::isZero(x.num) + } + calc def isUnit specializes NumericalFunctions::isUnit(x: ScalarQuantityValue): Boolean { + NumericalFunctions::isUnit(x.num) + } + + calc def '[' specializes BaseFunctions::'[' (x: Number, y: ScalarMeasurementReference): ScalarQuantityValue; - calc def Abs specializes NumericalFunctions::Abs (x: ScalarQuantityValue): ScalarQuantityValue; + calc def abs specializes NumericalFunctions::abs (x: ScalarQuantityValue): ScalarQuantityValue; calc def '+' specializes NumericalFunctions::'+' (x: ScalarQuantityValue, y: ScalarQuantityValue[0..1]): ScalarQuantityValue; calc def '-' specializes NumericalFunctions::'-' (x: ScalarQuantityValue, y: ScalarQuantityValue[0..1]): ScalarQuantityValue; @@ -20,16 +27,15 @@ package QuantityCalculations { calc def '<=' specializes NumericalFunctions::'<=' (x: ScalarQuantityValue, y: ScalarQuantityValue): Boolean; calc def '>=' specializes NumericalFunctions::'>=' (x: ScalarQuantityValue, y: ScalarQuantityValue): Boolean; - calc def Max specializes NumericalFunctions::Max (x: ScalarQuantityValue, y: ScalarQuantityValue): ScalarQuantityValue; - calc def Min specializes NumericalFunctions::Min (x: ScalarQuantityValue, y: ScalarQuantityValue): ScalarQuantityValue; + calc def max specializes NumericalFunctions::max (x: ScalarQuantityValue, y: ScalarQuantityValue): ScalarQuantityValue; + calc def min specializes NumericalFunctions::min (x: ScalarQuantityValue, y: ScalarQuantityValue): ScalarQuantityValue; - calc def '==' specializes BaseFunctions::'==' (x: ScalarQuantityValue, y: ScalarQuantityValue): Boolean; - calc def '!=' specializes BaseFunctions::'!=' (x: ScalarQuantityValue, y: ScalarQuantityValue): Boolean; + calc def '==' specializes DataFunctions::'==' (x: ScalarQuantityValue, y: ScalarQuantityValue): Boolean; - calc def Sqrt(x: ScalarQuantityValue): ScalarQuantityValue; + calc def sqrt(x: ScalarQuantityValue): ScalarQuantityValue; - calc def Floor(x: ScalarQuantityValue): ScalarQuantityValue; - calc def Round(x: ScalarQuantityValue): ScalarQuantityValue; + calc def floor (x: ScalarQuantityValue): ScalarQuantityValue; + calc def round (x: ScalarQuantityValue): ScalarQuantityValue; calc def ToString specializes BaseFunctions::ToString (x: ScalarQuantityValue): String; calc def ToInteger(x: ScalarQuantityValue): Integer; @@ -37,12 +43,16 @@ package QuantityCalculations { calc def ToReal(x: ScalarQuantityValue): Real; calc def ToDimensionOneValue(x: Real): DimensionOneValue; - calc def sum specializes ScalarFunctions::sum (collection: ScalarQuantityValue[0..*]): ScalarQuantityValue { - ScalarFunctions::sum0(collection, 0.0) + calc def sum specializes NumericalFunctions::sum (collection: ScalarQuantityValue[0..*]): ScalarQuantityValue { + private attribute zero : ScalarQuantityValue; + assert constraint { isZero(zero) } + NumericalFunctions::sum0(collection, zero) } - calc def product specializes ScalarFunctions::product (collection: ScalarQuantityValue[0..*]): ScalarQuantityValue { - ScalarFunctions::product1(collection, 1.0) + calc def product specializes NumericalFunctions::product (collection: ScalarQuantityValue[0..*]): ScalarQuantityValue { + private attribute one : ScalarQuantityValue; + assert constraint { isUnit(one) } + NumericalFunctions::product1(collection, one) } calc def ConvertQuantity(x: ScalarQuantityValue, targetMRef: ScalarMeasurementReference): ScalarQuantityValue; diff --git a/sysml.library/Domain Libraries/Quantities and Units/UnitsAndScales.sysml b/sysml.library/Domain Libraries/Quantities and Units/UnitsAndScales.sysml index cf4a8601..da49185b 100644 --- a/sysml.library/Domain Libraries/Quantities and Units/UnitsAndScales.sysml +++ b/sysml.library/Domain Libraries/Quantities and Units/UnitsAndScales.sysml @@ -55,7 +55,7 @@ package UnitsAndScales { * a VectorMeasurementReference) w.r.t. another (independent or reference) coordinate system. */ attribute def VectorMeasurementReference :> TensorMeasurementReference { - attribute :>> dimensions: Positive[1]; + attribute :>> dimensions: Positive[0..1]; attribute isOrthogonal: Boolean[1] default true; attribute placement: CoordinateTransformation[0..1]; } @@ -71,8 +71,7 @@ package UnitsAndScales { * and for consistency with tensor and vector measurement references. */ abstract attribute def ScalarMeasurementReference :> VectorMeasurementReference { - attribute :>> dimensions = 1; - attribute :>> order = 0; + attribute :>> dimensions = (); attribute :>> isOrthogonal = true; attribute :>> mRefs = self; attribute quantityDimension: QuantityDimension[1]; diff --git a/sysml.library/Domain Libraries/Quantities and Units/VectorCalculations.sysml b/sysml.library/Domain Libraries/Quantities and Units/VectorCalculations.sysml index 736d2e76..3875d9a1 100644 --- a/sysml.library/Domain Libraries/Quantities and Units/VectorCalculations.sysml +++ b/sysml.library/Domain Libraries/Quantities and Units/VectorCalculations.sysml @@ -1,14 +1,23 @@ package VectorCalculations { - import ScalarValues::*; - import Quantities::VectorQuantityValue; + private import ScalarValues::Boolean; + private import ScalarValues::Number; + private import Quantities::VectorQuantityValue; + + calc def isZeroVectorQuantity :> VectorFunctions::isZeroVector(: VectorQuantityValue[1]): Boolean; - /* Vector addition and subtraction */ - calc def '+' specializes NumericalFunctions::'+' (x: VectorQuantityValue, y: VectorQuantityValue): VectorQuantityValue; - calc def '-' specializes NumericalFunctions::'-' (x: VectorQuantityValue, y: VectorQuantityValue): VectorQuantityValue; - - /* Scalar-vector multiplication */ - calc def scalarVectorMult specializes NumericalFunctions::'*' (x: Real, y: VectorQuantityValue): VectorQuantityValue; - calc def vectorScalarMult specializes NumericalFunctions::'*' (x: VectorQuantityValue, y: Real): VectorQuantityValue; + /* Addition and subtraction */ + calc def '+' :> VectorFunctions::'+' (: VectorQuantityValue[1], : VectorQuantityValue[1]): VectorQuantityValue[1]; + calc def '-' :> VectorFunctions::'-' (: VectorQuantityValue[1], : VectorQuantityValue[1]): VectorQuantityValue[1]; + /* Multiplication and division */ + calc def scalarVectorMult :> VectorFunctions::scalarVectorMult (: Number[1], : VectorQuantityValue[1]): VectorQuantityValue[1]; + calc def vectorScalarMult :> VectorFunctions::vectorScalarMult (: VectorQuantityValue[1], : Number[1]): VectorQuantityValue[1]; + calc def vectorScalarDiv :> VectorFunctions::vectorScalarDiv (: Number[1], : VectorQuantityValue[1]): Number[1]; + calc def inner :> VectorFunctions::inner (: VectorQuantityValue, : VectorQuantityValue[1]): Number[1]; + alias '*' for scalarVectorMult; + + /* Norm and angle */ + calc def norm :> VectorFunctions::norm (: VectorQuantityValue[1]): Number[1]; + calc def angle :> VectorFunctions::angle (: VectorQuantityValue[1], : VectorQuantityValue[1]): Number[1]; } diff --git a/sysml.library/Kernel Library/CollectionFunctions.kerml b/sysml.library/Kernel Library/CollectionFunctions.kerml index 108442de..f405248c 100644 --- a/sysml.library/Kernel Library/CollectionFunctions.kerml +++ b/sysml.library/Kernel Library/CollectionFunctions.kerml @@ -6,6 +6,7 @@ package CollectionFunctions { private import Base::Anything; private import ScalarValues::*; private import SequenceFunctions::equals; + private import SequenceFunctions::includes; private import ControlFunctions::exists; import Collections::*; @@ -25,8 +26,12 @@ package CollectionFunctions { SequenceFunctions::notEmpty(col.elements) } - function contains(col: Collection[1], value: Anything[1]): Boolean[1] { - col.elements->exists {in x; x == value} + function contains(col: Collection[1], values: Anything[*]): Boolean[1] { + col.elements->includes(values) + } + + function containsAll(col1: Collection[1], col2: Collection[2]): Boolean[1] { + contains(col1, col2.elements) } function head(col: OrderedCollection[1]): Anything[0..1] { diff --git a/sysml.library/Kernel Library/Collections.kerml b/sysml.library/Kernel Library/Collections.kerml index 13e27eaf..cd3d1f5f 100644 --- a/sysml.library/Kernel Library/Collections.kerml +++ b/sysml.library/Kernel Library/Collections.kerml @@ -42,18 +42,28 @@ package Collections { * 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. 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 C programming language convention, - * namely the last index varies fastest. + * 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: Array can represent the generalized mathematical concept of an infinite matrix of any rank, i.e. not limited to rank two. + * 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. */ datatype Array :> OrderedCollection { // 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. - feature dimensions: Positive[1..*] ordered nonunique; + feature dimensions: Positive[0..*] ordered nonunique; feature rank: Natural[1] = size(dimensions); - feature flattenedSize: Natural[1] = dimensions->reduce '*'; + feature flattenedSize: Positive[1] = dimensions->reduce '*' ?? 1; inv { flattenedSize == size(elements) } } diff --git a/sysml.library/Kernel Library/ComplexFunctions.kerml b/sysml.library/Kernel Library/ComplexFunctions.kerml index abe7fc79..60107186 100644 --- a/sysml.library/Kernel Library/ComplexFunctions.kerml +++ b/sysml.library/Kernel Library/ComplexFunctions.kerml @@ -5,16 +5,23 @@ package ComplexFunctions { import ScalarValues::*; - feature i: Complex[1] = Rect(0.0, 1.0); + feature i: Complex[1] = rect(0.0, 1.0); - function Rect(re: Real[1], im: Real[1]): Complex[1]; - function Polar(abs: Real[1], arg: Real[1]): Complex[1]; + function rect(re: Real[1], im: Real[1]): Complex[1]; + function polar(abs: Real[1], arg: Real[1]): Complex[1]; - function Re(x: Complex[1]): Real[1]; - function Im(x: Complex[1]): Real[1]; + function re(x: Complex[1]): Real[1]; + function im(x: Complex[1]): Real[1]; - function Abs specializes NumericalFunctions::Abs (x: Complex[1]): Real[1]; - function Arg(x: Complex[1]): Real[1]; + function isZero specializes NumericalFunctions::isZero (x : Complex) { + re(x) == 0.0 and im(x) == 0.0 + } + function isUnit specializes NumericalFunctions::isUnit (x : Complex) { + re(x) == 1.0 and im(x) == 0.0 + } + + function abs specializes NumericalFunctions::abs (x: Complex[1]): Real[1]; + function arg(x: Complex[1]): Real[1]; function '+' specializes NumericalFunctions::'+' (x: Complex[1], y: Complex[0..1]): Complex[1]; function '-' specializes NumericalFunctions::'-' (x: Complex[1], y: Complex[0..1]): Complex[1]; @@ -28,11 +35,11 @@ package ComplexFunctions { function ToString specializes BaseFunctions::ToString (x: Complex[1]): String[1]; function ToComplex(x: String[1]): Complex[1]; - function sum specializes ScalarFunctions::sum (collection: Complex[0..*]): Complex[1] { - ScalarFunctions::sum0(collection, Rect(0.0, 0.0)) + function sum specializes NumericalFunctions::sum (collection: Complex[0..*]): Complex[1] { + NumericalFunctions::sum0(collection, rect(0.0, 0.0)) } - function product specializes ScalarFunctions::product (collection: Complex[0..*]): Complex[1] { - ScalarFunctions::product1(collection, Rect(1.0, 0.0)) + function product specializes NumericalFunctions::product (collection: Complex[0..*]): Complex[1] { + NumericalFunctions::product1(collection, rect(1.0, 0.0)) } } diff --git a/sysml.library/Kernel Library/ControlFunctions.kerml b/sysml.library/Kernel Library/ControlFunctions.kerml index a8b32a62..4af3e7de 100644 --- a/sysml.library/Kernel Library/ControlFunctions.kerml +++ b/sysml.library/Kernel Library/ControlFunctions.kerml @@ -6,8 +6,16 @@ package ControlFunctions { private import Base::Anything; private import ScalarValues::ScalarValue; private import ScalarValues::Boolean; - private import ScalarFunctions::Min; - private import ScalarFunctions::Max; + private import ScalarFunctions::min; + private import ScalarFunctions::max; + + abstract function '.' { + in feature source : Anything[0..*] nonunique { + abstract feature target : Anything[0..*] nonunique; + } + private feature chain is source.target; + chain + } abstract function '?'(test: Boolean[1]): Anything[0..*] ordered nonunique { abstract composite expr thenValue[0..1] (): Anything[0..*] ordered nonunique; @@ -84,12 +92,12 @@ package ControlFunctions { function minimize(collection: ScalarValue[1..*]): ScalarValue[1] { abstract composite expr fn[0..*] (argument: ScalarValue[1]): ScalarValue[1]; - collection->collect {in x; fn(x)}->reduce Min + collection->collect {in x; fn(x)}->reduce min } function maximize(collection: ScalarValue[1..*]): ScalarValue { abstract composite expr fn[0..*] (argument: ScalarValue[1]): ScalarValue[1]; - collection->collect {in x; fn(x)}->reduce Max + collection->collect {in x; fn(x)}->reduce max } } \ No newline at end of file diff --git a/sysml.library/Kernel Library/DataFunctions.kerml b/sysml.library/Kernel Library/DataFunctions.kerml index 24195409..2a9f3610 100644 --- a/sysml.library/Kernel Library/DataFunctions.kerml +++ b/sysml.library/Kernel Library/DataFunctions.kerml @@ -34,16 +34,5 @@ package DataFunctions { abstract function '==' specializes BaseFunctions::'=='(x: DataValue[0..1], y: DataValue[0..1]): Boolean[1]; - abstract function '..'(lower: DataValue[1], upper: DataValue[1]): DataValue[0..*] ordered; - - abstract function sum(collection: DataValue[0..*] ordered): DataValue[1]; - abstract function product(collection: DataValue[0..*] ordered): DataValue[1]; - - function sum0(collection: DataValue[0..*] ordered, zero: DataValue[1]): DataValue[1] { - collection->reduce '+' ?? zero - } - - function product1(collection: DataValue[0..*] ordered, one: DataValue[1]): DataValue[1] { - collection->reduce '*' ?? one - } + abstract function '..'(lower: DataValue[1], upper: DataValue[1]): DataValue[0..*] ordered; } \ No newline at end of file diff --git a/sysml.library/Kernel Library/IntegerFunctions.kerml b/sysml.library/Kernel Library/IntegerFunctions.kerml index 6bde559f..5440aa10 100644 --- a/sysml.library/Kernel Library/IntegerFunctions.kerml +++ b/sysml.library/Kernel Library/IntegerFunctions.kerml @@ -5,37 +5,37 @@ package IntegerFunctions { import ScalarValues::*; - function Abs specializes NumericalFunctions::Abs (x: Integer[1]): Natural[1]; + function abs specializes RationalFunctions::abs (x: Integer[1]): Natural[1]; - function '+' specializes NumericalFunctions::'+' (x: Integer[1], y: Integer[0..1]): Integer[1]; - function '-' specializes NumericalFunctions::'-' (x: Integer[1], y: Integer[0..1]): Integer[1]; - function '*' specializes NumericalFunctions::'*' (x: Integer[1], y: Integer[1]): Integer[1]; - function '/' specializes NumericalFunctions::'/' (x: Integer[1], y: Integer[1]): Rational; - function '**' specializes NumericalFunctions::'**' (x: Integer[1], y: Natural): Integer[1]; - function '^' specializes NumericalFunctions::'^' (x: Integer[1], y: Natural): Integer[1]; + function '+' specializes RationalFunctions::'+' (x: Integer[1], y: Integer[0..1]): Integer[1]; + function '-' specializes RationalFunctions::'-' (x: Integer[1], y: Integer[0..1]): Integer[1]; + function '*' specializes RationalFunctions::'*' (x: Integer[1], y: Integer[1]): Integer[1]; + function '/' specializes RationalFunctions::'/' (x: Integer[1], y: Integer[1]): Rational; + function '**' specializes RationalFunctions::'**' (x: Integer[1], y: Natural): Integer[1]; + function '^' specializes RationalFunctions::'^' (x: Integer[1], y: Natural): Integer[1]; function '%' specializes NumericalFunctions::'%' (x: Integer[1], y: Integer[1]): Integer[1]; - function '<' specializes NumericalFunctions::'<' (x: Integer[1], y: Integer[1]): Boolean[1]; - function '>' specializes NumericalFunctions::'>' (x: Integer[1], y: Integer[1]): Boolean[1]; - function '<=' specializes NumericalFunctions::'<=' (x: Integer[1], y: Integer[1]): Boolean[1]; - function '>=' specializes NumericalFunctions::'>=' (x: Integer[1], y: Integer[1]): Boolean[1]; + function '<' specializes RationalFunctions::'<' (x: Integer[1], y: Integer[1]): Boolean[1]; + function '>' specializes RationalFunctions::'>' (x: Integer[1], y: Integer[1]): Boolean[1]; + function '<=' specializes RationalFunctions::'<=' (x: Integer[1], y: Integer[1]): Boolean[1]; + function '>=' specializes RationalFunctions::'>=' (x: Integer[1], y: Integer[1]): Boolean[1]; - function Max specializes NumericalFunctions::Max (x: Integer[1], y: Integer[1]): Integer[1]; - function Min specializes NumericalFunctions::Min (x: Integer[1], y: Integer[1]): Integer[1]; + function max specializes RationalFunctions::max (x: Integer[1], y: Integer[1]): Integer[1]; + function min specializes RationalFunctions::min (x: Integer[1], y: Integer[1]): Integer[1]; function '==' specializes DataFunctions::'==' (x: Integer[0..1], y: Integer[0..1]): Boolean[1]; function '..' specializes ScalarFunctions::'..' (lower: Integer[1], upper: Integer[1]): Integer[0..*]; - function ToString specializes BaseFunctions::ToString (x: Integer[1]): String[1]; + function ToString specializes RationalFunctions::ToString (x: Integer[1]): String[1]; function ToNatural(x: Integer[1]): Natural[1]; function ToInteger(x: String[1]): Integer[1]; - function sum specializes ScalarFunctions::sum(collection: Integer[0..*]): Integer[1] { - ScalarFunctions::sum0(collection, 0) + function sum specializes RationalFunctions::sum(collection: Integer[0..*]): Integer[1] { + NumericalFunctions::sum0(collection, 0) } - function product specializes ScalarFunctions::product(collection: Integer[0..*]): Integer[1] { - ScalarFunctions::product1(collection, 1) + function product specializes RationalFunctions::product(collection: Integer[0..*]): Integer[1] { + NumericalFunctions::product1(collection, 1) } } diff --git a/sysml.library/Kernel Library/KerML.kerml b/sysml.library/Kernel Library/KerML.kerml index e2238e11..577af79f 100644 --- a/sysml.library/Kernel Library/KerML.kerml +++ b/sysml.library/Kernel Library/KerML.kerml @@ -71,8 +71,9 @@ package KerML { struct LiteralInfinity :> LiteralExpression; struct NullExpression :> Expression; struct OperatorExpression :> InvocationExpression; - struct PathStepExpression :> OperatorExpression; - struct PathSelectExpression :> OperatorExpression; + struct FeatureChainExpression :> OperatorExpression; + struct CollectExpression :> OperatorExpression; + struct SelectExpression :> OperatorExpression; struct Interaction :> Behavior, Association; struct ItemFlow :> Step, Connector; diff --git a/sysml.library/Kernel Library/NaturalFunctions.kerml b/sysml.library/Kernel Library/NaturalFunctions.kerml index 037f228a..bad9a9c2 100644 --- a/sysml.library/Kernel Library/NaturalFunctions.kerml +++ b/sysml.library/Kernel Library/NaturalFunctions.kerml @@ -15,7 +15,8 @@ package NaturalFunctions { function '<=' specializes IntegerFunctions::'<=' (x: Natural[1], y: Natural[1]): Boolean[1]; function '>=' specializes IntegerFunctions::'>=' (x: Natural[1], y: Natural[1]): Boolean[1]; - function Max specializes IntegerFunctions::Max (x: Natural[1], y: Natural[1]): Natural[1]; + function max specializes IntegerFunctions::max (x: Natural[1], y: Natural[1]): Natural[1]; + function min specializes IntegerFunctions::min (x: Natural[1], y: Natural[1]): Natural[1]; function '==' specializes IntegerFunctions::'==' (x: Natural[0..1], y: Natural[0..1]): Boolean[1]; diff --git a/sysml.library/Kernel Library/NumericalFunctions.kerml b/sysml.library/Kernel Library/NumericalFunctions.kerml index 89f2e533..054191ff 100644 --- a/sysml.library/Kernel Library/NumericalFunctions.kerml +++ b/sysml.library/Kernel Library/NumericalFunctions.kerml @@ -3,8 +3,12 @@ */ package NumericalFunctions { import ScalarValues::*; + private import ControlFunctions::reduce; - abstract function Abs(x: NumericalValue[1]): NumericalValue[1]; + abstract function isZero(x: NumericalValue[1]): Boolean; + abstract function isUnit(x : NumericalValue[1]): Boolean; + + abstract function abs(x: NumericalValue[1]): NumericalValue[1]; abstract function '+' specializes ScalarFunctions::'+' (x: NumericalValue[1], y: NumericalValue[0..1]): NumericalValue[1]; abstract function '-' specializes ScalarFunctions::'-' (x: NumericalValue[1], y: NumericalValue[0..1]): NumericalValue[1]; @@ -19,6 +23,19 @@ package NumericalFunctions { abstract function '<=' specializes ScalarFunctions::'<=' (x: NumericalValue[1], y: NumericalValue[1]): Boolean[1]; abstract function '>=' specializes ScalarFunctions::'>=' (x: NumericalValue[1], y: NumericalValue[1]): Boolean[1]; - abstract function Max specializes ScalarFunctions::Max (x: NumericalValue[1], y: NumericalValue[1]): NumericalValue[1]; - abstract function Min specializes ScalarFunctions::Min (x: NumericalValue[1], y: NumericalValue[1]): NumericalValue[1]; + abstract function max specializes ScalarFunctions::max (x: NumericalValue[1], y: NumericalValue[1]): NumericalValue[1]; + abstract function min specializes ScalarFunctions::min (x: NumericalValue[1], y: NumericalValue[1]): NumericalValue[1]; + + abstract function sum (collection: ScalarValue[0..*]): ScalarValue[1]; + abstract function product (collection: ScalarValue[0..*]): ScalarValue[1]; + + function sum0 (collection: NumericalValue[0..*], zero: ScalarValue[1]): ScalarValue { + inv { isZero(zero) } + collection->reduce '+' ?? zero + } + + function product1 (collection: ScalarValue[0..*], one: ScalarValue[1]): ScalarValue { + inv { isUnit(one) } + collection->reduce '*' ?? one + } } \ No newline at end of file diff --git a/sysml.library/Kernel Library/Objects.kerml b/sysml.library/Kernel Library/Objects.kerml index 50c1d2f2..f3b00443 100644 --- a/sysml.library/Kernel Library/Objects.kerml +++ b/sysml.library/Kernel Library/Objects.kerml @@ -9,8 +9,14 @@ package Objects { private import Occurrences::occurrences; private import Occurrences::HappensLink; private import Occurrences::SelfSameLifeLink; + private import Occurrences::WithinBoth; private import Performances::Performance; private import Performances::performances; + private import SequenceFunctions::isEmpty; + private import SequenceFunctions::notEmpty; + private import SequenceFunctions::union; + private import CollectionFunctions::contains; + private import ScalarValues::Integer; /** * Object is the most general class of structural occurrences that may change over time. @@ -26,7 +32,12 @@ package Objects { /** * Performances which are enacted by this object. */ - abstract step enactedPerformances: Performance[0..*] subsets involvingPerformances, suboccurrences; + abstract step enactedPerformances: Performance[0..*] subsets involvingPerformances, timeEnclosedOccurrences; + + /** + * A space boundary that is a structured space object. + */ + portion structuredSpaceBoundary : StructuredSpaceObject[0..1] subsets spaceBoundary; } /** @@ -56,4 +67,81 @@ package Objects { */ abstract feature binaryLinkObjects: BinaryLinkObject[0..*] nonunique subsets binaryLinks, linkObjects; -} \ No newline at end of file + + /** + * A Body is an Object of inner space dimension 3. + */ + struct all Body specializes Object { + feature redefines innerSpaceDimension = 3; + } + + /** + * A Surface is an Object of inner space dimension 2. + */ + struct all Surface specializes Object { + feature redefines innerSpaceDimension = 2; + /* The number of "holes" in this Surface, assuming it isClosed. */ + feature genus : Integer[0..1] default 0; + + inv { notEmpty(genus) implies (isClosed & genus >= 0) } + } + + /* + * A Curve is an Object of inner space dimension 1. + */ + struct all Curve specializes Object { + feature redefines innerSpaceDimension = 1; + } + + /* + * A Point is an Object of inner space dimension 0. + */ + struct all Point specializes Object { + feature redefines innerSpaceDimension = 0; + } + + /* + * A StructuredSpaceObject is an Object that is broken up into smaller structured space objects (cells) of + * the same or lower inner space dimension: faces that are surfaces, edges that are curves, and vertices + * that are points, with edges and vertices on the boundary of faces, and vertices on the boundary of + * edges. Cells overlap when a structured space object is closed, as required to be a space boundary of + * an object (faces overlap at their edges and/or vertices, while edges overlap at their vertices). The + * inner space dimension of structured space object is the highest of their cells. + */ + abstract struct StructuredSpaceObject specializes Object { + + abstract portion feature structuredSpaceObjectCells : StructuredSpaceObject[1..*] subsets Occurrence::spaceSlices + { feature cellOrientation : Integer [0..1]; + inv { notEmpty(cellOrientation) implies (cellOrientation >= -1 & cellOrientation <= 1) } + } + + portion feature faces : Surface[0..*] ordered subsets structuredSpaceObjectCells { + derived feature redefines spaceBoundary; + inv { isEmpty(spaceBoundary) == isEmpty(union(edges, vertices)) } + inv { notEmpty(spaceBoundary) implies contains(spaceBoundary.unionsOf, union(edges, vertices)) } + } + + portion feature edges : Curve[0..*] ordered subsets structuredSpaceObjectCells { + derived feature redefines spaceBoundary; + inv { isEmpty(spaceBoundary) == isEmpty(vertices) } + inv { notEmpty(spaceBoundary) implies contains(spaceBoundary.unionsOf, vertices) } + } + + portion feature vertices : Point[0..*] ordered subsets structuredSpaceObjectCells; + + derived feature redefines innerSpaceDimension = + (if notEmpty(faces)? 2 else (if notEmpty(edges)? 1 else 0)); + + connector feE :WithinBoth + from thisOccurrence :> faces.edges [0..*] + to thatOccuurence :> edges [0..*]; + + connector evV :WithinBoth + from thisOccurrence :> edges.vertices [0..*] + to thatOccuurence :> vertices [0..*]; + + connector fvV :WithinBoth + from thisOccurrence :> faces.vertices [0..*] + to thatOccuurence :> vertices [0..*]; + } +} diff --git a/sysml.library/Kernel Library/Occurrences.kerml b/sysml.library/Kernel Library/Occurrences.kerml index 938a709c..53aff80f 100644 --- a/sysml.library/Kernel Library/Occurrences.kerml +++ b/sysml.library/Kernel Library/Occurrences.kerml @@ -1,295 +1,563 @@ -/** - * This package defines the concept of occurrences and the associations between them - * that assert relationships modeling four-dimensional semantics. - * [Currently this is primarily time semantics.] - */ -package Occurrences { - private import Base::Anything; - private import Base::things; - private import Base::DataValue; - private import Links::*; - - /** - * Occurrence is the most general classifier of entities that have identity and - * may occur over time. - * - * The features of Occurrence specify the semantics of portions, slices and - * snapshots of an occurrence over time. - */ - abstract class Occurrence specializes Anything { - private import SequenceFunctions::*; - private import ControlFunctions::forAll; - - feature portionOfLife : Life[1] subsets portionOf; - - feature self : Occurrence[1] redefines Anything::self subsets timeSlices, sameLifeOccurrences; - feature sameLifeOccurrences : Occurrence[1..*] subsets things; - - /** - * Occurrences that end before this occurrence starts. - */ - feature predecessors: Occurrence[0..*] subsets occurrences; - - /** - * Occurrences that start after this occcurrence ends. - */ - feature successors: Occurrence[0..*] subsets occurrences; - - /** - * Occurrences that end just before this occurrence starts, with no - * possibility of other occurrences happening in the time between them. - */ - feature immediatePredecessors: Occurrence[0..*] subsets predecessors; - - /** - * Occurrences that start just after this occurrence ends, with no - * possibility of other occurrences happening in the time between them. - */ - feature immediateSuccessors: Occurrence[0..*] subsets successors; - - /** - * Occurrences that start no earlier than and end no later than - * this occurrence, including at least this occurrence. - */ - feature suboccurrences: Occurrence[1..*] subsets occurrences; - - /** - * Occurrences that are portions of this occurrence, including at - * least this occurrence. - */ - portion feature portions: Occurrence[1..*] subsets suboccurrences; - - /** - * Occurrences of which this occurrence is a portion, including at - * least this occurrence. - */ - feature portionOf : Occurrence[1..*]; - - /** - * Portions of an occurrence over some slice of time, including at - * least this occurrence. - */ - portion feature timeSlices: Occurrence[1..*] subsets portions; - - /** - * Occurrences of which this occurrence is a time slice, including at - * least this occurrence. - */ - feature timeSliceOf : Occurrence[1..*] subsets portionOf; - - /** - * Time slices of an occurrence that happen at a single instant of time - * (i.e., have no duration). - */ - portion feature all snapshots: Occurrence[1..*] subsets timeSlices; - inv { snapshots->forAll {in s:Occurrence; s.startShot == s.endShot} } - inv { snapshots == union(startShot, union(middleShots, endShot)) } - - /** - * Occurrences of which this occurrence is a snapshot. - */ - feature snapshotOf : Occurrence[0..*] subsets timeSliceOf; - - /** - * The snapshot representing the start of the occurrence in time. - */ - portion feature startShot: Occurrence[1] subsets snapshots; - - /** - * The snapshots in between the startShot and endShot. There are none - * when the startShot and endShot are the same. - */ - portion feature all middleShots: Occurrence[0..*] subsets snapshots; - inv { isEmpty(middleShots) == (startShot == endShot) } - - /** - * The snapshot at the end of the occurrence in time. - */ - portion feature endShot: Occurrence[1] subsets snapshots; - - /** - * The startShot happens before all middleShots. - */ - succession startShot[1] then middleShots[0..*]; - - /** - * The endShot happens after all middleShots. - */ - succession middleShots[0..*] then endShot[1]; - - /** - * The incoming transfers received by this occurrence. - */ - feature incomingTransfers: Transfers::Transfer[0..*] subsets Transfers::transfers { - end feature redefines source; - end feature redefines target; - } - - /** - * The incoming transfers with this occurrence as the target. - */ - feature all incomingTransfersToSelf subsets incomingTransfers { - end feature redefines source; - end feature redefines target; - } - binding incomingTransfersToSelf.target = self; - - /** - * The outgoing transfers sent from this occurrence. - */ - feature outgoingTransfers: Transfers::Transfer[0..*] subsets Transfers::transfers { - end feature redefines source; - end feature redefines target; - } - - /** - * The outgoing transfers with this occurrence as the source. - */ - feature all outgoingTransfersFromSelf subsets outgoingTransfers { - end feature redefines source; - end feature redefines target; - } - binding outgoingTransfersFromSelf.source = self; - } - - abstract class all Life specializes Occurrence { - /** - * Lives are only portions of themselves. - */ - binding portionOf = self; - } - - abstract feature occurrences: Occurrence[0..*] nonunique subsets things; - - /** - * SelfSameLifeLink is a binary association that is equivalent to SelfLink it the - * linked things are DataValues, but asserts that the link things are portions of - * the same Life if they are Occurrences. A SelfSameLink is not itself an Occurrence - * (SelfSameLifeLink is disjoint with LinkObject). - */ - assoc all SelfSameLifeLink specializes BinaryLink { - - end feature myselfSameLife: Anything[1..*] redefines source; - end feature selfSameLife: Anything[1..*] redefines target; - - feature all sourceOccurrence : Occurrence [0..1] subsets myselfSameLife; - feature all targetOccurrence : Occurrence [0..1] subsets selfSameLife, sourceOccurrence.sameLifeOccurrences; - binding oSelf of sourceOccurrence.portionOfLife = targetOccurrence.portionOfLife; - - feature all sourceDataValue : DataValue [0..1] subsets myselfSameLife; - feature all targetDataValue : DataValue [0..1] subsets selfSameLife; - binding dSelf of sourceDataValue = targetDataValue; - } - - subclassifier SelfLink specializes SelfSameLifeLink; - - /** - * HappensLink is the base of the associations that assert temporal relationships - * between a sourceOccurrence and a targetOccurrence. Because HappensLinks assert - * temporal relationships, they cannot themselves be Occurrences that happen in time. - * Therefore HappensLink is disjoint with LinkObject, that is, no HappensLink can - * also be a LinkObject. - */ - assoc HappensLink specializes BinaryLink { - end feature sourceOccurrence: Occurrence[0..*]; - end feature targetOccurrence: Occurrence[0..*]; - } - - /** - * HappensDuring asserts that the shorterOccurrence happens during the longerOccurrence. - * That is, the time interval of the shorterOccurrence is completely within that of the - * longerOccurrence, or every snapshot of the shorterOccurrence happens while (at the - * same time as) some snapshot of the longerOccurrence. Note that this means every - * occurrence happens during itself. - */ - assoc HappensDuring specializes HappensLink { - end feature shorterOccurrence: Occurrence[1..*] redefines sourceOccurrence subsets longerOccurrence.suboccurrences; - end feature longerOccurrence: Occurrence[1..*] redefines targetOccurrence; - - /* - * HappensDuring and HappensBefore constrain each other. All predecessors of - * (occurrences happening before) a HappenDuring's longerOccurrence are also - * predecessors of its shorterOccurrence. Inversely, all successors (occurrences - * happening after) its longerOccurrence are also successors of its shorterOccurrence. - */ - - subset longerOccurrence.predecessors subsets shorterOccurrence.predecessors; - subset longerOccurrence.successors subsets shorterOccurrence.successors; - - subset shorterOccurrence.suboccurrences subsets longerOccurrence.suboccurrences; - } - - /** - * HappensWhile asserts that two occurrences happen during each other, that is, they - * each start at the same time and end at the same time. - */ - assoc HappensWhile specializes HappensDuring { - end feature thisOccurrence: Occurrence[1..*] redefines shorterOccurrence; - end feature thatOccurrence: Occurrence[1..*] redefines longerOccurrence; - - connector :HappensDuring - from shorterOccurrence :> thatOccurrence - to longerOccurrence :> thisOccurrence; - } - - /** - * HappensBefore asserts that the earlierOccurrence happens before the laterOccurrence. - * That is, the time interval of the earlierOccurrence is completely before that of the - * laterOccurrence, or every snapshot of the earlierOccurrence happens before every - * snapshot of the laterOccurrence. Note that this means no occurrence happens before itself. - */ - assoc HappensBefore specializes HappensLink { - end feature earlierOccurrence: Occurrence[0..*] redefines BinaryLink::source subsets laterOccurrence.predecessors; - end feature laterOccurrence: Occurrence[0..*] redefines BinaryLink::target subsets earlierOccurrence.successors; - - subset laterOccurrence.successors subsets earlierOccurrence.successors; - - inv { earlierOccurrence != laterOccurrence } - } - - /** - * HappensJustBefore is HappensBefore asserting that the earlierOccurrence happens just - * before the laterOccurrence, with with no possibility of other occurrences happening in the - * time between them. - */ - assoc HappensJustBefore specializes HappensBefore { - end feature redefines earlierOccurrence: Occurrence[0..*] subsets laterOccurrence.immediatePredecessors; - end feature redefines laterOccurrence: Occurrence[0..*] subsets earlierOccurrence.immediateSuccessors; - - disjoint earlierOccurrence.successors from laterOccurrence.predecessors; - } - - /** - * PortionOf asserts one occurrence is a portion of another, including at least itself. - */ - assoc PortionOf specializes HappensDuring { - end feature portionedOccurrence: Occurrence[1..*] redefines longerOccurrence subsets portionOccurrence.portionOf; - end feature portionOccurrence: Occurrence[1..*] redefines shorterOccurrence subsets portionedOccurrence.portions; - } - - /** - * TimeSliceOf asserts once occurrence is a time slice of another, including at least itself. - */ - assoc TimeSliceOf specializes PortionOf { - end feature timeSlicedOccurrence: Occurrence[1..*] redefines portionedOccurrence subsets timeSliceOccurrence.timeSliceOf; - end feature timeSliceOccurrence: Occurrence[1..*] redefines portionOccurrence subsets timeSlicedOccurrence.timeSlices; - } - - /** - * SnapshotsOf asserts once occurrence is a snapshot of another. - */ - assoc SnapshotOf specializes TimeSliceOf { - end feature snapshottedOccurrence: Occurrence[1..*] redefines timeSlicedOccurrence subsets snapshotOcccurrence.snapshotOf; - end feature snapshotOcccurrence: Occurrence[1..*] redefines timeSliceOccurrence subsets snapshottedOccurrence.snapshots; - } - - /** - * happensBeforeLinks is a specialization of binaryLinks restricted to type HappensBefore. - * It is the default subsetting for succession connectors. - */ - feature happensBeforeLinks: HappensBefore[0..*] nonunique subsets binaryLinks { - end feature earlierOccurrence: Occurrence[0..*] redefines HappensBefore::earlierOccurrence, binaryLinks::source; - end feature laterOccurrence: Occurrence[0..*] redefines HappensBefore::laterOccurrence, binaryLinks::target; - } - -} \ No newline at end of file +/** + * This package defines modeling constructs for anything existing or occurring in time and space, with + * associations between them that assert temporal and spatial relationships. + */ +package Occurrences { + private import Base::Anything; + private import Base::things; + private import Base::DataValue; + private import ScalarValues::Natural; + private import ScalarValues::Boolean; + private import Links::*; + private import Collections::Set; + private import Collections::OrderedSet; + private import SequenceFunctions::includes; + private import CollectionFunctions::contains; + + /** + * Occurrence is the most general classifier of entities that have identity and + * occur over time and space. + * + * The features of Occurrence specify the semantics of associations between occurrences that + * assert complete inclusion and exclusion in time or space, or both, which includes + * portions of an occurrence (having the same identity). Portions include slices and shots + * over time and space. + */ + abstract class Occurrence specializes Anything { + private import SequenceFunctions::*; + + feature portionOfLife: Life[1] subsets portionOf; + + feature self: Occurrence[1] redefines Anything::self subsets timeSlices, spaceSlices, sameLifeOccurrences; + feature sameLifeOccurrences: Occurrence[1..*] subsets things; + + /** + * Occurrences that end before this occurrence starts. + */ + feature predecessors: Occurrence[0..*] subsets occurrences; + + /** + * Occurrences that start after this occcurrence ends. + */ + feature successors: Occurrence[0..*] subsets occurrences; + + /** + * Occurrences that end just before this occurrence starts, with no + * possibility of other occurrences happening in the time between them. + */ + feature immediatePredecessors: Occurrence[0..*] subsets predecessors; + + /** + * Occurrences that start just after this occurrence ends, with no + * possibility of other occurrences happening in the time between them. + */ + feature immediateSuccessors: Occurrence[0..*] subsets successors; + + /** + * Occurrences that start no earlier than and end no later than + * this occurrence, including at least this occurrence. + */ + feature timeEnclosedOccurrences: Occurrence[1..*] subsets occurrences; + + /** + * Occurrences that this one completely includes in space (not necessarily in time), + * including this one. + */ + feature spaceEnclosedOccurrences: Occurrence[1..*] subsets occurrences; + + /** + * Occurrences that this one completely includes in both space and time, + * including this one. + */ + feature spaceTimeEnclosedOccurrences: Occurrence[1..*] subsets timeEnclosedOccurrences, spaceEnclosedOccurrences; + + /** + * All space time enclosed occurrences that take up zero time and space. + */ + feature all spaceTimeEnclosedPoints : Occurrence[1..*] subsets spaceTimeEnclosedOccurrences { + redefines innerSpaceDimension = 0; + binding startShot[1] = endShot[1]; + } + + /** + * The number of variables need to identify space points in this occurrence, from 0 + * to 3, without regard to higher dimensional spaces it might be emedded in. + */ + feature innerSpaceDimension : Natural [1]; + inv { innerSpaceDimension >= 0 & innerSpaceDimension <= 3 } + + /** + * For occurrences of innerSpaceDimension 1 or 2, the number of variables need to + * identify their space points in higher dimensions they might be embedded in, from + * the innerSpaceDimension to 3. An outerSpaceDimension equal to innerSpaceDimension + * indicates the occurrence is spatially straight (innerSpaceDimension 1 embedded in + * 2 or 3 dimensions) or flat (innerSpaceDimension 2 embedded in 3 dimensions). + */ + feature outerSpaceDimension : Natural [0..1]; + inv { notEmpty(outerSpaceDimension) implies + (outerSpaceDimension >= innerSpaceDimension & outerSpaceDimension <= 3) } + + /** + * All spaceTimeEnclosedOccurrences that have the same portionOfLife (considered the same + * thing occurring), see PortionOf. + */ + portion feature all portions: Occurrence[1..*] subsets spaceTimeEnclosedOccurrences; + + /** + * Occurrences of which this occurrence is a portion, including at + * least this occurrence. + */ + feature portionOf : Occurrence[1..*]; + + /** + * Portions of an occurrence taking up all of its space over some period of time, + * including at least this occurrence. + */ + portion feature timeSlices: Occurrence[1..*] subsets portions; + + /** + * Occurrences of which this occurrence is a time slice, including at least this + * occurrence. + */ + feature timeSliceOf : Occurrence[1..*] subsets portionOf; + + /** + * Time slices of an occurrence that happen at a single instant of time + * (i.e., have no duration). + */ + portion feature all snapshots: Occurrence[1..*] subsets timeSlices { + binding startShot[1] = endShot[1]; + } + inv { snapshots == union(startShot, union(middleTimeSlice.snapshots, endShot)) } + + /** + * Occurrences of which this occurrence is a snapshot. + */ + feature snapshotOf : Occurrence[0..*] subsets timeSliceOf; + + /** + * The snapshot representing the start of the occurrence in time. + */ + portion feature startShot: Occurrence[1] subsets snapshots; + + /** + * A time slice that takes all the time between the start shot and end shot. There + * is none when the startShot and endShot are the same. + */ + portion feature middleTimeSlice: Occurrence[0..1] subsets timeSlices; + inv { isEmpty(middleTimeSlice) == (startShot == endShot) } + + /** + * The startShot happens immediately before the middle time slice. + */ + connector :HappensJustBefore + from earlierOccurrence :> startShot [1] + to laterOccurrence :> middleTimeSlice [0..1]; + + /** + * The snapshot at the end of the occurrence in time. + */ + portion feature endShot: Occurrence[1] subsets snapshots; + + /** + * The endShot happens after the middle time slice. + */ + connector :HappensJustBefore + from earlierOccurrence :> middleTimeSlice [0..1] + to laterOccurrence :> endShot [1]; + + /** + * Portions of this occurrence that extend for exactly the same time and some or all + * the space, relative to spatial location of this occurrence, including at least + * this occurrence. + + */ + portion feature spaceSlices: Occurrence[1..*] subsets portions; + + /** + * Occurrences of which this occurrence is a space slice, including at least this + * occurrence. + */ + feature spaceSliceOf: Occurrence[1..*] subsets portionOf; + + /** + * All spaceSlices of this occurrence that are of a lower inner space dimension than it. + */ + portion feature spaceShots: Occurrence[1..*] subsets spaceSlices; + + /** + * Occurrences of which this occurrence is a space shot. + */ + feature spaceShotOf: Occurrence[1..*] subsets spaceSliceOf; + + /** + * Sets of occurrences, where the time and space taken by all the occurrences in each + * set together is the same as taken by this occurrence (all four dimensional points in + * the occurrences of each set are at the same time and space as those of this + * occurrence). + */ + feature unionsOf: Set[0..*] { + feature redefines elements: Occurrence[0..*]; + feature union: Occurrence[0..1]; + + connector :Within + from smallerOccurrence :> elements [0..*] + to largerOccurrence :> union [1]; + connector :Within + from smallerOccurrence :> union.spaceTimeEnclosedPoints [0..*] + to largerOccurrence :> elements [1..*]; + } + binding unionsOf.union[0..1] = self[1]; + + /** + * Sets of occurrences, where the time and space taken in common between the occurrences + * in each set is at the same as taken by this occurrence (all four dimensional points + * common to the occurrences in each set are at the same time and space as those in this + * occurrence). + */ + feature intersectionsOf: Set[0..*] { + feature redefines elements: Occurrence[0..*] { + feature all notIntersection: Occurrence[0..*] subsets spaceTimeEnclosedPoints; + } + feature intersection: Occurrence[0..1]; + + connector :Within + from smallerOccurrence :> intersection [1] + to largerOccurrence :> elements [0..*]; + connector :Without + from separateOccurrenceToo :> elements.notIntersection [0..*] + to separateOccurrence :> intersection [1]; + connector :Without + from separateOccurrenceToo :> elements.notIntersection [0..*] + to separateOccurrence :> elements [1..*]; + } + binding intersectionsOf.intersection[0..1] = self[1]; + + /** + * Ordered sets of occurrences, where the time and space taken by first occurrence in + * each set that is not in the time and space taken by the remaining occurrences is the + * same as taken by this occurrence (all four dimensional points in the minuend that are + * not in any subtrahend are at the same time and space as those in this occurrence). + */ + feature differencesOf: OrderedSet[0..*] { + feature redefines elements: Occurrence[0..*]; + feature difference: Occurrence[0..1]; + feature minuend: Occurrence [0..1] subsets elements, interdiff.elements = head(elements); + feature subtrahend: Occurrence[*] subsets elements = tail(elements); + feature interdiff: Set [0..1] { + feature redefines elements: Occurrence[1..*]; + feature all notSubtrahend: Occurrence [0..*] subsets elements; + } + + connector :Without + from separateOccurrenceToo :> interdiff.notSubtrahend [0..*] + to separateOccurrence :> subtrahend [1..*]; + + inv { isEmpty(difference) == isEmpty(interdiff) } + inv { notEmpty(difference) implies (difference.intersectionsOf == interdiff) } + } + binding differencesOf.difference[0..1] = self[1]; + + /** + * A space slice of this occurrence that includes all its space shots except the + * space boundary, which must exist and be outsideOf it. The space interior must be + * of the same inner space dimension as this occurrence, except if it is zero, + * whereupon there is no space interior. + */ + portion feature spaceInterior: Occurrence[0..1] subsets spaceSlices; + + /** + * An Occurrence of which this one is the space interior. + */ + feature spaceInteriorOf: Occurrence[0..1] subsets spaceSliceOf; + inv { notEmpty(spaceInterior) implies spaceInterior.innerSpaceDimension == innerSpaceDimension } + inv { innerSpaceDimension == 0 implies isEmpty(spaceInterior) } + + /** + * A space shot of this Occurrence that is not among those of its space interior, of + * which it must be outside. It must have no spaceBoundary. + */ + portion feature spaceBoundary: Occurrence[0..1] subsets spaceShots { + feature redefines isClosed = true; + } + + /** + * An Occurrence of which this one is the space boundary. + */ + feature spaceBoundaryOf: Occurrence[0..*] subsets spaceShotOf; + + inv { isClosed implies contains(self.unionsOf, union(spaceBoundary, spaceInterior)) } + + connector :OutsideOf + from separateSpaceToo :> spaceInterior [0..1] + to separateSpace :> spaceBoundary [1]; + + /** + * Tells whether an occurrence has a spaceBoundary, true if it does, false otherwise. + */ + feature isClosed : Boolean [1]; + inv { isClosed == isEmpty(spaceBoundary) } + + /** + * The incoming transfers received by this occurrence. + */ + feature incomingTransfers: Transfers::Transfer[0..*] subsets Transfers::transfers { + end feature redefines source; + end feature redefines target; + } + + /** + * The incoming transfers with this occurrence as the target. + */ + feature all incomingTransfersToSelf subsets incomingTransfers { + end feature redefines source; + end feature redefines target; + } + binding incomingTransfersToSelf.target = self; + + /** + * The outgoing transfers sent from this occurrence. + */ + feature outgoingTransfers: Transfers::Transfer[0..*] subsets Transfers::transfers { + end feature redefines source; + end feature redefines target; + } + + /** + * The outgoing transfers with this occurrence as the source. + */ + feature all outgoingTransfersFromSelf subsets outgoingTransfers { + end feature redefines source; + end feature redefines target; + } + binding outgoingTransfersFromSelf.source = self; + } + + abstract class all Life specializes Occurrence { + /** + * Lives are only portions of themselves. + */ + binding portionOf = self; + } + + abstract feature occurrences: Occurrence[0..*] nonunique subsets things; + + /** + * SelfSameLifeLink is a binary association that is equivalent to SelfLink it the + * linked things are DataValues, but asserts that the link things are portions of + * the same Life if they are Occurrences. A SelfSameLink is not itself an Occurrence + * (SelfSameLifeLink is disjoint with LinkObject). + */ + assoc all SelfSameLifeLink specializes BinaryLink { + + end feature myselfSameLife: Anything[1..*] redefines source; + end feature selfSameLife: Anything[1..*] redefines target; + + feature all sourceOccurrence : Occurrence [0..1] subsets myselfSameLife; + feature all targetOccurrence : Occurrence [0..1] subsets selfSameLife, sourceOccurrence.sameLifeOccurrences; + binding oSelf of sourceOccurrence.portionOfLife = targetOccurrence.portionOfLife; + + feature all sourceDataValue : DataValue [0..1] subsets myselfSameLife; + feature all targetDataValue : DataValue [0..1] subsets selfSameLife; + binding dSelf of sourceDataValue = targetDataValue; + } + + subclassifier SelfLink specializes SelfSameLifeLink; + + /** + * HappensLink is the most general associations that assert temporal relationships between a + * sourceOccurrence and a targetOccurrence. Because HappensLinks assert temporal + * relationships, they cannot themselves be Occurrences that happen in time. Therefore + * HappensLink is disjoint with LinkObject, that is, no HappensLink can also be a + * LinkObject. + */ + assoc HappensLink specializes BinaryLink { + end feature sourceOccurrence: Occurrence[0..*] redefines BinaryLink::source; + end feature targetOccurrence: Occurrence[0..*] redefines BinaryLink::target; + } + + /** + * HappensDuring asserts that the shorterOccurrence happens during the longerOccurrence. + * That is, the time interval of the shorterOccurrence is completely within that of the + * longerOccurrence, or every snapshot of the shorterOccurrence happens while (at the + * same time as) some snapshot of the longerOccurrence. Note that this means every + * Occurrence HappensDuring itself and that HappensDuring is transitive. + */ + assoc HappensDuring specializes HappensLink { + end feature shorterOccurrence: Occurrence[1..*] redefines sourceOccurrence subsets longerOccurrence.timeEnclosedOccurrences; + end feature longerOccurrence: Occurrence[1..*] redefines targetOccurrence; + + /* + * HappensDuring and HappensBefore constrain each other. All predecessors of + * (occurrences happening before) a HappenDuring's longerOccurrence are also + * predecessors of its shorterOccurrence. Inversely, all successors (occurrences + * happening after) its longerOccurrence are also successors of its shorterOccurrence. + */ + + subset longerOccurrence.predecessors subsets shorterOccurrence.predecessors; + subset longerOccurrence.successors subsets shorterOccurrence.successors; + + subset shorterOccurrence.timeEnclosedOccurrences subsets longerOccurrence.timeEnclosedOccurrences; + } + + /** + * HappensWhile asserts that two occurrences happen during each other, that is, they + * each start at the same time and end at the same time. + */ + assoc HappensWhile specializes HappensDuring { + end feature thisOccurrence: Occurrence[1..*] redefines shorterOccurrence; + end feature thatOccurrence: Occurrence[1..*] redefines longerOccurrence; + + connector :HappensDuring + from shorterOccurrence :> thatOccurrence [1] + to longerOccurrence :> thisOccurrence [1]; + } + + /** + * InsideOf asserts that its largerSpace completely overlaps its smallerSpace in space (not + * necessarily in time, see HappensDuring). That is, all four dimensional points of the + * smallerSpace are in the spatial extent of the largerSpace. Note that this means every + * Occurrence is InsideOf itself and that InsideOf is transitive. + */ + assoc InsideOf specializes BinaryLink { + end feature smallerSpace: Occurrence[1..*] redefines source, largerSpace.spaceEnclosedOccurrences; + end feature largerSpace: Occurrence[1..*] redefines target; + + subset smallerSpace.spaceEnclosedOccurrences subsets largerSpace.spaceEnclosedOccurrences; + + inv { includes(largerSpace.timeEnclosedOccurrences, smallerSpace) implies (self istype Within) } + } + + /** + * Within asserts that its largerOccurrence completely overlaps its smallerOccurrence in + * time and space. That is, all four dimensional points of the smallerOccurrence happen + * during and are inside of the largerOccurrence. This means every occurrence is Within + * itself and Within is transitive. + */ + assoc all Within specializes HappensDuring, InsideOf { + end feature smallerOccurrence: Occurrence[1..*] redefines shorterOccurrence, smallerSpace + subsets largerOccurrence.spaceTimeEnclosedOccurrences; + end feature largerOccurrence: Occurrence[1..*] redefines longerOccurrence, largerSpace; + } + + /** + * WithinBoth asserts that two occurrences are Within each other, that is, they occupy the + * same four dimensional region. Note that this means every Occurrence is WithinBoth with + * itself and transitive. + */ + assoc WithinBoth specializes Within { + end feature thisOccurrence: Occurrence[1..*] redefines smallerOccurrence; + end feature thatOccurrence: Occurrence[1..*] redefines largerOccurrence; + + connector :Within + from smallerOccurrence :> thatOccurrence [1] + to largerOccurrence :> thisOccurrence [1]; + } + + /** + * PortionOf asserts one occurrence is a portion of another, including at least itself. + */ + assoc PortionOf specializes Within { + end feature portionOccurrence: Occurrence[1..*] redefines smallerOccurrence subsets portionedOccurrence.portions; + end feature portionedOccurrence: Occurrence[1..*] redefines largerOccurrence subsets portionOccurrence.portionOf; + + binding portionOccurrence.portionOfLife[1] = portionedOccurrence.portionOfLife[1]; + } + + /** + * TimeSliceOf asserts one occurrence is a time slice of another, including at least itself. + */ + assoc TimeSliceOf specializes PortionOf { + end feature timeSliceOccurrence: Occurrence[1..*] redefines portionOccurrence subsets timeSlicedOccurrence.timeSlices; + end feature timeSlicedOccurrence: Occurrence[1..*] redefines portionedOccurrence subsets timeSliceOccurrence.timeSliceOf; + } + + /** + * SnapshotsOf asserts one occurrence is a snapshot of another. + */ + assoc SnapshotOf specializes TimeSliceOf { + end feature snapshotOcccurrence: Occurrence[1..*] redefines timeSliceOccurrence subsets snapshottedOccurrence.snapshots; + end feature snapshottedOccurrence: Occurrence[0..*] redefines timeSlicedOccurrence subsets snapshotOcccurrence.snapshotOf; + } + + /** + * SpaceSliceOf asserts that it spaceSliceOccurrence extends for exactly the same time and + * some or all the space of the spaceSlicedOccurrence and that the spaceSliceOccurrence is + * of the same of lower innerSpaceDimension than the spaceSliceOccurrence. Note that this + * means every occurrence is a SpaceSliceOf itself and SpaceSliceOf is transitive. + */ + assoc SpaceSliceOf specializes PortionOf { + end feature spaceSliceOccurrence: Occurrence[1..*] redefines portionOccurrence subsets spaceSlicedOccurrence.spaceSlices; + end feature spaceSlicedOccurrence: Occurrence[1..*] redefines portionedOccurrence subsets spaceSliceOccurrence.spaceSliceOf; + + inv { spaceSliceOccurrence.innerSpaceDimension <= spaceSlicedOccurrence.innerSpaceDimension } + } + + /** + * SpaceShotOf asserts that its spaceShotOccurrence is of a lower inner space dimension than + * it spaceShottedOccurrence. + */ + assoc SpaceShotOf specializes SpaceSliceOf { + end feature spaceShotOcccurrence: Occurrence[1..*] redefines spaceSliceOccurrence subsets spaceShottedOccurrence.spaceShots; + end feature spaceShottedOccurrence: Occurrence[1..*] redefines spaceSlicedOccurrence subsets spaceShotOcccurrence.spaceShotOf; + } + + /** + * Without is the most general association that asserts complete separation (no overlap) in + * either space or time, or both, between two occurrences. That is, no four dimensional + * points are in both occurrences. Note that this means no Occurrence is Without itself. + */ + assoc Without specializes BinaryLink { + end feature separateOccurrenceToo: Occurrence[0..*] redefines BinaryLink::source; + end feature separateOccurrence: Occurrence[0..*] redefines BinaryLink::target; + + inv { separateOccurrenceToo != separateOccurrence } + } + + /** + * HappensBefore asserts that the earlierOccurrence is completely separated in time (not + * necessarily in space, see OutsideOf), with the earlierOccurrence happening completely + * before the laterOccurrence. That is, no snapshot of the earlierOccurrence happens at the + * same time as any snapshot of the laterOccurrence, with all snapshots of earlierOccurrence + * happening before those the laterOccurrence, including the endShot of the earlierOccurrence + * and startShot of the laterOccurrence. Note that this means no Occurrence HappensBefore + * itself. + */ + assoc HappensBefore specializes HappensLink, Without { + end feature earlierOccurrence: Occurrence[0..*] redefines sourceOccurrence, separateOccurrenceToo subsets laterOccurrence.predecessors; + end feature laterOccurrence: Occurrence[0..*] redefines targetOccurrence, separateOccurrence subsets earlierOccurrence.successors; + + /* HappensBefore is transitive. */ + subset laterOccurrence.successors subsets earlierOccurrence.successors; + } + + /** + * HappensJustBefore is HappensBefore asserting that there is no possibility of another + * occurrences happening in the time between the earlierOccurrence and laterOccurrence. + */ + assoc HappensJustBefore specializes HappensBefore { + end feature redefines earlierOccurrence: Occurrence[0..*] subsets laterOccurrence.immediatePredecessors; + end feature redefines laterOccurrence: Occurrence[0..*] subsets earlierOccurrence.immediateSuccessors; + + disjoint earlierOccurrence.successors from laterOccurrence.predecessors; + } + + /** + * happensBeforeLinks is a specialization of binaryLinks restricted to type HappensBefore. + * It is the default subsetting for succession connectors. + */ + feature happensBeforeLinks: HappensBefore[0..*] nonunique subsets binaryLinks { + end feature earlierOccurrence: Occurrence[0..*] redefines HappensBefore::earlierOccurrence, binaryLinks::source; + end feature laterOccurrence: Occurrence[0..*] redefines HappensBefore::laterOccurrence, binaryLinks::target; + } + + /** + * OutsideOf asserts that two occurrences do not overlap in space (not necessarily in time, + * see HappensBefore). That is, no four dimensional points of the occurrences are in the + * spatial extent of both of them. This means no Occurrence is OutsideOf itself. + */ + assoc OutsideOf specializes Without { + end feature separateSpaceToo: Occurrence[0..*] redefines separateOccurrenceToo; + end feature separateSpace: Occurrence[0..*] redefines separateOccurrence; + } +} diff --git a/sysml.library/Kernel Library/Performances.kerml b/sysml.library/Kernel Library/Performances.kerml index b677f8a7..96b31c91 100644 --- a/sysml.library/Kernel Library/Performances.kerml +++ b/sysml.library/Kernel Library/Performances.kerml @@ -31,7 +31,7 @@ package Performances { /** * suboccurrences of this Performance that are also Performances. */ - step subperformances: Performance[0..*] subsets performances, suboccurrences; + step subperformances: Performance[0..*] subsets performances, timeEnclosedOccurrences; /** * subperformances of this Performance that are Evaluations. diff --git a/sysml.library/Kernel Library/RationalFunctions.kerml b/sysml.library/Kernel Library/RationalFunctions.kerml index 793a9762..6f54efc7 100644 --- a/sysml.library/Kernel Library/RationalFunctions.kerml +++ b/sysml.library/Kernel Library/RationalFunctions.kerml @@ -5,43 +5,43 @@ package RationalFunctions { import ScalarValues::*; - function Rat(numer: Integer[1], denum: Integer[1]): Rational[1]; - function Numer(rat: Rational[1]): Integer[1]; - function Denom(rat: Rational[1]): Integer[1]; + function rat(numer: Integer[1], denum: Integer[1]): Rational[1]; + function numer(rat: Rational[1]): Integer[1]; + function denom(rat: Rational[1]): Integer[1]; - function Abs specializes NumericalFunctions::Abs (x: Rational[1]): Rational[1]; + function abs specializes RealFunctions::abs (x: Rational[1]): Rational[1]; - function '+' specializes NumericalFunctions::'+' (x: Rational[1], y: Rational[0..1]): Rational[1]; - function '-' specializes NumericalFunctions::'-' (x: Rational[1], y: Rational[0..1]): Rational[1]; - function '*' specializes NumericalFunctions::'*' (x: Rational[1], y: Rational[1]): Rational[1]; - function '/' specializes NumericalFunctions::'/' (x: Rational[1], y: Rational[1]): Rational[1]; - function '**' specializes NumericalFunctions::'**' (x: Rational[1], y: Rational[1]): Rational[1]; - function '^' specializes NumericalFunctions::'^' (x: Rational[1], y: Rational[1]): Rational[1]; + function '+' specializes RealFunctions::'+' (x: Rational[1], y: Rational[0..1]): Rational[1]; + function '-' specializes RealFunctions::'-' (x: Rational[1], y: Rational[0..1]): Rational[1]; + function '*' specializes RealFunctions::'*' (x: Rational[1], y: Rational[1]): Rational[1]; + function '/' specializes RealFunctions::'/' (x: Rational[1], y: Rational[1]): Rational[1]; + function '**' specializes RealFunctions::'**' (x: Rational[1], y: Rational[1]): Rational[1]; + function '^' specializes RealFunctions::'^' (x: Rational[1], y: Rational[1]): Rational[1]; - function '<' specializes NumericalFunctions::'<' (x: Rational[1], y: Rational[1]): Boolean[1]; - function '>' specializes NumericalFunctions::'>' (x: Rational[1], y: Rational[1]): Boolean[1]; - function '<=' specializes NumericalFunctions::'<=' (x: Rational[1], y: Rational[1]): Boolean[1]; - function '>=' specializes NumericalFunctions::'>=' (x: Rational[1], y: Rational[1]): Boolean[1]; + function '<' specializes RealFunctions::'<' (x: Rational[1], y: Rational[1]): Boolean[1]; + function '>' specializes RealFunctions::'>' (x: Rational[1], y: Rational[1]): Boolean[1]; + function '<=' specializes RealFunctions::'<=' (x: Rational[1], y: Rational[1]): Boolean[1]; + function '>=' specializes RealFunctions::'>=' (x: Rational[1], y: Rational[1]): Boolean[1]; - function Max specializes NumericalFunctions::Max (x: Rational[1], y: Rational[1]): Rational[1]; - function Min specializes NumericalFunctions::Min (x: Rational[1], y: Rational[1]): Rational[1]; + function max specializes RealFunctions::max (x: Rational[1], y: Rational[1]): Rational[1]; + function min specializes RealFunctions::min (x: Rational[1], y: Rational[1]): Rational[1]; - function '==' specializes DataFunctions::'==' (x: Rational[0..1], y: Rational[0..1]): Boolean[1]; + function '==' specializes RealFunctions::'==' (x: Rational[0..1], y: Rational[0..1]): Boolean[1]; - function GCD(x: Rational[1], y: Rational[1]): Integer[1]; + function gcd(x: Rational[1], y: Rational[1]): Integer[1]; - function Floor(x: Rational[1]): Integer[1]; - function Round(x: Rational[1]): Integer[1]; + function floor specializes RealFunctions::floor (x: Rational[1]): Integer[1]; + function round specializes RealFunctions::round (x: Rational[1]): Integer[1]; - function ToString specializes BaseFunctions::ToString (x: Rational[1]): String[1]; + function ToString specializes RealFunctions::ToString (x: Rational[1]): String[1]; function ToInteger(x: Rational[1]): Integer[1]; function ToRational(x: String[1]): Rational[1]; - function sum specializes ScalarFunctions::sum (collection: Rational[0..*]): Rational[1] { - ScalarFunctions::sum0(collection, Rat(0, 1)) + function sum specializes RealFunctions::sum (collection: Rational[0..*]): Rational[1] { + NumericalFunctions::sum0(collection, rat(0, 1)) } - function product specializes ScalarFunctions::product (collection: Rational[0..*]): Rational[1] { - ScalarFunctions::product1(collection, Rat(1, 1)) + function product specializes RealFunctions::product (collection: Rational[0..*]): Rational[1] { + NumericalFunctions::product1(collection, rat(1, 1)) } } diff --git a/sysml.library/Kernel Library/RealFunctions.kerml b/sysml.library/Kernel Library/RealFunctions.kerml index 7d15c8eb..af7a4d9c 100644 --- a/sysml.library/Kernel Library/RealFunctions.kerml +++ b/sysml.library/Kernel Library/RealFunctions.kerml @@ -5,40 +5,50 @@ package RealFunctions { import ScalarValues::*; - function Abs specializes NumericalFunctions::Abs (x: Real[1]): Real[1]; + function re :> ComplexFunctions::re(x: Real[1]): Real[1] { + x + } + function im :> ComplexFunctions::im(x: Real[1]): Real[1] { + 0.0 + } + + function abs specializes ComplexFunctions::abs (x: Real[1]): Real[1]; + function arg specializes ComplexFunctions::arg (x: Real[1]): Real[1] { + 0.0 + } - function '+' specializes NumericalFunctions::'+' (x: Real[1], y: Real[0..1]): Real[1]; - function '-' specializes NumericalFunctions::'-' (x: Real[1], y: Real[0..1]): Real[1]; - function '*' specializes NumericalFunctions::'*' (x: Real[1], y: Real[1]): Real[1]; - function '/' specializes NumericalFunctions::'/' (x: Real[1], y: Real[1]): Real[1]; - function '**' specializes NumericalFunctions::'**' (x: Real[1], y: Real[1]): Real[1]; - function '^' specializes NumericalFunctions::'^' (x: Real[1], y: Real[1]): Real[1]; + function '+' specializes ComplexFunctions::'+' (x: Real[1], y: Real[0..1]): Real[1]; + function '-' specializes ComplexFunctions::'-' (x: Real[1], y: Real[0..1]): Real[1]; + function '*' specializes ComplexFunctions::'*' (x: Real[1], y: Real[1]): Real[1]; + function '/' specializes ComplexFunctions::'/' (x: Real[1], y: Real[1]): Real[1]; + function '**' specializes ComplexFunctions::'**' (x: Real[1], y: Real[1]): Real[1]; + function '^' specializes ComplexFunctions::'^' (x: Real[1], y: Real[1]): Real[1]; function '<' specializes NumericalFunctions::'<' (x: Real[1], y: Real[1]): Boolean[1]; function '>' specializes NumericalFunctions::'>' (x: Real[1], y: Real[1]): Boolean[1]; function '<=' specializes NumericalFunctions::'<=' (x: Real[1], y: Real[1]): Boolean[1]; function '>=' specializes NumericalFunctions::'>=' (x: Real[1], y: Real[1]): Boolean[1]; - function Max specializes NumericalFunctions::Max (x: Real[1], y: Real[1]): Real[1]; - function Min specializes NumericalFunctions::Min (x: Real[1], y: Real[1]): Real[1]; + function max specializes NumericalFunctions::max (x: Real[1], y: Real[1]): Real[1]; + function min specializes NumericalFunctions::min (x: Real[1], y: Real[1]): Real[1]; - function '==' specializes DataFunctions::'==' (x: Real[0..1], y: Real[0..1]): Boolean[1]; + function '==' specializes ComplexFunctions::'==' (x: Real[0..1], y: Real[0..1]): Boolean[1]; - function Sqrt(x: Real[1]): Real[1]; + function sqrt(x: Real[1]): Real[1]; - function Floor(x: Real[1]): Integer[1]; - function Round(x: Real[1]): Integer[1]; + function floor(x: Real[1]): Integer[1]; + function round(x: Real[1]): Integer[1]; - function ToString specializes BaseFunctions::ToString (x: Real[1]): String[1]; + function ToString specializes ComplexFunctions::ToString (x: Real[1]): String[1]; function ToInteger(x: Real[1]): Integer[1]; function ToRational(x: Real[1]): Rational[1]; function ToReal(x: String[1]): Real[1]; - function sum specializes ScalarFunctions::sum (collection: Real[0..*]): Real { - ScalarFunctions::sum0(collection, 0.0) + function sum specializes ComplexFunctions::sum (collection: Real[0..*]): Real { + NumericalFunctions::sum0(collection, 0.0) } - function product specializes ScalarFunctions::product (collection: Real[0..*]): Real { - ScalarFunctions::product1(collection, 1.0) + function product specializes ComplexFunctions::product (collection: Real[0..*]): Real { + NumericalFunctions::product1(collection, 1.0) } } diff --git a/sysml.library/Kernel Library/ScalarFunctions.kerml b/sysml.library/Kernel Library/ScalarFunctions.kerml index a0fcc062..3aa7c4e5 100644 --- a/sysml.library/Kernel Library/ScalarFunctions.kerml +++ b/sysml.library/Kernel Library/ScalarFunctions.kerml @@ -3,7 +3,6 @@ */ package ScalarFunctions { import ScalarValues::*; - private import ControlFunctions::reduce; abstract function '+' specializes DataFunctions::'+' (x: ScalarValue[1], y: ScalarValue[0..1]): ScalarValue[1]; abstract function '-' specializes DataFunctions::'-' (x: ScalarValue[1], y: ScalarValue[0..1]): ScalarValue[1]; @@ -27,19 +26,8 @@ package ScalarFunctions { abstract function '<=' specializes DataFunctions::'<=' (x: ScalarValue[1], y: ScalarValue[1]): Boolean[1]; abstract function '>=' specializes DataFunctions::'>=' (x: ScalarValue[1], y: ScalarValue[1]): Boolean[1]; - abstract function Max specializes DataFunctions::Max (x: ScalarValue[1], y: ScalarValue[1]): ScalarValue[1]; - abstract function Min specializes DataFunctions::Min (x: ScalarValue[1], y: ScalarValue[1]): ScalarValue[1]; + abstract function max specializes DataFunctions::Max (x: ScalarValue[1], y: ScalarValue[1]): ScalarValue[1]; + abstract function min specializes DataFunctions::Min (x: ScalarValue[1], y: ScalarValue[1]): ScalarValue[1]; abstract function '..' specializes DataFunctions::'..' (lower: ScalarValue[1], upper: ScalarValue[1]): ScalarValue[0..*]; - - abstract function sum specializes DataFunctions::sum (collection: ScalarValue[0..*]): ScalarValue[1]; - abstract function product specializes DataFunctions::product (collection: ScalarValue[0..*]): ScalarValue[1]; - - function sum0 specializes DataFunctions::sum0 (collection: ScalarValue[0..*], zero: ScalarValue[1]): ScalarValue { - collection->reduce '+' ?? zero - } - - function product1 specializes DataFunctions::product1 (collection: ScalarValue[0..*], one: ScalarValue[1]): ScalarValue { - collection->reduce '*' ?? one - } } \ No newline at end of file diff --git a/sysml.library/Kernel Library/SequenceFunctions.kerml b/sysml.library/Kernel Library/SequenceFunctions.kerml index 30ebe24b..c550c820 100644 --- a/sysml.library/Kernel Library/SequenceFunctions.kerml +++ b/sysml.library/Kernel Library/SequenceFunctions.kerml @@ -22,7 +22,7 @@ package SequenceFunctions { !isEmpty(seq) } function includes(seq1: Anything[0..*] nonunique, seq2: Anything[0..*] nonunique): Boolean[1] { - seq2->forAll {in x; seq1->includes(x)} + seq2->forAll {in x; seq1->exists{in y; x == y}} } function includesOnly(seq1: Anything[0..*] nonunique, seq2: Anything[0..*] nonunique): Boolean[1] { seq1->includes(seq2) && seq2->includes(seq1) diff --git a/sysml.library/Kernel Library/SpatialFrames.kerml b/sysml.library/Kernel Library/SpatialFrames.kerml new file mode 100644 index 00000000..e2b178e9 --- /dev/null +++ b/sysml.library/Kernel Library/SpatialFrames.kerml @@ -0,0 +1,159 @@ +/** + * This package models spatial frames of reference for quantifying the position of points + * in a three-dimensional space. + */ +package SpatialFrames { + private import Clocks::*; + private import ScalarValues::NumericalValue; + private import VectorValues::ThreeVectorValue; + private import VectorValues::CartesianThreeVectorValue; + private import VectorFunctions::isZeroVector; + private import Objects::Body; + private import Objects::Point; + private import ControlFunctions::forAll; + private import SequenceFunctions::includes; + + /** + * defaultFrame is a fixed SpatialFrame used as a universal default. + */ + readonly feature defaultFrame : SpatialFrame[1]; + + /** + * A SpatialFrame is a three-dimensional Body that provides a spatial extent that + * acts as a frame of reference for defining the physical position and displacement + * vectors of Points over time. + */ + abstract struct SpatialFrame specializes Body; + + /** + * The PositionOf a Point relative to a SpatialFrame, at a specific time relative to a given + * Clock, as a positionVector that is a ThreeVectorValue. + */ + abstract function PositionOf { + in point : Point[1]; + in time : NumericalValue[1]; + in frame : SpatialFrame[1] default defaultFrame; + in clock : Clock[1] default defaultClock; + return positionVector : ThreeVectorValue[1]; + + /** + * The given point must exist at the given time. + */ + inv positionTimePrecondition { + TimeOf(point.startShot) <= time and + time <= TimeOf(point.endShot) + } + + /** + * The result positionVector is equal to the PositionOf the Point spaceShot of the + * frame that encloses the given point, at the given time. + */ + inv spacePositionConstraint { + (frame.spaceShots as Point)->forAll{in p : Point; + p.spaceTimeEnclosedOccurrences->includes(point) implies + positionVector == PositionOf(p, time, frame) + } + } + } + + /** + * The CurrentPositionOf a Point relative to a SpatialFrame and a Clock is the PositionOf + * the Point relative to the SpatialFrame at the currentTime of the Clock. + */ + abstract function CurrentPositionOf { + in point : Point[1]; + in frame : SpatialFrame[1] default defaultFrame; + in clock : Clock[1] default defaultClock; + return positionVector : ThreeVectorValue[1] = + PositionOf(point, clock.currentTime, frame, clock); + } + + /** + * The DisplacementOf two Points relative to a SpatialFrame, at a specific time relative to a + * given Clock, is the displacementVector computed as the difference between the PositionOf the + * first Point and PositionOf the second Point, relative to that SpatialFrame, at that time. + */ + function DisplacementOf { + in point1 : Point[1]; + in point2 : Point[1]; + in time : NumericalValue; + in frame : SpatialFrame[1] default defaultFrame; + in clock : Clock[1] default defaultClock; + return displacementVector : ThreeVectorValue[1] = + PositionOf(point2, time, frame, clock) - PositionOf(point1, time, frame, clock); + + /** + * If either point1 or point2 occurs within the other, then the displacementVector is + * the zero vector. + */ + inv zeroDisplacementConstraint { + (point1.spaceTimeEnclosedOccurrences->includes(point2) or + point2.spaceTimeEnclosedOccurrences->includes(point1)) implies + isZeroVector(displacementVector) + } + } + + /** + * The CurrentDisplacementOf two Points relative to a SpatialFrame and Clock is the DisplacementOf + * the Points relative to the SpacialFrame at the currentTime of the Clock. + */ + function CurrentDisplacementOf { + in point1 : Point[1]; + in point2 : Point[1]; + in frame : SpatialFrame[1] default defaultFrame; + in clock : Clock[1] default defaultClock; + return displacementVector : ThreeVectorValue[1] = + DisplacementOf(point1, point2, clock.currentTime, frame, clock); + } + + /** + * A CartesianSpatialFrame is a SpatialFrame relative to which all position and displacement + * vectors can be represented as CartesianThreeVectorValues. + */ + abstract struct CartesianSpatialFrame :> SpatialFrame; + + /** + * The PositionOf a Point relative to a CartesianSpatialFrame is a CartesianThreeVectorValue. + */ + abstract function CartesianPositionOf :> PositionOf { + in point : Point[1]; + in time : NumericalValue[1]; + in frame : CartesianSpatialFrame[1]; + in clock : Clock[1] default defaultClock; + return positionVector : CartesianThreeVectorValue[1]; + } + + /** + * The CurrentPositionOf a Point relative to a CartesianSpatialFrame is a CartesianThreeVectorValue. + */ + abstract function CartesianCurrentPositionOf :> CurrentPositionOf { + in point : Point[1]; + in frame : CartesianSpatialFrame[1]; + in clock : Clock[1] default defaultClock; + return positionVector : CartesianThreeVectorValue[1]; + } + + /** + * The DisplacementOf two Points relative to a CartesianSpatialFrame is a CartesianThreeVectorValue. + */ + function CartesianDisplacementOf :> DisplacementOf { + in point1 : Point[1]; + in point2 : Point[1]; + in time : NumericalValue[1]; + in frame : CartesianSpatialFrame[1]; + in clock : Clock[1] default defaultClock; + return displacementVector : CartesianThreeVectorValue[1]; + } + + /** + * The CurrentDisplacementOf two Points relative to a CartesianSpatialFrame is a CartesianThreeVectorValue. + */ + function CartesianCurrentDisplacementOf :> CurrentDisplacementOf { + in point1 : Point[1]; + in point2 : Point[1]; + in frame : CartesianSpatialFrame[1]; + in clock : Clock[1] default defaultClock; + return displacementVector : CartesianThreeVectorValue[1]; + } + +} \ No newline at end of file diff --git a/sysml.library/Kernel Library/TrigFunctions.kerml b/sysml.library/Kernel Library/TrigFunctions.kerml new file mode 100644 index 00000000..557e2ea5 --- /dev/null +++ b/sysml.library/Kernel Library/TrigFunctions.kerml @@ -0,0 +1,34 @@ +/** + * This package defines basic trigonometric functions on real numbers. + */ +package TrigFunctions { + import ScalarValues::Real; + + feature pi : Real; + inv piPrecision { RealFunctions::round(pi * 1E20) == 314159265358979323846.0 } + + function deg(theta_rad : Real) { + theta_rad * 180 / pi + } + function rad(theta_deg : Real) { + theta_deg * pi / 180 + } + + datatype UnitBoundedReal :> Real { + private x :>> self; + inv unitBound { -1.0 <= x & x <= 1.0 } + } + + function sin(theta : Real) : UnitBoundedReal; + function cos(theta : Real) : UnitBoundedReal; + function tan(theta : Real) : Real { + sin(theta) / cos(theta) + } + function cot(theta : Real) : Real { + cos(theta) / sin(theta) + } + + function arcsin(x : UnitBoundedReal) : Real; + function arccos(x : UnitBoundedReal) : Real; + function arctan(x : Real) : Real; +} \ No newline at end of file diff --git a/sysml.library/Kernel Library/VectorFunctions.kerml b/sysml.library/Kernel Library/VectorFunctions.kerml new file mode 100644 index 00000000..1d8377d1 --- /dev/null +++ b/sysml.library/Kernel Library/VectorFunctions.kerml @@ -0,0 +1,192 @@ +/** + * This package defines abstract functions on VectorValues corresponding to the algebraic operations + * provided by a vector space with inner product. It also includes concrete implementations of these + * functions specifically for CartesianVectorValues. + */ +package VectorFunctions { + private import ScalarValues::NumericalValue; + private import ScalarValues::Positive; + private import ScalarValues::Real; + private import ScalarValues::Boolean; + private import NumericalFunctions::*; + private import RealFunctions::sqrt; + private import TrigFunctions::arccos; + private import SequenceFunctions::size; + private import ControlFunctions::*; + + import VectorValues::*; + + /* Generic arithmetic functions for all VectorValues. */ + + /** + * Return whether a VectorValue is a zero vector. + */ + abstract function isZeroVector(v: VectorValue[1]): Boolean[1]; + + /** + * With two arguments, returns the sum of two VectorValues. With one argument, returns that VectorValue. + */ + abstract function '+' specializes DataFunctions::'+' (v: VectorValue[1], w: VectorValue[0..1]) u: VectorValue[1] { + inv zeroAddition { w == null or isZeroVector(w) implies u == w } + inv commutivity { w != null implies u == w + v } + } + + /** + * With two arguments, returns the difference of two VectorValues. With one arguments, returns the inverse + * of the given VectorValue, that is, the VectorValue that, when added to the original VectorValue, results in + * the zeroVector. + */ + abstract function '-' specializes DataFunctions::'-' (v: VectorValue[1], w: VectorValue[0..1]) u: VectorValue[1] { + inv negation { w == null implies isZeroVector(v + u) } + inv difference { w != null implies v + u == w } + } + + /** + * Return the sum of a collection of VectorValues. If the collection is empty, return a given zero vector. + */ + abstract function sum0 (coll: VectorValue[*] nonunique, zero: VectorValue[1]) s: VectorValue[1] { + inv precondition { isZeroVector(zero) } + coll->reduce '+' ?? zero + } + + /* Functions specific to NumericalVectorValues. */ + + /** + * Construct a NumericalVectorValue whose elements are a non-empty list of component NumericalValues. + * The dimension of the NumericalVectorValue is equal to the number of components. + */ + function VectorOf(components: NumericalValue[1..*] ordered nonunique): NumericalVectorValue { + NumericalVectorValue ( + dimension = size(components), + elements = components + ) + } + + /** + * Scalar product of a NumericalValue and a NumericalVectorValue. + */ + abstract function scalarVectorMult specializes DataFunctions::'*' (x: NumericalValue[1], v: NumericalVectorValue[1]) w: NumericalVectorValue[1] { + inv scaling { norm(w) == x * norm(v) } + inv zeroLength { isZeroVector(w) implies isZero(norm(w))} + } + alias '*' for scalarVectorMult; + + /** + * Scalar product of a NumericalVectorValue and a NumericalValue, which has the same value as the scalar product of the + * NumericalValue and the NumericalVectorValue. + */ + abstract function vectorScalarMult specializes DataFunctions::'*' (v: NumericalVectorValue[1], x: NumericalValue[1]) w: NumericalVectorValue[1] { + scalarVectorMult(x, v) + } + + /** + * Scalar quotient of a NumericalVectorValue and a NumericalValue, defined as the scalar product of the inverse of the + * NumericalValue and the NumericalVectorValue. + */ + abstract function vectorScalarDiv specializes DataFunctions::'/' (v: NumericalVectorValue[1], x: NumericalValue[1]) w: NumericalVectorValue[1] { + scalarVectorMult(1.0 / x, v) + } + + /** + * Inner product of two NumericalVectorValues. + */ + abstract function inner specializes DataFunctions::'*'(v: NumericalVectorValue[1], w: NumericalVectorValue[1]) x: NumericalValue[1] { + inv commmutivity { x == inner(w, v) } + inv zeroInner { isZeroVector(v) or isZeroVector(w) implies isZero(x)} + } + + /** + * The norm (magnitude) of a NumericalVectorValue, as a NumericalValue. + */ + abstract function norm(v: NumericalVectorValue[1]) l : NumericalValue[1] { + inv squareNorm { l * l == inner(v,v) } + inv lengthZero { isZero(l) == isZeroVector(v) } + } + + /** + * The angle between two NumericalVectorValues, as a NumericalValue. + */ + abstract function angle(v: NumericalVectorValue[1], w: NumericalVectorValue[1]) theta: NumericalValue[1] { + inv commutivity { theta == angle(w, v) } + inv lengthInsensitive { theta == angle(w / norm(w), v / norm(v)) } + } + + /* Specialized functions with concrete definitions for CartesianVectorValues. */ + + /** + * Construct a CartesianVectorValue whose elements are a non-empty list of Real components. + * The dimension of the NumericalVectorValue is equal to the number of components. + */ + function CartesianVectorOf(components: Real[*]): CartesianVectorValue { + CartesianVectorValue ( + dimension = size(components), + elements = components + ) + } + function CartesianThreeVectorOf specializes CartesianVectorOf(components: Real[3]): CartesianThreeVectorValue; + + /** + * Cartesian zero vectors of 1, 2 and 3 dimensions. + */ + feature cartesianZeroVector: CartesianVectorValue[3] = + ( + CartesianVectorOf(0.0), + CartesianVectorOf((0.0, 0.0)), + CartesianThreeVectorOf((0.0, 0.0, 0.0)) + ); + feature cartesian3DZeroVector: CartesianThreeVectorValue[1] = + cartesianZeroVector[3]; + + /** + * A CartesianVectorValue is a zero vector if all its elements are zero. + */ + function isCartesianZeroVector specializes isZeroVector (v: CartesianVectorValue): Boolean { + v.elements->forAll{in x; x == 0.0} + } + + function 'cartesian+' specializes '+' (v: CartesianVectorValue[1], w: CartesianVectorValue[0..1]) u: CartesianVectorValue[1] { + inv precondition { w != null implies v.dimension == w.dimension } + if w == null? v + else CartesianVectorOf( + (1..w.dimension)->collect{in i : Positive; v[i] + w[i]} + ) + } + + function 'cartesian-' specializes '-' (v: CartesianVectorValue[1], w: CartesianVectorValue[0..1]) u: CartesianVectorValue[1] { + inv precondition { w != null implies v.dimension == w.dimension } + CartesianVectorOf( + if w == null? CartesianVectorOf(v.elements->collect{in x : Real; -x}) + else CartesianVectorOf( + (1..v.dimension)->collect{in i : Positive; v[i] - w[i]} + ) + ) + } + + function cartesianScalarVectorMult specializes scalarVectorMult (x: Real[1], v: CartesianVectorValue[1]) w: CartesianVectorValue[1] { + CartesianVectorOf( + v.elements->collect{in y : Real; x * y} + ) + } + function cartesianVectorScalarMult specializes vectorScalarMult (v: CartesianVectorValue[1], x: Real[1]) w: CartesianVectorValue[1] { + cartesianScalarVectorMult(x, v) + } + + function cartesianInner specializes inner(v: CartesianVectorValue[1], w : CartesianVectorValue[1]) x: Real[1]{ + inv precondition { v.dimension == w.dimension } + (1..v.dimension)->collect{in i : Positive; v[i] * w[i]}->reduce RealFunctions::'+' + } + + function cartesianNorm specializes norm(v: CartesianVectorValue[1]) l : NumericalValue[1] { + sqrt(cartesianInner(v, v)) + } + + function cartesianAngle specializes angle(v: CartesianVectorValue[1], w: CartesianVectorValue[1]) theta: Real[1] { + inv precondition { v.dimension == w.dimension } + arccos(cartesianInner(v, w) / (norm(v) * norm(w))) + } + + function sum(coll: CartesianThreeVectorValue): CartesianThreeVectorValue { + sum0(coll, cartesian3DZeroVector) + } + +} \ No newline at end of file diff --git a/sysml.library/Kernel Library/VectorValues.kerml b/sysml.library/Kernel Library/VectorValues.kerml new file mode 100644 index 00000000..e9c2d57c --- /dev/null +++ b/sysml.library/Kernel Library/VectorValues.kerml @@ -0,0 +1,51 @@ +/** + * This package provides a basic model of abstract vectors as well as concrete vectors + * whose components are numerical values. The package VectorFunctions defines the + * corresponding vector-space functions. + */ +package VectorValues { + private import ScalarValues::NumericalValue; + private import ScalarValues::Real; + private import Collections::Array; + + /** + * A VectorValue is an abstract data type whose values may be operated on using + * VectorFunctions. + */ + abstract datatype VectorValue; + + /** + * A NumericalVectorValue is a kind of VectorValue that is specifically represented + * as a one-dimensional array of NumericalValues. The dimension is allowed to be empty, + * permitting a NumericalVectorValue of rank 0, which is essentially isomorphic to a + * scalar NumericalValue. + */ + datatype NumericalVectorValue :> VectorValue, Array { + feature dimension[0..1] :>> dimensions; + feature :>> elements : NumericalValue; + } + + /** + * CartesianVectorValue is a specialization Numerical VectorValue for which there are + * specific implementations in VectorFunctions of the abstract vector-space functions. + * + * Note: The restriction of the element type to Real is to facilitate + * the complete definition of these functions. + */ + datatype CartesianVectorValue :> NumericalVectorValue { + feature :>> elements : Real; + } + + /** + * A ThreeVectorValue is a NumericalVectorValue that has dimension 3. + */ + datatype ThreeVectorValue :> NumericalVectorValue { + feature :>> dimension = 3; + } + + /** + * A CartesianThreeVectorValue is a NumericalVectorValue that is both Cartesian and + * has dimension 3. + */ + datatype CartesianThreeVectorValue :> CartesianVectorValue, ThreeVectorValue; +} \ No newline at end of file diff --git a/sysml.library/Systems Library/Items.sysml b/sysml.library/Systems Library/Items.sysml index 1622b9c9..f5febb52 100644 --- a/sysml.library/Systems Library/Items.sysml +++ b/sysml.library/Systems Library/Items.sysml @@ -9,6 +9,9 @@ package Items { private import Parts::parts; private import Constraints::ConstraintCheck; private import Constraints::constraintChecks; + private import SequenceFunctions::notEmpty; + private import SequenceFunctions::includes; + private import ControlFunctions::forAll; /** * Item is the most general class of objects that are part of, exist in or flow through a system. @@ -20,6 +23,36 @@ package Items { item start: Item :>> startShot; item done: Item :>> endShot; + /** + * The shape of an Item is its spatial boundary. + */ + item shape : Item :>> spaceBoundary; + + /** + * Other shapes that spatially envelop this Item. + */ + item envelopingShapes : Item[0..*] { + attribute :>> innerSpaceDimension = shape.innerSpaceDimension; + } + + /** + * An Item is enveloped by all its envelopingShapes. That is, for each envelopingShape, there + * is an Item with that shape that encloses this Item in space for its entire lifetime. + */ + assert constraint envelopingShapeConstraint { + envelopingShapes->forAll { in envelopingShape : Item; + item envelopingItem { + item :>> shape = envelopingShape; + } + envelopingItem.spaceTimeEnclosedOccurrences->includes(Item::self) + } + } + + /** + * An Item is solid if it is three-dimensional and has a non-empty shape (boundary). + */ + attribute isSolid = innerSpaceDimension == 3 and notEmpty(shape); + /** * The Items that are composite subitems of this Item. */ diff --git a/sysml.library/Systems Library/Ports.sysml b/sysml.library/Systems Library/Ports.sysml index 1a309cfb..a662bfc4 100644 --- a/sysml.library/Systems Library/Ports.sysml +++ b/sysml.library/Systems Library/Ports.sysml @@ -16,7 +16,7 @@ package Ports { /** * The Ports that are subports of this Port. */ - port subports: Port :> suboccurrences; + port subports: Port :> timeEnclosedOccurrences; } /** diff --git a/sysml/src/examples/Geometry Examples/CarWithEnvelopingShape.sysml b/sysml/src/examples/Geometry Examples/CarWithEnvelopingShape.sysml new file mode 100644 index 00000000..c340d9bf --- /dev/null +++ b/sysml/src/examples/Geometry Examples/CarWithEnvelopingShape.sysml @@ -0,0 +1,17 @@ +package CarWithEnvelopingShape { + import ShapeItems::Box; + import SI::mm; + + /** + * Example car with simple enveloping shape that is a solid box + */ + part def Car { + + private item :> envelopingShapes : Box[1] { + :>> length = 4800 [mm]; + :>> width = 1840 [mm]; + :>> height = 1350 [mm]; + } + + } +} \ No newline at end of file diff --git a/sysml/src/examples/Geometry Examples/CarWithShapeAndCSG.sysml b/sysml/src/examples/Geometry Examples/CarWithShapeAndCSG.sysml new file mode 100644 index 00000000..510a3c0b --- /dev/null +++ b/sysml/src/examples/Geometry Examples/CarWithShapeAndCSG.sysml @@ -0,0 +1,41 @@ +package CarWithShapeAndCSG { + import SpatialItems::*; + import ShapeItems::*; + import Objects::Point; + import Quantities::VectorQuantityValue; + + item def Car :> CompoundSpatialItem { + item :>> shape : Cuboid [1] { + /* Quantify faces, etc, by redefining nested features. */ + } + part powerSource : Engine [1] :> componentItems; + } + + part def Engine :> SpatialItem { + item :>> shape [1]; + + /* Specify relative positions of c1 and c2 here. */ + private attribute c1Position : VectorQuantityValue; + private attribute c2Position : VectorQuantityValue; + + private item c1 : Cylinder, SpatialItem [1] { + /* Quantify faces, etc, by redefining nested features. */ + attribute :>> coordinateFrame { + attribute origin = c1Position; + } + } + + private item c2 : Cylinder, SpatialItem [1] { + /* Quantify faces, etc, by redefining nested features. */ + attribute :>> coordinateFrame { + attribute origin = c2Position; + } + } + + /* CSG intersection of c1 and c2. */ + attribute :> intersectionsOf[1] { + item :>> elements = (c1, c2); + } + + } +} \ No newline at end of file diff --git a/sysml/src/examples/Geometry Examples/ExternalShapeRefExample.sysml b/sysml/src/examples/Geometry Examples/ExternalShapeRefExample.sysml new file mode 100644 index 00000000..dabcdaa3 --- /dev/null +++ b/sysml/src/examples/Geometry Examples/ExternalShapeRefExample.sysml @@ -0,0 +1,29 @@ +package ExternalShapeRefExample { + import ScalarValues::String; + import ShapeItems::*; + import ISQ::mass; + import SI::mm; + + /** + * Metadata to reference an externally defined shape. + */ + attribute def ExternalShapeRef { + attribute purpose : String[1]; + attribute shapeIri : String[1]; + } + + part myBatteryUnit { + item :>> shape : Shell { + metadata ExternalShapeRef { + purpose = "highLoD"; + shapeIri = "file:/detailed-geometry/LEMS-250W_BatteryHousing_Example.step"; + } + } + + private item envelopingBoxBatteryUnit : Box :> envelopingShapes { + :>> length = 140[mm]; + :>> width = 148[mm]; + :>> height = 90[mm]; + } + } +} \ No newline at end of file diff --git a/sysml/src/examples/Interaction Sequencing Examples/ServerSequenceModel.sysml b/sysml/src/examples/Interaction Sequencing Examples/ServerSequenceModel.sysml index db73d0fb..d3e98436 100644 --- a/sysml/src/examples/Interaction Sequencing Examples/ServerSequenceModel.sysml +++ b/sysml/src/examples/Interaction Sequencing Examples/ServerSequenceModel.sysml @@ -37,7 +37,7 @@ package ServerSequenceModel { part consumer { event occurrence subscribe_source_event; - then event occurrence deliver_target_event :> suboccurrences; + then event occurrence deliver_target_event; } } } \ No newline at end of file diff --git a/sysml/src/examples/Mass Roll-up Example/MassConstraintExample.sysml b/sysml/src/examples/Mass Roll-up Example/MassConstraintExample.sysml index 0282c229..a580366b 100644 --- a/sysml/src/examples/Mass Roll-up Example/MassConstraintExample.sysml +++ b/sysml/src/examples/Mass Roll-up Example/MassConstraintExample.sysml @@ -1,7 +1,7 @@ package MassConstraintExample { import ISQ::*; import SI::*; - import ScalarFunctions::*; + import NumericalFunctions::*; part def Engine { attribute m :> mass; diff --git a/sysml/src/examples/Mass Roll-up Example/MassRollup.sysml b/sysml/src/examples/Mass Roll-up Example/MassRollup.sysml index 1e32be28..dd7d6471 100644 --- a/sysml/src/examples/Mass Roll-up Example/MassRollup.sysml +++ b/sysml/src/examples/Mass Roll-up Example/MassRollup.sysml @@ -1,5 +1,5 @@ package MassRollup { - import ScalarFunctions::*; + import NumericalFunctions::*; part def MassedThing { attribute mass :> ISQ::mass; @@ -21,7 +21,7 @@ package MassRollup { abstract attribute minMass :> ISQ::mass; attribute totalMass redefines MassedThing::totalMass = - mass + sum(subcomponents.totalMass.{in p :> ISQ::mass; p > minMass}); + mass + sum(subcomponents.totalMass.?{in p :> ISQ::mass; p > minMass}); } } \ No newline at end of file diff --git a/sysml/src/examples/Simple Tests/CalculationTest.sysml b/sysml/src/examples/Simple Tests/CalculationTest.sysml index 406d0702..5ccfac7a 100644 --- a/sysml/src/examples/Simple Tests/CalculationTest.sysml +++ b/sysml/src/examples/Simple Tests/CalculationTest.sysml @@ -1,6 +1,6 @@ package CalculationExample { import ISQ::*; - import ScalarFunctions::*; + import NumericalFunctions::*; part def VehiclePart { attribute m : MassValue; diff --git a/sysml/src/examples/Simple Tests/ConstraintTest.sysml b/sysml/src/examples/Simple Tests/ConstraintTest.sysml index c0cbe06d..d7f8fed2 100644 --- a/sysml/src/examples/Simple Tests/ConstraintTest.sysml +++ b/sysml/src/examples/Simple Tests/ConstraintTest.sysml @@ -1,7 +1,7 @@ package ConstraintTest { import ISQ::MassValue; import SI::kg; - import ScalarFunctions::sum; + import NumericalFunctions::sum; constraint def MassAnalysis { attribute totalMass: MassValue; diff --git a/sysml/src/examples/Vehicle Example/SysML v2 Spec Annex B VehicleModel.sysml b/sysml/src/examples/Vehicle Example/SysML v2 Spec Annex B VehicleModel.sysml index 6147c234..ba31157b 100644 --- a/sysml/src/examples/Vehicle Example/SysML v2 Spec Annex B VehicleModel.sysml +++ b/sysml/src/examples/Vehicle Example/SysML v2 Spec Annex B VehicleModel.sysml @@ -416,7 +416,7 @@ package sfriedenthal_VehicleModel_1_simplified{ package AttributeDefinitions{ import ScalarValues::*; // Scalar Functions provides Sum expression - import ScalarFunctions::*; + import NumericalFunctions::*; import ISQ::*; import SI::*; import USCustomaryUnits::*; @@ -446,7 +446,7 @@ package sfriedenthal_VehicleModel_1_simplified{ // kpl is approx .425 * mpg kpl : DerivedUnit = km / L; - rpm : DerivedUnit = 1 / min; + rpm : DerivedUnit = 1 / SI::min; kW : DerivedUnit = kilo * W; // } diff --git a/sysml/src/examples/Vehicle Example/VehicleModel_1_Simplified.sysml b/sysml/src/examples/Vehicle Example/VehicleModel_1_Simplified.sysml index efcfad46..dbd5902c 100644 --- a/sysml/src/examples/Vehicle Example/VehicleModel_1_Simplified.sysml +++ b/sysml/src/examples/Vehicle Example/VehicleModel_1_Simplified.sysml @@ -10,6 +10,8 @@ package VehicleModel_1_simplified{ * objectiveFunction to evaluationFunction * riskLevels (low, medium, high) * 2021-12-30: Allocated flow to interface and mass requirement to vehicle.mass + * 2022-02-16: Added change and time events from release 2022-01 to Vehicle health states + ^ 2022-03-09: Added Swimlanes package and view to OtherFunctionality */ } } @@ -49,7 +51,6 @@ package VehicleModel_1_simplified{ perform action applyParkingBrake; perform action senseTemperature; //the following uses a single concept of event for signal, change, and time event - //the time event will be replaced by when eventname exhibit state vehicleStates parallel { ref controller : VehicleController; state operatingStates { @@ -86,7 +87,9 @@ package VehicleModel_1_simplified{ state healthStates { entry action initial; - do senseTemperature (out temp); + do senseTemperature{ + out temp; + } state normal; state maintenance; @@ -101,7 +104,7 @@ package VehicleModel_1_simplified{ transition normal_To_degraded first normal - accept when senseTemperature.temp > Tmax + accept when senseTemperature.temp > Tmax do send OverTemp() to controller then degraded; @@ -434,9 +437,8 @@ package VehicleModel_1_simplified{ } } package AttributeDefinitions{ + //import Quantities::*; import ScalarValues::*; - // Scalar Functions provides Sum expression - import ScalarFunctions::*; import ISQ::*; import SI::*; import USCustomaryUnits::*; @@ -551,6 +553,7 @@ package VehicleModel_1_simplified{ } } package VehicleConfigurations{ + import NumericalFunctions::sum; package VehicleConfiguration_a{ package PartsTree{ part vehicle_a:Vehicle{ @@ -1793,5 +1796,33 @@ package VehicleModel_1_simplified{ } } } + package SwimLanes{ + part def Part0; + part def Part1; + part def Part2; + part part0:Part0{ + perform action0; + part part1: Part1{ + perform action0.action1; + perform action0.action4; + } + part part2 : Part2 { + perform action0.action2; + perform action0.action3; + } + } + action action0 { + action1; + action2; + action3; + action4; + + first start then action1; + first action1 then action2; + first action2 then action3; + first action3 then action4; + first action4 then done; + } + } } -} \ No newline at end of file +} diff --git a/sysml/src/training/28. Expressions/MassRollup1.sysml b/sysml/src/training/28. Expressions/MassRollup1.sysml index 94bc06ef..6a374b41 100644 --- a/sysml/src/training/28. Expressions/MassRollup1.sysml +++ b/sysml/src/training/28. Expressions/MassRollup1.sysml @@ -1,5 +1,5 @@ package MassRollup1 { - import ScalarFunctions::*; + import NumericalFunctions::*; part def MassedThing { attribute simpleMass :> ISQ::mass; diff --git a/sysml/src/training/28. Expressions/MassRollup2.sysml b/sysml/src/training/28. Expressions/MassRollup2.sysml index 036763d2..93c72e33 100644 --- a/sysml/src/training/28. Expressions/MassRollup2.sysml +++ b/sysml/src/training/28. Expressions/MassRollup2.sysml @@ -1,5 +1,5 @@ package MassRollup2 { - import ScalarFunctions::*; + import NumericalFunctions::*; part def MassedThing { attribute simpleMass :> ISQ::mass; @@ -15,7 +15,7 @@ package MassRollup2 { part filteredMassThing :> compositeThing { attribute minMass :> ISQ::mass; attribute :>> totalMass = - simpleMass + sum(subcomponents.totalMass.{in p:>ISQ::mass; p >= minMass}); + simpleMass + sum(subcomponents.totalMass.?{in p:>ISQ::mass; p >= minMass}); } } \ No newline at end of file diff --git a/sysml/src/training/29. Calculations/Calculation Definitions.sysml b/sysml/src/training/29. Calculations/Calculation Definitions.sysml index 927098f7..00c606f9 100644 --- a/sysml/src/training/29. Calculations/Calculation Definitions.sysml +++ b/sysml/src/training/29. Calculations/Calculation Definitions.sysml @@ -1,6 +1,5 @@ package 'Calculation Definitions' { import ScalarValues::Real; - import RealFunctions::Sqrt; import ISQ::*; calc def Power (whlpwr : PowerValue, Cd : Real, Cf : Real, tm : MassValue, v : SpeedValue ) : PowerValue { diff --git a/sysml/src/training/30. Constraints/Constraint Assertions-1.sysml b/sysml/src/training/30. Constraints/Constraint Assertions-1.sysml index 8d6d12d8..6331222e 100644 --- a/sysml/src/training/30. Constraints/Constraint Assertions-1.sysml +++ b/sysml/src/training/30. Constraints/Constraint Assertions-1.sysml @@ -1,7 +1,7 @@ package 'Constraint Assertions-1' { import ISQ::*; import SI::*; - import ScalarFunctions::*; + import NumericalFunctions::*; part def Engine; part def Transmission; diff --git a/sysml/src/training/30. Constraints/Constraint Assertions-2.sysml b/sysml/src/training/30. Constraints/Constraint Assertions-2.sysml index 83b93506..42067e8d 100644 --- a/sysml/src/training/30. Constraints/Constraint Assertions-2.sysml +++ b/sysml/src/training/30. Constraints/Constraint Assertions-2.sysml @@ -1,7 +1,7 @@ package 'Constraint Assertions-2' { import ISQ::*; import SI::*; - import ScalarFunctions::*; + import NumericalFunctions::*; part def Engine; part def Transmission; diff --git a/sysml/src/training/30. Constraints/Constraints Example-1.sysml b/sysml/src/training/30. Constraints/Constraints Example-1.sysml index 194f313a..c0a64176 100644 --- a/sysml/src/training/30. Constraints/Constraints Example-1.sysml +++ b/sysml/src/training/30. Constraints/Constraints Example-1.sysml @@ -1,7 +1,7 @@ package 'Constraints Example-1' { import ISQ::*; import SI::*; - import ScalarFunctions::*; + import NumericalFunctions::*; part def Engine; part def Transmission; diff --git a/sysml/src/training/30. Constraints/Constraints Example-2.sysml b/sysml/src/training/30. Constraints/Constraints Example-2.sysml index 1832b851..cc9c8c8f 100644 --- a/sysml/src/training/30. Constraints/Constraints Example-2.sysml +++ b/sysml/src/training/30. Constraints/Constraints Example-2.sysml @@ -1,7 +1,7 @@ package 'Constraints Example-2' { import ISQ::*; import SI::*; - import ScalarFunctions::*; + import NumericalFunctions::*; part def Engine; part def Transmission; diff --git a/sysml/src/validation/10-Analysis and Trades/10a-Analysis.sysml b/sysml/src/validation/10-Analysis and Trades/10a-Analysis.sysml index 4d12d297..0330dbda 100644 --- a/sysml/src/validation/10-Analysis and Trades/10a-Analysis.sysml +++ b/sysml/src/validation/10-Analysis and Trades/10a-Analysis.sysml @@ -1,7 +1,7 @@ package '10a-Analysis' { import ISQ::*; import SI::*; - import ScalarFunctions::*; + import NumericalFunctions::*; package VehicleDesignModel { part def Vehicle { diff --git a/sysml/src/validation/15-Properties-Values-Expressions/15_01-Constants.sysml b/sysml/src/validation/15-Properties-Values-Expressions/15_01-Constants.sysml index 95ef6316..79d36a8b 100644 --- a/sysml/src/validation/15-Properties-Values-Expressions/15_01-Constants.sysml +++ b/sysml/src/validation/15-Properties-Values-Expressions/15_01-Constants.sysml @@ -21,10 +21,10 @@ package '15_01-Constants' { */ package 'Mathematical Constants' { attribute e: Real { - assert constraint { Round(e * 1E20) == 271828182845904523536.0 } + assert constraint { round(e * 1E20) == 271828182845904523536.0 } } attribute pi: Real { - assert constraint { Round(pi * 1E20) == 314159265358979323846.0 } + assert constraint { round(pi * 1E20) == 314159265358979323846.0 } } } diff --git a/sysml/src/validation/15-Properties-Values-Expressions/15_03-Value Expression.sysml b/sysml/src/validation/15-Properties-Values-Expressions/15_03-Value Expression.sysml index 6bb9118a..651ac894 100644 --- a/sysml/src/validation/15-Properties-Values-Expressions/15_03-Value Expression.sysml +++ b/sysml/src/validation/15-Properties-Values-Expressions/15_03-Value Expression.sysml @@ -1,7 +1,6 @@ package '15_03-Value Expression' { import SI::*; import USCustomaryUnits::*; - import BasicGeometry::AxisPlacement3DCartesian; part def Vehicle_1 { attribute mass: MassValue = 1200 [kg]; @@ -13,7 +12,6 @@ package '15_03-Value Expression' { part def Wheel { attribute hubDiameter: LengthValue = 18 ['in']; attribute width: LengthValue = 245 [mm]; - attribute placement: AxisPlacement3DCartesian[0..1]; /** * This binds 'outDiameter' to the result of a computed attribute. * There is no need to mark it as "derived".