Initial version of the PVS table generator.

package ca.mcscert.jtet.pvsgenerator;

import ca.mcscert.jtet.tabularexpression.Table;

/**

 * @author matthew

 * Produces an equivalent PVS function for the given table.

 * <p>

 * This table generator produces the contents of a PVS file, ready to be used by PVS to verify the properties of a given

 * table.  This file contains a single function representing the given table, which can be called from any other generic

 * PVS code.

 * @author Matthew Dawson

 */

public class PVSTableGenerator {

    public PVSTableGenerator(Table table) {

        m_table = table;

    }

    public void setTable(Table table) {

        m_table = table;

    }

    public String generate() {

        StringBuilder ret = new StringBuilder();

        ret.append(m_table.getName())

                .append(":THEORY\nBEGIN\n")

                .append(m_table.getName())

                .append("(")

                .append(variableDeclarationGenerator.GenerateVariablesDeclaration(m_table.getVariables().getInputVariablesList()))

                .append("):");

        variableDeclarationGenerator.generateVariableTypeInformation(ret, m_table.getVariables().getOutputVariablesList().iterator().next());

        ret.append(" = \n")

                .append(m_table.walk(new HierarchicalGridPVSGenerator()))

                .append("END ")

                .append(m_table.getName())

                .append("\n");

        return ret.toString();

    }

    private Table m_table;

    private final static PVSVariableDeclarationGenerator variableDeclarationGenerator = new PVSVariableDeclarationGenerator();

}

/*

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

import ca.mcscert.jtet.tabularexpression.HierarchicalCell;

import ca.mcscert.jtet.tabularexpression.HierarchicalGrid;

import ca.mcscert.jtet.tabularexpression.Table;

import ca.mcscert.jtet.tabularexpression.TwoDimensionalGrid;

import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;

import java.util.List;

import static org.hamcrest.CoreMatchers.is;

import static org.junit.Assert.assertThat;

/**

 * @author matthew

 */

@RunWith(JUnit4.class)

public class PVSTableGeneratorTest {

    @Test

    public void testSimpleTable() {

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

        VariableCollection variableCollection = new VariableCollection(new PartialVariableCollection(new Variable("x", new RealType())), new PartialVariableCollection(outputVar));

        Table table = new Table("oneLayerTable", variableCollection, MatlabParser.Parser);

        HierarchicalGrid leftGrid = table.getLeftGrid();

        List<HierarchicalCell> cells = leftGrid.getSubHierarchy();

        cells.add(new HierarchicalCell("x >= 0"));

        cells.add(new HierarchicalCell("x < 0"));

        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 2);

        outputGrid.get(0,0).setContents("1");

        outputGrid.get(0,1).setContents("2");

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

        PVSTableGenerator generator = new PVSTableGenerator(table);

        assertThat(generator.generate(), is("oneLayerTable:THEORY\n" +

                "BEGIN\n" +

                "oneLayerTable(x:real):real = \n" +

                "COND\n" +

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

                "\t(x < 0) -> 2\n" +

                "ENDCOND\n" +

                "END oneLayerTable\n"));

    }

}