updated block mask output

                for i = 1:size(in_handles,1)

                    mask_string = [mask_string 'port_label(''input'',' int2str(i) ',''' get_param(in_handles(i),'Name') ''');' ];

                end

                mask_string = [mask_string 'text(0.5, 0.6, ''Tabular Expression'', ''horizontalAlignment'', ''center'')'];

                out_handles=find_system(code_block, 'SearchDepth',1,'FindAll','On','FollowLinks','On','LookUnderMasks','All','BlockType','Outport');

                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'')'];

              if checked == 0  

                mask_string = [mask_string 'color(''red'')text(0.5, 0.4, ''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.4, ''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);

   <!--

This HTML is auto-generated from an M-file.

To make changes, update the M-file and republish this document.

      --><title>Product Overview</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-08-31"><meta name="m-file" content="TT_gs_over"><style type="text/css">

      --><title>Product Overview</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-09-01"><meta name="m-file" content="TT_gs_over"><style type="text/css">

body {

  background-color: white;

    output = 8;

  <span class="keyword">end</span>

<span class="keyword">end</span>

</pre><p>If we go back and look at our model window we can see that our Tabular Expression block has updated based on our specified inputs and outputs.</p><p><img vspace="5" hspace="5" src="walk5.png" alt=""> </p><h2>Proving a Table<a name="6"></a></h2><p>Let us assume that a table designer has specified the following function table:</p><p><img vspace="5" hspace="5" src="walk6.png" alt=""> </p><p>In order for a tabular expression to be considered "proper" it must satisfy a <b>Completness</b> and <b>Disjointness</b> condition</p><div><ul><li>Completness means that in the specification of a function we have considered all possible inputs in a condition cell.</li><li>Disjointness means that in the specification of a function all condition cells in a grid are pairwise disjoint, in other words for all possible inputs it is not the case that two conditions are true at the same time.</li></ul></div><p>We desire these properties to ensure that our function is total and is deterministic. A function that is not total or not deterministic can have undesired effects, potentially causing safety critical problems depending on the requirements of the software. The graphical layout of a table helps the designer to evaluate a table for these conditions. Some times it is a non-trivial problem to determine if these conditions have been meet, so we employ the use of a theorem proving software to mechanically prove the properties.</p><p>Consider our example table, the designer of this table has failed to consider the case when x is equal to 1, the completness condition is not satisfied. Clicking on the PVS button will start the proof and popup a process dialog as shown below:</p><p><img vspace="5" hspace="5" src="walk7.png" alt=""> </p><p>If the proof fails it will pop up a dialog giving the user some feedback of why the proof failed as seen in the next image.</p><p><img vspace="5" hspace="5" src="walk8.png" alt=""> </p><p>The Typecheck summary window will display the formula for which a proof was not found. If a proof fails PVS attempts to find a counter example. In this senario pvs has found that a counter example to the formula is x = 1. When a counter example is found the tool will give visual feedback on which conditions were true and which were false for that counter example. A condition coloured red indicates that the condition was false for the given counter example, a green colour indicates that a condition is true. For this example we can see that both possible conditions are false for the counter example indicating to the table designer that they failed to consider a case of the input.</p><p><img vspace="5" hspace="5" src="walk9.png" alt=""> </p><p>In the example above, the designer of the table has captured the case where x = 0 in both conditions of the table. The tool has highlighted both cells green to indicate to the user that for the counter example of x = 0 both of these conditions are true.</p><p class="footer"><br>

</pre><p>If we go back and look at our model window we can see that our Tabular Expression block has updated based on our specified inputs and outputs.</p><p><img vspace="5" hspace="5" src="walk5.png" alt=""> </p><h2>Proving a Table<a name="6"></a></h2><p>Let us assume that a table designer has specified the following function table:</p><p><img vspace="5" hspace="5" src="walk6.png" alt=""> </p><p>In order for a tabular expression to be considered "proper" it must satisfy a <b>Completness</b> and <b>Disjointness</b> condition</p><div><ul><li>Completness means that in the specification of a function we have considered all possible inputs in a condition cell.</li><li>Disjointness means that in the specification of a function all condition cells in a grid are pairwise disjoint, in other words for all possible inputs it is not the case that two conditions are true at the same time.</li></ul></div><p>We desire these properties to ensure that our function is total and is deterministic. A function that is not total or not deterministic can have undesired effects, potentially causing safety critical problems depending on the requirements of the software. The graphical layout of a table helps the designer to evaluate a table for these conditions. Some times it is a non-trivial problem to determine if these conditions have been meet, so we employ the use of a theorem proving software to mechanically prove the properties.</p><p>Consider our example table, the designer of this table has failed to consider the case when x is equal to 1, the completness condition is not satisfied. Clicking on the PVS button will start the proof and popup a process dialog as shown below:</p><p><img vspace="5" hspace="5" src="walk7.png" alt=""> </p><p>If the proof fails it will pop up a dialog giving the user some feedback of why the proof failed as seen in the next image.</p><p><img vspace="5" hspace="5" src="walk8.png" alt=""> </p><p>The Typecheck summary window will display the formula for which a proof was not found. If a proof fails PVS attempts to find a counter example. In this senario pvs has found that a counter example to the formula is x = 1. When a counter example is found the tool will give visual feedback on which conditions were true and which were false for that counter example. A condition coloured red indicates that the condition was false for the given counter example, a green colour indicates that a condition is true. For this example we can see that both possible conditions are false for the counter example indicating to the table designer that they failed to consider a case of the input.</p><p><img vspace="5" hspace="5" src="walk9.png" alt=""> </p><p>In the example above, the designer of the table has captured the case where x = 0 in both conditions of the table. The tool has highlighted both cells green to indicate to the user that for the counter example of x = 0 both of these conditions are true, the designer has failed to unambiguosly specify what should happen in this senario.</p><p class="footer"><br>

      Published with MATLAB&reg; 7.10<br></p></div><!--

##### SOURCE BEGIN #####

%% Product Overview

% In the example above, the designer of the table has captured the case

% where x = 0 in both conditions of the table. The tool has highlighted

% both cells green to indicate to the user that for the counter example of

% x = 0 both of these conditions are true.

% x = 0 both of these conditions are true, the designer has failed to

% unambiguosly specify what should happen in this senario.

%

##### SOURCE END #####

--></body></html>

 No newline at end of file

<matlabrelease>2010a</matlabrelease>

<name>Table Toolbox</name>

<type>toolbox</type>

<type>Toolbox</type>

<icon>$toolbox/simulink/simulink/simulinkicon.gif</icon>

<help_location>./html</help_location>

<help_contents_icon>$toolbox/matlab/icons/bookicon.gif</help_contents_icon>