Commit 76525f24 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add support for multiple outputs to the PVS table generator. 

Major pieces of work are now in place.
parent 1fb29f6e

src/main/java/ca/mcscert/jtet/pvsgenerator/PVSTableGenerator.java

+11 −1
Original line number Diff line number Diff line
@@ -29,8 +29,11 @@ 


package ca.mcscert.jtet.pvsgenerator;



import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.tabularexpression.Table;



import java.util.Collection;



/**

 * Produces an equivalent PVS function for the given table.

 * <p>
@@ -58,7 +61,14 @@ public class PVSTableGenerator { 
                .append(variableDeclarationGenerator.GenerateVariablesDeclaration(m_table.getVariables().getInputVariablesList()))

                .append("):");



        Collection<Variable> outputVariables = m_table.getVariables().getOutputVariablesList();

        if (outputVariables.size() == 1) {

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

        } else {

            ret.append("[# ");

            ret.append(variableDeclarationGenerator.GenerateVariablesDeclaration(outputVariables));

            ret.append(" #]");

        }



        ret.append(" = \n")

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

src/test/java/ca/mcscert/jtet/pvsgenerator/test/PVSTableGeneratorTest.java

+33 −0
Original line number Diff line number Diff line
@@ -79,4 +79,37 @@ public class PVSTableGeneratorTest { 
                "ENDCOND\n" +

                "END oneLayerTable\n"));

    }



    @Test

    public void testMultipleOutputEnumeratedTable() {

        Variable outputVar1 = new Variable("o1", new RealType());

        Variable outputVar2 = new Variable("o2", new RealType());

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

        Table table = new Table("oneLayerComplexTable", 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(outputVar1, outputGrid);



        outputGrid = new TwoDimensionalGrid(1, 2);

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

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

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



        PVSTableGenerator generator = new PVSTableGenerator(table);

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

                "BEGIN\n" +

                "oneLayerComplexTable(x:real):[# o1:real,o2:real #] = \n" +

                "COND\n" +

                "\t(x >= 0) -> (#o1 := 1, o2 := 3#),\n" +

                "\t(x < 0) -> (#o1 := 2, o2 := 4#)\n" +

                "ENDCOND\n" +

                "END oneLayerComplexTable\n"));

    }

}