+TableBlock/delete_recursive.m

@@ -13,7 +13,7 @@ end
 LineChild = get( line_handle, 'LineChildren' ) ;
 if ~isempty( LineChild )
     for i=1:length( LineChild )
-        obj.delete_recursive( LineChild( i ) );
+        TableBlock.delete_recursive( LineChild( i ) );
     end
 else
     if get( line_handle, 'DstPortHandle' ) < 0

+TableBlock/set_block_display.m

@@ -22,11 +22,11 @@ for i = 1:size(out_handles,1)
     mask_string = [mask_string 'port_label(''output'',' int2str(i) ',''' get_param(out_handles(i),'Name') ''');' ];
 end
 
-mask_string = [mask_string 'text(0.5, 0.9, ''Tabular Expression'', ''horizontalAlignment'', ''center'')'];
+mask_string = [mask_string 'text(0.5, 0.9, ''Tabular Expression'', ''horizontalAlignment'', ''center'');'];
 if checked == 0
-    mask_string = [mask_string 'color(''red'')text(0.5, 0.1, ''Not Checked'', ''horizontalAlignment'', ''center'')'];
+    mask_string = [mask_string 'color(''red'');text(0.5, 0.1, ''Not Checked'', ''horizontalAlignment'', ''center'')'];
 else
-    mask_string = [mask_string 'color(''green'')text(0.5, 0.1, ''Checked'', ''horizontalAlignment'', ''center'')'];
+    mask_string = [mask_string 'color(''green'');text(0.5, 0.1, ''Checked'', ''horizontalAlignment'', ''center'')'];
     
 end
 set_param(getfullname(block_handle),'MaskDisplay',mask_string);

+TableBlock/set_code.m

@@ -40,7 +40,11 @@ code_blocks = find_system(getfullname(block_handle),'LookUnderMasks','all','Bloc
 % if the code block does not already exists we need to create a
 % new one
 if (isempty(code_blocks))
-    code_blocks = add_block('simulink/User-Defined Functions/Embedded MATLAB Function',code_block);
+    if (sum(version('-release') >= '2011a') >= 5)
+        code_blocks = add_block('simulink/User-Defined Functions/MATLAB Function',code_block);
+    else
+        code_blocks = add_block('simulink/User-Defined Functions/Embedded MATLAB Function',code_block);
+    end        
 end
 
 eml_handle = code_blocks;
@@ -83,6 +87,8 @@ for i=1:size(inports,1)
     
     for j=1:size(in_handles,1)
         if strcmp(get_param(inports(i),'Name'),get_param(in_handles(j),'Name'))
+            % Make sure the port numbers agree.
+            set_param(inports(i), 'Port', get_param(in_handles(j), 'Port'));
             found = 1;
         end
     end
@@ -117,6 +123,8 @@ for j = 1:size(in_handles,1)
         add_block('simulink/Sources/In1',new_port);
         new_port_num = sprintf('%s/1',get_param(in_handles(j),'Name'));
         dest_port = sprintf('%s/%d','code',j);
+        % Set the port number so the ports line up properly.
+        set_param(new_port, 'Port', get_param(in_handles(j), 'Port'));
         % sometimes line will be created automatically
         try
             add_line(getfullname(block_handle),new_port_num,dest_port);
@@ -135,6 +143,10 @@ for i=1:size(outports,1)
     
     for j=1:size(out_handles,1)
         if strcmp(get_param(outports(i),'Name'),get_param(out_handles(j),'Name'))
+                        
+            % Set the port number so the ports line up properly. 
+            set_param(outports(i), 'Port', get_param(out_handles(j), 'Port'));
+            
             found = 1;
         end
     end
@@ -166,6 +178,10 @@ for j = 1:size(out_handles,1)
         add_block('simulink/Sinks/Out1',new_port);
         new_port_num = sprintf('%s/1',get_param(out_handles(j),'Name'));
         dest_port = sprintf('%s/%d','code',j);
+        
+        % Set the port number so the ports line up properly.  
+        set_param(new_port, 'Port', get_param(out_handles(j), 'Port'));
+     
         try
             add_line(getfullname(block_handle),dest_port,new_port_num);
         end

@CVC_checker/CVC_checker.m

+% Author: Colin Eles elesc@mcmaster.ca
+% Organization: McMaster Centre for Software Certification
 classdef CVC_checker
-    %CVC_CHECKER Summary of this class goes here
-    %   Detailed explanation goes here
     
     properties
         
-        command = 'cvc3'
+        command = 'cvc3';
         data = [];
         
     end
@@ -12,15 +12,21 @@ classdef CVC_checker
     
     methods(Static)
         
-        [ code , query] = generate_cvc_grid( grid , level)
-        [ code ] = find_parents( grid )
-        cvc_string = matlab_to_cvc_syntax_translation(matlab_string)
-        [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type )
+        [ code , query] = generate_cvc_grid( grid , level);
+        [ code ] = find_parents( grid );
+        cvc_string = matlab_to_cvc_syntax_translation(matlab_string);
+        [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type );
         
     end
     
     methods
         
+        %% CVC_checker
+        %    constructor
+        % inputs:
+        %   data:Data - data to generate from
+        % outputs:
+        %   object:CVC_checker - generated object.
         function object = CVC_checker(data)
             object.data = data;
         end

@CVC_checker/cvc_check.m

+%% cvc_check
+% checks a table using cvc, parses results and returns them
+%
+% inputs:
+%   object:cvc_checker - cvc_checker object
+%
+% outputs;
+%   check:boolean - 0 if check fails, 1 if succeds
+%   seqs:structure - if typecheck succeds then output contains
+%       parsed output from cvc
+% Author: Colin Eles elesc@mcmaster.ca
+% Organization: McMaster Centre for Software Certification
+
 function [ check, seqs ] = cvc_check( object )
 %CVC_CHECK Summary of this function goes here
 %   Detailed explanation goes here
@@ -6,13 +19,15 @@ function [ check, seqs ] = cvc_check( object )
 [filename, queries] = object.generate_file;
 
     waitbar(.10,box,'Running Proof');
-
-[status, result] = system(['cvc3 ' filename ' +model'])
-
+%tic
+    % run the cvc command
+[status, result] = safe_execute_external_command(['cvc3 ' filename ' +model']);
+%toc
+% check return status for errors
 if (status ~= 0)
     
     if (status == 127)
-        msgbox('CVC3 command not found')
+        msgbox('CVC3 command not found');
     else
         msgbox(['an error has occured!' char(10) result]);
     end
@@ -26,19 +41,7 @@ end
 
 seqs = [];
 
-% look for incompleteness, happens with non-linear artihmetic, ie.
-% % multiplication
-% incomplete = regexp(result,'CVC3 was incomplete in this example due to','match');
-% if ~isempty(incomplete)
-%     incomplete_reason = regexp(result,'(?<=CVC3 was incomplete in this example due to:\n)[^\n]*','match','once')
-%     msgbox(['CVC could not typecheck this table for the following reasons:' char(10) incomplete_reason]);
-%     
-%         check = 0;
-%         seqs = 'canceled';
-%         delete(box);
-%         return;
-%     
-% end
+
 
 % look for parse errors
 fatal_exception = regexp(result,'*** Fatal exception');
@@ -66,10 +69,7 @@ for i = 1:size(queries,2)
         % formula was found to be invalid
         % look for a counter example
         asserts =  regexp(char(query_result),'(?<=ASSERT[ ]*\()[^\n]*(?==)|(?<==)[^\n]*(?=\);)','match');
-%         for j = 1:size(asserts,2)
-%             splits = {splits regexp(asserts(j),'=','split')};
-% 
-%         end
+
     
     if mod(i,2) == 1
         name = [filename '_' num2str(i) '_DIS'];

@CVC_checker/find_parents.m

+%% find_parents
+% function will find all the parents of a cell, used to determine what
+% preconditions must be true.
+%
+% inputs:
+%   cell:Cell - cell to find the parents of
+%
+% outputs;
+%   code:string - string of conjunction of all parent cells.
+% Author: Colin Eles elesc@mcmaster.ca
+% Organization: McMaster Centre for Software Certification
+
 function [ code ] = find_parents( cell )
 % assumption, initial input will be grid we want to find parents for not
-% parent cell itself
+%  cell itself
 
 code = '';
 if isempty(cell)

@CVC_checker/generate_cvc_grid.m

+%% genereate_cvc_grid
+% generate the queries for cvc for the inputted grid.
+%
+% inputs:
+%   grid:Grid - grid to generate conditions for.
+%   level:int - count of the queries generated.
+%
+% outputs;
+%   code:string - string representing code to generate including comments
+%   query:cell array - contains string representing both the disjoint and
+%   complete without the comments, used for validation report.
+% Author: Colin Eles elesc@mcmaster.ca
+% Organization: McMaster Centre for Software Certification
+
 function [ code , query] = generate_cvc_grid( grid , level)
-%GENERATE_CVC_GRID Summary of this function goes here
-%   Detailed explanation goes here
 
 % generate the formulas for the main grid
 
@@ -9,25 +21,12 @@ if isempty(parents);
     disjoint = 'QUERY (';
     complete = 'QUERY (';
 else
-    disjoint = ['QUERY ' parents ' => ('];
-    complete = ['QUERY ' parents ' => ('];
+    disjoint = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents) ' => ('];
+    complete = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents) ' => ('];
 end
 
 for i=1:size(grid.cells,2)
     
-%   1
-%   2  
-%   3
-%   
-%   1 2
-%   1 3
-%   2 3
-%   
-%   1 2 3 4
-%   1 2
-%   1 3
-%   1 4
-%   
   
     for j = i+1:size(grid.cells,2)
         % compare i to j

@CVC_checker/generate_file.m

+%% genereate_file
+% generate the cvc file to be inputted into cvc, calls the generate grid
+% function. generates all the variable declarations.
+%
+% inputs:
+%   object:CVC_checker - current object.
+%
+% outputs;
+%   filename:string - the filename of the generated file
+%   queries:cell arrray - a list of queries generated by the grids.
+% Author: Colin Eles elesc@mcmaster.ca
+% Organization: McMaster Centre for Software Certification
+
 function [ filename, queries ] = generate_file( object )
-%GENERATE_FILE Summary of this function goes here
-%   Detailed explanation goes here
 
 function_names = EMLGenerator.parse_inputs(object.data.function_name);
 function_name = char(function_names{1}(1));
@@ -28,7 +39,7 @@ if size(object.data.Grid2.cells,2) > 1
 end
 code = [code new_code];
 
-if size(object.data.Grid1.cells,2) > 1
+if object.data.multi_mode == 0 && size(object.data.Grid1.cells,2) > 1
     [new_code,new_queries] = CVC_checker.generate_cvc_grid(object.data.Grid1,size(queries,2));
     queries = [queries new_queries];
     code = [code new_code];
@@ -36,12 +47,6 @@ if size(object.data.Grid1.cells,2) > 1
 end   
 
 
-% generate grid 2
-
-
-
-char(code)
-
 fileid = fopen([function_name '.cvc'],'w');
 fprintf(fileid,'%s',char(code));
 fclose(fileid);

@CVC_checker/matlab_to_cvc_syntax_translation.m

@@ -12,6 +12,13 @@
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 function cvc_string = matlab_to_cvc_syntax_translation(matlab_string)
+
+s = [matlab_string(1,:)];
+for j = 2:size(matlab_string,1)
+   s = [s ' ' matlab_string(j,:)];
+end
+matlab_string = s;
+
 cvc_string = regexprep(matlab_string,'&&',' AND ');
 cvc_string = regexprep(cvc_string,'~(?!=)',' NOT ');
 cvc_string = regexprep(cvc_string,'~=',' /= ');

@CVC_checker/pvs_to_cvc_subtypes.m

+%% pvs_to_cvc_subtypes
+% converts types of the pvs syntax to cvc3 syntax. the syntax for doing
+% typing in the two languages is slightly different so we need to write
+% this function to translate between them.
+%
+% inputs:
+%   pvs_type:string - a string of a pvs type
+% outputs;
+%   cvc_type:string - a string of the cvc type.
+% Author: Colin Eles elesc@mcmaster.ca
+% Organization: McMaster Centre for Software Certification
+
 function [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type )
 %PVS_TO_CVC_SUBTYPES Summary of this function goes here
 %   Detailed explanation goes here

@Cell/purge.m

+%% purge
+%    Removes useless data from the block on saving, avoiding unnecessary
+%    changes and data storage.
+% inputs:
+%   object - Cell object
+% outputs:
+%   none
+% Author: Matthew Dawson <matthew@mjdsystems.ca>
+% Organization: McMaster Centre for Software Certification
+function  purge( object )
+object.grid_pb = [];
+object.cond = [];
+object.color = []; % This is always regenerated, so it is safe to kill.
+
+for i=1:size(object.subgrid,2)
+    object.subgrid(i).purge;
+end
+end
+

@Cell/upgrade.m

+%% upgrade
+%    Preforms any necessary upgrades to the TET to comply with the latest version.
+% inputs:
+%   object - Cell object
+% outputs:
+%   none
+% Author: Matthew Dawson <matthew@mjdsystems.ca>
+% Organization: McMaster Centre for Software Certification
+function  upgrade( object )
+if iscell(object.cond_text)
+    object.cond_text = object.cond_text{1};
+end
+
+for i=1:size(object.subgrid,2)
+    object.subgrid(i).upgrade;
+end
+end
+

@Data/purge.m

+%% purge
+%    Removes useless data from the block on saving, avoiding unnecessary
+%    changes and data storage.
+% inputs:
+%   object - Data object
+% outputs:
+%   none
+% Author: Matthew Dawson <matthew@mjdsystems.ca>
+% Organization: McMaster Centre for Software Certification
+function purge( object )
+object.Grid0.purge
+
+object.Grid1.purge
+object.Grid2.purge
+end
+

@Data/upgrade.m

+%% upgrade
+%    Preforms any necessary upgrades to the TET to comply with the latest version.
+% inputs:
+%   object - Data object
+% outputs:
+%   none
+% Author: Matthew Dawson <matthew@mjdsystems.ca>
+% Organization: McMaster Centre for Software Certification
+function upgrade( object )
+object.Grid0.upgrade
+
+object.Grid1.upgrade
+object.Grid2.upgrade
+end
+

@EMLGenerator/EMLGenerator.m

@@ -11,11 +11,11 @@ classdef EMLGenerator < handle
     end
     
     methods(Static)
-        revised_input = parse_inputs(input_string)
+        revised_input = parse_inputs(input_string);
         
         
         
-        converted = type_convert(name,type,expression)
+        converted = type_convert(name,type,expression);
         
         
         

@EMLGenerator/generate_preamble.m

@@ -37,7 +37,18 @@ else
     output = 'output';
 end
 
-code = sprintf('function [%s] = %s(%s)\n%s\n',output,char(function_name{1}(1)),input,'%%#eml');
+exception_flag = object.data.settings.except;
+
+if (exception_flag)
+    code = sprintf('function [%s, exception] = %s(%s)\n%s\n',output,char(function_name{1}(1)),input,'%%#eml');    
+else
+    code = sprintf('function [%s] = %s(%s)\n%s\n',output,char(function_name{1}(1)),input,'%%#eml');
+end
+
+
+
+
+
 % simulink forces you to have an output for all execution paths
 % since it can't compute completness and disjointness we need
 % to have a default value, if the user builds the table
@@ -48,13 +59,19 @@ code = sprintf('function [%s] = %s(%s)\n%s\n',output,char(function_name{1}(1)),i
 % guaranteed to
 % be filled in, regardless of the dimensionality of the table.
 
+left_top_right_top_cell = object.data.Grid2.cells(1);
+while size(left_top_right_top_cell.subgrid) ~= 0
+    left_top_right_top_cell = left_top_right_top_cell.subgrid.cells(1);
+end
+
+
 if (object.data.multi_mode == 1)
     for i=1:size(object.data.Grid1.cells,2)
         parsed_output = EMLGenerator.parse_inputs(strtrim(char(object.data.Grid1.cells(i).cond_text)));
         
         output_str = char(parsed_output{1}(1));
-        
-        code = [code sprintf('%s=%s;\n',output_str,EMLGenerator.type_convert(output_str,object.datatype,char(object.data.Grid0.Cells(i).result_text)))];
+
+        code = [code sprintf('%s=%s;\n',output_str,EMLGenerator.type_convert(output_str,object.datatype,char(object.data.Grid0.search_return(object.data.Grid1.cells(i), left_top_right_top_cell).result_text)))];
         
     end
     
@@ -63,6 +80,44 @@ else
     output_string = EMLGenerator.type_convert(test,object.datatype,char(object.data.Grid0.Cells(1).result_text) );
     code = [code sprintf('output=%s;\n', output_string )];
     
+end
+
+
+if (exception_flag)
+    
+    % generate NaN exceptions
+    nan_string = '';
+    
+    % genereate constraint exception
+    cons_string = '';
+
+    for i = 1:size(parsed_input,2)
+       % for each input consider if a NaN
+       
+       nan_string = [nan_string 'isnan(' char(parsed_input{i}(1)) ')'];
+       
+       if i ~= size(parsed_input,2)
+            nan_string = [nan_string '||'];
+       end
+       
+       if size(parsed_input{i},2) == 2
+           
+           str = regexp(parsed_input{i}(2),'(?<=\|).*(?=})','match','once');
+           
+           if (~isempty(char(str)))
+                cons_string = [cons_string sprintf('if ~(%s) \n  exception = true;\n  return;\nelse\n  exception = false;\nend\n',char(str))];
+           end
+           
+       end
+       
+       
+       
+    end
+    code = [code sprintf('if (%s) \n  exception = true;\n  return;\nelse\n  exception = false;\nend\n',nan_string)];
+        code = [code cons_string];
+    
+    
+    
 end
 
 end

@EMLGenerator/parse_inputs.m

@@ -42,7 +42,7 @@ for i=1:size(new_inputs,2)
     new_inputs{i}(1) = regexprep(new_inputs{i}(1),'\s','');
     
     valid = regexp(new_inputs{i}(1),'[a-zA-Z][_a-zA-Z0-9]*','match');
-    if isempty(char(new_inputs{i}(1))) || ~strcmp(new_inputs{i}(1),valid{1})
+    if isempty(char(new_inputs{i}(1))) || length(valid{1}(1)) == 0 || ~strcmp(new_inputs{i}(1),valid{1}(1))
         new_inputs{i}(2) = {'error'};
         %revised_input = cat(2,revised_input,[char(inputs{i}(1)); 'error'])
     end

@GUI/GUI.m

@@ -64,7 +64,7 @@ classdef GUI < handle
         multi_opt_out = [];
         prover_opt_pvs = [];
         prover_opt_cvc = [];
-        version = '0.2';
+        version = '0.7.4';
         undo_man = [];
         undo_opt = [];
         redo_opt = [];
@@ -92,7 +92,7 @@ classdef GUI < handle
     end
     
     methods(Static)
-        msgbox_scroll(msg)
+        msgbox_scroll(msg);
         
     end
 end

@GUI/about_call.m

@@ -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 2010\nColin Eles\nMcMaster Center for Software Certification',object.version),'About Table Tool','modal');
-end
\ No newline at end of file
+    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/check_call.m

@@ -15,7 +15,7 @@ error = 0;
 
 msg = object.check_inputs;
 if (isempty(msg))
-    set(object.function_inputs_control,'BackgroundColor',[1 1 1])
+    set(object.function_inputs_control,'BackgroundColor',[1 1 1]);
     msg = object.check_grid_condition(object.Grid2);
     if object.multi_mode == 0
         msg = [msg object.check_grid_condition(object.Grid1)];