Merge pull request #355 from Systems-Modeling/ST6RI-532

ST6RI-532 Minor fixes to space modeling & shape library

Author: seidewitz

sysml.library/Domain Libraries/Geometry/ShapeItems.sysml

@@ -9,21 +9,35 @@ package ShapeItems {
 	private import Objects::*;
 	private import Items::Item;
 	private import SequenceFunctions::isEmpty;
-	
+	private import SequenceFunctions::notEmpty;
+	private import SequenceFunctions::size;	
+	private import ControlFunctions::'?';
+
 	/**
-	 * A Line is a Curve that is a straight line of a given length.
+	 * A PlanarCurve is a Curve with a given length embeddable in a plane.
 	 */
-	item def Line :> Curve {
-		attribute :>> length;
-		attribute :>> outerSpaceDimension = 1;
+	item def PlanarCurve :> Curve {
+		attribute :>> length [1] ;
+
+		constraint { notEmpty(outerSpaceDimension) &  outerSpaceDimension <= 2 }
 	}
 
 	/**
 	 * A PlanarSurface is a flat Surface with a given area.
 	 */
 	item def PlanarSurface :> Surface {
-		attribute :>> area;
+		attribute :>> area [1];
 		attribute :>> outerSpaceDimension = 2;
+
+		item :>> shape : PlanarCurve;
+	}
+
+	/**
+	 * A Line is a Curve that is a straight line of a given length.
+	 */
+	item def Line :> PlanarCurve {
+		attribute :>> length [1];
+		attribute :>> outerSpaceDimension = 1;
 	}
 
 	/**
@@ -39,12 +53,12 @@ package ShapeItems {
 	/**
 	 * A Circle is a Path in the shape of a circle of a given radius.
 	 */
-	item def Circle :> Path {
-		attribute radius :>> radius;
+	item def Circle :> Path, PlanarCurve {
+		attribute :>> radius;
 
 		item :>> faces [0];
 		item :>> edges [1] {
-			attribute circumference :>> length = Circle::radius * TrigFunctions::pi;
+			attribute circumference :>> length = Circle::radius * TrigFunctions::pi * 2;
 			item :>> shape : Item [0];
 			item :>> vertices [0];
 		}
@@ -54,15 +68,15 @@ package ShapeItems {
 	/**
 	 * A Disc is a Shell bounded by a Circle.
 	 */
-	item def Disc :> Shell {
-		attribute radius :>> radius;
+	item def Disc :> Shell, PlanarSurface {
+		attribute :>> radius;
 
 		item :>> shape : Circle [1] {
 			attribute :>> radius = Disc::radius;
 		}
 
 		item :>> faces : PlanarSurface [1] {
-			item :>> edges [1]; 
+			item :>> edges [1];
 		}
 		item :>> edges : Circle [1] = shape;
 		item :>> vertices [0];
@@ -76,38 +90,42 @@ package ShapeItems {
 	item def Sphere :> Shell {
 		attribute :>> radius;
 
-		item faces : Surface [1] :>> faces;
+		item :>> faces [1];
 		item :>> edges [0];
 		item :>> vertices [0];
+
+		attribute :>> genus = 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 baseRadius [1] = radius;
+		attribute apexRadius [1] default 0 [m];
+		attribute :>> height [1];
+
+		attribute :>> radius [1];
 		attribute isTruncated : Boolean [1] = (apexRadius > 0);
 
-		item faces : Surface [2..3] :>> faces;
+		item :>> faces [2..3];
 		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 { 
+		item :>> edges : Circle [2..4];
+		item be [2] :> edges { 
 			attribute :>> radius = baseRadius;
 		}
-		item ae [0..1] :> edges { 
+		item ae [0..2] :> edges { 
 			attribute :>> radius = apexRadius;
 		}
-		constraint { isEmpty(af) == isEmpty(ae) }
+		constraint { isEmpty(af) ? isEmpty(ae) : size(ae) == 2 }
 
-		item vertices : Point [0..1] :>> vertices;
-		constraint { isEmpty(ae) == isEmpty(vertices) }
+		item :>> vertices [0..1];
+		constraint { isEmpty(ae) == notEmpty(vertices) }
 
 		/* Faces to edges */
 		connection :WithinBoth connect bf.edges [1] to be [0..*];
@@ -122,38 +140,37 @@ package ShapeItems {
 		connection :WithinBoth connect be [2] to be [2];
 		connection :WithinBoth connect ae [2] to ae [2];
 
+		attribute :>> genus = 0;
 	}
 
 	/**
 	 * 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;
+		attribute :>> apexRadius = baseRadius;
 	}
 
 	/**
 	 * 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;
+		attribute :>> length [1];
+		attribute :>> width [1];
+		attribute :>> height [1];
 
 		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 tf [1] :> faces;
+		item bf [1] :> faces;
+		item ff [1] :> faces;
+		item rf [1] :> faces;
+		item slf [1] :> faces;
+		item srf [1] :> faces;
+
+		item :>> edges : Line [24] {
 			item :>> vertices [2]; 
 		}
 		item tfe [2]  :> edges { attribute :>> length = Cuboid::length; }
@@ -169,7 +186,7 @@ package ShapeItems {
 		item urle [2] :> edges { attribute :>> length = Cuboid::height; }
 		item urre [2] :> edges { attribute :>> length = Cuboid::height; }
 
-		item vertices : Point [8] :>> vertices;
+		item :>> vertices [24];
 		item tflv [3] :> vertices;
 		item tfrv [3] :> vertices;
 		item trlv [3] :> vertices;
@@ -261,6 +278,8 @@ package ShapeItems {
 		connection :WithinBoth connect bfrv [3] to bfrv [3];
 		connection :WithinBoth connect brlv [3] to brlv [3];
 		connection :WithinBoth connect brrv [3] to brrv [3];
+
+		attribute :>> genus = 0;
 	}
 	alias Box for Cuboid;
 }

sysml.library/Kernel Library/Objects.kerml

@@ -16,7 +16,8 @@ package Objects {
 	private import SequenceFunctions::notEmpty;
 	private import SequenceFunctions::union;
 	private import CollectionFunctions::contains;
-	private import ScalarValues::Integer;	     
+	private import ScalarValues::Integer;
+	private import ScalarValues::Natural;
 
 	/**
 	 * Object is the most general class of structural occurrences that may change over time.
@@ -81,9 +82,9 @@ package Objects {
 	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;
+		feature genus : Natural[0..1] default 0;
 
-		inv { notEmpty(genus) implies (isClosed & genus >= 0) }
+		inv { notEmpty(genus) implies isClosed }
 	}
 
 	/*

sysml.library/Kernel Library/Occurrences.kerml

@@ -37,7 +37,7 @@ package Occurrences {
 		feature predecessors: Occurrence[0..*] subsets occurrences;
 
 		/**
-		 * Occurrences that start after this occcurrence ends.
+		 * Occurrences that start after this occurrence ends.
 		 */
 		feature successors: Occurrence[0..*] subsets occurrences;
 
@@ -84,7 +84,8 @@ package Occurrences {
 		 * to 3, without regard to higher dimensional spaces it might be emedded in.
 		 */
 		feature innerSpaceDimension : Natural [1];
-		inv { innerSpaceDimension >= 0 & innerSpaceDimension <= 3 }
+
+		inv { innerSpaceDimension <= 3 }
 
 		/**
 		 * For occurrences of innerSpaceDimension 1 or 2, the number of variables need to
@@ -188,7 +189,7 @@ package Occurrences {
 		/**
 		 * Occurrences of which this occurrence is a space shot.
 		 */
-		feature spaceShotOf: Occurrence[1..*] subsets spaceSliceOf;
+		feature spaceShotOf: Occurrence[0..*] subsets spaceSliceOf;
 
 		/**
 		 * Sets of occurrences, where the time and space taken by all the occurrences in each
@@ -270,12 +271,12 @@ package Occurrences {
 		 * 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.
+		 * A space shot of this Occurrence that is not among those of its space interior, 
+		 * which must be outside it. It must not have a spaceBoundary.
 		 */
 		portion feature spaceBoundary: Occurrence[0..1] subsets spaceShots { 
 			feature redefines isClosed = true;
@@ -286,7 +287,8 @@ package Occurrences {
 		 */
 		feature spaceBoundaryOf: Occurrence[0..*] subsets spaceShotOf;
 
-		inv { isClosed implies contains(self.unionsOf, union(spaceBoundary, spaceInterior)) }
+		inv { !isClosed implies contains(self.unionsOf, union(spaceBoundary, spaceInterior)) }
+		inv { innerSpaceDimension == 0 implies isEmpty(spaceBoundary) }
 
 		connector :OutsideOf 
 			from separateSpaceToo :> spaceInterior [0..1]
@@ -476,8 +478,8 @@ package Occurrences {
 	 * 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;
+		end feature snapshotOccurrence: Occurrence[1..*] redefines timeSliceOccurrence subsets snapshottedOccurrence.snapshots;
+		end feature snapshottedOccurrence: Occurrence[0..*] redefines timeSlicedOccurrence subsets snapshotOccurrence.snapshotOf;
 	}
 
 	/**
@@ -498,8 +500,10 @@ package Occurrences {
 	 * 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;
+		end feature spaceShotOccurrence: Occurrence[1..*] redefines spaceSliceOccurrence subsets spaceShottedOccurrence.spaceShots;
+		end feature spaceShottedOccurrence: Occurrence[1..*] redefines spaceSlicedOccurrence subsets spaceShotOccurrence.spaceShotOf;
+
+		inv { spaceShotOccurrence.innerSpaceDimension < spaceShottedOccurrence.innerSpaceDimension }
 	}
 
 	/**

sysml/src/examples/Geometry Examples/CarWithShapeAndCSG.sysml

@@ -6,30 +6,34 @@ package CarWithShapeAndCSG {
 
 	item def Car :> CompoundSpatialItem {
 		item :>> shape : Cuboid [1] {
-			/* Quantify faces, etc, by redefining nested features. */
+			/* Quantify height, etc, by redefining nested features. */
 		}
 		part powerSource : Engine [1] :> componentItems;
 	}
 
 	part def Engine :> SpatialItem {
-  		item :>> shape [1];
-  		
+		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;
- 			}
+		private item c1 : SpatialItem [1] {
+			item :>> shape : Cylinder [1] {
+				 /* Quantify radius, etc, by redefining nested features. */
+			}
+			attribute :>> coordinateFrame {
+				attribute origin = c1Position;
+			}
+		}
+		
+		private item c2 : SpatialItem [1] {
+			item :>> shape : Cylinder [1] {
+				 /* Quantify radius, etc, by redefining nested features. */
+			}
+			attribute :>> coordinateFrame {
+				attribute origin = c2Position;
+			}
 		}
 
 		/* CSG intersection of c1 and c2. */