From bf57899cd797957dde9aa9285e546d72dd56df80 Mon Sep 17 00:00:00 2001 From: Yanjun Jiang Date: Fri, 21 Nov 2014 16:01:18 -0500 Subject: [PATCH] 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. --- @EventBGenerator/EventBGenerator.m | 21 ++++++++++++ @EventBGenerator/genereate_eventb_project.m | 34 +++++++++++++++++++ @GUI/GUI.m | 7 ++++ @GUI/eventb_ext_call.m | 18 ++++++++++ @GUI/eventb_refinement_mode_select_call.m | 23 +++++++++++++ @GUI/init.m | 16 +++++++-- @GUI/save_data.m | 3 ++ @GUI/save_settings.m | 2 ++ @GUI/setData.m | 6 ++++ ...date_eventb_refinement_mode_check_status.m | 21 ++++++++++++ 10 files changed, 149 insertions(+), 2 deletions(-) create mode 100644 @EventBGenerator/EventBGenerator.m create mode 100644 @EventBGenerator/genereate_eventb_project.m create mode 100644 @GUI/eventb_ext_call.m create mode 100644 @GUI/eventb_refinement_mode_select_call.m create mode 100644 @GUI/update_eventb_refinement_mode_check_status.m diff --git a/@EventBGenerator/EventBGenerator.m b/@EventBGenerator/EventBGenerator.m new file mode 100644 index 0000000..bc22323 --- /dev/null +++ b/@EventBGenerator/EventBGenerator.m @@ -0,0 +1,21 @@ +% 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 diff --git a/@EventBGenerator/genereate_eventb_project.m b/@EventBGenerator/genereate_eventb_project.m new file mode 100644 index 0000000..d9389d9 --- /dev/null +++ b/@EventBGenerator/genereate_eventb_project.m @@ -0,0 +1,34 @@ +%% 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 + diff --git a/@GUI/GUI.m b/@GUI/GUI.m index 080fbf0..045df48 100644 --- a/@GUI/GUI.m +++ b/@GUI/GUI.m @@ -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 = []; diff --git a/@GUI/eventb_ext_call.m b/@GUI/eventb_ext_call.m new file mode 100644 index 0000000..e79ea26 --- /dev/null +++ b/@GUI/eventb_ext_call.m @@ -0,0 +1,18 @@ +%% 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 diff --git a/@GUI/eventb_refinement_mode_select_call.m b/@GUI/eventb_refinement_mode_select_call.m new file mode 100644 index 0000000..70df3cf --- /dev/null +++ b/@GUI/eventb_refinement_mode_select_call.m @@ -0,0 +1,23 @@ +%% 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 diff --git a/@GUI/init.m b/@GUI/init.m index 5cd7b44..7cb727b 100644 --- a/@GUI/init.m +++ b/@GUI/init.m @@ -157,6 +157,11 @@ uimenu(editmenu,'Label','Ports and Data Manager','Accelerator','p','Callback',@( multi_mode_menu = uimenu(editmenu,'Label','Output Mode'); object.multi_opt_reg = uimenu(multi_mode_menu,'Label','One Output','Callback',@(src,event)multi_select_call(object,src,event)); object.multi_opt_out = uimenu(multi_mode_menu,'Label','Multiple Outputs','Callback',@(src,event)multi_select_call(object,src,event)); + +eventb_refinement_mode_menu = uimenu(editmenu,'Label','EventB Refinement Mode'); +object.eventb_refinement_opt_reg = uimenu(eventb_refinement_mode_menu,'Label','No Refinement','Callback',@(src,event)eventb_refinement_mode_select_call(object,src,event)); +object.eventb_refinement_opt_out = uimenu(eventb_refinement_mode_menu,'Label','With Refinement','Callback',@(src,event)eventb_refinement_mode_select_call(object,src,event)); + uimenu(checkmenu,'Label','Typecheck','Accelerator','t','Callback',@(src,event)typecheck_call(object,src,event)); prover_menu = uimenu(checkmenu,'Label','Default Prover'); object.prover_opt_cvc = uimenu(prover_menu,'Label','CVC3','Callback',@(src,event)prover_select_call(object,src,event)); @@ -164,7 +169,7 @@ object.prover_opt_pvs = uimenu(prover_menu,'Label','PVS','Callback',@(src,event) object.prover_opt_smtlib = uimenu(prover_menu,'Label','Z3','Callback',@(src,event)prover_select_call(object,src,event)); uimenu(checkmenu,'Label', 'Syntax Check','Callback',@(src,event)check_call(object,src,event)); - +uimenu(checkmenu,'Label','EventB Generate Project','Separator','on','Callback',@(src,event)eventb_ext_call(object,src,event)); uimenu(checkmenu,'Label','CVC Typecheck','Separator','on','Callback',@(src,event)cvc_ext_call(object,src,event)); uimenu(checkmenu,'Label','CVC Generate File'); @@ -196,12 +201,19 @@ else end +if isfield(object.Data.settings,'eventb_refinement_mode') + object.eventb_refinement_mode = object.Data.settings.eventb_refinement_mode; +else + object.eventb_refinement_mode = 0; +end + object.undo_man = UndoManager(); object.update_Statusbar; object.update_multi_check_status; +object.update_eventb_refinement_mode_check_status; object.update_prover_check_status; object.update_undoredo; @@ -210,7 +222,7 @@ object.EMLGen = EMLGenerator(object.Data); object.CVC = CVC_checker(object.Data); - +object.EventB = EventBGenerator(object.Data); object.initialized = 1; object.Data.open = 1; diff --git a/@GUI/save_data.m b/@GUI/save_data.m index 52c555b..455a87e 100644 --- a/@GUI/save_data.m +++ b/@GUI/save_data.m @@ -20,11 +20,14 @@ object.Data.function_inputs = get(object.function_inputs_control,'String'); object.Data.checked = object.pvs_checked; object.Data.multi_mode = object.multi_mode; +%settings Struct set.set = 1; set.inputs = object.settings.pvs_includes; set.count = object.settings.counter_trials; set.range = object.settings.counter_range; set.except = object.settings.except; +set.eventb_refinement_mode = object.eventb_refinement_mode; + object.Data.settings = set; end diff --git a/@GUI/save_settings.m b/@GUI/save_settings.m index ff588cd..4316940 100644 --- a/@GUI/save_settings.m +++ b/@GUI/save_settings.m @@ -11,6 +11,8 @@ set.set = 1; set.inputs = object.settings.pvs_includes; set.count = object.settings.counter_trials; set.range = object.settings.counter_range; +set.eventb_refinement_mode = object.eventb_refinement_mode; + object.Data.settings = set; object.Data.function_name = get(object.function_name_control,'String'); object.Data.function_inputs = get(object.function_inputs_control,'String'); diff --git a/@GUI/setData.m b/@GUI/setData.m index f86079c..a59065e 100644 --- a/@GUI/setData.m +++ b/@GUI/setData.m @@ -16,8 +16,14 @@ object.pvs_checked = Data.checked; object.function_name_text = Data.function_name; object.function_inputs_text = Data.function_inputs; object.multi_mode = Data.multi_mode; + if isempty(object.multi_mode) object.multi_mode = 0; end + +if isempty(object.eventb_refinement_mode) + object.eventb_refinement_mode = 0; +end + end diff --git a/@GUI/update_eventb_refinement_mode_check_status.m b/@GUI/update_eventb_refinement_mode_check_status.m new file mode 100644 index 0000000..013ada5 --- /dev/null +++ b/@GUI/update_eventb_refinement_mode_check_status.m @@ -0,0 +1,21 @@ +%% update_eventb_refinement_mode_check_status +% updates the menu item checked status for with refinement vs. +% no refinement based on the current status of the program. +% inputs: +% object - current GUI object +% outputs: +% none +% Author: Yanjun Jiang jiangy76@mcmaster.ca +% Organization: McMaster Centre for Software Certification +function update_eventb_refinement_mode_check_status(object) + + +if object.eventb_refinement_mode == 0 + set(object.eventb_refinement_opt_reg,'Checked','on'); + set(object.eventb_refinement_opt_out,'Checked','off'); +else + set(object.eventb_refinement_opt_reg,'Checked','off'); + set(object.eventb_refinement_opt_out,'Checked','on'); +end + +end -- GitLab