From 078a40d1329ef88cfd52177c146f6c14532ae886 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 12 Jan 2024 13:40:01 +0000 Subject: [PATCH] More rule-model tweaks --- fmi2/rule-model/Common.vdmsl | 4 +- fmi2/rule-model/EffectiveVariables.vdmsl | 4 +- fmi2/rule-model/FMIModelDescription.vdmsl | 8 +- .../Rules/FmiModelDescription.adoc.vdmsl | 174 +++++++++--------- .../Rules/TypeDefinitions.adoc.vdmsl | 2 +- fmi2/rule-model/TypeDefinitions.vdmsl | 2 +- 6 files changed, 100 insertions(+), 94 deletions(-) diff --git a/fmi2/rule-model/Common.vdmsl b/fmi2/rule-model/Common.vdmsl index 34e8351..4110df5 100644 --- a/fmi2/rule-model/Common.vdmsl +++ b/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 elseif is_(v, Boolean) or is_(v, BooleanType) then diff --git a/fmi2/rule-model/EffectiveVariables.vdmsl b/fmi2/rule-model/EffectiveVariables.vdmsl index 37b793e..e6d1645 100644 --- a/fmi2/rule-model/EffectiveVariables.vdmsl +++ b/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) == diff --git a/fmi2/rule-model/FMIModelDescription.vdmsl b/fmi2/rule-model/FMIModelDescription.vdmsl index 913fa1c..88641ae 100644 --- a/fmi2/rule-model/FMIModelDescription.vdmsl +++ b/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)) ] ]); diff --git a/fmi2/rule-model/Rules/FmiModelDescription.adoc.vdmsl b/fmi2/rule-model/Rules/FmiModelDescription.adoc.vdmsl index f53a50b..8048ff4 100644 --- a/fmi2/rule-model/Rules/FmiModelDescription.adoc.vdmsl +++ b/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 = }, - 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 = ) +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 { , }) + 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 { , }) }, + | 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 = ) +validOutputs: FmiModelDescription * ModelVariables +> bool +validOutputs(fmd, evs) == + let outputIndexes = { svi | svi in set inds evs & evs(svi).causality = } 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 = ) ]) - | 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 = + and sv.initial in set { , }) + + or (sv.causality = ) + + or (sv in set ctVars + and sv.initial in set { , }) + + or (sv in set sdVars + and sv.initial in set { , }) } + 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 = diff --git a/fmi2/rule-model/Rules/TypeDefinitions.adoc.vdmsl b/fmi2/rule-model/Rules/TypeDefinitions.adoc.vdmsl index c1d9e22..5d6a028 100644 --- a/fmi2/rule-model/Rules/TypeDefinitions.adoc.vdmsl +++ b/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 ([ diff --git a/fmi2/rule-model/TypeDefinitions.vdmsl b/fmi2/rule-model/TypeDefinitions.vdmsl index 90690bf..f23192d 100644 --- a/fmi2/rule-model/TypeDefinitions.vdmsl +++ b/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): -> inv_RealType'(tdef.fmi2SimpleType), -> inv_IntegerType'(tdef.fmi2SimpleType), -> inv_BooleanType'(tdef.fmi2SimpleType),