Commit bed9d045 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Merge branch 'master' into TableTool_jmerge 

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10540 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parents 314a0465 e3b00992

@GUI/GUI.m

+1 −1
Original line number Diff line number Diff line
@@ -64,7 +64,7 @@ classdef GUI < handle 
        multi_opt_out = [];

        prover_opt_pvs = [];

        prover_opt_cvc = [];

        version = '0.6';

        version = '0.7';

        undo_man = [];

        undo_opt = [];

        redo_opt = [];

@GUI/about_call.m

+2 −2
Original line number Diff line number Diff line
@@ -7,5 +7,5 @@ 
% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function [] = about_call(object,src,event)

    msgbox(sprintf('Table Toolbox v%s\nCopyright 2011\nColin Eles\nMcMaster Center for Software Certification',object.version),'About Table Tool','modal');

    msgbox(sprintf('Tabular Expression Toolbox v%s\nCopyright 2011\nColin Eles & 2012 Matthew Dawson, Mark Lawford\nMcMaster Center for Software Certification',object.version),'About Tabular Expression Toolbox','modal');

end

@GUI/evaluate_counter_grid.m

+6 −4
Original line number Diff line number Diff line
@@ -41,11 +41,13 @@ check_string = [check_string counter sprintf('\n')]; 
for i=1:size(grid.cells,2)

    condition_string = get(grid.cells(i).cond,'string');

    

    if size(condition_string,1) > 0

        s = [condition_string(1,:)];

        for j = 2:size(condition_string,1)

           s = [s ' ' condition_string(j,:)];

        end

        condition_string = s;

    end

    

    if(~isempty(condition_string))

@GUI/init.m

+1 −1
Original line number Diff line number Diff line
@@ -174,7 +174,7 @@ uimenu(checkmenu,'Label','PVS Generate file','Callback',@(src,event)pvs_file_cal 
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));

uimenu(helpmenu,'Label','About Tabular Expression Toolbox','Callback',@(src,event)about_call(object,src,event));



object.set_command_pos;

object.reset_wh();

@PVS_checker/parse_pvs_result.m

+3 −3
Original line number Diff line number Diff line
@@ -24,12 +24,12 @@ else 
            % These parsing depend on the version of PVS used,

            % which may be a bad idea, although pvs is not

            

            if strncmp(object.pvs_version,'PVS Version 4.0',15)

            if object.pvs_version <= 4.0

                % find the TCC that was unprovable

                search_str = sprintf('(?<=Proving formula %s[\\n]*)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)),char(found(i)));

            elseif strncmp(object.pvs_version,'PVS Version 4.2',15)

            elseif object.pvs_version <= 4.2

                search_str =  sprintf('(?<=Installing rewrite rule \\w+\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));

            elseif strncmp(object.pvs_version,'PVS Version ',12) && str2num(object.pvs_version(13:15))>=5.0

            elseif object.pvs_version >= 5.0

                search_str =  sprintf('(?<=Installing rewrite rule.*\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));

            end

            found2 = regexp(result,char(search_str),'match','once');