Commit 8c3baa54 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add a SAL Grid generator. 

Add a SAL grid generator, using the depth first search walker.  It currently
just generates simple IF statements for each condition, nest IF statements as
appropriate.
parent d1053738

src/main/java/ca/mcscert/jtet/salgenerator/HierarchicalGridSALGenerator.java

0 → 100644
+112 −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.salgenerator;



import ca.mcscert.jtet.expression.BooleanVariableType;

import ca.mcscert.jtet.expression.RealVariableType;

import ca.mcscert.jtet.expression.SALGenerator;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridCheckerGeneratorV2;

import ca.mcscert.jtet.tablularexpression.TwoDimensionalGrid;



/**

 * Created by matthew on 6/3/14.

 */

public class HierarchicalGridSALGenerator implements HierarchicalGridCheckerGeneratorV2 {



    public HierarchicalGridSALGenerator(VariableCollection variableDefinitions, TwoDimensionalGrid outputGrid)

    {

        this.variableDefinitions = variableDefinitions;

        this.outputGrid = outputGrid;

    }



    @Override

    public void descendIntoGridFromCell(Cell cell)

    {

        outputCellPrelude(cell);

        m_firstCell = true;

    }



    @Override

    public void ascendFromGrid()

    {

        result.append("ENDIF ");

        m_firstCell = false;

    }



    private void outputCellPrelude(Cell cell)

    {

        m_currentlyRunning = true;

        if (m_firstCell) {

            result.append("IF ");

        } else {

            result.append("ELSIF ");

        }

        m_firstCell = false;

        result.append(MatlabParser.parseMatlabCode(variableDefinitions, cell.contents()).getCheckerOutput(m_generator, BooleanVariableType.Type));

        result.append(" THEN ");

    }



    @Override

    public void handleLeafCell(Cell cell)

    {

        outputCellPrelude(cell);

        result.append(MatlabParser.parseMatlabCode(variableDefinitions, outputGrid.get(0, m_rightMostGridIndex++).contents()).getCheckerOutput(m_generator, RealVariableType.Type));

        result.append(" ");

    }



    @Override

    public void handleEdgeCell(Cell cell)

    {

    }



    @Override

    public String getFinalString()

    {

        if (m_currentlyRunning && result.length() != 0) {

            result.append("ENDIF");

            m_currentlyRunning = false;

        }

        return result.toString();

    }



    final private StringBuilder result = new StringBuilder();



    private boolean m_currentlyRunning = false;

    private boolean m_firstCell = true;

    private int m_rightMostGridIndex = 0;



    final private VariableCollection variableDefinitions;

    final private TwoDimensionalGrid outputGrid;



    final private SALGenerator m_generator = new SALGenerator();

}

src/main/java/ca/mcscert/jtet/tablularexpression/HierarchicalGridCheckerGeneratorV2.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 HierarchicalGridCheckerGeneratorV2 {

    void descendIntoGridFromCell(Cell cell);

    void ascendFromGrid();



    void handleLeafCell(Cell cell);

    void handleEdgeCell(Cell cell);



    String getFinalString();

}

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

0 → 100644
+59 −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;



import java.util.List;



/**

 *

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

public class HierarchicalGridCheckerWalkerGeneratorV2 {



    private static void HandleGrid(SubHierarchyFetcher grid, HierarchicalGridCheckerGeneratorV2 generator) {

        List<HierarchicalCell> cells = grid.getSubHiearchy();

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

            HierarchicalCell cell = cells.get(i);



            if (cell.getSubHiearchy().isEmpty()) {

                generator.handleLeafCell(cell);

            } else {

                generator.handleEdgeCell(cell);

                generator.descendIntoGridFromCell(cell);

                HandleGrid(cell, generator);

                generator.ascendFromGrid();

            }

        }

    }



    public static String GenerateCheckerFromGrid(HierarchicalGrid grid, HierarchicalGridCheckerGeneratorV2 generator) {

        HandleGrid(grid, generator);

        return generator.getFinalString();

    }

}

src/test/java/ca/mcscert/jtet/salgenerator/HierarchicalGridSALGeneratorTest.java

0 → 100644
+90 −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.salgenerator;



import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.tablularexpression.*;

import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;



import java.util.List;



import static org.junit.Assert.assertEquals;



/**

 *

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

@RunWith(JUnit4.class)

public class HierarchicalGridSALGeneratorTest {



    // Exercise the cvc3 generator using a table designed in matlab.

    @Test

    public void exerciseCVC3Generator() {

        HierarchicalGrid grid = new HierarchicalGrid();

        List<HierarchicalCell> topCells = grid.getSubHiearchy();



        topCells.add(new HierarchicalCell("x > 0"));

        topCells.add(new HierarchicalCell("x == 0"));

        topCells.add(new HierarchicalCell("0 > x"));



        List<HierarchicalCell> nextGrid = topCells.get(1).getSubHiearchy();

        nextGrid.add(new HierarchicalCell("z > 0"));

        nextGrid.add(new HierarchicalCell("z == 0"));

        nextGrid.add(new HierarchicalCell("0 > z"));



        nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));



        outputGrid.resize(1, 5);

        for (int i = 0; i < outputGrid.sizeY(); ++i) {

            outputGrid.get(0, i).setContents(String.valueOf(i + 1));

        }



        String out = HierarchicalGridCheckerWalkerGeneratorV2.GenerateCheckerFromGrid(grid, new HierarchicalGridSALGenerator(variableParser.parseVariables("x,z"), outputGrid));



        String expected = "IF (x > 0) THEN 1 ELSIF (x = 0) THEN IF (z > 0) THEN 2 ELSIF (z = 0) THEN IF (z = 0) THEN 3 ENDIF ELSIF (0 > z) THEN 4 ENDIF ELSIF (0 > x) THEN 5 ENDIF";

        assertEquals(expected, out);

    }



    // Test the smtlib generator using an empty table

    @Test

    public void testEmptyTable() {

        HierarchicalGrid grid = new HierarchicalGrid();



        String out = HierarchicalGridCheckerWalkerGeneratorV2.GenerateCheckerFromGrid(grid, new HierarchicalGridSALGenerator(variableParser.parseVariables("x,z"), outputGrid));



        String expected = "";



        assertEquals(expected, out);

    }



    VariableParser variableParser = new VariableParser();

    TwoDimensionalGrid outputGrid = new TwoDimensionalGrid();

}