Verify target of Real variables with attribute 'derivative'

[filip-stenstrom]

When a variable references what other variable they are a derivative of, no warning/error is produced if the referenced variable cannot have a derivative.

Example of part of XML that doesn't produce any warnings/errors:

<ModelVariables>
    <!-- idx: 1 -->
    <ScalarVariable name="state_var" valueReference="0" variability="discrete" initial="exact">
      <Boolean start="true"/>
    </ScalarVariable>
    <!-- idx: 2 -->
    <ScalarVariable name="der(state_var)" valueReference="1" causality="output" variability="continuous" initial="approx">
      <Real derivative="1" start="1.0"/>
    </ScalarVariable>
</ModelVariables>

<ModelStructure>
  <Derivatives>
    <Unknown index="2"/>
  </Derivatives>
</ModelStructure>

I believe there are two levels of strictness:

1. continuous/discrete Real variables
2. (continuous/discrete) state variables - the target of the derivative attribute has some more limitations (I guess it has to have causality=local/output)

[nickbattle]

@filip-stenstrom In VDMCheck2, we check the following:

• The rules only apply if this is ModelExchange, or CS with providesDirectionalDerivative, else no check is made.
• Calculate the set of derivative SV indexes, where an SV is included if it's Real and it has the "derivative" flag set.
• If the set above is not empty, then it must equal the ModelStructure.derivatives set
• Otherwise if the derivatives set is empty, so must be the ModelStructure derivatives.

But I think I agree that our check for being a state derivatives could be more precise. The standard doesn't really clearly say how a state derivative is defined (or a continuous time state, come to that).

[filip-stenstrom]

Thanks that's good to know.

I'm not either certain about definition of state variables. I take it as "anything referenced by ModelStructure.Derivatives is a state variable", and from the spec. I can see that it "can" be a local, and by intuition I assume it can be flagged as an output (no other causality makes sense).

For your point 1, I see the point in skipping CS if no providesDirectionalDerivative, since they can't be via the API with their property as a state variable. But at the same time, if someone decides to still use the ModelStructure.Derivatives without providesDirectionalDerivative, I think the check should be made, since the standard should still be followed.

(Also, in my main post I wrote only continuous Reals, but discrete should also be checked, updating...)

[filip-stenstrom]

• Calculate the set of derivative SV indexes, where an SV is included if it's Real and it has the "derivative" flag set.
• If the set above is not empty, then it must equal the ModelStructure.derivatives set

I don't believe the sets have to equal, since derivative attribute can be used for e.g. Real inputs.

[nickbattle]

It is frustrating trying to work out the formal interpretation of an informal standard! Though hopefully the effort of doing so will be paid back one day :-)

I interpreted the standard to mean that the SVs (or something else?) defines the states, and the ModelStructure derivatives have to be "Exactly all of the (exposed) state derivatives", taken from the XSD annotation. Though it may be that "exposed" is not something that can be determined by looking at the SVs (the term is not defined). It also says, "A ModelExchange
FMU must expose all derivatives of its continuous-time states in element <Derivatives>". I'm not sure whether "states" is always short for "continuous-time states" - though I think the latter are things that are real/continuous SVs that also have a real/continuous SV that is their derivative. So depending on what they mean, you might be right about the sets not having to be equal (though derivatives has to be a subset, presumably).

These are the definitions that I currently have. I'd be very interested to know if I should tighten/change them!

	isContinuousTimeState: nat1 * seq of ScalarVariable +> bool
	isContinuousTimeState(i, svs) ==
		is_Real(svs(i).variable)
		and svs(i).variability = <continuous> 
		and exists j in seq svs &
			is_Real(j.variable) and j.variable.derivative = i;

	isStateDerivative: ScalarVariable +> bool
	isStateDerivative(sv) ==
		is_Real(sv.variable) and sv.variable.derivative <> nil;

I see your point about verifying the derivatives even if this is a CS only FMU. The standard does say that the derivatives are ignored in that case, but perhaps warnings would be appropriate anyway.

[iakovn]

my 2 cents:

The state derivatives of an FMU are listed under element . All ScalarVariables listed in this element must have attribute derivative (in order that the continuous-time states are uniquely defined).
Derivatives: Ordered list of all state derivatives, in other words, a list of ScalarVariable indices where every corresponding ScalarVariable must be a state derivative. [Note that only continuous Real variables are listed here...

There is no way AFAIK to know which and how many discrete states are present and so this is referring to continuous states.
However, it's "derivates" are listed under ModelStructure and then those refer to states. "derivative" variables are Real but do not (in general) need to be continuous [could be constant or input]. The referred "states" must be continuous. "derivative" that has "dependencies" on states/inputs listed must be continuous.

derivative: if present, this variable is the derivative of variable with ScalarVariable index "derivative".

There may be other variables with this attribute at least for aliases or for algebraic variables (probably rare case and not much used if used at all). Theoretically, FMU might even be indicating that it expects two inputs to have "derivative" relation to each other. Other pure theoretical case where target of derivative does not need to be continuous is if derivative is constant zero. I would therefore vote for checking target to be continuous but will not enforce that all variables with derivate attribute are listed under ModelStructure.

[nickbattle]

@iakovn OK, I think that is getting clearer; thanks for the extra input. So it sounds like I need to relax the current check that all SVs labelled as "derivative" must be in ModelStructure. And you're saying that a derivative need not be continuous (because it could be constant), unless it is listed as having dependencies, in which case it must be continuous.

If that's correct, it is easy to state formally (for the checker). Trying to fix the wording in the standard seems harder (ironically!)

[nickbattle]

(@filip-stenstrom Sorry if I'm hijacking this discussion, but this is the best input I've had so far on what the Standard means!)

I've changed the formal model to say the following. (Hopefully the VDM-SL syntax is obvious. The strange looking set={true} constructs are to ensure that every test in the set is made; an and-clause would stop at the first falsity):

-- ModelStructure derivative indexes must be valid and if the derivative has dependencies, then
-- it must be continuous. Note that SVs can have derivative set but not be listed here.
(
	md.modelExchange <> nil
	or (md.coSimulation <> nil and nilBool(md.coSimulation.providesDirectionalDerivative)) =>
		md.modelStructure.derivatives <> nil =>
		{
			/* @OnFail("2.2.8 Derivative index out of range at line %s", u.location) */
			( u.index <= len eModelVariables )

			and let sv = eModelVariables(u.index) in
			{
				/* @OnFail("2.2.8 SV not a state derivative at line %s", u.location) */
				( isStateDerivative(sv) ),

				/* @OnFail("2.2.8 Derivative must be continuous at line %s", u.location) */
				( u.dependencies <> nil => sv.variability = <continuous> )
			}
			= {true}

			| u in seq md.modelStructure.derivatives
		}
		= {true}
),

That now picks up various cases in the cross-check repository, like this:

------------------------------- ./me/win64/Easy5/2017.1/Linear_Pos/Linear_Pos.fmu
...
2.2.8 SV not a state derivative at line 97
2.2.8 SV not a state derivative at line 98
2.2.8 SV not a state derivative at line 99
...
Errors found.

This is because they have listed various variables in the ModelStructure derivatives, but they are not "derivative" in the ModelVariables section (though they are continuous Reals).