code: /******************************************************************************
   *
   *	Copyright (c) 2017-2022, INTO-CPS Association,
   *	c/o Professor Peter Gorm Larsen, Department of Engineering
   *	Finlandsgade 22, 8200 Aarhus N.
   *
   *	This file is part of the INTO-CPS toolchain.
   *
   *	xsd2vdm is free software: you can redistribute it and/or modify
   *	it under the terms of the GNU General Public License as published by
   *	the Free Software Foundation, either version 3 of the License, or
   *	(at your option) any later version.
   *
   *	xsd2vdm is distributed in the hope that it will be useful,
   *	but WITHOUT ANY WARRANTY; without even the implied warranty of
   *	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   *	GNU General Public License for more details.
   *
   *	You should have received a copy of the GNU General Public License
   *	along with xsd2vdm. If not, see <http://www.gnu.org/licenses/>.
   *	SPDX-License-Identifier: GPL-3.0-or-later
   *
   ******************************************************************************/
  
  package xsd2vdm;
  
  import java.io.File;
  import java.io.FileInputStream;
  import java.io.FileOutputStream;
  import java.io.IOException;
  import java.io.InputStream;
  import java.io.PrintStream;
  import java.util.Date;
  import java.util.HashSet;
  import java.util.List;
  import java.util.Map;
  import java.util.Properties;
  import java.util.Set;
  import java.util.Vector;
  
  import javax.xml.XMLConstants;
  import javax.xml.parsers.SAXParser;
  import javax.xml.parsers.SAXParserFactory;
  import javax.xml.transform.Source;
  import javax.xml.transform.stream.StreamSource;
  import javax.xml.validation.Schema;
  import javax.xml.validation.SchemaFactory;
  import javax.xml.validation.Validator;
  
  import org.xml.sax.SAXException;
  
  import types.Type;
  
  public class Xsd2VDM
  {
  	private static final String INDENT = "    ";
  	private static Properties mappingsProperties = null;
  	
  	private static void usage()
  	{
  		System.err.println("Usage: Xsd2VDM -xsd <XSD schema> [-vdm <output>] [-xml <XML file> [-name <varname>]] [-nowarn]");
  		System.err.println("Default mapping file is 'xsd2vdm.properties' located in same dir as XSD.");
  		System.err.println("Properties:");
  		System.err.println("    -Dmappings=<file>  Set an alternative mappings file");
  		System.err.println("    -Dmappings.debug   List possible mapping paths");
  		System.exit(1);
  	}
  	
  	/**
  	 * Static main method for command line XSD to VDM conversion.
  	 */
  	public static void main(String[] args)
  	{
  		int arg = 0;
  		File xsdFile = null;
  		File vdmFile = null;
  		File xmlFile = null;
  		String varName = null;
  		boolean noWarn = false;
  		
  		while (arg < args.length)
  		{
  			try
  			{
  				switch (args[arg])
  				{
  					case "-xsd":
  						xsdFile = new File(args[++arg]);
  						break;
  						
  					case "-vdm":
  						vdmFile = new File(args[++arg]);
  						break;
  						
  					case "-xml":
  						xmlFile = new File(args[++arg]);
  						break;
  						
  					case "-name":
  						varName = args[++arg];
  						break;
  						
  					case "-nowarn":
  						noWarn = true;
  						break;
  						
  					default:
  						usage();
  				}
  			}
  			catch (Exception e)
  			{
  				usage();
  			}
  			
  			arg++;
  		}
  		
  		if (xsdFile == null || (varName != null && xmlFile == null))
  		{
  			usage();
  		}
  		
  		Xsd2VDM xsd2vdm = new Xsd2VDM();
  		xsd2vdm.convert(xsdFile, vdmFile, xmlFile, varName, noWarn);
  	}
  	
  	/**
  	 * Method for internal conversions, for example via the VDMCheck tools.
  	 * If vdmFile is null, the VDM is written to standard output. If the
  	 * xmlFile is null, the schema is written, else the XML value mapping.
  	 * Note that the XML is always validated.
  	 */
  	public void convert(File xsdFile, File vdmFile, File xmlFile, String varName, boolean noWarn)
  	{
  		try
  		{
  			loadProperties(xsdFile);
  			Map<String, Type> schema = createVDMSchema(xsdFile, vdmFile, (xmlFile == null), noWarn);
  			
  			if (xmlFile != null)
  			{
  				validate(xmlFile, xsdFile);
  				createVDMValue(schema, vdmFile, xmlFile, varName);
  			}
  		}
  		catch (Exception e)
  		{
  			if (e.getMessage() != null)
  			{
  				System.err.println("Exception: " + e.getMessage());
  			}
  			else
  			{
  				e.printStackTrace();
  			}
  			
  			System.exit(1);
  		}
  	}
  
  	public static void loadProperties(File xsdFile) throws IOException
  	{
  		mappingsProperties = new Properties();
  		File properties = new File(xsdFile.getParent(),
  				System.getProperty("mappings", "xsd2vdm.properties"));
  		
  		if (properties.exists())
  		{
  			InputStream is = new FileInputStream(properties);
  			
  			if (is != null)
  			{
  				mappingsProperties.load(is);
  			}
  			
  			is.close();
  		}
  	}
  	
  	public static String getProperty(String name)
  	{
  		if (System.getProperty("mappings.debug") != null)
  		{
  			System.err.println(name);
  		}
  
  		if (mappingsProperties.containsKey(name))
  		{
  			return mappingsProperties.getProperty(name);
  		}
  		
  		return System.getProperty(name);
  	}
  
  	private void validate(File xml, File xsd)
  	{
  		try
  		{
  			// Note that we pass a stream to allow the validator to determine the
  			// encoding, rather than passing a File, which seems to use default encoding.
  			Source xmlFile = new StreamSource(new FileInputStream(xml));
  			xmlFile.setSystemId(xml.toURI().toASCIIString());
  			Source xsdFile = new StreamSource(new FileInputStream(xsd));
  			xsdFile.setSystemId(xsd.toURI().toASCIIString());
  			SchemaFactory schemaFactory = SchemaFactory.newInstance(XMLConstants.W3C_XML_SCHEMA_NS_URI);
  			
  			Schema schema = schemaFactory.newSchema(xsdFile);
  			Validator validator = schema.newValidator();
  			validator.validate(xmlFile);
  		}
  		catch (SAXException e)
  		{
  			System.err.println("XML validation: " + e);		// Raw exception gives file/line/col
  			System.exit(1);
  		}
  		catch (Exception e)
  		{
  			System.err.println("XML validation: " + e.getMessage());
  			System.exit(1);
  		}
  	}
  
  	/**
  	 * Convert the root schema file passed in and write out VDM-SL to the output. 
  	 * @param b 
  	 */
  	public Map<String, Type> createVDMSchema(File xsdFile, File vdmFile, boolean writeVDM, boolean noWarn) throws Exception
  	{
  		SAXParserFactory factory = SAXParserFactory.newInstance();
  		// factory.setNamespaceAware(true);
  		SAXParser saxParser = factory.newSAXParser();
  		
  		Set<File> processed = new HashSet<File>();
  		List<String> includes = new Vector<String>();
  		List<XSDElement> roots = new Vector<XSDElement>();
  
  		File parent = xsdFile.getParentFile();
  		includes.add(xsdFile.getName());
  		
  		while (!includes.isEmpty())
  		{
  			File file = new File(parent, includes.remove(0));
  			
  			if (!processed.contains(file))
  			{
  				XSDSaxHandler handler = new XSDSaxHandler();
  				saxParser.parse(file, handler);
  				
  				processed.add(file);
  				includes.addAll(handler.getIncludes());
  				roots.addAll(handler.getRoots());
  			}
  		}
  
  		// Select a version of the XSD schema to convert...
  		XSDConverter converter = new XSDConverter_v11(noWarn);
  		
  		Map<String, Type> vdmSchema = converter.convertSchemas(roots);
  
  		if (vdmSchema != null && writeVDM)
  		{
  			PrintStream output = (vdmFile != null) ?
  				new PrintStream(new FileOutputStream(vdmFile)) :
  				System.out;
  
  			output.println("/**");
  			output.println(" * VDM schema created from " + xsdFile + " on " + new Date());
  			output.println(" * DO NOT EDIT!");
  			output.println(" */");
  			
  //			if (!converter.getFunctions().isEmpty())
  //			{
  //				output.println("functions");
  //
  //				for (String function: converter.getFunctions())
  //				{
  //					xsdStandardFunction(output, function);
  //				}
  //			}
  			
  			xsdStandardTypes(output);
  			
  			for (String def: vdmSchema.keySet())
  			{
  				output.println(vdmSchema.get(def));
  			}
  			
  			if (vdmFile != null) output.close();
  		}
  		else if (vdmSchema == null)
  		{
  			System.err.println("Errors found.");
  			System.exit(1);
  		}
  		
  		return vdmSchema;
  	}
  	
  	public void createVDMValue(Map<String, Type> schema, File vdmFile, File xmlFile, String varName) throws Exception
  	{
  		SAXParserFactory factory = SAXParserFactory.newInstance();
  		SAXParser saxParser = factory.newSAXParser();
  		XMLSaxHandler handler = new XMLSaxHandler(schema);
  		saxParser.parse(xmlFile, handler);
  		
  		PrintStream output = (vdmFile != null) ?
  				new PrintStream(new FileOutputStream(vdmFile)) :
  				System.out;
  
  		String name = (varName == null) ? "modelDescription" : varName;
  		
  		output.println("/**");
  		output.println(" * VDM value created from " + xmlFile);
  		output.println(" */");
  		
  		// xsdStandardDefinitions(output);
  		
  		output.println("values");
  		output.println("    " + name + " =\n" + handler.getVDMValue().toVDM("    ") + ";\n");
  
  		if (vdmFile != null) output.close();
  	}
  
  	private void xsdStandardTypes(PrintStream output)
  	{
  		output.println("types\n");
  
  		output.println("AnyString = seq of char;\n");
  
  		output.println("NormalizedString = seq of char");
  		output.println("inv ns ==");
  		output.println(INDENT + "forall c in seq ns & c not in set {\'\\r\', \'\\n\', \'\\t\'};\n");
  		
  		output.println("Location ::");
  		output.println("    file : seq1 of char");
  		output.println("    line : nat1");
  		output.println(";\n");
  	}
  
  	@SuppressWarnings("unused")
  	private void xsdStandardDefinitions(PrintStream output)
  	{
  		output.println("values");
  		output.println(INDENT + "POSITIVE_INFINITY : real = 9218868437227405312;  -- 0x7ff0000000000000");
  		output.println(INDENT + "NEGATIVE_INFINITY : real = -4503599627370496;    -- 0xfff0000000000000");
  		output.println(INDENT + "NOT_A_NUMBER : real      = 9221120237041090560;  -- 0x7ff8000000000000");
  		output.println();
  	}
  
  	@SuppressWarnings("unused")
  	private void xsdStandardFunction(PrintStream output, String function)
  	{
  		switch (function)
  		{
  			case "xsdTotalDigits":
  				output.println(INDENT + "xsdTotalDigits: real +> bool");
  				output.println(INDENT + "xsdTotalDigits(value) == is not yet specified;");
  				break;
  
  			case "xsdFractionDigits":
  				output.println(INDENT + "xsdFractionDigits: real +> bool");
  				output.println(INDENT + "xsdFractionDigits(value) == is not yet specified;");
  				break;
  
  			case "xsdAssertion":
  				output.println(INDENT + "xsdAssertion: ? * seq of char +> bool");
  				output.println(INDENT + "xsdAssertion(value, test) == is not yet specified;");
  				break;
  
  			case "xsdPattern":
  				output.println(INDENT + "xsdPattern: ? * seq of char +> bool");
  				output.println(INDENT + "xsdPattern(value, pattern) == is not yet specified;");
  				break;
  
  			case "xsdExplicitTimezone":
  				output.println(INDENT + "xsdExplicitTimezone: seq1 of char * seq of char +> bool");
  				output.println(INDENT + "xsdExplicitTimezone(date, setting) == is not yet specified;");
  				break;
  
  			case "xsdWhitespace":
  				output.println(INDENT + "xsdWhitespace: seq of char * seq of char +> bool");
  				output.println(INDENT + "xsdWhitespace(string, setting) == is not yet specified;");
  				break;
  
  			default:
  				System.err.println("Error: unknown facet function: " + function);
  				break;
  		}
  		
  		output.println();
  	}
  }
  