Add MaestroCheckFMI2 and rename fmiN-rule-model/static-model

INTO-CPS-Association · Jan 25, 2024 · 29f8fee · 29f8fee
1 parent d9c7be8
commit 29f8fee
Show file tree

Hide file tree

Showing 16 changed files with 470 additions and 47 deletions.
diff --git a/fmi2/rule-model/Tests/Tests.vdmsl b/fmi2/rule-model/Tests/Tests.vdmsl
@@ -35,9 +35,9 @@ functions
 	tests() ==
 	[
 		-- @Printf("------------ controlledTemperature\n")
-		isValidFMIConfiguration(controlledTemperature, nil, nil),
+		isValidFMIConfigurations(controlledTemperature, nil, nil),
 		-- @Printf("------------ integrateSignal\n")
-		isValidFMIConfiguration(integrateSignal, nil, nil),
+		isValidFMIConfigurations(integrateSignal, nil, nil),
 		-- @Printf("------------ springMassDamper\n")
-		isValidFMIConfiguration(springMassDamper, nil, nil)
+		isValidFMIConfigurations(springMassDamper, nil, nil)
 	];
diff --git a/fmi2/rule-model/Validation.vdmsl b/fmi2/rule-model/Validation.vdmsl
@@ -27,6 +27,23 @@
  *
  *********************************************************************************/
 functions
+	/**
+	 * This function is called via VDMCheck.sh and MaestroCheckFMI2, being passed a single
+	 * XML type.
+	 */
+	isValidFMIConfiguration: FmiModelDescription | FmiBuildDescription | FmiTerminalsAndIcons +> bool
+	isValidFMIConfiguration(conf) ==
+		if is_(conf, FmiModelDescription)
+		then inv_FmiModelDescription'(conf)
+
+		elseif is_(conf, FmiBuildDescription)
+		then inv_FmiBuildDescription'(conf)
+
+		else if is_(conf, FmiTerminalsAndIcons)
+		then inv_FmiTerminalsAndIcons'(mk_(conf, nil))
+
+		else undefined;		-- Undefined top level type
+
 	/**
 	 * Top level function to validate the top level records. This just
 	 * calls the invariant function for the corresponding "prime" checked type.

diff --git a/fmi2/rule-model/pom.xml b/fmi2/rule-model/pom.xml
@@ -32,7 +32,7 @@
 							<goal>copy-resources</goal>
 						</goals>
 						<configuration>
-							<outputDirectory>.generated/fmi2model</outputDirectory>
+							<outputDirectory>.generated/fmi2-rule-model</outputDirectory>
 							<resources>
 								<resource>
 									<directory>.</directory>
@@ -75,8 +75,8 @@
 							<outputDirectory>.generated</outputDirectory>
 							<classesDirectory>.generated</classesDirectory>
 							<includes>
-								<include>fmi2model/*.vdmsl</include>
-								<include>fmi2model/Rules/*.adoc</include>
+								<include>fmi2-rule-model/*.vdmsl</include>
+								<include>fmi2-rule-model/Rules/*.adoc</include>
 								<include>MIT-LICENCE</include>
 							</includes>
 						</configuration>

diff --git a/fmi2/static-model/pom.xml b/fmi2/static-model/pom.xml
@@ -37,7 +37,7 @@
 								<goal>copy-resources</goal>
 							</goals>
 							<configuration>
-								<outputDirectory>.generated/fmi2model</outputDirectory>
+								<outputDirectory>.generated/fmi2-static-model</outputDirectory>
 								<resources>
 									<resource>
 										<directory>.</directory>
@@ -79,7 +79,7 @@
 							<outputDirectory>.generated</outputDirectory>
 							<classesDirectory>.generated</classesDirectory>
 							<includes>
-								<include>fmi2model/*.vdmsl</include>
+								<include>fmi2-static-model/*.vdmsl</include>
 								<include>MIT-LICENCE</include>
 							</includes>
 						</configuration>

diff --git a/fmi2/vdmcheck/src/main/java/VDMCheck.java b/fmi2/vdmcheck/src/main/java/VDMCheck.java
@@ -265,7 +265,7 @@ private static boolean run(String filename, XMLFile tempXML, String vdmOUT)
 			runCommand(jarLocation, tempOUT,
 					"java", "-Xmx1g", "-cp", String.join(File.pathSeparator, dependencies), 
 					"com.fujitsu.vdmj.VDMJ", "-vdmsl", "-q", "-annotations",
-					"-e", "isValidFMIConfiguration(" + varName + ")", "fmi2model", tempVDM.getCanonicalPath());
+					"-e", "isValidFMIConfiguration(" + varName + ")", "fmi2-static-model", tempVDM.getCanonicalPath());
 
 			sed(tempOUT, System.out,
 					"^true$", "No errors found.",

diff --git a/fmi2/vdmcheck/src/main/java/VDMCheckPlus.java b/fmi2/vdmcheck/src/main/java/VDMCheckPlus.java
@@ -94,8 +94,21 @@ private static boolean run(File filename, String vdmOUT, String prefix)
 			tempOUT.deleteOnExit();
 
 			String[] dependencies = {"vdmj.jar", "annotations.jar", "xsd2vdm.jar", "fmuReader.jar"};
-			File rules = new File(jarLocation.getAbsolutePath(), "fmi2model/Rules");
+			File rule_model = new File(jarLocation.getAbsolutePath(), "fmi2-rule-model");
+			File rules = new File(jarLocation.getAbsolutePath(), "fmi2-rule-model/Rules");
+			File static_model = new File(jarLocation.getAbsolutePath(), "fmi2-static-model");
+
 			List<String> args = new Vector<String>();
+			File model = null;
+
+			if (rule_model.exists())
+			{
+				model = rule_model;
+			}
+			else
+			{
+				model = static_model;
+			}
 
 			args.add("java");
 			args.add("-Xmx1g");
@@ -111,7 +124,7 @@ private static boolean run(File filename, String vdmOUT, String prefix)
 			args.add("-annotations");
 			args.add("-e");
 			args.add("isValidFMIConfigurations(modelDescription, buildDescription, terminalsAndIcons)");
-			args.add("fmi2model");
+			args.add(model.getName());
 			args.add(filename.getAbsolutePath());
 
 			if (rules.exists())
@@ -127,7 +140,7 @@ public boolean accept(File dir, String name)
 
 				for (String adoc: rules.list(filter))
 				{
-					args.add("fmi2model" + File.separator + "Rules" + File.separator + adoc);
+					args.add("fmi2-rule-model" + File.separator + "Rules" + File.separator + adoc);
 				}
 			}
 

diff --git a/fmi2/vdmcheck/src/main/java/maestro/MaestroCheck.java b/fmi2/vdmcheck/src/main/java/maestro/MaestroCheck.java
@@ -145,26 +145,26 @@ public List<OnFailError> check(File xmlFile) throws Exception {
             if (vdmFile.exists())    // Means successful?
             {
                 copyResources(vdmsl,
-            		"/fmi2model/CoSimulation_4.3.1.vdmsl",
-            		"/fmi2model/DefaultExperiment_2.2.5.vdmsl",
-            		"/fmi2model/FMI2Schema.vdmsl",
-                    "/fmi2model/FMIModelDescription_2.2.1.vdmsl",
-                    "/fmi2model/LogCategories_2.2.4.vdmsl",
-                    "/fmi2model/Misc.vdmsl",
-                    "/fmi2model/ModelExchange_3.3.1.vdmsl",
-                    "/fmi2model/ModelStructure_2.2.8.vdmsl",
-                    "/fmi2model/ModelVariables_2.2.7.vdmsl",
-                    "/fmi2model/TypeDefinitions_2.2.3.vdmsl",
-                    "/fmi2model/UnitDefinitions_2.2.2.vdmsl",
-                    "/fmi2model/VariableNaming_2.2.9.vdmsl",
-                    "/fmi2model/VendorAnnotations_2.2.6.vdmsl",
-
-                    "/fmi2model/BuildConfiguration_2.3.vdmsl",
-                    "/fmi2model/GraphicalRepresentation_2.3.vdmsl",
-                    "/fmi2model/Terminals_2.3.vdmsl",
-                    "/fmi2model/VendorAnnotations_2.3.vdmsl",
-                    "/fmi2model/Validation.vdmsl",
-                    "/fmi2model/XSD.vdmsl");
+            		"/fmi2-static-model/CoSimulation_4.3.1.vdmsl",
+            		"/fmi2-static-model/DefaultExperiment_2.2.5.vdmsl",
+            		"/fmi2-static-model/FMI2Schema.vdmsl",
+                    "/fmi2-static-model/FMIModelDescription_2.2.1.vdmsl",
+                    "/fmi2-static-model/LogCategories_2.2.4.vdmsl",
+                    "/fmi2-static-model/Misc.vdmsl",
+                    "/fmi2-static-model/ModelExchange_3.3.1.vdmsl",
+                    "/fmi2-static-model/ModelStructure_2.2.8.vdmsl",
+                    "/fmi2-static-model/ModelVariables_2.2.7.vdmsl",
+                    "/fmi2-static-model/TypeDefinitions_2.2.3.vdmsl",
+                    "/fmi2-static-model/UnitDefinitions_2.2.2.vdmsl",
+                    "/fmi2-static-model/VariableNaming_2.2.9.vdmsl",
+                    "/fmi2-static-model/VendorAnnotations_2.2.6.vdmsl",
+
+                    "/fmi2-static-model/BuildConfiguration_2.3.vdmsl",
+                    "/fmi2-static-model/GraphicalRepresentation_2.3.vdmsl",
+                    "/fmi2-static-model/Terminals_2.3.vdmsl",
+                    "/fmi2-static-model/VendorAnnotations_2.3.vdmsl",
+                    "/fmi2-static-model/Validation.vdmsl",
+                    "/fmi2-static-model/XSD.vdmsl");
 
                 Properties.init();
                 Settings.annotations = true;