Commit aeb14e87 authored by Colin Eles's avatar Colin Eles
Browse files

updated GUI to generalize the typecheck procedure, default prover is now CVC,... 

updated GUI to generalize the typecheck procedure, default prover is now CVC, although this can be changed, currently not saved to the block, so each time you open it will go back to CVC, may want to change this in the future. need to fix some stuff in validation report

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6562 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent a32b4a99

@GUI/GUI.m

+7 −0
Original line number Diff line number Diff line
@@ -62,10 +62,17 @@ classdef GUI < handle 
        multi_grp = [];

        multi_opt_reg = [];

        multi_opt_out = [];

        prover_opt_pvs = [];

        prover_opt_cvc = [];

        version = '0.2';

        undo_man = [];

        undo_opt = [];

        redo_opt = [];

        

        default_prover = [];

        PVS_const = 1;

        CVC_const = 2;

        

    end

    

    methods

@GUI/init.m

+29 −15
Original line number Diff line number Diff line
@@ -59,22 +59,26 @@ object.save_ext_pb = uicontrol('style','push',... 
    'Parent',object.fig,...

    'callback',@(src,event)save_ext_call(object,src,event));



% PVS button

object.pvs_pb = uicontrol('style','push',...

    'units','pix',...

    'string','PVS',...

    'HorizontalAlign','left',...

    'Parent',object.fig,...

    'callback',@(src,event)pvs_ext_call(object,src,event));



% Check button

object.check_pb = uicontrol('style','push',...

    'units','pix',...

    'string','Check',...

    'string','Syntax',...

    'HorizontalAlign','left',...

    'Parent',object.fig,...

    'Max',2.0,...

    'callback',@(src,event)check_call(object,src,event));







% PVS button

object.pvs_pb = uicontrol('style','push',...

    'units','pix',...

    'string','Typecheck',...

    'HorizontalAlign','left',...

    'Parent',object.fig,...

    'callback',@(src,event)typecheck_call(object,src,event));



% Input/Output button

object.input_pb = uicontrol('style','push',...

    'units','pix',...
@@ -139,7 +143,7 @@ end 
% Set up Menu

filemenu = uimenu('Label','File');

editmenu = uimenu('Label','Edit');

pvsmenu = uimenu('Label','PVS');

checkmenu = uimenu('Label','Typecheck');

helpmenu = uimenu('Label','Help');

uimenu(filemenu,'Label','New','Accelerator','n','Callback',@(src,event)new_call(object,src,event));

uimenu(filemenu,'Label','Open...','Callback',@(src,event)open_call(object,src,event));
@@ -153,12 +157,19 @@ 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));

uimenu(pvsmenu,'Label','Typecheck','Accelerator','t','Callback',@(src,event)pvs_ext_call(object,src,event));

uimenu(pvsmenu,'Label','PVS Settings','Callback',@(src,event)settings_call(object,src,event));

uimenu(pvsmenu,'Label','Check Status','Callback',@(src,event)prf_file_call(object,src,event));

uimenu(pvsmenu,'Label','Generate PVS file','Callback',@(src,event)pvs_file_call(object,src,event));

uimenu(pvsmenu,'Label','Typecheck SimTypes','Callback',@(src,event)pvs_ext_call_sim(object,src,event));

uimenu(pvsmenu,'Label','CVC Solve','Callback',@(src,event)cvc_ext_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));

object.prover_opt_pvs = uimenu(prover_menu,'Label','PVS','Callback',@(src,event)prover_select_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');



uimenu(checkmenu,'Label','PVS Typecheck','Separator','on','Callback',@(src,event)pvs_ext_call(object,src,event));

uimenu(checkmenu,'Label','PVS Settings','Callback',@(src,event)settings_call(object,src,event));

uimenu(checkmenu,'Label','PVS Check Status','Callback',@(src,event)prf_file_call(object,src,event));

uimenu(checkmenu,'Label','PVS Generate file','Callback',@(src,event)pvs_file_call(object,src,event));

uimenu(checkmenu,'Label','PVS Typecheck SimTypes','Callback',@(src,event)pvs_ext_call_sim(object,src,event));



uimenu(helpmenu,'Label','Product Help','Callback',@(src,event)help_call(object,src,event));

uimenu(helpmenu,'Label','About Table Tool','Callback',@(src,event)about_call(object,src,event));
@@ -169,6 +180,8 @@ object.draw_allgrids(1); 
object.saved = 1;

object.setPBenable;



object.default_prover = object.CVC_const;





object.settings = Settings();

if isfield(object.Data.settings,'set')
@@ -184,6 +197,7 @@ object.undo_man = UndoManager(); 


object.update_Statusbar;

object.update_multi_check_status;

object.update_prover_check_status;

object.update_undoredo;



object.PVS = PVS_checker(object.Data);

@GUI/prover_select_call.m

0 → 100644
+11 −0
Original line number Diff line number Diff line 
function [] = prover_select_call(object,src,event)

label = get(src,'Label');

% determine which label the user clicked on

if strcmp(label,'CVC3')

    object.default_prover = object.CVC_const;

else

    object.default_prover = object.PVS_const;

end



object.update_prover_check_status;

end
 
 No newline at end of file

@GUI/typecheck_call.m

0 → 100644
+14 −0
Original line number Diff line number Diff line 
function [ output_args ] = typecheck_call( object,src,event )

%TYPECHECK_CALL Summary of this function goes here

%   Detailed explanation goes here



if object.default_prover == object.CVC_const

    

    cvc_ext_call(object,src,event);

else

    pvs_ext_call(object,src,event);

end





end

@GUI/update_prover_check_status.m

0 → 100644
+22 −0
Original line number Diff line number Diff line 
%% update_prover_check_status

%    updates the menu item checked status for singal output vs. multioutput based on the

%    current status of the program.

% inputs:

%   object - current GUI object

% outputs:

%   none

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function update_prover_check_status( object )





if object.default_prover == object.CVC_const

    set(object.prover_opt_cvc,'Checked','on');

    set(object.prover_opt_pvs,'Checked','off');

else

    set(object.prover_opt_cvc,'Checked','off');

    set(object.prover_opt_pvs,'Checked','on');

end



end