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

Started working on generating EventB projects from tabular expressions. 

This is a whole bunch of combined commits. The main features supported in
the version are: support four kinds of tool modes(buttons to select from
refinement/no refinement modes and single/multiple outputs modes),support
enumeration type.
parent b5fdb3be

@EventBGenerator/EventBGenerator.m

0 → 100644
+21 −0
Original line number Diff line number Diff line 
% Author: Yanjun Jiang jiangy76@mcmaster.ca

% Organization: McMaster Centre for Software Certification

classdef EventBGenerator



    properties

        data = [];

    end



    methods

        %% EventB_generator

        %    constructor

        % inputs:

        %   data:Data - data to generate from

        % outputs:

        %   object:EventB_generator - generated object.

        function object = EventBGenerator(data)

            object.data = data;

        end

    end



end

@EventBGenerator/genereate_eventb_project.m

0 → 100644
+34 −0
Original line number Diff line number Diff line 
%% genereate_eventb_project

% Generate the EventB project and all the files contained in the project.

% Step1, Convert Matlab table to Java table.

% Step2, Create an eventB project object and pass the table parameters to it.

% Step3, Convert refinement mode & set project Folder path.

% Step4, Generate the EventB project.

%

% inputs:

%   object:EventBGenerator - current object.



% Author: Yanjun Jiang jiangy76@mcmaster.ca

% Organization: McMaster Centre for Software Certification



function genereate_eventb_project(object)

    %Convert Matlab table to Java table.

    table = TableBlock.convert_table_to_java_table(object.data);



    %Create an eventB project object and pass the table parameter to it

    eventBProject = ca.mcscert.jtet.eventbgenerator.EventBProject(table.getName());

    eventBProject.setTable(table);



    %Convert refinement mode & set project Folder path

    if (object.data.settings.eventb_refinement_mode == 0)

        projectFolderPath = strcat('NR/', char(table.getName()), '/');

        refine_mode = ca.mcscert.jtet.eventbgenerator.RefinementMode.WithoutRefinement;

    else

         projectFolderPath = strcat('WR/', char(table.getName()), '/');

        refine_mode = ca.mcscert.jtet.eventbgenerator.RefinementMode.WithRefinement;

    end



    % Generate the EventB project

    eventBProject.generate(projectFolderPath, refine_mode);

end

@GUI/GUI.m

+7 −0
Original line number Diff line number Diff line
@@ -51,6 +51,7 @@ classdef GUI < handle 
        Data = [];

        PVS = [];

        CVC = [];

        EventB = [];

        pvs_checked = [];

        mode = [];

        EMLGen = [];
@@ -62,6 +63,12 @@ classdef GUI < handle 
        multi_grp = [];

        multi_opt_reg = [];

        multi_opt_out = [];



        %For EventB Project

        eventb_refinement_mode = [];

        eventb_refinement_opt_reg = [];

        eventb_refinement_opt_out = [];



        prover_opt_pvs = [];

        prover_opt_cvc = [];

        prover_opt_smtlib = [];

@GUI/eventb_ext_call.m

0 → 100644
+18 −0
Original line number Diff line number Diff line 
%% eventb_ext_call

% generate the eventb file, calls the generate grid

% function. generates all the variable declarations.

%

% inputs:

%   object:EventBGenerator - current object.



% Author: Yanjun Jiang jiangy76@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function eventb_ext_call(object,~,~)

    object.save_data;

    error = object.check_call([],2);



    if (~error)

        object.EventB.genereate_eventb_project;

        msgbox('EventB Project Generated!');

    end

end

@GUI/eventb_refinement_mode_select_call.m

0 → 100644
+23 −0
Original line number Diff line number Diff line 
%% eventb_refinement_mode_select_call

%   called whenever a user selects a refinement mode,

%   no refinement (0) vs. without refinement (1).

% inputs:

%   object:GUI - GUI handle

%   src - calling object

%   event - event data

% outputs:

%   none

% Author: Yanjun Jiang jiangy76@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function [] = eventb_refinement_mode_select_call(object,src,~)

    label = get(src,'Label');



    if strcmp(label,'With Refinement')

        object.eventb_refinement_mode = 1;

    else %No refinement

        object.eventb_refinement_mode = 0;

    end



    object.update_eventb_refinement_mode_check_status;



end