Commit 6bdf0208 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Move the grid walkers into the Table class.

In preparation for the walkers to internalize the various details of tables,
move them inside the Table class.  This forces code generating grids to get
a proper table instance, pushing the table into more places, making things
more organized.
parent 6f95caa5
Loading
Loading
Loading
Loading
+1 −1
Original line number Diff line number Diff line
@@ -65,7 +65,7 @@ final public class EventBTableGenerator {
            HierarchicalGridEventBGenerator hierarchicalGridEventBGenerator;
            int refineLayerNo = (RefinementMode.WithoutRefinement == m_refineMode) ? Integer.MAX_VALUE : i;//No Refinement mode layerCount is set to infinity so that handleLeafCell is always executed.
            hierarchicalGridEventBGenerator = new HierarchicalGridEventBGenerator(m_refineMode, refineLayerNo, m_table);
            output += HierarchicalGridDepthFirstCheckerWalkerGenerator.GenerateCheckerFromGrid(m_table.getLeftGrid(), hierarchicalGridEventBGenerator);
            output += m_table.walk(hierarchicalGridEventBGenerator);

            //Step 4: Generate the file Refine Relation Xml
            if (hierarchicalGridEventBGenerator.isRefineRelationNecessary()) {
+4 −4
Original line number Diff line number Diff line
@@ -34,8 +34,7 @@ import ca.mcscert.jtet.smtlibchecker.antlr.SMTLibOutParserBaseListener;
import ca.mcscert.jtet.smtlibchecker.antlr.SMTLibOutParserLexer;
import ca.mcscert.jtet.smtlibchecker.antlr.SMTLibOutParserListener;
import ca.mcscert.jtet.smtlibchecker.antlr.SMTLibOutParserParser;
import ca.mcscert.jtet.tablularexpression.HierarchicalGrid;
import ca.mcscert.jtet.tablularexpression.HierarchicalGridBreadthFirstCheckerWalkerGenerator;
import ca.mcscert.jtet.tablularexpression.Table;
import org.antlr.v4.runtime.ANTLRInputStream;
import org.antlr.v4.runtime.CommonTokenStream;
import org.antlr.v4.runtime.misc.NotNull;
@@ -59,12 +58,13 @@ import java.util.Map;
 * @author Matthew Dawson <matthew@mjdsystems.ca>
 */
final public class CheckerRunner {
    public static List<CheckerRunnerResult> RunZ3(HierarchicalGrid grid, VariableCollection vars) {
    public static List<CheckerRunnerResult> RunZ3(Table table) {
        final VariableCollection vars = table.getVariables();
        List<CheckerRunnerResult> ret = new ArrayList<CheckerRunnerResult>();

        // Get the queries
        HierarchicalGridSMTLIBGenerator queryGenerator = new HierarchicalGridSMTLIBGenerator(vars);
        HierarchicalGridBreadthFirstCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, queryGenerator);
        table.walk(queryGenerator);

        // Start Z3
        ProcessBuilder pb;
+0 −66
Original line number Diff line number Diff line
/*
 * Copyright (C) 2013 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;

import java.util.List;

/**
 *
 * @author Matthew Dawson <matthew@mjdsystems.ca>
 */
public class HierarchicalGridBreadthFirstCheckerWalkerGenerator {

    private static void HandleGrid(SubHierarchyFetcher grid, HierarchicalGridBreadthFirstCheckerGenerator generator) {
        List<HierarchicalCell> cells = grid.getSubHierarchy();
        for (int i = 0; i < cells.size(); ++i) {
            HierarchicalCell cell = cells.get(i);

            if (cell.getSubHierarchy().isEmpty()) {
                generator.handleLeafCell(cell);
            } else {
                generator.handleEdgeCell(cell);
            }
        }

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

            if (!cell.getSubHierarchy().isEmpty()) {
                generator.descendIntoGridFromCell(cell);
                HandleGrid(cell, generator);
                generator.ascendFromGrid();
            }
        }
    }

    public static String GenerateCheckerFromGrid(HierarchicalGrid grid, HierarchicalGridBreadthFirstCheckerGenerator generator) {
        HandleGrid(grid, generator);
        return generator.getFinalString();
    }
}
+0 −61
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
 * 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 java.util.List;

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

    private static void HandleGrid(SubHierarchyFetcher grid, HierarchicalGridDepthFirstCheckerGenerator generator) {
        List<HierarchicalCell> cells = grid.getSubHierarchy();
        for (int i = 0; i < cells.size(); ++i) {
            HierarchicalCell cell = cells.get(i);

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

    public static String GenerateCheckerFromGrid( HierarchicalGrid leftGrid, HierarchicalGridDepthFirstCheckerGenerator generator) {
        HandleGrid(leftGrid, generator);
        return generator.getFinalString();
    }
}
+33 −0
Original line number Diff line number Diff line
@@ -95,6 +95,39 @@ public class Table {
        }
    }

    public String walk(HierarchicalGridDepthFirstCheckerGenerator generator) {
        HandleGrid(leftGrid, generator);
        return generator.getFinalString();
    }

    private static void HandleGrid(SubHierarchyFetcher grid, HierarchicalGridBreadthFirstCheckerGenerator generator) {
        List<HierarchicalCell> cells = grid.getSubHierarchy();
        for (int i = 0; i < cells.size(); ++i) {
            HierarchicalCell cell = cells.get(i);

            if (cell.getSubHierarchy().isEmpty()) {
                generator.handleLeafCell(cell);
            } else {
                generator.handleEdgeCell(cell);
            }
        }

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

            if (!cell.getSubHierarchy().isEmpty()) {
                generator.descendIntoGridFromCell(cell);
                HandleGrid(cell, generator);
                generator.ascendFromGrid();
            }
        }
    }

    public String walk(HierarchicalGridBreadthFirstCheckerGenerator generator) {
        HandleGrid(leftGrid, generator);
        return generator.getFinalString();
    }

    private String tableName;
    private VariableCollection m_variables;
    private final HierarchicalGrid leftGrid = new HierarchicalGrid();
Loading