More rule-model tweaks

fmi2/rule-model/Common.vdmsl

@@ -37,6 +37,7 @@ types
 
 types
 	Variable = Real | Integer | Boolean | String | Enumeration;
+	NumType = RealType | IntegerType | EnumerationType;
 
 	-- Value references
 	fmi2ValueReference = nat;
@@ -94,7 +95,8 @@ functions
 	/**
 	 * Turn a Variable or Type into a Kind.
 	 */
-	kindOf: Real | Integer | Boolean | String | Enumeration | SimpleType +> Kind
+	kindOf: Real | Integer | Boolean | String | Enumeration |
+			RealType | IntegerType | BooleanType | StringType | EnumerationType +> Kind
 	kindOf(v) ==
 		if     is_(v, Integer) or is_(v, IntegerType) then <Integer>
 		elseif is_(v, Boolean) or is_(v, BooleanType) then <Boolean>

fmi2/rule-model/EffectiveVariables.vdmsl

@@ -51,7 +51,7 @@ functions
 		in
 			if decltype = nil
 			then effectivetypeVariable(mv)
-			elseif kindOf(decltype) = kind
+			elseif kindOf(decltype.fmi2SimpleType) = kind
 			then effectiveTypedVariable(mv, decltype)
 			else mv;		-- Type error reported elsewhere
 
@@ -193,7 +193,7 @@ functions
 
 			others -> undefined
 		end
-	pre kindOf(decltype) = kindOf(mv.fmi2ScalarVariable);
+	pre kindOf(decltype.fmi2SimpleType) = kindOf(mv.fmi2ScalarVariable);
 
 	effectivetypeVariable: ScalarVariable +> ScalarVariable
 	effectivetypeVariable(mv) ==

fmi2/rule-model/FMIModelDescription.vdmsl

@@ -61,9 +61,9 @@ types
 			rule("validMinMax", validMinMax(fmd, evs)),
 			rule("validStart", validStart(fmd, evs)),
 			rule("validMultipleSets", validMultipleSets(fmd, evs)),
-			rule("validOutput", validOutput(fmd, evs)),
-			rule("validInitialUnknowns", validInitialUnknowns(fmd, evs)),
-			rule("validOutputReferences", validOutputReferences(fmd, evs)),
-			rule("validUnknownDependencies", validUnknownDependencies(fmd, evs))
+			rule("validVariableUnits", validVariableUnits(fmd, evs)),
+			rule("validOutputs", validOutputs(fmd, evs)),
+			rule("validDerivatives", validDerivatives(fmd, evs)),
+			rule("validInitialUnknowns", validInitialUnknowns(fmd, evs))
 		]
 	]);

fmi2/rule-model/Rules/FmiModelDescription.adoc.vdmsl

@@ -57,7 +57,7 @@ validVariableTypes(fmd) == allOf
 
 			-- @OnFail("%NAME: %s type %s mismatch at %s",
 			-- mv.name, mv.declaredType, loc2str(mv.location))
-			and ( kindOf(tdef) = kindOf(mv.fmi2ScalarVariable) )
+			and ( kindOf(tdef.fmi2SimpleType) = kindOf(mv.fmi2ScalarVariable) )
 
 		| mv in seq fmd.modelVariables
 	]);
@@ -155,105 +155,109 @@ validReinits(fmd) == allOf
 	]);
 ----
 ----
-validOutput: FmiModelDescription * ModelVariables +> bool
-validOutput(fmd, evs) ==
-	let outputRefs = { ev.valueReference | ev in seq evs & ev.causality = <output> },
-		structRefs = { u.valueReference | u in seq
-						default[seq of Unknown](fmd.modelStructure.outputs, []) }
-	in
-		if outputRefs <> {}
-		then
-			-- @OnFail("%NAME: Output variables but no outputs declared at %s",
-			-- loc2str(fmd.modelStructure.location))
-			( structRefs <> {} )
-
-			and
-			-- @OnFail("%NAME: Outputs section does not match output variables at %s",
-			-- loc2str(fmd.modelStructure.location))
-			( structRefs = outputRefs )
-		else
-			-- @OnFail("%NAME: Outputs should be omitted at %s",
-			-- loc2str(fmd.modelStructure.location))
-			( structRefs = {} );
-----
-----
-validInitialUnknowns: FmiModelDescription * ModelVariables +> bool
-validInitialUnknowns(fmd, evs) ==
-	let ctVars = continuousTimeStates(evs),
-		sdVars = stateDerivatives(evs),
-		required = { ev.valueReference | ev in seq evs &
-			(ev.causality = <calculatedParameter>)
+validVariableUnits: FmiModelDescription * ModelVariables +> bool
+validVariableUnits(fmd, evs) == allOf
+([
+	is_Real(sv.fmi2ScalarVariable) => allOf
+	([
+		-- @OnFail(1019, "2.2.7 ScalarVariable %s, Real unit must be defined for displayUnit %s at %s",
+		--	sv.name, sv.fmi2ScalarVariable.displayUnit, loc2str(sv.location))
+		( sv.fmi2ScalarVariable.displayUnit <> nil => sv.fmi2ScalarVariable.unit <> nil ),
 
-			or (ev in set ctVars
-				and ev.initial in set { <approx>, <calculated> })
+		sv.fmi2ScalarVariable.unit <> nil =>
+			-- @OnFail(1020, "2.2.7 ScalarVariable %s, Real unit %s not defined in UnitDefinitions at %s",
+			--	sv.name, sv.fmi2ScalarVariable.unit, loc2str(sv.location))
+			( fmd.unitDefinitions <> nil
+				and exists u in seq fmd.unitDefinitions & u.name = sv.fmi2ScalarVariable.unit )
+	])
 
-			or (ev in set sdVars
-				and ev.initial in set { <approx>, <calculated> }) },
+	| sv in seq evs
+]);
 
-		IUs      = default[seq of Unknown](fmd.modelStructure.initialUnknowns, []),
-		allIUs   = { iu.valueReference | iu in seq IUs }
-	in
-		allOf
-		([
-			-- ?? @OnFail("%NAME: InitialUnknowns must include refs: %s",
-			-- required \ allIUs) ?? This may not be true!
-			-- ( required subset allIUs ),
-
-			-- @OnFail("%NAME: InitialUnknowns can only include refs: %s",
-			-- required union optional)
-			( allIUs subset required union optional ),
-
-			-- @OnFail("%NAME: InitialUnknowns cannot include EventIndicators: %s ",
-			-- allIUs inter allEIs)
-			( allIUs inter allEIs = {} ),
-
-			-- @OnFail("%NAME: InitialUnknowns must not have duplicates: %s")
-			( card allIUs = len IUs ),
-
-			[
-				iu.dependencies <> nil and iu.dependencies <> [] =>
-					-- @OnFail("%NAME: InitialUnknown dependencies must all be known at %s",
-					-- loc2str(iu.location))
-					( forall d in seq iu.dependencies & d not in set allIUs )
-
-				| iu in seq IUs
-			]
-		]);
 ----
 ----
-validOutputReferences: FmiModelDescription * ModelVariables +> bool
-validOutputReferences(fmd, evs) ==
-	fmd.modelStructure.outputs <> nil => allOf
-	([
-		-- @OnFail("%NAME: Output valueReference %s is not an output at %s",
-		--  ei.valueReference, loc2str(ei.location))
-		( exists ev in seq evs &
-			ev.valueReference = ei.valueReference and ev.causality = <output> )
+validOutputs: FmiModelDescription * ModelVariables +> bool
+validOutputs(fmd, evs) ==
+	let outputIndexes = { svi | svi in set inds evs & evs(svi).causality = <output> } in
+		if outputIndexes <> {}
+		then
+			-- @OnFail(1022, "2.2.8 Output variables but no outputs declared at %s",
+			--	loc2str(fmd.modelStructure.location))
+			( fmd.modelStructure.outputs <> nil )
 
-		| ei in seq fmd.modelStructure.outputs
-	]);
+			and let structIndexes = { u.index | u in seq fmd.modelStructure.outputs } in allOf
+			([
+
+				-- @OnFail(1023, "2.2.8 Outputs section does not match output variables at %s",
+				--	loc2str(fmd.modelStructure.location))
+				( structIndexes = outputIndexes ),
+
+				-- @OnFail(1024, "2.2.8 Output indexes out of range at %s",
+				--	loc2str(fmd.modelStructure.location))
+				( forall i in set structIndexes & i <= len evs )
+			])
+		else
+			/* @OnFail(1025, "2.2.8 Outputs should be omitted at %s",
+				loc2str(fmd.modelStructure.location)) */
+			( fmd.modelStructure.outputs = nil );
 ----
 ----
-validUnknownDependencies: FmiModelDescription * ModelVariables +> bool
-validUnknownDependencies(fmd, evs) ==
-	let allUnknowns = conc
-	[
-		default[seq of Unknown](fmd.modelStructure.outputs, []),
-		default[seq of Unknown](fmd.modelStructure.initialUnknowns, [])
-	] in
-		allUnknowns <> [] => allOf
+validDerivatives: FmiModelDescription * ModelVariables +> bool
+validDerivatives(fmd, evs) ==
+	fmd.modelExchange <> nil
+	or (fmd.coSimulation <> nil and fmd.coSimulation.providesDirectionalDerivative = true) =>
+		fmd.modelStructure.derivatives <> nil => allOf
 		([
-			unk.dependencies <> nil and unk.dependencies <> [] => allOf
+			-- @OnFail(1026, "2.2.8 Derivative index out of range at %s", loc2str(u.location))
+			( u.index <= len evs )
+
+			and let sv = evs(u.index) in allOf
 			([
-				-- @OnFail("%NAME: Unknown dependency %s invalid at %s", vr, loc2str(unk.location))
-				( exists ev in seq evs & ev.valueReference = vr )
+				-- @OnFail(1027, "2.2.8 SV not a state derivative at %s", loc2str(u.location))
+				( isStateDerivative(sv) ),
 
-				| vr in seq unk.dependencies
+				-- @OnFail(1028, "2.2.8 Derivative must be continuous at %s", loc2str(u.location))
+				( u.dependencies <> nil => sv.variability = <continuous> )
 			])
 
-			| unk in seq allUnknowns
+			| u in seq fmd.modelStructure.derivatives
 		]);
 ----
+----
+validInitialUnknowns: FmiModelDescription * ModelVariables +> bool
+validInitialUnknowns(fmd, evs) ==
+	let ctVars = continuousTimeStates(evs),
+		sdVars = stateDerivatives(evs),
+		initIndexes = { svi | svi in set inds evs &
+			let sv = evs(svi) in
+				(sv.causality = <output>
+					and sv.initial in set { <approx>, <calculated> })
+
+				or (sv.causality = <calculatedParameter>)
+
+				or (sv in set ctVars
+					and sv.initial in set { <approx>, <calculated> })
+
+				or (sv in set sdVars
+					and sv.initial in set { <approx>, <calculated> }) }
+	in
+		initIndexes <> {} =>
+			let ius = fmd.modelStructure.initialUnknowns in allOf
+			([
+				-- @OnFail(1029, "2.2.8 InitialUnknowns must include: %s", initIndexes)
+				( ius <> nil ),
+
+				-- @OnFail(1030, "2.2.8 InitialUnknowns must not include: %s",
+				-- { u.index | u in seq ius } \ initIndexes )
+				( ius <> nil => { u.index | u in seq ius } subset initIndexes ),
+
+				-- @OnFail(1031, "2.2.8 InitialUnknowns are not sorted: %s",
+				-- [ u.index | u in seq ius ])
+				( ius <> nil => 
+						forall i in set inds ius &
+							i = len ius or ius(i).index < ius(i+1).index )
+			]);
+----
 
 values
 	FmiModelDescription_refs : ReferenceMap =

fmi2/rule-model/Rules/TypeDefinitions.adoc.vdmsl

@@ -11,7 +11,7 @@ validTypeDefinitionNames(tdefs) ==
 			len names = card elems names );
 ----
 ----
-validTypeMinMax: RealType | IntegerType | EnumerationType +> bool
+validTypeMinMax: NumType +> bool
 validTypeMinMax(type) ==
 	let mk_(kmin, kmax) = minMaxOfKind(kindOf(type)) in allOf
 	([

fmi2/rule-model/TypeDefinitions.vdmsl

@@ -38,7 +38,7 @@ types
 
 	SimpleType' = SimpleType	-- The union of all types
 	inv tdef ==
-		cases kindOf(tdef):
+		cases kindOf(tdef.fmi2SimpleType):
 			<Real>	        -> inv_RealType'(tdef.fmi2SimpleType),
 			<Integer>	    -> inv_IntegerType'(tdef.fmi2SimpleType),
 			<Boolean>	    -> inv_BooleanType'(tdef.fmi2SimpleType),