Implement a PVS HierarchicalGridGenerator.

/*

 * 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.pvsgenerator;

import ca.mcscert.jtet.expression.BooleanType;

import ca.mcscert.jtet.expression.Expression;

import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.expression.Type;

import ca.mcscert.jtet.tabularexpression.HierarchicalGridDepthFirstCheckerGenerator;

import org.apache.commons.lang3.StringUtils;

import java.util.ArrayList;

import java.util.List;

import java.util.Map;

/** Generates a COND statement for PVS from a tabular expression

 * @author matthew

 */

public class HierarchicalGridPVSGenerator implements HierarchicalGridDepthFirstCheckerGenerator {

    /**

     * {@inheritDoc}

     * <p>

     * This outputs the condition for this level of cells, and starts a new COND expression.

     */

    @Override

    public void descendIntoGridFromCell(Expression inputCellExpression) {

        outputConditionCell(inputCellExpression);

        m_result.append("COND\n");

        ++m_indentation;

        m_isNewLevel = true;

    }

    /**

     * {@inheritDoc}

     * <p>

     * Finishes a COND expression

     */

    @Override

    public void ascendFromGrid() {

        --m_indentation;

        m_result.append("\n")

            .append(StringUtils.repeat('\t', m_indentation))

            .append("ENDCOND");

    }

    /**

     * {@inheritDoc}

     * <p>

     * Creates an output for this leaf cell.

     */

    @Override

    public void handleLeafCell(Expression inputCellExpression, Map<Variable, Expression> outputCellsExpression) {

        outputConditionCell(inputCellExpression);

        List<String> outputAssignements = new ArrayList<String>(outputCellsExpression.size());

        for(Map.Entry<Variable, Expression> outputCell : outputCellsExpression.entrySet()) {

            String output = "";

            if (outputCellsExpression.size() != 1) {

                output += outputCell.getKey().name() + " := ";

            }

            output +=  parseExpression(outputCell.getValue(), outputCell.getKey().type());

            outputAssignements.add(output);

        }

        if (outputCellsExpression.size() != 1) {

            m_result.append("(#");

        }

        m_result.append(StringUtils.join(outputAssignements, ", "));

        if (outputCellsExpression.size() != 1) {

            m_result.append("#)");

        }

    }

    /**

     * {@inheritDoc}

     * <p>

     * Unused.

     */

    @Override

    public void handleEdgeCell(Expression inputCellExpression) {

    }

    /**

     * Generate PVS code for the given expression with the given type.

     * @param inputCellExpression The expression to convert to PVS code

     * @param outputType Type to generate the PVS expression for

     * @return PVS code for the given expression

     */

    private String parseExpression(Expression inputCellExpression, Type outputType) {

        return inputCellExpression.getCheckerOutput(PVSExpressionGenerator.Generator, outputType);

    }

    /**

     * Outputs a condition for the current COND statement, ready to accept the output.

     * @param inputCellExpression The condition expression

     */

    private void outputConditionCell(Expression inputCellExpression) {

        if (m_isNewLevel) {

            m_isNewLevel = false;

        } else {

            m_result.append(",\n");

        }

        m_result.append(StringUtils.repeat('\t', m_indentation))

            .append(parseExpression(inputCellExpression, BooleanType.Type))

            .append(" -> ");

    }

    @Override

    public String getFinalString() {

        if (m_isRunning) {

            m_result.append("\nENDCOND\n");

            m_isRunning = false;

        }

        return m_result.toString();

    }

    private StringBuilder m_result = new StringBuilder("COND\n");

    private boolean m_isNewLevel = true;

    private boolean m_isRunning = true;

    private int m_indentation = 1;

}

/*

 * 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.pvsgenerator.test;

import ca.mcscert.jtet.expression.PartialVariableCollection;

import ca.mcscert.jtet.expression.RealType;

import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.pvsgenerator.HierarchicalGridPVSGenerator;

import ca.mcscert.jtet.tabularexpression.*;

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 HierarchicalGridPVSGeneratorTest {

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

    @Test

    public void exercisePVSGenerator() {

        Variable outputVar = new Variable("output", new RealType());

        Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x, z"), new PartialVariableCollection(outputVar)), MatlabParser.Parser);

        HierarchicalGrid grid = table.getLeftGrid();

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

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

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

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

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

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

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

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

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

        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 5);

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

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

        }

        table.getVariableOutputs().put(outputVar, outputGrid);

        String out = table.walk(new HierarchicalGridPVSGenerator());

        String expected = "COND\n" +

                "\t(x > 0) -> 1,\n" +

                "\t(x = 0) -> COND\n" +

                "\t\t(z > 0) -> 2,\n" +

                "\t\t(z = 0) -> COND\n" +

                "\t\t\t(z = 0) -> 3\n" +

                "\t\tENDCOND,\n" +

                "\t\t(0 > z) -> 4\n" +

                "\tENDCOND,\n" +

                "\t(0 > x) -> 5\n" +

                "ENDCOND\n";

        assertEquals(expected, out);

    }

    VariableParser variableParser = new VariableParser();

}