Added validCSEventMode

INTO-CPS-Association · Oct 7, 2022 · 5f720c0 · 5f720c0
1 parent 1f5a096
commit 5f720c0
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 5 deletions.
diff --git a/fmi3/rule-model/CoSimulation.vdmsl b/fmi3/rule-model/CoSimulation.vdmsl
@@ -27,16 +27,17 @@
  *
  *********************************************************************************/
 types
-	CoSimulation' = [CoSimulation]
-	inv cs == cs <> nil => allOf
+	CoSimulation' = [CoSimulation] * FmiModelDescription
+	inv mk_(cs, fmd) == cs <> nil => allOf
 	([
 		inv_Annotations'(cs.annotations),
 
 		let ecs = effectiveCoSimulation(cs) in
 		[
 			-- Rules a defined in CoSimulation.adoc
 			rule("validCSModelIdentifier", validCSModelIdentifier(ecs)),
-			rule("validCSIntermediateUpdate", validCSIntermediateUpdate(ecs))
+			rule("validCSIntermediateUpdate", validCSIntermediateUpdate(ecs)),
+			rule("validCSEventMode", validCSEventMode(ecs, fmd))
 		]
 	]);
 

diff --git a/fmi3/rule-model/FMIModelDescription.vdmsl b/fmi3/rule-model/FMIModelDescription.vdmsl
@@ -34,7 +34,7 @@ types
 	inv fmd == allOf
 	([
 		inv_ModelExchange'(fmd.modelExchange),
-		inv_CoSimulation'(fmd.coSimulation),
+		inv_CoSimulation'(mk_(fmd.coSimulation, fmd)),
 		inv_ScheduledExecution'(fmd.scheduledExecution),
 		inv_UnitDefinitions'(fmd.unitDefinitions),
 		inv_TypeDefinitions'(fmd.typeDefinitions),

diff --git a/fmi3/rule-model/Rules/CoSimulation.adoc b/fmi3/rule-model/Rules/CoSimulation.adoc
@@ -29,10 +29,25 @@ validCSIntermediateUpdate: CoSimulation +> bool
 validCSIntermediateUpdate(cs) ==
 	-- @OnFail("%NAME: canReturnEarlyAfterIntermediateUpdate requires providesIntermediateUpdate at %s",
 	-- loc2str(cs.location))
-	( cs.canReturnEarlyAfterIntermediateUpdate = true => cs.providesIntermediateUpdate = true )
+	( cs.canReturnEarlyAfterIntermediateUpdate = true => cs.providesIntermediateUpdate = true );
 ----
 // {vdm}
 - See <<table-CoSimulation-details>>.
+
+===== A.{section}.{subsection}.{counter:typerule} Rule: validCSEventMode
+[[validCSEventMode]]
+// {vdm}
+----
+validCSEventMode: CoSimulation * FmiModelDescription +> bool
+validCSEventMode(cs, fmd) == 
+	-- @OnFail("%NAME: hasEventMode must be true since FMU has clocks at %s",
+	-- loc2str(cs.location))
+	( let hasClocks = exists mv in seq fmd.modelVariables & is_Clock(mv) in
+		hasClocks => cs.hasEventMode );
+----
+// {vdm}
+- See <<table-CoSimulation-details>>.
+
 // This adds the docrefs for VDM only
 ifdef::hidden[]
 // {vdm}
@@ -46,6 +61,11 @@ values
 		],
 
 		"validCSIntermediateUpdate" |->
+		[
+			"<FMI3_STANDARD>#table-CoSimulation-details"
+		],
+
+		"validCSEventMode" |->
 		[
 			"<FMI3_STANDARD>#table-CoSimulation-details"
 		]