diff --git a/fmi2/rule-model/Validation.vdmsl b/fmi2/rule-model/Validation.vdmsl index 61b8b8c..03a7651 100644 --- 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 index 42d93df..3456d23 100644 --- a/fmi2/vdmcheck/src/main/java/maestro/MaestroCheckFMI2.java +++ b/fmi2/vdmcheck/src/main/java/maestro/MaestroCheckFMI2.java @@ -141,8 +141,10 @@ public List check(File modelFile, File buildFile, File termsFile) t Xsd2VDM.loadProperties(xsdFile); Map 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 index 6c92f93..f36e0dd 100644 --- 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 index 8c23d07..c66b17b 100644 --- a/fmi3/vdmcheck/src/main/java/maestro/MaestroCheckFMI3.java +++ b/fmi3/vdmcheck/src/main/java/maestro/MaestroCheckFMI3.java @@ -139,9 +139,11 @@ public List check(File modelFile, File buildFile, File termsFile) t Xsd2VDM converter = new Xsd2VDM(); Xsd2VDM.loadProperties(xsdFile); Map 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 index 384b3fc..949f33e 100644 --- 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 schema = writeSchema(output); String varName = ""; + missingVariable("validationError : [seq of char]", output); + if (xmlContent.contains("