Support obtaining output information from the cell. (0be5eefd) · Commits · tables / jtet

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

0 → 100644

+52 −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 java.io.BufferedWriter;
		import java.io.FileOutputStream;
		import java.io.IOException;
		import java.io.OutputStreamWriter;

		/**
		*
		* @author Yanjun Jiang <jiangy76@mcmaster.ca>
		*/
		final public class EventBFileWriter {

		public static void writeEventBFile(String fileName, String fileContent) {
		try {
		BufferedWriter br = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(fileName + ".bum"), "UTF8"));
		br.write(fileContent);
		br.flush();
		br.close();
		} catch (IOException e) {
		e.printStackTrace();
		}
		}
		}

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

+16 −7

Original line number	Diff line number	Diff line
		@@ -30,8 +30,9 @@ package ca.mcscert.jtet.eventbgenerator;

		import ca.mcscert.jtet.expression.EventBGenerator;
		import ca.mcscert.jtet.expression.VariableCollection;
		import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerWalkerGenerator;
		import ca.mcscert.jtet.tablularexpression.HierarchicalGrid;
		import ca.mcscert.jtet.tablularexpression.*;

		import java.util.List;

		/**
		*
		@@ -39,9 +40,12 @@ import ca.mcscert.jtet.tablularexpression.HierarchicalGrid;
		*/
		final public class EventBTableGenerator {

		public EventBTableGenerator(VariableCollection variableDefinitions, HierarchicalGrid grid) {
		public EventBTableGenerator(VariableCollection variableDefinitions, String tableName, HierarchicalGrid leftGrid, List<String> outputVariables, TwoDimensionalGrid outputGrid) {
		m_variableDefinitions = variableDefinitions;
		m_grid = grid;
		m_tableName = tableName;
		m_leftGrid = leftGrid;
		m_outputVariables = outputVariables;
		m_outputGrid = outputGrid;
		}

		public String generateEventBXml(){
		@@ -57,7 +61,8 @@ final public class EventBTableGenerator {
		m_output += m_eventBGenerator.GenerateVariablesDeclaration(m_variableDefinitions);

		//Step 3: Generate the Events Xml
		m_output += HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(m_grid, (new HierarchicalGridEventBGenerator(m_variableDefinitions)));
		m_hierarchcialGridCheckerGenerator = new HierarchicalGridEventBGenerator(m_variableDefinitions, m_tableName, m_outputVariables, m_outputGrid);
		m_output += HierarchcialGridEventBCheckerWalkerGenerator.GenerateCheckerFromGrid(m_leftGrid, m_hierarchcialGridCheckerGenerator);

		//Step 3: Generate the Post Xml
		m_output += machineFileCfgPostXml;
		@@ -66,7 +71,11 @@ final public class EventBTableGenerator {
		}

		String m_output = "";
		HierarchicalGrid m_grid;
		String m_tableName = "";
		HierarchicalGrid m_leftGrid;
		List<String> m_outputVariables;
		TwoDimensionalGrid m_outputGrid;
		VariableCollection m_variableDefinitions;
		EventBGenerator m_eventBGenerator = new EventBGenerator();
		HierarchcialGridCheckerGenerator m_hierarchcialGridCheckerGenerator;
		}
		No newline at end of file

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

+22 −17

Original line number	Diff line number	Diff line
		@@ -34,9 +34,11 @@ import ca.mcscert.jtet.expression.VariableCollection;
		import ca.mcscert.jtet.parsers.MatlabParser;
		import ca.mcscert.jtet.tablularexpression.Cell;
		import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerGenerator;
		import ca.mcscert.jtet.tablularexpression.TwoDimensionalGrid;

		import java.util.ArrayDeque;
		import java.util.Deque;
		import java.util.List;

		/**
		* This class generate common non-initialisation events
		@@ -44,8 +46,11 @@ import java.util.Deque;
		*/
		final public class HierarchicalGridEventBGenerator implements HierarchcialGridCheckerGenerator {

		public HierarchicalGridEventBGenerator(VariableCollection variableDefinitions) {
		public HierarchicalGridEventBGenerator(VariableCollection variableDefinitions, String tableName, List<String> outputVariables, TwoDimensionalGrid outputGrid) {
		m_variableDefinitions = variableDefinitions;
		m_tableName = tableName;
		m_outputGrid = outputGrid;
		m_outputVariables = outputVariables;
		}

		private String getCurrentEventName(){
		@@ -60,37 +65,36 @@ final public class HierarchicalGridEventBGenerator implements HierarchcialGridCh
		return "<org.eventb.core.guard name=\"Guard" + guardNo + "\" org.eventb.core.label=\"grd" + + guardNo + "\" org.eventb.core.predicate=\"" + guard +"\"/>\n";
		}

		private String generateEventActionXmlPre() {
		int actionNo = 1;
		return "<org.eventb.core.action name=\"Action" + actionNo + "\" org.eventb.core.assignment=\"output ≔ " + m_currentEventNo +"\"";
		private String generateEventActionXml(int actionNo) {
		String value = m_outputGrid.get(0, m_currentEventNo - 1).contents();
		return "<org.eventb.core.action name=\"Action" + actionNo + "\" org.eventb.core.assignment=\"" + m_outputVariables.get(0) + " ≔ " + value + "\" org.eventb.core.label=\"act" + actionNo + "\"/>\n";
		}

		private String generateEventActionXmlPost(int actionNo) {
		return " org.eventb.core.label=\"act" + actionNo + "\"/>\n";
		}
		private String generateEventActionsXml() {
		int actionNo = 1;
		String ret = "";

		private String generateEventActionsXml(int actionNo) {
		return generateEventActionXmlPre() + generateEventActionXmlPost(actionNo);
		ret += generateEventActionXml(actionNo);
		return ret;
		}


		private String generateEventXml(String currentCellContent) {
		int guardNo = 1;
		String ret = "";
		final String eventXmlPost = "</org.eventb.core.event>\n";
		int guardNo = 1;
		ret += generateEventLabelXml(m_currentEventNo);

		ret += generateEventLabelXml(m_currentEventNo);
		for (String parentCellContent: m_parentCellsEventBCode){
		ret += generateEventGuardXml(guardNo++, parentCellContent);
		}

		ret += generateEventGuardXml(guardNo, currentCellContent);
		ret += generateEventActionsXml(1);
		ret += generateEventActionsXml();
		ret += eventXmlPost;

		return ret;
		}


		private void outputCell(String currentCellContent) {
		m_eventsXml += generateEventXml(currentCellContent);
		}
		@@ -125,12 +129,13 @@ final public class HierarchicalGridEventBGenerator implements HierarchcialGridCh
		return m_eventsXml;
		}

		Deque<String> m_parentCellsEventBCode = new ArrayDeque<String>();
		int m_currentEventNo = 0;

		String m_eventsXml = "";

		String m_tableName = "";
		List<String> m_outputVariables;
		TwoDimensionalGrid m_outputGrid;
		VariableCollection m_variableDefinitions;
		Deque<String> m_parentCellsEventBCode = new ArrayDeque<String>();
		static BooleanVariableType m_booleanType = new BooleanVariableType();
		EventBGenerator m_eventBGenerator = new EventBGenerator();
		}

src/main/java/ca/mcscert/jtet/expression/EventBGenerator.java

+0 −15

Original line number	Diff line number	Diff line
		@@ -104,9 +104,7 @@ final public class EventBGenerator implements CheckerGenerator{
		String variablesRelatedXml = "";

		variablesRelatedXml += generateVariablesXml(variableCollection);
		variablesRelatedXml += generateOutputVariableXml();
		variablesRelatedXml += generateInvariantsXml(variableCollection);
		variablesRelatedXml += generateOutputInvariantXml();
		variablesRelatedXml += generateInitEventXml(variableCollection);

		return variablesRelatedXml;
		@@ -154,14 +152,6 @@ final public class EventBGenerator implements CheckerGenerator{
		return "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"" + variableName +"\" org.eventb.core.identifier=\"";
		}

		private String generateOutputVariableXml() {
		return "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\""+ "outputVariable" +"\" org.eventb.core.identifier=\"outputVar\"/>\n";
		}

		private String generateOutputInvariantXml() {
		return "<org.eventb.core.invariant name=\"" + "outputInvariant" + "\" org.eventb.core.label=\"outputInv" + "\" org.eventb.core.predicate=\"output ∈ ℤ\"/>\n";
		}

		private String generateInvariantsXml(VariableCollection variableCollection) {
		String ret = "";
		int invariantsNum = 1;
		@@ -189,10 +179,6 @@ final public class EventBGenerator implements CheckerGenerator{
		return "</org.eventb.core.event>\n";
		}

		private String generateInitEventOutputActionXml(int actionNo) {
		return "<org.eventb.core.action name=\"OutputAction\" org.eventb.core.assignment=\"output ≔ 0\" org.eventb.core.label=\"act" + actionNo + "\"/>\n";
		}

		private String generateInitEventActionXmlPre(int actionNo) {

		return "<org.eventb.core.action name=\"InitAction" + actionNo + "\" org.eventb.core.assignment=\"";
		@@ -207,7 +193,6 @@ final public class EventBGenerator implements CheckerGenerator{
		String ret = "";
		ret += generateInitEventXmlPre();
		ret += generateInitEventActionsXml(variableCollection);
		ret += generateInitEventOutputActionXml(0);
		ret += generateInitEventXmlPost();

		return ret;

src/main/java/ca/mcscert/jtet/tablularexpression/HierarchcialGridEventBCheckerWalkerGenerator.java

0 → 100644

+65 −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.tablularexpression;

		import ca.mcscert.jtet.eventbgenerator.HierarchicalGridEventBGenerator;

		import java.util.List;

		/**
		*
		* @author Tony Jiang <jiangy76@mcmaster.ca>
		*/
		public class HierarchcialGridEventBCheckerWalkerGenerator {

		private static void HandleGrid(SubHierarchyFetcher grid, HierarchcialGridCheckerGenerator generator) {
		List<HierarchicalCell> cells = grid.getSubHiearchy();

		for (int i = 0; i < cells.size(); ++i) {
		HierarchicalCell cell = cells.get(i);

		if (!cell.getSubHiearchy().isEmpty()) {
		generator.handleEdgeCell(cell);
		generator.descendIntoGridFromCell(cell);
		HandleGrid(cell, generator);
		generator.ascendFromGrid();
		}
		else
		{
		generator.handleLeafCell(cell);
		}
		}
		}

		public static String GenerateCheckerFromGrid( HierarchicalGrid leftGrid, HierarchcialGridCheckerGenerator generator) {
		HandleGrid(leftGrid, generator);
		return generator.getFinalString();
		}
		}