@@ -31,81 +31,85 @@ package VehicleIndividuals {
3131
3232 package IndividualSnapshots {
3333 public import IndividualDefinitions::*;
34+ private import Occurrences::HappensJustBefore;
3435
3536 attribute t0: DateTime;
3637 attribute t1: DateTime;
3738
38- snapshot part vehicle1_t0: Vehicle1 {
39- doc
40- /*
41- * This is a snapshot of Vehicle1 at time t0;
42- */
43-
44- // Note: Timestamping of snapshots is not yet formalized.
45- attribute t = t0;
46- }
47-
48- timeslice part vehicle1_t0_t1: Vehicle1 {
49- doc
50- /*
51- * This is a time slice of Vehicle1 starting at snapshot vehicle1_t0
52- * (time t0) and ending at time t1.
53- */
54-
55- snapshot :>> start = vehicle1_t0;
56- snapshot :>> done {
57- attribute t = t1;
58- }
39+ individual part vehicle1 : Vehicle1 {
40+ snapshot vehicle1_t0 {
41+ doc
42+ /*
43+ * This is a snapshot of Vehicle1 at time t0;
44+ */
45+
46+ attribute :>> localClock.currentTime = t0;
47+ }
48+
49+ succession : HappensJustBefore first vehicle1_t0 then vehicle1_t0_t1;
50+
51+ timeslice vehicle1_t0_t1 {
52+ doc
53+ /*
54+ * This is a time slice of Vehicle1 starting at snapshot vehicle1_t0
55+ * (time t0) and ending at time t1.
56+ */
57+
58+ snapshot :>> done {
59+ attribute :>> localClock.currentTime = t1;
60+ }
61+ }
5962 }
6063 }
6164
6265 package IndividualConfigurations {
6366 public import IndividualSnapshots::*;
6467
65- individual part vehicle1_C2: Vehicle1 :> vehicle_C2 {
68+ individual part vehicle1_C2: Vehicle1 :> vehicle_C2, vehicle1 {
6669 doc
6770 /*
6871 * This asserts that for some portion of its lifetime, Vehicle1 conforms
6972 * to the configuration vehicle_C2;
7073 */
71- }
72-
73- snapshot part vehicle1_C2_t0 : Vehicle1 :> vehicle1_C2, vehicle1_t0 {
74- doc
75- /*
76- * This is a snapshot of Vehicle1 in configuration vehicle1_C2 at time t0.
77- */
78-
79- snapshot axleAssembly1_t0: AxleAssembly1 :>> frontAxleAssembly {
80- doc
81- /*
82- * frontAxleAssembly is a feature of vehicle1_C2.
83- */
8474
85- snapshot leftFrontWheel_t0: Wheel1 :>> leftFrontWheel {
86- doc
87- /*
88- * This asserts that Wheel1 is the leftFrontWheel of vehicle_C2_t0
89- * (leftFrontWheel is a feature of vehicle_C2::frontAxleAssembly).
90- */
91- }
92- }
93- }
75+ snapshot vehicle1_C2_t0 :> vehicle1_t0 {
76+ doc
77+ /*
78+ * This is a snapshot of Vehicle1 in configuration vehicle1_C2 at time t0.
79+ */
80+
81+ individual axleAssembly1_t0: AxleAssembly1 :>> frontAxleAssembly {
82+ doc
83+ /*
84+ * frontAxleAssembly is a feature of vehicle1_C2.
85+ */
86+
87+ individual leftFrontWheel_t0: Wheel1 :>> leftFrontWheel {
88+ doc
89+ /*
90+ * This asserts that Wheel1 is the leftFrontWheel of vehicle_C2_t0
91+ * (leftFrontWheel is a feature of vehicle_C2::frontAxleAssembly).
92+ */
93+ }
94+ }
95+ }
9496
95- snapshot part vehicle1_C2_t1 : Vehicle1 :> vehicle1_C2, vehicle1_t0_t1.done {
96- doc
97- /*
98- * This is a snapshot of Vehicle1 in configuration vehicle_C2 at time t1.
99- */
100-
101- snapshot axleAssembly1_t1: AxleAssembly1 :>> frontAxleAssembly {
102- snapshot rightFrontWheel_t1: Wheel1 :>> rightFrontWheel {
103- doc
104- /*
105- * This asserts that Wheel1 is the rightFrontWheel of vehicle_C2_t1.
106- */
107- }
108- }
109- }
97+ snapshot vehicle1_C2_t1 :> vehicle1_t0_t1.done {
98+ doc
99+ /*
100+ * This is a snapshot of Vehicle1 in configuration vehicle_C2 at time t1.
101+ */
102+
103+ individual axleAssembly1_t1: AxleAssembly1 :>> frontAxleAssembly {
104+ individual rightFrontWheel_t1: Wheel1 :>> rightFrontWheel {
105+ doc
106+ /*
107+ * This asserts that Wheel1 is the rightFrontWheel of vehicle_C2_t1.
108+ */
109+ }
110+ }
111+ }
112+
113+ }
110114 }
111115}
0 commit comments