integrate with vdm

[markaren]

@nickbattle @CThuleHansen

This PR allows specifying the path to the fmi2vdm.jar. When supplied, sspgen will perform a check on the included FMUs (FMI 2.0) for informative purposes.

e.g:

ssp("QuarterTruck") {

  resources {
    file("$fmuPath/chassis.fmu")
    file("$fmuPath/wheel.fmu")
    file("$fmuPath/ground.fmu")
  }

}.validate(pathToVdm)

prints

VDMCheck found..
Checking modelDescription of chassis.fmu using VDMCheck..
2.2.8 InitialUnknowns must include: {36, 38}
Errors found.
Checking modelDescription of wheel.fmu using VDMCheck..
2.2.8 InitialUnknowns must include: {39, 42, 43}
Errors found.
Checking modelDescription of ground.fmu using VDMCheck..
2.2.8 InitialUnknowns must include: {15, 16}
Errors found.
VDMCheck finished..

Closes #15

[nickbattle]

Very interesting, thanks for letting us know.

[nickbattle]

A thought: presumably, the error messages from the check are still being sent to stdout?

Messages are raised by "annotations" in the formal model, called @OnFail. When the sub-clause after such an annotation fails, a message is raised. (This allows us to keep the error message handling separate from the formal specification).

When VDMCheck was integrated with the Maestro tool, they implemented an alternative @OnFail which routes the error messages in a more convenient way for error reporting. If that is useful for the sspgen integration, let me know and I'll expand on what is needed.

[markaren]

A thought: presumably, the error messages from the check are still being sent to stdout?

Yes.

So this is basically the entire implementation:

private fun vdmCheck(vdmJar: File?) {
        if (vdmJar != null && vdmJar.exists() && vdmJar.extension == "jar") {

            println("VDMCheck found..")
            val cl = URLClassLoader(arrayOf(vdmJar.toURI().toURL()))
            val vdm = cl.loadClass("VDMCheck")

            val vdmMethod = vdm.getDeclaredMethod(
                "run",
                String::class.java, String::class.java, String::class.java, String::class.java
            )
            resources.filter { it.name.endsWith(".fmu") }.forEach { resource ->
                val name = resource.name
                println("Checking modelDescription of $name using VDMCheck..")
                val xml = FmiModelDescriptionUtil.extractModelDescriptionXml(resource.openStream())
                val version = FmiModelDescriptionUtil.extractVersion(xml)
                if (version.startsWith("2.")) {
                    val xml1 = if (xml.startsWith("<?xml version")) {
                        xml.split("\n").drop(1).joinToString("\n")
                    } else {
                        xml
                    }
                    vdmMethod.isAccessible = true
                    vdmMethod.invoke(null, null, xml1, null, "schema/fmi2ModelDescription.xsd")
                } else {
                    System.err.println("Unable to check FMU adhering to version $version of the FMI standard..")
                }
            }
            println("VDMCheck finished..")
        }

    }

a resource in this context is any file bundled with the SSP archive, but filtered for .fmu for the purpose of the VDMCheck.

The cavecat here is that I'm relying on private API calls (main calls System.exit, so I have to use run)

If that is useful for the sspgen integration, let me know and I'll expand on what is needed.

I think this does the job ok, unless there are error reports I'm not catching?

[nickbattle]

I think this does the job ok, unless there are error reports I'm not catching?

All the reports come out on stdout, so you're not missing anything, though it looks like you're not quite using the latest VDMCheck version? The latest 1.0.2 build 201203 includes a (unique) error number before the FMI section number in each message. Maestro uses this to filter out some warnings or errors that are not considered "fatal".

https://github.com/INTO-CPS-Association/FMI-VDM-Model/releases/download/1.0.2-snapshot/FMI2-vdmcheck-1.0.2-SNAPSHOT-201203-distribution.zip

[markaren]

Thanks, tested with 1.0.2.

VDMCheck found..
Checking modelDescription of chassis.fmu using VDMCheck..
1029: 2.2.8 InitialUnknowns must include: {36, 38}
Errors found.
Checking modelDescription of wheel.fmu using VDMCheck..
1029: 2.2.8 InitialUnknowns must include: {39, 42, 43}
Errors found.
Checking modelDescription of ground.fmu using VDMCheck..
1029: 2.2.8 InitialUnknowns must include: {15, 16}
Errors found.
VDMCheck finished..

This implementation supports at least both 1.0.0 and 1.0.2