Create a validationError VDM variable

INTO-CPS-Association · Apr 10, 2024 · 111269e · 111269e
1 parent f965d32
commit 111269e
Show file tree

Hide file tree

Showing 5 changed files with 72 additions and 7 deletions.
diff --git a/fmi2/rule-model/Validation.vdmsl b/fmi2/rule-model/Validation.vdmsl
@@ -33,7 +33,10 @@ functions
 	 */
 	isValidFMIConfiguration: FmiModelDescription | FmiBuildDescription | FmiTerminalsAndIcons +> bool
 	isValidFMIConfiguration(conf) ==
-		if is_(conf, FmiModelDescription)
+		if validationError <> nil
+		then /* @Printf("%s\n", validationError) */ false
+
+		elseif is_(conf, FmiModelDescription)
 		then inv_FmiModelDescription'(conf)
 
 		elseif is_(conf, FmiBuildDescription)
@@ -51,6 +54,8 @@ functions
 	isValidFMIConfigurations: [FmiModelDescription] * [FmiBuildDescription] * [FmiTerminalsAndIcons] +> bool
 	isValidFMIConfigurations(model, build, terminals) == allOf
 	([
+		validationError <> nil => /* @Printf("%s\n", validationError) */ false,
+
 		model <> nil => inv_FmiModelDescription'(model),
 		build <> nil => inv_FmiBuildDescription'(build),
 		terminals <> nil => inv_FmiTerminalsAndIcons'(mk_(terminals, model))

diff --git a/fmi2/vdmcheck/src/main/java/maestro/MaestroCheckFMI2.java b/fmi2/vdmcheck/src/main/java/maestro/MaestroCheckFMI2.java
@@ -141,8 +141,10 @@ public List<OnFailError> check(File modelFile, File buildFile, File termsFile) t
             Xsd2VDM.loadProperties(xsdFile);
             Map<String, Type> vdmSchema = converter.createVDMSchema(xsdFile, null, false, true);
 
+            missingVariable("validationError : [seq of char]", vdmFile);
+
             if (modelFile != null) {
-                converter.createVDMValue(vdmSchema, vdmFile, modelFile, "modelDescription");
+                converter.createVDMValue(vdmSchema, vdmFile, modelFile, "modelDescription", true);
             } else {
                 missingVariable("modelDescription", vdmFile);
             }

diff --git a/fmi3/rule-model/Validation.vdmsl b/fmi3/rule-model/Validation.vdmsl
@@ -33,7 +33,10 @@ functions
 	 */
 	isValidFMIConfiguration: FmiModelDescription | FmiBuildDescription | FmiTerminalsAndIcons +> bool
 	isValidFMIConfiguration(conf) ==
-		if is_(conf, FmiModelDescription)
+		if validationError <> nil
+		then /* @Printf("%s\n", validationError) */ false
+
+		elseif is_(conf, FmiModelDescription)
 		then inv_FmiModelDescription'(conf)
 
 		elseif is_(conf, FmiBuildDescription)
@@ -51,6 +54,8 @@ functions
 	isValidFMIConfigurations: [FmiModelDescription] * [FmiBuildDescription] * [FmiTerminalsAndIcons] +> bool
 	isValidFMIConfigurations(model, build, terminals) == allOf
 	([
+		validationError <> nil => /* @Printf("%s\n", validationError) */ false,
+
 		model <> nil => inv_FmiModelDescription'(model),
 		build <> nil => inv_FmiBuildDescription'(build),
 		terminals <> nil => inv_FmiTerminalsAndIcons'(mk_(terminals, model))

diff --git a/fmi3/vdmcheck/src/main/java/maestro/MaestroCheckFMI3.java b/fmi3/vdmcheck/src/main/java/maestro/MaestroCheckFMI3.java
@@ -139,9 +139,11 @@ public List<OnFailError> check(File modelFile, File buildFile, File termsFile) t
             Xsd2VDM converter = new Xsd2VDM();
             Xsd2VDM.loadProperties(xsdFile);
             Map<String, Type> vdmSchema = converter.createVDMSchema(xsdFile, null, false, true);
+
+            missingVariable("validationError : [seq of char]", vdmFile);
 
             if (modelFile != null) {
-                converter.createVDMValue(vdmSchema, vdmFile, modelFile, "modelDescription");
+                converter.createVDMValue(vdmSchema, vdmFile, modelFile, "modelDescription", true);
             } else {
                 missingVariable("modelDescription", vdmFile);
             }

diff --git a/fmuReader/src/main/java/fmureader/FMUReader.java b/fmuReader/src/main/java/fmureader/FMUReader.java
@@ -67,6 +67,8 @@ public class FMUReader implements ExternalFormatReader
 	private static final String TERMINALS_AND_ICONS = "icons/terminalsAndIcons.xml";
 	private static final String TERMINALS_AND_ICONS_204 = "terminalsAndIcons/terminalsAndIcons.xml";
 
+	private String exception = null;
+
 	@Override
 	public char[] getText(File file, Charset charset) throws IOException
 	{
@@ -84,10 +86,11 @@ else if (file.getName().toLowerCase().endsWith(".fmu"))
 		}
 	}
 
-	private void validate(File filename, Reader xml) throws IOException
+	private void validate(File filename, Reader xml)
 	{
 		try
 		{
+			exception = null;
 			File xsd = new File(System.getProperty("fmureader.xsd", "schema/fmi3.xsd"));
 
 			// Note that we pass a stream to allow the validator to determine the
@@ -104,17 +107,23 @@ private void validate(File filename, Reader xml) throws IOException
 		}
 		catch (SAXException e)
 		{
-			throw new IOException("XML validation: " + e);		// Raw exception gives file/line/col
+			exception = "XML validation: " + e;		// Raw exception gives file/line/col
 		}
 		catch (Exception e)
 		{
-			throw new IOException("XML validation: " + e.getMessage());
+			exception = "XML validation: " + e.getMessage();
 		}
 	}
 
 	private char[] processXML(File xmlFile) throws IOException
 	{
 		validate(xmlFile, new InputStreamReader(new FileInputStream(xmlFile), "utf8"));
+
+		if (exception != null)
+		{
+			return validationException();
+		}
+
 		String xmlContent = readFile(xmlFile);
 
 		try
@@ -125,6 +134,8 @@ private char[] processXML(File xmlFile) throws IOException
 			Map<String, Type> schema = writeSchema(output);
 			String varName = "";
 
+			missingVariable("validationError : [seq of char]", output);
+
 			if (xmlContent.contains("<fmiModelDescription"))
 			{
 				varName = "modelDescription";
@@ -180,13 +191,27 @@ private char[] processFMU(File fmuFile) throws IOException
 			Xsd2VDM converter = new Xsd2VDM();
 
 			validate(new File(MODEL_DESCRIPTION), new StringReader(modelDescription));
+
+			if (exception != null)
+			{
+				return validationException();
+			}
+
+			missingVariable("validationError : [seq of char]", output);
+
 			InputSource input = new InputSource(new StringReader(modelDescription));
 			input.setSystemId(new File(MODEL_DESCRIPTION).toURI().toASCIIString());
 			converter.createVDMValue(schema, output, input, fmuFile.getAbsolutePath(), "modelDescription");
 
 			if (buildDescription != null)
 			{
 				validate(new File(BUILD_DESCRIPTION), new StringReader(buildDescription));
+
+				if (exception != null)
+				{
+					return validationException();
+				}
+
 				input = new InputSource(new StringReader(buildDescription));
 				input.setSystemId(new File(BUILD_DESCRIPTION).toURI().toASCIIString());
 				converter.createVDMValue(schema, output, input, fmuFile.getAbsolutePath(), "buildDescription");
@@ -199,6 +224,12 @@ private char[] processFMU(File fmuFile) throws IOException
 			if (terminalsAndIcons != null)
 			{
 				validate(new File(TERMINALS_AND_ICONS), new StringReader(terminalsAndIcons));
+
+				if (exception != null)
+				{
+					return validationException();
+				}
+
 				input = new InputSource(new StringReader(terminalsAndIcons));
 				input.setSystemId(new File(TERMINALS_AND_ICONS).toURI().toASCIIString());
 				converter.createVDMValue(schema, output, input, fmuFile.getAbsolutePath(), "terminalsAndIcons");		
@@ -218,6 +249,26 @@ private char[] processFMU(File fmuFile) throws IOException
 		}
 	}
 
+	private char[] validationException() throws IOException
+	{
+		ByteArrayOutputStream result = new ByteArrayOutputStream();
+		PrintStream output = new PrintStream(result);
+
+		output.println("/**");
+		output.println(" * XML validation error");
+		output.println(" */");
+		output.println("values");
+		output.printf("    validationError : [seq of char] = \"%s\";\n\n", exception);
+
+		missingVariable("modelDescription", output);
+		missingVariable("buildDescription", output);
+		missingVariable("terminalsAndIcons", output);
+
+		writeVDM(result);
+
+		return result.toString("utf8").toCharArray();
+	}
+
 	private void missingVariable(String varName, PrintStream output)
 	{
 		output.println("/**");