Create eventB project. (260c9ded) · Commits · tables / jtet

src/main/java/ca/mcscert/jtet/eventbgenerator/EventBProject.java

0 → 100644

+95 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2014 Yanjun Jiang <jiangy76@mcmaster.ca>
		*
		* Redistribution and use in source and binary forms, with or without
		* modification, are permitted provided that the following conditions are
		* met:
		*
		* * Redistributions of source code must retain the above copyright
		* notice, this list of conditions and the following disclaimer.
		* * Redistributions in binary form must reproduce the above copyright
		* notice, this list of conditions and the following disclaimer in
		* the documentation and/or other materials provided with the distribution
		* * Neither the name of the McMaster Centre for Software Certification nor the names
		* of its contributors may be used to endorse or promote products derived
		* from this software without specific prior written permission.
		*
		* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
		* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
		* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
		* ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
		* LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
		* CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
		* SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
		* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
		* CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
		* ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
		* POSSIBILITY OF SUCH DAMAGE.
		*/
		package ca.mcscert.jtet.eventbgenerator;

		import ca.mcscert.jtet.tablularexpression.Table;
		import java.io.*;

		/**
		*
		* @author Yanjun Jiang <jiangy76@mcmaster.ca>
		*/
		final public class EventBProject {
		public EventBProject(String projectName) {
		m_projectName = projectName;
		}

		public void setTable(Table table) {
		m_table = table;
		}

		public void generate(String folderPath) throws IOException {
		//create Project Folder and Project File
		createEventProjectFolder(folderPath);
		writeProjectFile(m_projectName, folderPath);

		//generate Table EventB File
		m_eventBTableGenerator = new EventBTableGenerator(m_table);
		m_eventBTableGenerator.generateEventBXml(folderPath);
		}

		private String constructProjectFile(String projectName){
		return "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" +
		"<projectDescription>\n" +
		" <name>" + projectName + "</name>\n" +
		" <comment></comment>\n" +
		" <projects>\n" +
		" </projects>\n" +
		" <buildSpec>\n" +
		" <buildCommand>\n" +
		" <name>org.rodinp.core.rodinbuilder</name>\n" +
		" <arguments>\n" +
		" </arguments>\n" +
		" </buildCommand>\n" +
		" </buildSpec>\n" +
		" <natures>\n" +
		" <nature>org.rodinp.core.rodinnature</nature>\n" +
		" </natures>\n" +
		"</projectDescription>\n";
		}

		private void writeProjectFile(String projectName, String folderPath) throws IOException {
		String fileContent = constructProjectFile(projectName);
		String fileName = folderPath + ".project";

		EventBFileWriter.writeEventBBumFile(fileName ,fileContent);
		}

		private static void createEventProjectFolder(String folderPath) throws IOException {
		if(!(new File(folderPath).isDirectory())) {
		if (!(new File(folderPath).mkdirs())){
		throw new IOException("Failed to create project folder");
		}
		}
		}

		Table m_table;
		String m_projectName;
		EventBTableGenerator m_eventBTableGenerator;
		}

src/main/java/ca/mcscert/jtet/eventbgenerator/EventBTableGenerator.java

+11 −8

Original line number	Diff line number	Diff line
		@@ -31,6 +31,8 @@ package ca.mcscert.jtet.eventbgenerator;
		import ca.mcscert.jtet.expression.EventBGenerator;
		import ca.mcscert.jtet.tablularexpression.*;

		import java.io.IOException;

		/**
		*
		* @author Yanjun Jiang <jiangy76@mcmaster.ca>
		@@ -41,30 +43,31 @@ final public class EventBTableGenerator {
		m_table = table;
		}

		public String generateEventBXml(){
		public void generateEventBXml(String folderPath) throws IOException {
		final String versionEncodingXml = "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n";
		final String machineFileCfgPreXml = "<org.eventb.core.machineFile org.eventb.core.configuration=\"org.eventb.core.fwd;de.prob.units.mchBase\" version=\"5\">\n";
		final String machineFileCfgPostXml = "</org.eventb.core.machineFile>";

		String output= "";

		//Step 1: Generate the Pre Xml
		m_output += versionEncodingXml;
		m_output += machineFileCfgPreXml;
		output += versionEncodingXml;
		output += machineFileCfgPreXml;

		//Step 2: Generate the Variables & Invariants Xml
		m_output += m_eventBGenerator.GenerateVariablesDeclaration(m_table.getInputVariables());
		output += m_eventBGenerator.GenerateVariablesDeclaration(m_table.getInputVariables());

		//Step 3: Generate the Events Xml
		m_hierarchcialGridCheckerGenerator = new HierarchicalGridEventBGenerator(m_table);
		m_output += HierarchcialGridEventBCheckerWalkerGenerator.GenerateCheckerFromGrid(m_table.getLeftGrid(), m_hierarchcialGridCheckerGenerator);
		output += HierarchcialGridEventBCheckerWalkerGenerator.GenerateCheckerFromGrid(m_table.getLeftGrid(), m_hierarchcialGridCheckerGenerator);

		//Step 3: Generate the Post Xml
		m_output += machineFileCfgPostXml;
		output += machineFileCfgPostXml;

		return m_output;
		EventBFileWriter.writeEventBBumFile(folderPath + m_table.getTableName() + ".bum", output);
		}

		Table m_table;
		String m_output = "";
		EventBGenerator m_eventBGenerator = new EventBGenerator();
		HierarchcialGridCheckerGenerator m_hierarchcialGridCheckerGenerator;
		}
		No newline at end of file

src/test/java/ca/mcscert/jtet/eventbgenerator/ParameterizedEventBTableGeneratorTest.java

+17 −8

Original line number	Diff line number	Diff line
		@@ -195,21 +195,30 @@ public class ParameterizedEventBTableGeneratorTest {
		}

		public void doTest() throws IOException {
		m_folderPath = folder.getRoot().toString() + m_table.getTableName() + "/";
		m_folderPath = folder.getRoot().toString() + "/";
		m_generatedFileName = m_folderPath + m_table.getTableName() + ".bum";
		m_expectedFileName = "/expected/NR/" + m_table.getTableName() + "/" + m_table.getTableName() + ".bum";
		String generated = execute();
		assertResult(generated);
		execute();
		assertResult();
		}

		private String execute() throws IOException {
		EventBTableGenerator eventBProject = new EventBTableGenerator(m_table);
		return eventBProject.generateEventBXml();
		private void execute() throws IOException {
		EventBProject eventBProject = new EventBProject(m_table.getTableName());
		eventBProject.setTable(m_table);
		eventBProject.generate(m_folderPath);
		}

		public void assertResult(String generated) throws IOException {
		String expected;
		public void assertResult() throws IOException {
		String generated, expected;
		InputStream inStream = null;
		try {
		inStream = new FileInputStream(m_generatedFileName);
		generated = readOutput(inStream);
		} finally {
		if (inStream != null) {
		inStream.close();
		}
		}

		try {
		inStream = ParameterizedEventBTableGeneratorTest.class.getResourceAsStream(m_expectedFileName);