Initialize plugin

[CThuleHansen]

It is time to lay the foundations of the initialize plugin for Maestro2. This issue shall contain the initial discussions on how to do so.

The current initialize plugin utilizes the existing COE and intercepts all the FMI calls, which it turns into statements.

I was wondering if you guys have worked on a formal model of initializing a set of FMUs? i.e. when to set what kind of parameters based on their properties, connections and so forth.

Otherwise I suggest we create a formal model that I can base the plugin on.

[nickbattle]

I started some work on this. See here.

The isValidCoSimulationConfig function defines the static semantic tests that I could think of at the time for a network of connected FMUs. But it was written many months ago and I can't remember all of the details.

Note that this model includes the FMI2 static model, and so calls the isValidFMIModelDescription for each configured FMU as one of the rules. The rest is to do with the connections between FMUs. There is also the concept of a "connection map" between inputs and outputs (internally) and outputs and inputs (externally). This is used to check for algebraic loops.

The next stage (from memory) was going to be an analysis of the network to try to identify the initialization order. But I stopped at this point (and went on to produce VDMCheck instead!).

[CThuleHansen]

I just checked it, and I think we should convert it into a verifier plugin for maestro2, when it is time for it. It does not seem to go through the stages of an FMU - i.e.: something like this:

for each instance
{    
    instantiate
    SetINI (which variables are included here?)
    SetupExperiment
    EnterInitializationMode
    Set Independant variables not part of external dependences (which ones?)
}
Set the variables according to a topological sorting based on: external and internal depedencies 

and perhaps we can use the vdm code to verify the sequence or we can create a model checker mdel

[nickbattle]

Yes, it's a static semantic check of a collection of connected FMUs. It would inform subsequent dynamic rules for the process and order of instantiation, but I didn't complete that aspect before moving to VDMCheck.

At the moment, the VDM logic is quite small. It would probably be best to convert it to Java to perform "the same checks". We could consider a code-generated translation, which would be more reliable, and allow us to maintain the formal model as "the rules", but have the performance at runtime.

[nickbattle]

Incidentally, the COSIM_to_VDM project is a simple bit of Java to take a Maestro JSON configuration file and spit out the equivalent VDM objects so that the COSIM model can verify it.

But note that I only had JSON examples to work from, so I was guessing the schema and layout; if this has changed, the tool will need to be updated. If you look in src/test/resources, there is an example of the sort of JSON file that it expects.

[CThuleHansen]

Yes, it's a static semantic check of a collection of connected FMUs. It would inform subsequent dynamic rules for the process and order of instantiation, but I didn't complete that aspect before moving to VDMCheck.

At the moment, the VDM logic is quite small. It would probably be best to convert it to Java to perform "the same checks". We could consider a code-generated translation, which would be more reliable, and allow us to maintain the formal model as "the rules", but have the performance at runtime.

Check. I got it. Let us discuss more, once we have created some initial documentation. You are envisioned to be introduced more thoroughly to the efforts in the review phase: https://github.com/INTO-CPS-Association/maestro/issues/42

Incidentally, the COSIM_to_VDM project is a simple bit of Java to take a Maestro JSON configuration file and spit out the equivalent VDM objects so that the COSIM model can verify it.

But note that I only had JSON examples to work from, so I was guessing the schema and layout; if this has changed, the tool will need to be updated. If you look in src/test/resources, there is an example of the sort of JSON file that it expects.

The json has not really changed, but the constraints on the JSON has changed. Let us discuss this again in the review phase

[CThuleHansen]

Adding @SimplisticCode as he has now created a plugin. We will be looking into verifying it.

[SimplisticCode]

Simon: I just started looking into the verification of the initialization. I just went through Nick's code https://github.com/INTO-CPS-Association/FMI-VDM-Model/blob/master/COSIM/CoSimulationConfig.vdmsl which are recognizing invalid co-simulation configuration. I was wondering how you guys envisioned a verification of the initialization – would you create some VDM-code as Casper suggested for making sure that all FMUs are correctly initialized?

Nick: As I see it, we can either use the VDM model as a separate definition of "the rules" which we then implement by hand, or we can try to use the VDM processor to actually test a configuration against the rules. (The VDM model itself can be tested with real configurations to check that it embodies the rules we want, or in principle we can do formal analysis of the model to convince ourselves that it is what we want. But that is separate from how we use the model in practice).

If we do the former, then the technology is simple, but we have to be careful that we have implemented the rules correctly(!) and keep the implementation up to date with the formal rules if/when they change.

If we do the latter, the implementation is guaranteed to match the formal specification of the rules, but we have to somehow "call" the VDM rules. That can either be by using code-generation to turn the VDM rules into Java which is then called, or we use the VDMJ/Overture interpreter directly.

Note: the VDM model is not complete; it only contains the start of an analysis, and will probably be enhanced to account for type conversion and compatibility between links at least. So we should expect change, assuming we do want to maintain a formal model in the future.

[SimplisticCode]

Okay. I think the second option sounds more appealing to me - what do you think Casper? But I think we need to add some specific VDM code to cope with the initialization phase - something like what @CThuleHansen suggested.

I just checked it, and I think we should convert it into a verifier plugin for maestro2, when it is time for it. It does not seem to go through the stages of an FMU - i.e.: something like this:

for each instance
{    
    instantiate
    SetINI (which variables are included here?)
    SetupExperiment
    EnterInitializationMode
    Set Independant variables not part of external dependences (which ones?)
}
Set the variables according to a topological sorting based on: external and internal depedencies 

[nickbattle]

One other possibility for invoking VDMJ is to use the VDMJUnit library. This is intended to be used with JUnit tests of a VDM specification, but it works perfectly well if you just want to evaluate expressions against a VDM model.

I'll attached the VDMJUnit documentation (it's part of the User Guide), but if you see the very last section, you'll see how you can call the methods without using JUnit. Basically it would mean calling readSpecification to load the spec and JSON-converted data, followed by init and then runBool to evaluate the verification function. You would still need to call something to convert the JSON to VDM first, of course.

(This might also help with #63 - I'll mention it there too). VDMJUnit.pdf

[SimplisticCode]

I went another way and used the prolog code by Claudio from this article Gomes et al_2019_Generation of Co-simulation Algorithms Subject to Simulator Contracts.pdf to verify the initialization order up against it. It doesn't verify everything of the plugin, but I think it covers the essential part (the topological ordering). And I think if we combine it with the #63, we will have covered a big part of the verification. This feature is added as an extra check to ensure the correctness of the initialization order - and this feature can be turned on and off using a configuration to the initialization plugin.