Generalize the EventB walker into a general depth first walker. (d1053738) · Commits · tables / jtet

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

+2 −2

Original line number	Diff line number	Diff line
		@@ -66,7 +66,7 @@ final public class EventBTableGenerator {
		HierarchicalGridEventBGenerator hierarchcialGridEventBGenerator;
		int refineLayerNo = (RefinementMode.WithoutRefinement == m_refineMode) ? Integer.MAX_VALUE : i;//No Refinement mode layerCount is set to infinity so that handleLeafCell is always executed.
		hierarchcialGridEventBGenerator = new HierarchicalGridEventBGenerator(m_refineMode, refineLayerNo, m_table);
		output += HierarchcialGridEventBCheckerWalkerGenerator.GenerateCheckerFromGrid(m_table.getLeftGrid(), hierarchcialGridEventBGenerator);
		output += HierarchicalGridDepthFirstCheckerWalkerGenerator.GenerateCheckerFromGrid(m_table.getLeftGrid(), hierarchcialGridEventBGenerator);

		//Step 4: Generate the file Refine Relation Xml
		if (hierarchcialGridEventBGenerator.isRefineRelationNecessary()) {

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

+1 −1

Original line number	Diff line number	Diff line
		@@ -43,7 +43,7 @@ import java.util.*;
		* This class generate common non-initialisation events
		* @author Yanjun Jiang <jiangy76@mcmaster.ca>
		*/
		final public class HierarchicalGridEventBGenerator implements HierarchcialGridCheckerGenerator {
		final public class HierarchicalGridEventBGenerator implements HierarchicalGridDepthFirstCheckerGenerator {

		public HierarchicalGridEventBGenerator(RefinementMode refineMode, int refineLayerNo, Table table) {
		m_refineMode = refineMode;

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

0 → 100644

+43 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2014 Matthew Dawson <matthew@mjdsystems.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;

		/**
		*
		* @author Matthew Dawson <matthew@mjdsystems.ca>
		*/
		public interface HierarchicalGridDepthFirstCheckerGenerator {
		void descendIntoGridFromCell(Cell cell);
		void ascendFromGrid();

		void handleLeafCell(Cell cell);
		void handleEdgeCell(Cell cell);

		String getFinalString();
		}

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

+9 −11

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2014 Matthew Dawson <matthew@mjdsystems.ca>
		* Copyright (C) 2014 Yanjun Jiang <jiangy76@mcmaster.ca>
		*
		* Redistribution and use in source and binary forms, with or without
		@@ -26,38 +27,35 @@
		* 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 java.util.List;

		/**
		*
		* @author Matthew Dawson <matthew@mjdsystems.ca>
		* @author Tony Jiang <jiangy76@mcmaster.ca>
		*/
		public class HierarchcialGridEventBCheckerWalkerGenerator {
		public class HierarchicalGridDepthFirstCheckerWalkerGenerator {

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

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

		if (!cell.getSubHiearchy().isEmpty()) {
		if (cell.getSubHiearchy().isEmpty()) {
		generator.handleLeafCell(cell);
		} else {
		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);
		public static String GenerateCheckerFromGrid(HierarchicalGrid grid, HierarchicalGridDepthFirstCheckerGenerator generator) {
		HandleGrid(grid, generator);
		return generator.getFinalString();
		}
		}

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

+5 −5

File changed.

Contains only whitespace changes.