latest updates to help file

% m-file. Tabular Expressions can be proved to be disjoint and complete

% using the PVS theorem prover. This allows users to ensure that the table

% they are designing has covered all possible inputs and is deterministic.

%

%% Creating a new table

% To create a new table block locate the Tabular Expression block in the

% simulink library.

%

% <<walk1.png>>

%

% Drag the Tabular Expression block to a new or existing model.

%

% <<walk2.png>>

%

%% Table Tool Dialog

% To edit the functionality of the table double click on the block to bring

% up the Table Tool dialog. From this dialog you can create the layout for

% the table and edit the conditions and outputs for the function.

%

% <<walk3.png>>

%

%% Example Table

% An example of a 2-dimensional table is shown below

%

% <<walk4.png>>

%

% This table specifies a function with 3 inputs x, y, and z, and one

% output. Saving the table will generate the following embedded matlab

% code:

function output  = demo_table(x,y,z)

%%#eml

if(x>0)

  if(y>1)

    if(z>1)

      output = 1;

    elseif(z<=1)

      output = 5;

    end

  elseif(y<=1)

    if(z>1)

      output = 2;

    elseif(z<=1)

      output = 6;

    end

  end

elseif(x==0)

  if(z>1)

    output = 3;

  elseif(z<=1)

    output = 7;

  end

elseif(x<0)

  if(z>1)

    output = 4;

  elseif(z<=1)

    output = 8;

  end

end

%%

% 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.

%

% <<walk5.png>>

%

%% Proving a Table

%

% Let us assume that a table designer has specified the following function

% table:

%

% <<walk6.png>>

% 

% In order for a tabular expression to be considered "proper" it must

% satisfy a *Completness* and *Disjointness* condition

%

% * Completness means that in the specification of a function we have

% considered all possible inputs in a condition cell.

% * 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.

%

% 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.

%%

% 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:

%

% <<walk7.png>>

%

% 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.

%

% <<walk8.png>>

%

% 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.

%

% <<walk9.png>>

% 

% 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.

%

   <!--

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-30"><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-08-31"><meta name="m-file" content="TT_gs_over"><style type="text/css">

body {

  background-color: white;

  color: gray;

}

  </style></head><body><div class="content"><h1>Product Overview</h1><p>This product allows users to interactively design a tabular expression. The resusulting function can be saved as a Simulink block or to a Matlab m-file. Tabular Expressions can be proved to be disjoint and complete using the PVS theorem prover. This allows users to ensure that the table they are designing has covered all possible inputs and is deterministic.</p><p class="footer"><br>

  </style></head><body><div class="content"><h1>Product Overview</h1><!--introduction--><p>This product allows users to interactively design a tabular expression. The resusulting function can be saved as a Simulink block or to a Matlab m-file. Tabular Expressions can be proved to be disjoint and complete using the PVS theorem prover. This allows users to ensure that the table they are designing has covered all possible inputs and is deterministic.</p><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Creating a new table</a></li><li><a href="#2">Table Tool Dialog</a></li><li><a href="#3">Example Table</a></li><li><a href="#6">Proving a Table</a></li></ul></div><h2>Creating a new table<a name="1"></a></h2><p>To create a new table block locate the Tabular Expression block in the simulink library.</p><p><img vspace="5" hspace="5" src="walk1.png" alt=""> </p><p>Drag the Tabular Expression block to a new or existing model.</p><p><img vspace="5" hspace="5" src="walk2.png" alt=""> </p><h2>Table Tool Dialog<a name="2"></a></h2><p>To edit the functionality of the table double click on the block to bring up the Table Tool dialog. From this dialog you can create the layout for the table and edit the conditions and outputs for the function.</p><p><img vspace="5" hspace="5" src="walk3.png" alt=""> </p><h2>Example Table<a name="3"></a></h2><p>An example of a 2-dimensional table is shown below</p><p><img vspace="5" hspace="5" src="walk4.png" alt=""> </p><p>This table specifies a function with 3 inputs x, y, and z, and one output. Saving the table will generate the following embedded matlab code:</p><pre class="codeinput"><span class="keyword">function</span> output  = demo_table(x,y,z)

</pre><pre class="codeinput"><span class="comment">%%#eml</span>

<span class="keyword">if</span>(x&gt;0)

  <span class="keyword">if</span>(y&gt;1)

    <span class="keyword">if</span>(z&gt;1)

      output = 1;

    <span class="keyword">elseif</span>(z&lt;=1)

      output = 5;

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

  <span class="keyword">elseif</span>(y&lt;=1)

    <span class="keyword">if</span>(z&gt;1)

      output = 2;

    <span class="keyword">elseif</span>(z&lt;=1)

      output = 6;

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

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

<span class="keyword">elseif</span>(x==0)

  <span class="keyword">if</span>(z&gt;1)

    output = 3;

  <span class="keyword">elseif</span>(z&lt;=1)

    output = 7;

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

<span class="keyword">elseif</span>(x&lt;0)

  <span class="keyword">if</span>(z&gt;1)

    output = 4;

  <span class="keyword">elseif</span>(z&lt;=1)

    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>

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

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

%% Product Overview

% m-file. Tabular Expressions can be proved to be disjoint and complete

% using the PVS theorem prover. This allows users to ensure that the table

% they are designing has covered all possible inputs and is deterministic.

%

%% Creating a new table

% To create a new table block locate the Tabular Expression block in the

% simulink library.

%

% <<walk1.png>>

%

% Drag the Tabular Expression block to a new or existing model.

%

% <<walk2.png>>

%

%% Table Tool Dialog

% To edit the functionality of the table double click on the block to bring

% up the Table Tool dialog. From this dialog you can create the layout for

% the table and edit the conditions and outputs for the function.

%

% <<walk3.png>>

%

%% Example Table

% An example of a 2-dimensional table is shown below

%

% <<walk4.png>>

%

% This table specifies a function with 3 inputs x, y, and z, and one

% output. Saving the table will generate the following embedded matlab

% code:

function output  = demo_table(x,y,z)

%%#eml

if(x>0)

  if(y>1)

    if(z>1)

      output = 1;

    elseif(z<=1)

      output = 5;

    end

  elseif(y<=1)

    if(z>1)

      output = 2;

    elseif(z<=1)

      output = 6;

    end

  end

elseif(x==0)

  if(z>1)

    output = 3;

  elseif(z<=1)

    output = 7;

  end

elseif(x<0)

  if(z>1)

    output = 4;

  elseif(z<=1)

    output = 8;

  end

end

%%

% 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.

%

% <<walk5.png>>

%

%% Proving a Table

%

% Let us assume that a table designer has specified the following function

% table:

%

% <<walk6.png>>

% 

% In order for a tabular expression to be considered "proper" it must

% satisfy a *Completness* and *Disjointness* condition

%

% * Completness means that in the specification of a function we have

% considered all possible inputs in a condition cell.

% * 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.

%

% 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.

%%

% 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:

%

% <<walk7.png>>

%

% 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.

%

% <<walk8.png>>

%

% 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.

%

% <<walk9.png>>

% 

% 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.

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

--></body></html>

 No newline at end of file