Commit 6eb468b6 authored by Yanjun Jiang's avatar Yanjun Jiang Committed by Matthew Dawson
Browse files

Support table refinement. 

From this version, two kinds of mode, i.e., Single Output No Refinement
(SONR),Single Output With Refinement(SOWR) are supported.
parent 260c9ded

src/main/java/ca/mcscert/jtet/eventbgenerator/EventBProject.java

+2 −2
Original line number Diff line number Diff line
@@ -44,13 +44,13 @@ final public class EventBProject { 
       m_table = table;

    }



    public void generate(String folderPath) throws IOException {

    public void generate(String folderPath, RefinementMode refineMode) throws IOException {

        //create Project Folder and Project File

        createEventProjectFolder(folderPath);

        writeProjectFile(m_projectName, folderPath);



        //generate Table EventB File

        m_eventBTableGenerator = new EventBTableGenerator(m_table);

        m_eventBTableGenerator = new EventBTableGenerator(m_table, refineMode);

        m_eventBTableGenerator.generateEventBXml(folderPath);

    }

src/main/java/ca/mcscert/jtet/eventbgenerator/EventBTableGenerator.java

+73 −15
Original line number Diff line number Diff line
@@ -32,6 +32,7 @@ import ca.mcscert.jtet.expression.EventBGenerator; 
import ca.mcscert.jtet.tablularexpression.*;



import java.io.IOException;

import java.util.List;



/**

 *
@@ -39,8 +40,9 @@ import java.io.IOException; 
 */

final public class EventBTableGenerator {



    public EventBTableGenerator(Table table) {

    public EventBTableGenerator(Table table, RefinementMode refineMode) {

        m_table = table;

        m_refineMode = refineMode;

    }



    public void generateEventBXml(String folderPath) throws IOException {
@@ -48,26 +50,82 @@ final public class EventBTableGenerator { 
        final String machineFileCfgPreXml = "<org.eventb.core.machineFile org.eventb.core.configuration=\"org.eventb.core.fwd;de.prob.units.mchBase\" version=\"5\">\n";

        final String machineFileCfgPostXml = "</org.eventb.core.machineFile>";



        String output= "";

        int outputLayerNum = calculateOutputLayerNum();

        for (int i = 0; i < outputLayerNum; i++) {



        //Step 1: Generate the Pre Xml

            //Step 1: Append the Pre Xml

            String output = "";

            output += versionEncodingXml;

            output += machineFileCfgPreXml;



            //Step 2: Generate the Variables & Invariants Xml

            EventBGenerator m_eventBGenerator = new EventBGenerator();

            output += m_eventBGenerator.GenerateVariablesDeclaration(m_table.getInputVariables());



            //Step 3: Generate the Events Xml

        m_hierarchcialGridCheckerGenerator = new HierarchicalGridEventBGenerator(m_table);

        output  += HierarchcialGridEventBCheckerWalkerGenerator.GenerateCheckerFromGrid(m_table.getLeftGrid(), m_hierarchcialGridCheckerGenerator);

            HierarchicalGridEventBGenerator hierarchcialGridEventBGenerator;

            int refineLayerNo = (RefinementMode.WithoutRefinement == m_refineMode) ? Integer.MAX_VALUE : i;//No Refinement mode layerCount is set to infinity so that handleLeafCell is always executed.

            hierarchcialGridEventBGenerator = new HierarchicalGridEventBGenerator(m_refineMode, refineLayerNo, m_table);

            output += HierarchcialGridEventBCheckerWalkerGenerator.GenerateCheckerFromGrid(m_table.getLeftGrid(), hierarchcialGridEventBGenerator);



        //Step 3: Generate the Post Xml

            //Step 4: Generate the file Refine Relation Xml

            if (hierarchcialGridEventBGenerator.isRefineRelationNecessary()) {

                output += generateFileRefineRelation(refineLayerNo);

            }



            //Step 5: Append the Post Xml

            output += machineFileCfgPostXml;



        EventBFileWriter.writeEventBBumFile(folderPath + m_table.getTableName() + ".bum", output);

            //Step 6: Write out EventB code into file in the project folder

            EventBFileWriter.writeEventBBumFile(getFullFileName(i, folderPath) ,output);

        }

    }



    String getFullFileName(int no, String folderPath) {

        String fullName = folderPath;



        if (m_refineMode == RefinementMode.WithRefinement) {

            fullName += m_table.getTableName() + "_M" + no + ".bum";

        } else {

            fullName += m_table.getTableName()  + ".bum";

        }



        return fullName;

    }



    private int calculateOutputLayerNum() {

        if (RefinementMode.WithoutRefinement  == m_refineMode) {

            return 1;

        }

        else {

            return calculateMaxRefineLayerNum(m_table.getLeftGrid());

        }

    }



    //m_maxRefineLayerNum is also the max Recursion Depth

    private int calculateMaxRefineLayerNum(SubHierarchyFetcher grid) {

        int maxRecursionDepth = 0;

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



        for (HierarchicalCell cell : cells) {

            int subGridMaxRefineLayerNum = calculateMaxRefineLayerNum(cell) + 1;

            if (subGridMaxRefineLayerNum > maxRecursionDepth){

                maxRecursionDepth = subGridMaxRefineLayerNum;

            }

        }



        return maxRecursionDepth;

    }



    private String generateFileName(int fileNo) {

        return m_table.getTableName() + "M" + fileNo;

    }



    private String generateFileRefineRelation(int refinerFileNo) {

        int refinedFileNo = refinerFileNo - 1;

        return "<org.eventb.core.refinesMachine name=\"" + generateFileName(refinerFileNo) + "\" org.eventb.core.target=\"" + generateFileName(refinedFileNo) + "\"/>\n";

    }



    Table m_table;

    EventBGenerator m_eventBGenerator = new EventBGenerator();

    HierarchcialGridCheckerGenerator m_hierarchcialGridCheckerGenerator;

    RefinementMode m_refineMode;

}
 
 No newline at end of file

src/main/java/ca/mcscert/jtet/eventbgenerator/HierarchicalGridEventBGenerator.java

+121 −34
Original line number Diff line number Diff line
@@ -33,14 +33,11 @@ import ca.mcscert.jtet.expression.EventBGenerator; 
import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerGenerator;

import ca.mcscert.jtet.tablularexpression.*;

import org.apache.commons.lang3.StringUtils;

import ca.mcscert.jtet.tablularexpression.Table;

import ca.mcscert.jtet.tablularexpression.TwoDimensionalGrid;



import java.util.ArrayDeque;

import java.util.Deque;

import java.util.List;

import java.util.*;



/**

 * This class generate common non-initialisation events
@@ -48,95 +45,185 @@ import java.util.List; 
 */

final public class HierarchicalGridEventBGenerator implements HierarchcialGridCheckerGenerator {



    public HierarchicalGridEventBGenerator(Table table) {

    public HierarchicalGridEventBGenerator(RefinementMode refineMode, int refineLayerNo, Table table) {

        m_refineMode = refineMode;

        m_refineLayerNo = refineLayerNo;

        m_variableDefinitions = table.getInputVariables();

        m_tableName = table.getTableName();

        m_outputGrid = table.getVariableOutputs().get(0);

        m_outputVariables = table.getOutputVariables();

    }



    private String getCurrentEventName(){

        return "Event" + m_currentEventNo;

    }



    private String generateEventLabelXml(int eventNo) {

        return "<org.eventb.core.event name=\"" + getCurrentEventName() + "\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt" + eventNo + "\">\n";

    }



    private String generateEventGuardXml(int guardNo, String guard) {

        return "<org.eventb.core.guard name=\"Guard" + guardNo + "\" org.eventb.core.label=\"grd" + + guardNo + "\" org.eventb.core.predicate=\"" + guard +"\"/>\n";

    }



    private String generateEventActionXml(int actionNo) {

        String value = m_outputGrid.get(0, m_currentEventNo - 1).contents();

        return "<org.eventb.core.action name=\"Action" + actionNo + "\" org.eventb.core.assignment=\"" + m_outputVariables.get(0) +  " ≔ " + value + "\" org.eventb.core.label=\"act" + actionNo + "\"/>\n";

     private String generateOneEventActionXml(int actionNo, String variable, String value) {

        return  "<org.eventb.core.action name=\"Action" + (actionNo + 1) + "\" org.eventb.core.assignment=\"" + variable +  " ≔ " + value + "\" org.eventb.core.label=\"act" + (actionNo + 1) + "\"/>\n";

    }



    private String generateEventActionsXml() {

        int actionNo = 1;

        String ret = "";

        String outputVariable;

        String outputValue;

        int actionNo = 0;



        if (m_collectedOutputValues.size() == 1) { // leaf action

            outputValue = m_collectedOutputValues.get(0);

            outputVariable = m_outputVariables.get(actionNo).name();

            ret += generateOneEventActionXml(actionNo, outputVariable, outputValue);

        } else {

            String topGridName = m_outputVariables.get(actionNo).name();

            String columnVector = "{";

            columnVector += StringUtils.join(m_collectedOutputValues, ',');

            columnVector += "}";

            ret += "<org.eventb.core.action name=\"Action" + (actionNo + 1) + "\" org.eventb.core.assignment=\"" + topGridName + " :∈ " + columnVector + "\" org.eventb.core.label=\"act" + (actionNo + 1) + "\"/>\n";

            m_collectedOutputValues.clear();

        }



        ret += generateEventActionXml(actionNo);

        return ret;

    }



    private String generateEventXml(String currentCellContent) {

    private String getEventName(){

        return "Event" + m_eventNo;

    }



    private String getEventLabelName(String eventNo){

        return "evt" + eventNo;

    }



    private String generateEventLabelXml() {

        return "<org.eventb.core.event name=\"" + getEventName() + "\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"" + getEventLabelName(m_eventNo) + "\">\n";

    }



    private String getRefineName(){

        if (m_cellLayerNo < m_refineLayerNo || m_parentEventNo.equals("")) {

            return getEventLabelName(m_eventNo);

        } else {

            return getEventLabelName(m_parentEventNo);

        }

    }

    private String generateEventRefineRelationXml(){

        return "<org.eventb.core.refinesEvent name=\"" + getRefineName() + "\" org.eventb.core.target=\"" + getRefineName() + "\"/>\n";

    }



    private String generateEventXml() {

        int guardNo = 1;

        String ret = "";

        final String eventXmlPost = "</org.eventb.core.event>\n";



        ret += generateEventLabelXml(m_currentEventNo);

        for (String parentCellContent: m_parentCellsEventBCode){

        ret += generateEventLabelXml();



        for (String parentCellContent: m_eventBGuards){

            ret += generateEventGuardXml(guardNo++, parentCellContent);

        }



        ret += generateEventGuardXml(guardNo, currentCellContent);

        ret += generateEventActionsXml();



        if (isRefineRelationNecessary()) {

            ret += generateEventRefineRelationXml();

        }



        ret += eventXmlPost;



        m_collectedOutputValues.clear();



        return ret;

    }



    private void outputCell(String currentCellContent) {

        m_eventsXml += generateEventXml(currentCellContent);

    public void generateEventNo() {

        m_eventNo = m_parentEventNo;



        if (!m_eventNo.equals("")) {

            m_eventNo += "_";

            m_eventNo += m_subGridCellIndex;

        }

        else{

            m_eventNo += m_subGridCellIndex;

        }

    }



    @Override

    public void descendIntoGridFromCell(Cell cell) {

        m_parentCellsEventBCode.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_eventBGenerator, BooleanVariableType.Type));

        m_oldParentEventNo.push(m_parentEventNo);

        m_oldSubGridCellIndex.push(m_subGridCellIndex);

        m_subGridCellIndex = 0;



        m_cellLayerNo++;

        m_parentEventNo = m_eventNo;

        m_eventBGuards.push(handleCell(cell));

    }



    @Override

    public void ascendFromGrid() {

        m_parentCellsEventBCode.removeFirst();

        m_cellLayerNo--;

        m_parentEventNo = m_oldParentEventNo.pop();

        m_subGridCellIndex = m_oldSubGridCellIndex.pop();

        if (m_cellLayerNo == m_refineLayerNo) {

            m_eventsXml += generateEventXml();//outputEdgeCells

        }

        m_eventBGuards.pop();

    }



    @Override

    public void handleEdgeCell(Cell cell) {

        m_subGridCellIndex++;

        generatorGenerateEventNo();

    }



    @Override

    public void handleLeafCell(Cell cell) {

        m_currentEventNo++;

        String parsedCellCode = handleCell(cell);

        outputCell(parsedCellCode);

        m_tableRowNo++;

        m_subGridCellIndex++;

        generatorGenerateEventNo();



        m_eventBGuards.push(handleCell(cell));

        collectEdgeGridValues();

        if (m_cellLayerNo <= m_refineLayerNo) {

            m_eventsXml += generateEventXml();//outputLeafCells

        }

        m_eventBGuards.pop();

    }



    private void generatorGenerateEventNo() {

        if (m_cellLayerNo <= m_refineLayerNo) {

            generateEventNo();

        }

    }



    public String handleCell(Cell cell) {

    private void collectEdgeGridValues() {

        String outputValue = m_outputGrid.get(0, m_tableRowNo - 1).contents();

        m_collectedOutputValues.add(outputValue);

    }



    private String handleCell(Cell cell) {

        return MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_eventBGenerator, BooleanVariableType.Type);

    }



    public boolean isRefineRelationNecessary() {

        return (0 != m_refineLayerNo) && (RefinementMode.WithoutRefinement != m_refineMode);//the first layer also has not refinement.

    }



    @Override

    public String getFinalString() {

        return m_eventsXml;

    }



    int m_currentEventNo = 0;

    int m_tableRowNo = 0;

    int m_cellLayerNo = 0;

    int m_subGridCellIndex = 0;

    int m_refineLayerNo = 0;//is also the current column number

    String m_eventsXml = "";

    String m_tableName = "";

    String m_eventNo = "";//like evt1_3_2

    String m_parentEventNo = "";//like evt1_3

    List<Variable> m_outputVariables;

    TwoDimensionalGrid m_outputGrid;

    VariableCollection m_variableDefinitions;

    Deque<String> m_parentCellsEventBCode = new ArrayDeque<String>();

    List<String> m_collectedOutputValues = new ArrayList<String>();

    EventBGenerator m_eventBGenerator = new EventBGenerator();

    Stack<String> m_eventBGuards = new Stack<String>();

    Stack<String> m_oldParentEventNo = new Stack<String>();

    Stack<Integer> m_oldSubGridCellIndex = new Stack<Integer>();

    RefinementMode m_refineMode;

}

src/main/java/ca/mcscert/jtet/eventbgenerator/RefinementMode.java

0 → 100644
+38 −0
Original line number Diff line number Diff line 
/*

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



/**

 *

 * @author Yanjun Jiang

 */

public enum RefinementMode {

    WithoutRefinement,

    WithRefinement

}

src/main/java/ca/mcscert/jtet/expression/EventBGenerator.java

+2 −1
Original line number Diff line number Diff line
@@ -208,7 +208,8 @@ final public class EventBGenerator implements CheckerGenerator{ 
            actionNo++;

            ret += generateInitEventActionXmlPre(actionNo);

            ret += var.outputName();

            ret += " ≔ 0";

            ret += " :∈ ";

            ret += GenerateVariableType(var.type());

            ret += generateInitEventActionXmlPost(actionNo);

            ret += "\n";

        }