Skip to content
%% Regenerate documentation
% This file regenerates documentation in the current directory. It only
% works on files starting with 'TT_', and does not recurse. It also
% doesn't evaluate code.
files = dir
c = 0
for i = 1:length(files)
if files(i).isdir == 0 && strcmp(files(i).name(1:3), 'TT_')
files(i).name
publish(files(i).name, struct('evalCode', false))
end
end
\ No newline at end of file
......@@ -3,7 +3,7 @@
<toc version="2.0">
<!-- First tocitem specifies top level in Help browser Contents pane -->
<!-- This can be a roadmap page, as shown below, or a content page -->
<tocitem target="html/TT_help.html">MyToolbox Toolbox
<tocitem target="html/TT_help.html">Tabular Expression Toolbox
<!-- Nest tocitems to create hierarchical entries in Contents-->
<!-- To include icons, use the following syntax for tocitems: -->
<!-- <tocitem target="foo.html" image="HelpIcon.NAME"> -->
......@@ -15,7 +15,7 @@
<!-- matlabroot/toolbox/matlab/icons -->
<!-- A Getting Started Guide usually comes first -->
<tocitem target="html/TT_gs_top.html" image="HelpIcon.GETTING_STARTED">
Getting Started with the MyToolbox Toolbox
Getting Started with the Tabular Expression Toolbox
<tocitem target="html/TT_gs_req.html">System Requirements
</tocitem>
<tocitem target="html/TT_gs_over.html">Product Overview
......@@ -39,9 +39,9 @@
<!-- First item is page describing function categories, if any -->
<!-- Optional link or links to your or other Web sites -->
<tocitem target="http://www.mathworks.com"
<tocitem target="http://www.cas.mcmaster.ca/~lawford/TET"
image="$toolbox/matlab/icons/webicon.gif">
MyToolbox Web Site (Example only: goes to mathworks.com)
Tabular Expression Toolbox Web Site
</tocitem>
</tocitem>
......
......@@ -3,7 +3,7 @@
<toc version="2.0">
<!-- First tocitem specifies top level in Help browser Contents pane -->
<!-- This can be a roadmap page, as shown below, or a content page -->
<tocitem target="mytoolbox_product_page.html">MyToolbox Toolbox
<tocitem target="mytoolbox_product_page.html">Tabular Expression Toolbox
<!-- Nest tocitems to create hierarchical entries in Contents-->
<!-- To include icons, use the following syntax for tocitems: -->
<!-- <tocitem target="foo.html" image="HelpIcon.NAME"> -->
......@@ -36,9 +36,9 @@
<!-- First item is page describing function categories, if any -->
<!-- Optional link or links to your or other Web sites -->
<tocitem target="http://www.mathworks.com"
<tocitem target="http://www.cas.mcmaster.ca/~lawford/TET"
image="$toolbox/matlab/icons/webicon.gif">
MyToolbox Web Site (Example only: goes to mathworks.com)
Tabular Expression Toolbox Web Site
</tocitem>
</tocitem>
......
......@@ -4,63 +4,66 @@
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
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-09-01"><meta name="m-file" content="TT_gs_over"><style type="text/css">
body {
background-color: white;
margin:10px;
}
h1 {
color: #990000;
font-size: x-large;
}
h2 {
color: #990000;
font-size: medium;
}
/* Make the text shrink to fit narrow windows, but not stretch too far in
wide windows. */
p,h1,h2,div.content div {
max-width: 600px;
/* Hack for IE6 */
width: auto !important; width: 600px;
}
pre.codeinput {
background: #EEEEEE;
padding: 10px;
}
@media print {
pre.codeinput {word-wrap:break-word; width:100%;}
}
span.keyword {color: #0000FF}
span.comment {color: #228B22}
span.string {color: #A020F0}
span.untermstring {color: #B20000}
span.syscmd {color: #B28C00}
pre.codeoutput {
color: #666666;
padding: 10px;
}
pre.error {
color: red;
}
p.footer {
text-align: right;
font-size: xx-small;
font-weight: lighter;
font-style: italic;
color: gray;
}
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Product Overview</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_gs_over.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</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>
......@@ -91,8 +94,7 @@ p.footer {
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, 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><!--
</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 Typecheck 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_p1.png" alt=""> </p><p><img vspace="5" hspace="5" src="walk8_p2.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_p1.png" alt=""> </p><p><img vspace="5" hspace="5" src="walk9_p2.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><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Product Overview
% This product allows users to interactively design a tabular expression.
......@@ -187,7 +189,7 @@ end
%%
% 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
% satisfied. Clicking on the Typecheck button will start the proof and popup a
% process dialog as shown below:
%
% <<walk7.png>>
......@@ -195,7 +197,9 @@ end
% 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>>
% <<walk8_p1.png>>
%
% <<walk8_p2.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.
......@@ -208,7 +212,9 @@ end
% false for the counter example indicating to the table designer that they
% failed to consider a case of the input.
%
% <<walk9.png>>
% <<walk9_p1.png>>
%
% <<walk9_p2.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
......
......@@ -4,86 +4,91 @@
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML is auto-generated from an M-file.
To make changes, update the M-file and republish this document.
--><title>Tabular Expressions References</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-09-02"><meta name="m-file" content="TT_gs_ref"><style type="text/css">
body {
background-color: white;
margin:10px;
}
h1 {
color: #990000;
font-size: x-large;
}
h2 {
color: #990000;
font-size: medium;
}
/* Make the text shrink to fit narrow windows, but not stretch too far in
wide windows. */
p,h1,h2,div.content div {
max-width: 600px;
/* Hack for IE6 */
width: auto !important; width: 600px;
}
pre.codeinput {
background: #EEEEEE;
padding: 10px;
}
@media print {
pre.codeinput {word-wrap:break-word; width:100%;}
}
span.keyword {color: #0000FF}
span.comment {color: #228B22}
span.string {color: #A020F0}
span.untermstring {color: #B20000}
span.syscmd {color: #B28C00}
pre.codeoutput {
color: #666666;
padding: 10px;
}
pre.error {
color: red;
}
p.footer {
text-align: right;
font-size: xx-small;
font-weight: lighter;
font-style: italic;
color: gray;
}
</style></head><body><div class="content"><h1>Tabular Expressions References</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Background Information</a></li><li><a href="#2">Tabular Expressions in Industry</a></li></ul></div><h2>Background Information<a name="1"></a></h2><p>Tabular Expressions have been around for many years, below are some papers discussing some of the fundamentals behind tabular expressions.</p><div><ul><li>Y.&nbsp;Jin and D.&nbsp;L. Parnas, "Defining the meaning of tabular mathematical expressions," Science of Computer Programming, vol.&nbsp;In Press, Corrected Proof, 2010.</li><li>Parnas, D.L., "Tabular Representation of Relations", CRL Report 260, McMaster University, Communications Research Laboratory, TRIO (Telecommunications Research Institute of Ontario), October 1992, 17 pgs.</li><li>R.&nbsp;Janicki, D.&nbsp;L. Parnas, and J.&nbsp;Zucker, "Tabular representations in relational documents," in in Relational Methods in Computer Science, pp.&nbsp;184-196, Springer Verlag, 1996.</li></ul></div><h2>Tabular Expressions in Industry<a name="2"></a></h2><p>Tabular Expressions have been used in numerous industrial projects, below are some papers describing some of such projects.</p><div><ul><li>A.&nbsp;Wassyng and M.&nbsp;Lawford, "Lessons learned from a successful implementation of formal methods in an industrial project," in FME 2003: International Symposium of Formal Methods Europe Proceedings (K.&nbsp;Araki, S.&nbsp;Gnesi, and D.&nbsp;Mandrioli, eds.), vol.&nbsp;2805 of Lecture Notes in Computer Science, pp.&nbsp;133-153, Springer-Verlag, Aug. 2003.</li><li>R.&nbsp;L. Baber, D.&nbsp;L. Parnas, S.&nbsp;A. Vilkomir, P.&nbsp;Harrison, and T.&nbsp;O'Connor, "Disciplined methods of software specification: A case study," in ITCC '05: Proceedings of the International Conference on Information Technology: Coding and Computing (ITCC'05) - Volume II, (Washington, DC, USA), pp.&nbsp;428-437, IEEE Computer Society, 2005.</li></ul></div><p class="footer"><br>
Published with MATLAB&reg; 7.10<br></p></div><!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Tabular Expressions References</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_gs_ref.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>Tabular Expressions References</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Tabular Expression Toolbox Publications</a></li><li><a href="#2">Background Information</a></li><li><a href="#3">Tabular Expressions in Industry</a></li></ul></div><h2>Tabular Expression Toolbox Publications<a name="1"></a></h2><div><ul><li>C. Eles and M. Lawford, "A tabular expression toolbox for Matlab/Simulink," NASA Formal Methods, LNCS Vol. 6617, pp. 494-499, Springer, 2011.</li></ul></div><h2>Background Information<a name="2"></a></h2><p>Tabular Expressions have been around for many years, below are some papers discussing some of the fundamentals behind tabular expressions.</p><div><ul><li>Y. Jin and D. L. Parnas, "Defining the meaning of tabular mathematical expressions," Science of Computer Programming, Vol. 75, no. 11, pp. 980-1000, 2010.</li><li>Parnas, D.L., "Tabular Representation of Relations", CRL Report 260, McMaster University, Communications Research Laboratory, TRIO (Telecommunications Research Institute of Ontario), October 1992, 17 pgs.</li><li>R. Janicki, D.L. Parnas, and J. Zucker, "Tabular representations in relational documents," in in Relational Methods in Computer Science, pp. 184-196, Springer Verlag, 1996.</li></ul></div><h2>Tabular Expressions in Industry<a name="3"></a></h2><p>Tabular Expressions have been used in numerous industrial projects, below are some papers describing some of such projects.</p><div><ul><li>A. Wassyng and M. Lawford, "Lessons learned from a successful implementation of formal methods in an industrial project," in FME 2003: International Symposium of Formal Methods Europe Proceedings (K. Araki, S. Gnesi, and D. Mandrioli, eds.), vol. 2805 of Lecture Notes in Computer Science, pp. 133-153, Springer-Verlag, Aug. 2003.</li><li>R. L. Baber, D. L. Parnas, S. A. Vilkomir, P. Harrison, and T. O'Connor, "Disciplined methods of software specification: A case study," in ITCC '05: Proceedings of the International Conference on Information Technology: Coding and Computing (ITCC'05) - Volume II, (Washington, DC, USA), pp. 428-437, IEEE Computer Society, 2005.</li></ul></div><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Tabular Expressions References
%% Tabular Expression Toolbox Publications
% * C. Eles and M. Lawford, "A tabular expression toolbox for Matlab/Simulink," NASA Formal Methods, LNCS Vol. 6617, pp. 494-499, Springer, 2011.
%% Background Information
% Tabular Expressions have been around for many years, below are some
% papers discussing some of the fundamentals behind tabular expressions.
%
% * Y. Jin and D. L. Parnas, "Defining the meaning of tabular mathematical
% expressions," Science of Computer Programming, vol. In Press, Corrected Proof, 2010.
% * Y. Jin and D. L. Parnas, "Defining the meaning of tabular mathematical
% expressions," Science of Computer Programming, Vol. 75, no. 11, pp. 980-1000, 2010.
% * Parnas, D.L., "Tabular Representation of Relations", CRL Report 260,
% McMaster University, Communications Research Laboratory, TRIO
% (Telecommunications Research Institute of Ontario), October 1992, 17 pgs.
% * R. Janicki, D. L. Parnas, and J. Zucker, "Tabular representations in
% relational documents," in in Relational Methods in Computer Science, pp. 184-196, Springer Verlag, 1996.
% * R. Janicki, D.L. Parnas, and J. Zucker, "Tabular representations in
% relational documents," in in Relational Methods in Computer Science, pp. 184-196, Springer Verlag, 1996.
%% Tabular Expressions in Industry
% Tabular Expressions have been used in numerous industrial projects, below
% are some papers describing some of such projects.
%
% * A. Wassyng and M. Lawford, "Lessons learned from a successful
% implementation of formal methods in an industrial project," in FME 2003: International Symposium of Formal Methods Europe Proceedings (K. Araki, S. Gnesi, and D. Mandrioli, eds.), vol. 2805 of Lecture Notes in Computer Science, pp. 133-153, Springer-Verlag, Aug. 2003.
% * R. L. Baber, D. L. Parnas, S. A. Vilkomir, P. Harrison, and
% T. O'Connor, "Disciplined methods of software specification: A case study," in ITCC '05: Proceedings of the International Conference on Information Technology: Coding and Computing (ITCC'05) - Volume II, (Washington, DC, USA), pp. 428-437, IEEE Computer Society, 2005.
% * A. Wassyng and M. Lawford, "Lessons learned from a successful
% implementation of formal methods in an industrial project," in FME 2003: International Symposium of Formal Methods Europe Proceedings (K. Araki, S. Gnesi, and D. Mandrioli, eds.), vol. 2805 of Lecture Notes in Computer Science, pp. 133-153, Springer-Verlag, Aug. 2003.
% * R. L. Baber, D. L. Parnas, S. A. Vilkomir, P. Harrison, and
% T. O'Connor, "Disciplined methods of software specification: A case study," in ITCC '05: Proceedings of the International Conference on Information Technology: Coding and Computing (ITCC'05) - Volume II, (Washington, DC, USA), pp. 428-437, IEEE Computer Society, 2005.
##### SOURCE END #####
--></body></html>
\ No newline at end of file
......@@ -4,79 +4,97 @@
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML is auto-generated from an M-file.
To make changes, update the M-file and republish this document.
--><title>System Requirements</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-08-30"><meta name="m-file" content="TT_gs_req"><style type="text/css">
body {
background-color: white;
margin:10px;
}
h1 {
color: #990000;
font-size: x-large;
}
h2 {
color: #990000;
font-size: medium;
}
/* Make the text shrink to fit narrow windows, but not stretch too far in
wide windows. */
p,h1,h2,div.content div {
max-width: 600px;
/* Hack for IE6 */
width: auto !important; width: 600px;
}
pre.codeinput {
background: #EEEEEE;
padding: 10px;
}
@media print {
pre.codeinput {word-wrap:break-word; width:100%;}
}
span.keyword {color: #0000FF}
span.comment {color: #228B22}
span.string {color: #A020F0}
span.untermstring {color: #B20000}
span.syscmd {color: #B28C00}
pre.codeoutput {
color: #666666;
padding: 10px;
}
pre.error {
color: red;
}
p.footer {
text-align: right;
font-size: xx-small;
font-weight: lighter;
font-style: italic;
color: gray;
}
</style></head><body><div class="content"><h1>System Requirements</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Matlab/Simulink</a></li><li><a href="#2">PVS (Prototype Verification System)</a></li></ul></div><h2>Matlab/Simulink<a name="1"></a></h2><div><ul><li>Tested with Matlab Simulink 2009b and 2010a</li></ul></div><h2>PVS (Prototype Verification System)<a name="2"></a></h2><div><ul><li>PVS is required to be installed in order to check for completness and disjointness of tables.</li><li>PVS is downloadable from <a href="http://pvs.csl.sri.com/">http://pvs.csl.sri.com/</a></li><li>System has been tested on PVS versions 4.2 and 4.1</li><li>Ensure that pvs executable is on shell path</li><li><b>Note:</b> PVS is a linux and OS X application and will not run natively on Windows.</li></ul></div><p class="footer"><br>
Published with MATLAB&reg; 7.10<br></p></div><!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>System Requirements</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_gs_req.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>System Requirements</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Matlab/Simulink</a></li><li><a href="#2">Table Checking</a></li><li><a href="#3">CVC3</a></li><li><a href="#4">PVS (Prototype Verification System)</a></li></ul></div><h2>Matlab/Simulink<a name="1"></a></h2><div><ul><li>Tested with Matlab Simulink 2011b, 2011a, 2010a, 2009b</li></ul></div><h2>Table Checking<a name="2"></a></h2><div><ul><li>The tool supports checking of table completness and disjointness through the support of external tools</li><li>This tool will work with either or both of the tools installed.</li><li>It is recommened that both tools be installed, as they are built on different technologies, and have different strengths and weaknesses.</li></ul></div><h2>CVC3<a name="3"></a></h2><div><ul><li>CVC3 is supported for checking for completness and disjointness of tables</li><li>CVC3 can be downloaded from <a href="http://cs.nyu.edu/acsys/cvc3/">http://cs.nyu.edu/acsys/cvc3/</a></li><li>Ensure that cvc3 is executable on the shell path.</li><li>CVC3 is available for Linux/OS X and Windows.</li></ul></div><h2>PVS (Prototype Verification System)<a name="4"></a></h2><div><ul><li>PVS is supported for checking for completness and disjointness of tables.</li><li>PVS is downloadable from <a href="http://pvs.csl.sri.com/">http://pvs.csl.sri.com/</a></li><li>System has been tested on PVS versions 5.0, 4.2 and 4.1</li><li>Ensure that pvs executable is on shell path</li><li><b>Note:</b> PVS is a Linux and MacOS X application and will not run natively on Windows.</li></ul></div><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% System Requirements
%
%% Matlab/Simulink
%
% * Tested with Matlab Simulink 2009b and 2010a
% * Tested with Matlab Simulink 2011b, 2011a, 2010a, 2009b
%
%% Table Checking
% * The tool supports checking of table completness and disjointness
% through the support of external tools
% * This tool will work with either or both of the tools installed.
% * It is recommened that both tools be installed, as they are built on
% different technologies, and have different strengths and weaknesses.
%
%% CVC3
% * CVC3 is supported for checking for completness and disjointness of
% tables
% * CVC3 can be downloaded from http://cs.nyu.edu/acsys/cvc3/
% * Ensure that cvc3 is executable on the shell path.
% * CVC3 is available for Linux/OS X and Windows.
%
%% PVS (Prototype Verification System)
% * PVS is required to be installed in order to check for completness and
% * PVS is supported for checking for completness and
% disjointness of tables.
% * PVS is downloadable from http://pvs.csl.sri.com/
% * System has been tested on PVS versions 4.2 and 4.1
% * System has been tested on PVS versions 5.0, 4.2 and 4.1
% * Ensure that pvs executable is on shell path
% * *Note:* PVS is a linux and OS X application and will not run natively
% * *Note:* PVS is a Linux and MacOS X application and will not run natively
% on Windows.
##### SOURCE END #####
--></body></html>
\ No newline at end of file
......@@ -4,72 +4,74 @@
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML is auto-generated from an M-file.
To make changes, update the M-file and republish this document.
--><title>Getting Started</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-08-30"><meta name="m-file" content="TT_gs_top"><style type="text/css">
body {
background-color: white;
margin:10px;
}
h1 {
color: #990000;
font-size: x-large;
}
h2 {
color: #990000;
font-size: medium;
}
/* Make the text shrink to fit narrow windows, but not stretch too far in
wide windows. */
p,h1,h2,div.content div {
max-width: 600px;
/* Hack for IE6 */
width: auto !important; width: 600px;
}
pre.codeinput {
background: #EEEEEE;
padding: 10px;
}
@media print {
pre.codeinput {word-wrap:break-word; width:100%;}
}
span.keyword {color: #0000FF}
span.comment {color: #228B22}
span.string {color: #A020F0}
span.untermstring {color: #B20000}
span.syscmd {color: #B28C00}
pre.codeoutput {
color: #666666;
padding: 10px;
}
pre.error {
color: red;
}
p.footer {
text-align: right;
font-size: xx-small;
font-weight: lighter;
font-style: italic;
color: gray;
}
</style></head><body><div class="content"><h1>Getting Started</h1><div><ul><li><a href="TT_gs_req.html">Requirements</a></li><li><a href="TT_gs_ref.html">Tabular Expresssion References</a></li><li><a href="TT_gs_over.html">Product Overview</a></li></ul></div><p class="footer"><br>
Published with MATLAB&reg; 7.10<br></p></div><!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Getting Started</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_gs_top.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>Getting Started</h1><div><ul><li><a href="TT_gs_req.html">Requirements</a></li><li><a href="TT_gs_over.html">Product Overview</a></li><li><a href="TT_gs_ref.html">Tabular Expresssion References</a></li></ul></div><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Getting Started
%
% * <TT_gs_req.html Requirements>
% * <TT_gs_ref.html Tabular Expresssion References>
% * <TT_gs_over.html Product Overview>
% * <TT_gs_ref.html Tabular Expresssion References>
%
##### SOURCE END #####
......
......@@ -4,73 +4,77 @@
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML is auto-generated from an M-file.
To make changes, update the M-file and republish this document.
--><title>Table Toolbox</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-09-17"><meta name="m-file" content="TT_help"><style type="text/css">
body {
background-color: white;
margin:10px;
}
h1 {
color: #990000;
font-size: x-large;
}
h2 {
color: #990000;
font-size: medium;
}
/* Make the text shrink to fit narrow windows, but not stretch too far in
wide windows. */
p,h1,h2,div.content div {
max-width: 600px;
/* Hack for IE6 */
width: auto !important; width: 600px;
}
pre.codeinput {
background: #EEEEEE;
padding: 10px;
}
@media print {
pre.codeinput {word-wrap:break-word; width:100%;}
}
span.keyword {color: #0000FF}
span.comment {color: #228B22}
span.string {color: #A020F0}
span.untermstring {color: #B20000}
span.syscmd {color: #B28C00}
pre.codeoutput {
color: #666666;
padding: 10px;
}
pre.error {
color: red;
}
p.footer {
text-align: right;
font-size: xx-small;
font-weight: lighter;
font-style: italic;
color: gray;
}
</style></head><body><div class="content"><h1>Table Toolbox</h1><p><b>Available Documentation</b></p><div><ul><li><a href="TT_gs_top.html">Getting Started</a></li></ul></div><p class="footer"><br>
Published with MATLAB&reg; 7.10<br></p></div><!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Tabular Expression Toolbox</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_help.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>Tabular Expression Toolbox</h1><p><b>Available Documentation</b></p><div><ul><li><a href="TT_gs_top.html">Getting Started</a></li><li><a href="TT_ug.html">User Guide</a></li></ul></div><p>Copyright 2010 Colin Eles</p><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Table Toolbox
%% Tabular Expression Toolbox
%
% *Available Documentation*
%
% * <TT_gs_top.html Getting Started>
% * <TT_ug.html User Guide>
%
% Copyright 2010 Colin Eles
##### SOURCE END #####
--></body></html>
\ No newline at end of file
......@@ -4,70 +4,77 @@
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML is auto-generated from an M-file.
To make changes, update the M-file and republish this document.
--><title>User Guide</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-09-13"><meta name="m-file" content="TT_ug"><style type="text/css">
body {
background-color: white;
margin:10px;
}
h1 {
color: #990000;
font-size: x-large;
}
h2 {
color: #990000;
font-size: medium;
}
/* Make the text shrink to fit narrow windows, but not stretch too far in
wide windows. */
p,h1,h2,div.content div {
max-width: 600px;
/* Hack for IE6 */
width: auto !important; width: 600px;
}
pre.codeinput {
background: #EEEEEE;
padding: 10px;
}
@media print {
pre.codeinput {word-wrap:break-word; width:100%;}
}
span.keyword {color: #0000FF}
span.comment {color: #228B22}
span.string {color: #A020F0}
span.untermstring {color: #B20000}
span.syscmd {color: #B28C00}
pre.codeoutput {
color: #666666;
padding: 10px;
}
pre.error {
color: red;
}
p.footer {
text-align: right;
font-size: xx-small;
font-weight: lighter;
font-style: italic;
color: gray;
}
</style></head><body><div class="content"><h1>User Guide</h1><div><ul><li><a href="TT_ug_opening.html">Creating a new Table</a></li><li><a href="TT_ug_editing.html">Editing a Tabular Expression</a></li></ul></div><p class="footer"><br>
Published with MATLAB&reg; 7.10<br></p></div><!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>User Guide</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_ug.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>User Guide</h1><div><ul><li><a href="TT_ug_opening.html">Creating a new Table</a></li><li><a href="TT_ug_editing.html">Editing a Table</a></li><li><a href="TT_ug_checking.html">Typechecking a Table</a></li><li><a href="TT_ug_floating.html">Floating Point Numbers</a></li><li><a href="TT_ug_saving.html">Saving a Table</a></li></ul></div><p>Copyright 2010 Colin Eles</p><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% User Guide
%
% * <TT_ug_opening.html Creating a new Table>
% * <TT_ug_editing.html Editing a Tabular Expression>
% * <TT_ug_editing.html Editing a Table>
% * <TT_ug_checking.html Typechecking a Table>
% * <TT_ug_floating.html Floating Point Numbers>
% * <TT_ug_saving.html Saving a Table>
%
% Copyright 2010 Colin Eles
##### SOURCE END #####
--></body></html>
\ No newline at end of file
<!DOCTYPE html
PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Tabular Expressions</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_ug_background.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>Tabular Expressions</h1><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Tabular Expressions
%
%
##### SOURCE END #####
--></body></html>
\ No newline at end of file
<!DOCTYPE html
PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Typechecking a Table</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_ug_checking.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>Typechecking a Table</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Overview</a></li><li><a href="#2">Syntax Check</a></li><li><a href="#3">CVC3</a></li><li><a href="#4">PVS</a></li><li><a href="#5">PVS or CVC3</a></li><li><a href="#6">Typechecking Report</a></li></ul></div><h2>Overview<a name="1"></a></h2><p>Of of the main features of tabular expressions is the facilitation of the inspection of completeness and disjointness conditions. This tool has support for external tools to automate this process. Currently two tools based on different ideas and technologies are supported. In order to typecheck a table at least one of these tools must be installed on the system, see the <a href="TT_gs_req.html">System Requirements</a> in the <a href="TT_gs_top.html">Getting Started Guide</a>.</p><p>It is recommended that both systems be installed as they have different advantages and disadvantages, additionally with both installed a single point of failure for typechecking the table is avoided.</p><p>The default typechecker is CVC3 as it is easier to install and available for more platforms. however this can be changed from the typecheck menu, see screenshot below.</p><p><img vspace="5" hspace="5" src="ug_check_1.png" alt=""> </p><p>Both tools will appear to operate the same way to the user; the details of how the tools run and their interfaces are hidden from the user of the table tool. If a table is valid the user will be notified with a message box as seen below. if the table is not valid a typechecking report will be generated see below for more details.</p><p><img vspace="5" hspace="5" src="ug_check_3.png" alt=""> </p><h2>Syntax Check<a name="2"></a></h2><p>Pressing the "Syntax" button or selecting "Syntax Check" from the Typecheck menu will perform a syntactic check on the table. The syntactic check will look at the inputs, conditions, and outputs to ensure that all variables are defined and all expressions are proper Matlab syntax. The syntax check will highlight the problem cells in red as seen in the example below. Condition cells must evaluate to a value that can be interpreted as a boolean value.</p><p><img vspace="5" hspace="5" src="ug_check_10.png" alt=""> </p><p>In this example the reason there is a syntax error is because the variable declared in the inputs field is x1 whereas the variable being used in the conditions is x. To fix this error one could either change the inputs field to be x or the each x in the table to be x1.</p><h2>CVC3<a name="3"></a></h2><p>CVC3 is the third iteration of a SMT solver developed at NYU.</p><p><b>CVC3 Typecheck</b></p><p>Typecheck the current table using CVC3, will perform a syntax check prior to running the typecheck operation.</p><p><b>Generate CVC File</b></p><p>Generate a CVC file with the required proof obligations. Calling the typecheck function will also do this, but this function will not attempt to prove the file.</p><h2>PVS<a name="4"></a></h2><p>PVS is a general purpose theorem prover developed by SRI.</p><p><b>PVS Typecehck</b></p><p>Typecheck the current table using PVS, will perform a syntax check prior to running the typecheck operation.</p><p><b>PVS Settings</b></p><p>A few settings for running the pvs commands can be adjusted using the pvs settings window. See the screenshot below.</p><p><img vspace="5" hspace="5" src="ug_check_2.png" alt=""> </p><div><ul><li><b>Imports:</b> Allows to specify one or more pvs files to import, can be used if other functions or types are referenced.</li><li><b>Test Count:</b> Used to adjust the number of attempts when generating a counterexample to an unproven theorem. Increasing this will increase the chances of finding a counterexample but will also increase the time taken to find a counterexample.</li><li><b>Test Range:</b> Used to adjust the range of possible counterexamples tested. the range of numbers to test will be in the range (-size..size). for example if your theorem is only false for the value 500 then you would require a range value &gt;= 500 in order to find the counterexample.</li></ul></div><p><b>PVS Check Status</b></p><p>Check if the current file has already been typechecked, used when a table was manually proven in pvs rather than being automatically proven using the tool. If the tool fails to generate a counterexample it is possible that the theorem is true but the automatic PVS proof strategies were not sufficient to prove the table, in this case it may be neccessary to prove the table manually using the pvs interface. This command allows you to read the state of the proof into the table tool.</p><p><b>PVS Generate File</b></p><p>Generate a pvs file representing the table. Calling the typecheck function will also do this, but this function will not attempt to prove the file.</p><p><b>PVS Typecheck SimTypes</b></p><p>Typechecking the table with regards to the Simulink types will ignore any typing information in the inputs or function name fields. typng information will be taken from the simulink diagram, so any port datatypes specified in the ports and data manager window will be used. inorder to determine any inherited types the tool will compile the simulink diagram. Therefore any errors in the diagram (alegbraic loops, etc.) will need to be resolved before being able to use this mode of typechecking.</p><h2>PVS or CVC3<a name="5"></a></h2><p>PVS and CVC3 are based on 2 different technologies, which means that they will have different advantages and disadvantages.</p><p>CVC3 will generally be much faster than PVS, and is usually better at finding a counterexample, however it is not as robust as PVS and if any expressions involve nonlinear mathematics the tool may not perform as expected. As CVC3 is an SMT solver, proving something is an all or nothing operation either the query is valid, invalid, or unknown; there is no way to manually guide or direct the proof in anyway.</p><p>PVS is a very general purpose theorem prover, it is very powerful, and as such has a larger overhead than CVC3, as a result it takes longer to run a proof on PVS. PVS's tactics for generating counterexamples is not very sophisticated so it is not always the case that it will find one; it generally takes a substantial amount of time to run a check for counterexamples. PVS has a robust proof engine that allows for users to manually guide a proof through its completion. When typechecking a table using PVS, PVS may not be able to prove the theorems correct, if a counterexample is not found it may mean that the default proof strategy was not sufficient rather than it being false. In this case the tool allows you to go into pvs to attempt to manually prove the table, this will require knowledge of the pvs proof engine and language, we recomend you find more information here <a href="http://pvs.csl.sri.com">&lt;http://pvs.csl.sri.com</a>&gt;</p><p>For these reasons, to get the full power the tool it is recomended that both PVS and CVC3 be installed. Typechecking with both tools eliminates a single point of failure in the typechecking step, and provides greater assurance to the designer that the table is correct.</p><h2>Typechecking Report<a name="6"></a></h2><p>If a table fails to be proven valid a typechecking report will be generated. The report serves a number of functions it shows the user what the unproven sequent (logical statement) was, the report will display a counter example should one be generated. The report will highlight in the table the state of cells for the generated counterexamples, this makes it very easy to see where the error was made.</p><p>Below is the report for a CVC3 typecheck then for a PVS typecheck.</p><p><img vspace="5" hspace="5" src="ug_check_4.png" alt=""> </p><p><img vspace="5" hspace="5" src="ug_check_5.png" alt=""> </p><p>There is a minor difference between the CVC3 and the PVS report. The PVS report has a button called "Open" this will open the current theory in PVS allowing for the user to attempt to prove the theorems.</p><p>If more than one sequent is unproveable, the "next" button will be enabled, this allows the user to view the other unprovable sequents and possible counterexamples.</p><p>When viewing a sequent that has a counterexample the report will highlight on the table window the state of the conditions.</p><div><ul><li>A <b>Red</b> colour indicates that the given cell has evaulated to <b>False</b> for the current counterexample.</li><li>A <b>Green</b> colour indicates that the given cell has evaulated to <b>True</b> for the current counterexample.</li></ul></div><p>Ideally you want one and only one green cell in each grid. Some examples follow:</p><p><b>Non-disjoint tables</b></p><p><img vspace="5" hspace="5" src="ug_check_7.png" alt=""> </p><p><img vspace="5" hspace="5" src="ug_check_8.png" alt=""> </p><p><b>Incomplete tables</b></p><p><img vspace="5" hspace="5" src="ug_check_6.png" alt=""> </p><p><img vspace="5" hspace="5" src="ug_check_9.png" alt=""> </p><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Typechecking a Table
%% Overview
%
% Of of the main features of tabular expressions is the facilitation of the
% inspection of completeness and disjointness conditions. This tool has
% support for external tools to automate this process. Currently two
% tools based on different ideas and technologies are supported.
% In order to typecheck a table at least one of these tools must be
% installed on the system, see the <TT_gs_req.html System Requirements> in the <TT_gs_top.html Getting
% Started Guide>.
%
% It is recommended that both systems be installed as they have different
% advantages and disadvantages, additionally with both installed a single
% point of failure for typechecking the table is avoided.
%
% The default typechecker is CVC3 as it is easier to install and available
% for more platforms. however this can be changed from the typecheck
% menu, see screenshot below.
%
% <<ug_check_1.png>>
%
% Both tools will appear to operate the same way to the user; the details of how the tools run and
% their interfaces are hidden from the user of the table tool. If a table
% is valid the user will be notified with a message box as seen below. if
% the table is not valid a typechecking report will be generated see below
% for more details.
%
% <<ug_check_3.png>>
%
%% Syntax Check
%
% Pressing the "Syntax" button or selecting "Syntax Check" from the
% Typecheck menu will perform a syntactic check on the table. The syntactic
% check will look at the inputs, conditions, and outputs to ensure that all
% variables are defined and all expressions are proper Matlab syntax. The syntax check will
% highlight the problem cells in red as seen in the example below.
% Condition cells must evaluate to a value that can be interpreted as a
% boolean value.
%
% <<ug_check_10.png>>
%
% In this example the reason there is a syntax error is because the
% variable declared in the inputs field is x1 whereas the variable being
% used in the conditions is x. To fix this error one could either change
% the inputs field to be x or the each x in the table to be x1.
%
%% CVC3
% CVC3 is the third iteration of a SMT solver developed at NYU.
%
% *CVC3 Typecheck*
%
% Typecheck the current table using CVC3, will perform a syntax check
% prior to running the typecheck operation.
%
% *Generate CVC File*
%
% Generate a CVC file with the required proof obligations. Calling the typecheck
% function will also do this, but this function will not attempt to prove
% the file.
%
%% PVS
% PVS is a general purpose theorem prover developed by SRI.
%
% *PVS Typecehck*
%
% Typecheck the current table using PVS, will perform a syntax check
% prior to running the typecheck operation.
%
% *PVS Settings*
%
% A few settings for running the pvs commands can be adjusted using the pvs
% settings window. See the screenshot below.
%
% <<ug_check_2.png>>
%
% * *Imports:* Allows to specify one or more pvs files to import, can be
% used if other functions or types are referenced.
% * *Test Count:* Used to adjust the number of attempts when generating a counterexample
% to an unproven theorem. Increasing this will increase the chances of
% finding a counterexample but will also increase the time taken to find a
% counterexample.
% * *Test Range:* Used to adjust the range of possible counterexamples
% tested. the range of numbers to test will be in the range (-size..size).
% for example if your theorem is only false for the value 500 then you
% would require a range value >= 500 in order to find the counterexample.
%
% *PVS Check Status*
%
% Check if the current file has already been typechecked, used when a
% table was manually proven in pvs rather than being
% automatically proven using the tool. If the tool fails to generate a
% counterexample it is possible that the theorem is true but the automatic
% PVS proof strategies were not sufficient to prove the table, in this case it may be
% neccessary to prove the table manually using the pvs interface. This
% command allows you to read the state of the proof into the table tool.
%
% *PVS Generate File*
%
% Generate a pvs file representing the table. Calling the typecheck
% function will also do this, but this function will not attempt to prove
% the file.
%
% *PVS Typecheck SimTypes*
%
% Typechecking the table with regards to the Simulink types will ignore any
% typing information in the inputs or function name fields. typng
% information will be taken from the simulink diagram, so any port
% datatypes specified in the ports and data manager window will be used.
% inorder to determine any inherited types the tool will compile the
% simulink diagram. Therefore any errors in the diagram (alegbraic loops,
% etc.) will need to be resolved before being able to use this mode of
% typechecking.
%
%% PVS or CVC3
% PVS and CVC3 are based on 2 different technologies, which means that they
% will have different advantages and disadvantages.
%
% CVC3 will generally be much faster than PVS, and is usually better at finding a counterexample,
% however it is not as robust as PVS and if any expressions involve
% nonlinear mathematics the tool may not perform as expected. As CVC3 is an
% SMT solver, proving something is an all or nothing operation either the
% query is valid, invalid, or unknown; there is no way to manually guide or
% direct the proof in anyway.
%
% PVS is a very general purpose theorem prover, it is very powerful, and as
% such has a larger overhead than CVC3, as a result it takes longer to run
% a proof on PVS. PVS's tactics for generating counterexamples is not very
% sophisticated so it is not always the case that it will find one; it
% generally takes a substantial amount of time to run a check for
% counterexamples. PVS has a robust proof engine that allows for users to
% manually guide a proof through its completion. When typechecking a table
% using PVS, PVS may not be able to prove the theorems correct, if a
% counterexample is not found it may mean that the default proof strategy
% was not sufficient rather than it being false. In this case the tool allows you to go into pvs to
% attempt to manually prove the table, this will require knowledge of the
% pvs proof engine and language, we recomend you find more information here
% <http://pvs.csl.sri.com http://pvs.csl.sri.com>
%
% For these reasons, to get the full power the tool it is recomended that
% both PVS and CVC3 be installed. Typechecking with both tools eliminates
% a single point of failure in the typechecking step, and provides greater
% assurance to the designer that the table is correct.
%
%% Typechecking Report
%
% If a table fails to be proven valid a typechecking report will be
% generated. The report serves a number of functions it shows the user what
% the unproven sequent (logical statement) was, the report will display a counter
% example should one be generated. The report will highlight in the
% table the state of cells for the generated
% counterexamples, this makes it very easy to see where the error was made.
%
% Below is the report for a CVC3 typecheck then for a PVS typecheck.
%
% <<ug_check_4.png>>
%
% <<ug_check_5.png>>
%
% There is a minor difference between the CVC3 and the PVS report. The PVS
% report has a button called "Open" this will open the current theory in
% PVS allowing for the user to attempt to prove the theorems.
%
% If more than one sequent is unproveable, the "next" button will be
% enabled, this allows the user to view the other unprovable sequents and
% possible counterexamples.
%
% When viewing a sequent that has a counterexample the report will
% highlight on the table window the state of the conditions.
%
% * A *Red* colour indicates that the given cell has evaulated to *False*
% for the current counterexample.
% * A *Green* colour indicates that the given cell has evaulated to *True*
% for the current counterexample.
%
% Ideally you want one and only one green cell in each grid. Some examples follow:
%
% *Non-disjoint tables*
%
% <<ug_check_7.png>>
%
% <<ug_check_8.png>>
%
% *Incomplete tables*
%
% <<ug_check_6.png>>
%
% <<ug_check_9.png>>
%
%
##### SOURCE END #####
--></body></html>
\ No newline at end of file
......@@ -4,72 +4,74 @@
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML is auto-generated from an M-file.
To make changes, update the M-file and republish this document.
--><title>Editing a Tabular Expression</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-10-07"><meta name="m-file" content="TT_ug_editing"><style type="text/css">
body {
background-color: white;
margin:10px;
}
h1 {
color: #990000;
font-size: x-large;
}
h2 {
color: #990000;
font-size: medium;
}
/* Make the text shrink to fit narrow windows, but not stretch too far in
wide windows. */
p,h1,h2,div.content div {
max-width: 600px;
/* Hack for IE6 */
width: auto !important; width: 600px;
}
pre.codeinput {
background: #EEEEEE;
padding: 10px;
}
@media print {
pre.codeinput {word-wrap:break-word; width:100%;}
}
span.keyword {color: #0000FF}
span.comment {color: #228B22}
span.string {color: #A020F0}
span.untermstring {color: #B20000}
span.syscmd {color: #B28C00}
pre.codeoutput {
color: #666666;
padding: 10px;
}
pre.error {
color: red;
}
p.footer {
text-align: right;
font-size: xx-small;
font-weight: lighter;
font-style: italic;
color: gray;
}
</style></head><body><div class="content"><h1>Editing a Tabular Expression</h1><!--introduction--><p>The Tabular Expression Dialog allows users to graphically layout a tabular expression, for which conditions and outputs can be filled in using the embedded matlab subset of the Matlab languauge.</p><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Layout</a></li><li><a href="#2">Inputs</a></li><li><a href="#3">Expression Name</a></li><li><a href="#4">Conditions</a></li><li><a href="#5">Outputs</a></li></ul></div><h2>Layout<a name="1"></a></h2><p>The Dialog interface allows for the creation of 1-Dimensional vertical and horizontal tables, as well as 2-Dimensional tables. The tool supports multiple outputs for 1-Dimensional vertical tables.</p><p>The figure below shows an example 2-Dimensional Table with the Vertical Conditions, Horizontal Conditions, and Outputs notated.</p><p><img vspace="5" hspace="5" src="ug_layout_2.png" alt=""> </p><p>The "new" button will create an additional condition box for a particular grid. The "delete" button will remove the last condition box in a grid. For each condition in the vertical conditions, a subgrid can be created. To create a subgrid for a condition click on the "+" button next to the intended box.</p><p>Whenever the configuration of the vertical and horizontal conditions is changed the corresponding output boxes will update as well.</p><h2>Inputs<a name="2"></a></h2><h2>Expression Name<a name="3"></a></h2><h2>Conditions<a name="4"></a></h2><p>Text input for a condition box must be valid embedded matlab code. Expressions in condition boxes will be evaulated with the assumed type of boolean. Since embedded matlab is not typechecked this is a pottential cause of errors. By running pvs on a table, each expression in a condition box will be checked that it is of type boolean.</p><p>For a table with multiple outputs, the horizontal condition boxes represent different outputs. In the example below, the table has 2 different outputs labeled, out1 and out2. The syntax of the output specification is the same as for the inputs; this allows for outputs to have different types.</p><p><img vspace="5" hspace="5" src="ug_layout_3.png" alt=""> </p><h2>Outputs<a name="5"></a></h2><p class="footer"><br>
Published with MATLAB&reg; 7.10<br></p></div><!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Editing a Tabular Expression</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_ug_editing.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>Editing a Tabular Expression</h1><!--introduction--><p>The Table Tool allows users to graphically layout a tabular expression, for which conditions and outputs can be specified using the embedded Matlab subset of the Matlab language.</p><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Layout</a></li><li><a href="#2">Inputs</a></li><li><a href="#3">Expression Name</a></li><li><a href="#4">Conditions</a></li><li><a href="#5">Outputs</a></li><li><a href="#6">Ports</a></li><li><a href="#7">Edit Mode</a></li></ul></div><h2>Layout<a name="1"></a></h2><p>The Dialog interface allows for the creation of 1-Dimensional vertical and horizontal tables, as well as 2-Dimensional tables. The tool supports multiple outputs for 1-Dimensional vertical tables.</p><p>The figure below shows an example 2-Dimensional Table with the Vertical Conditions, Horizontal Conditions, and Outputs notated.</p><p><img vspace="5" hspace="5" src="ug_layout_2.png" alt=""> </p><p>The "new" button will create an additional condition box for a particular grid. The "delete" button will remove the last condition box in a grid. For each condition in the vertical conditions, a subgrid can be created. To create a subgrid for a condition click on the "+" button next to the intended box.</p><p>Whenever the configuration of the vertical and horizontal conditions is changed the corresponding output boxes will update as well.</p><h2>Inputs<a name="2"></a></h2><p>The input box labeled "Inputs" allows for the specification of inputs to the table. There is no limit in the number of inputs supported. Inputs are specified in a comma delimited list. names of inputs must conform to the Matlab syntax conventions.</p><p><b>Typing</b></p><p>Typing information can be specified for each input declared. This allows for users to declare inputs as dependent types. The format for typing follows that of PVS, some examples:</p><div><ul><li><tt>x, y, z</tt> - 3 inputs with the default type</li><li><tt>x, y:bool</tt> - 2 inputs, y with specified type, x has the default type.</li><li><tt>x:real, y:real, z:bool</tt> - 2 inputs of type real and one of type bool</li><li><tt>x:real, y:{t:real|t&gt;x}</tt> - 2 inputs of type real, y is dependent on x, and is restricted to those value strictly greater than x</li></ul></div><h2>Expression Name<a name="3"></a></h2><p>the expression name will be the name identifying the block, it will also be the function name for generated Matlab code.</p><p><b>Typing</b></p><p>For single output tables, typing information for the output type of the function can be specified in this textbox. formatting for the typing is the same as that for inputs.</p><h2>Conditions<a name="4"></a></h2><p>Text input for a condition box must be valid embedded Matlab code. Expressions in condition boxes will be evaluated with the assumed type of boolean. Since embedded Matlab is not typechecked this is a potential cause of errors. By running a syntax check on a table, each expression in a condition box will be checked that it is of type boolean.</p><p>For a table with multiple outputs, the horizontal condition boxes represent different outputs, more detail about this in the following section.</p><h2>Outputs<a name="5"></a></h2><p>The outputs of the function are specified in the outputs grid. Outputs must be an expression that will evaluate to a definite value. Each output specified should be the same type, however since Matlab is not strongly typed, almost every possible value will be interpreted as a compatible type. The tool supports 2 output modes: single output and multiple output.</p><p>The output mode can be specified from the edit menu as seen in the following figure:</p><p><img vspace="5" hspace="5" src="ug_layout_4.png" alt=""> </p><p><b>Single Output</b></p><p>For a single output table, the vertical grid can be used for another dimension of conditions. Each output cell shall be a single expression which will evaluate to the output under the interpreted conditions.</p><p><b>Multiple Output</b></p><p>For a table with multiple outputs, the horizontal condition grid is used to specify the outputs of the table. The same rules for typing apply as noted in the inputs and expression section of this document.</p><p>Each cell in the condition grid specifies the name (and type) of an output. See the following figure for an example. Each cell in the output grid specifies an output that corresponds to the output specified in the horizontal grid above it.</p><p>In the example below the table has 2 different outputs labeled, output1 and output2; the outputs have different types. Multiple outputs facilitates robust function specification.</p><p><img vspace="5" hspace="5" src="ug_layout_5.png" alt=""> </p><h2>Ports<a name="6"></a></h2><p>The "Ports" button will bring up the ports and data manager window (see next figure.) From here you can specify the datatypes of signals, as well as any other functionality as you would with another Simulink block.</p><p><img vspace="5" hspace="5" src="ug_layout_6.png" alt=""> </p><h2>Edit Mode<a name="7"></a></h2><p>The edit button is a toggle button which allows for the user to hide the editing buttons which include the new row, delete row, new subgrid, etc. buttons. Hiding these buttons allows for cleaner looking table with fewer distractions allowing the user to concentrate on the content in the table. see an example below.</p><p><img vspace="5" hspace="5" src="ug_layout_7.png" alt=""> </p><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Editing a Tabular Expression
%
% The Tabular Expression Dialog allows users to graphically layout a
% tabular expression, for which conditions and outputs can be filled in
% using the embedded matlab subset of the Matlab languauge.
% The Table Tool allows users to graphically layout a
% tabular expression, for which conditions and outputs can be specified
% using the embedded Matlab subset of the Matlab language.
%% Layout
% The Dialog interface allows for the creation of 1-Dimensional vertical
% and horizontal tables, as well as 2-Dimensional tables. The tool supports
......@@ -89,23 +91,96 @@ p.footer {
% Whenever the configuration of the vertical and horizontal conditions
% is changed the corresponding output boxes will update as well.
%% Inputs
% The input box labeled "Inputs" allows for the specification of inputs to
% the table. There is no limit in the number of inputs supported. Inputs
% are specified in a comma delimited list. names of inputs must conform to
% the Matlab syntax conventions.
%
% *Typing*
%
% Typing information can be specified for each input declared. This allows
% for users to declare inputs as dependent types. The format for typing follows that of
% PVS, some examples:
%
% * |x, y, z| - 3 inputs with the default type
% * |x, y:bool| - 2 inputs, y with specified type, x has the default
% type.
% * |x:real, y:real, z:bool| - 2 inputs of type real and one of type bool
% * |x:real, y:{t:real|t>x}| - 2 inputs of type real, y is dependent on x,
% and is restricted to those value strictly greater than x
%
%% Expression Name
% the expression name will be the name identifying the block, it will also
% be the function name for generated Matlab code.
%
% *Typing*
%
% For single output tables, typing information for the output type of the
% function can be specified in this textbox. formatting for the typing is
% the same as that for inputs.
%
%% Conditions
% Text input for a condition box must be valid embedded matlab code.
% Expressions in condition boxes will be evaulated with the assumed type of
% boolean. Since embedded matlab is not typechecked this is a pottential
% cause of errors. By running pvs on a table, each expression in a
% Text input for a condition box must be valid embedded Matlab code.
% Expressions in condition boxes will be evaluated with the assumed type of
% boolean. Since embedded Matlab is not typechecked this is a potential
% cause of errors. By running a syntax check on a table, each expression in a
% condition box will be checked that it is of type boolean.
%
% For a table with multiple outputs, the horizontal condition boxes
% represent different outputs. In the example below, the table has 2
% different outputs labeled, out1 and out2. The syntax of the output specification
% is the same as for the inputs; this allows for outputs to have
% different types.
%
% <<ug_layout_3.png>>
% represent different outputs, more detail about this in the following
% section.
%
%% Outputs
% The outputs of the function are specified in the outputs grid. Outputs must be an expression that
% will evaluate to a definite value. Each output specified should be the same type, however since
% Matlab is not strongly typed, almost every possible value will be interpreted as a compatible type.
% The tool supports 2 output modes: single output and multiple output.
%
% The output mode can be specified from the edit menu as seen in the
% following figure:
%
% <<ug_layout_4.png>>
%
% *Single Output*
%
% For a single output table, the vertical grid can be used for another
% dimension of conditions. Each output cell shall be a single expression
% which will evaluate to the output under the interpreted conditions.
%
% *Multiple Output*
%
% For a table with multiple outputs, the horizontal condition grid is used
% to specify the outputs of the table. The same rules for typing apply as noted in the
% inputs and expression section of this document.
%
% Each cell in the condition grid
% specifies the name (and type) of an output. See the following figure for
% an example. Each cell in the output grid specifies an output that
% corresponds to the output specified in the horizontal grid above it.
%
% In the example below
% the table has 2
% different outputs labeled, output1 and output2; the outputs have
% different types. Multiple outputs facilitates robust function specification.
%
% <<ug_layout_5.png>>
%
%% Ports
%
% The "Ports" button will bring up the ports and data manager window (see
% next figure.) From here you can specify the datatypes of signals, as well
% as any other functionality as you would with another Simulink block.
%
% <<ug_layout_6.png>>
%
%% Edit Mode
%
% The edit button is a toggle button which allows for the user to hide the
% editing buttons which include the new row, delete row, new subgrid, etc.
% buttons. Hiding these buttons allows for cleaner looking table with fewer
% distractions allowing the user to concentrate on the content in the
% table. see an example below.
%
% <<ug_layout_7.png>>
##### SOURCE END #####
--></body></html>
\ No newline at end of file
<!DOCTYPE html
PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Working with floating point numbers</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_ug_floating.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>Working with floating point numbers</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Floating point numbers</a></li><li><a href="#2">Proving tables with floating point numbers</a></li></ul></div><h2>Floating point numbers<a name="1"></a></h2><p>One of the limitations with computers is the way that we have to represent real numbers. In a theoretical sense the real numbers has infinite range and infinite precision, however when we want to represent these numbers in a machine using the standard numerical representation for a variety of reasons we lose these properties.</p><p>Matlab and most computers use the IEEE 754 floating point standard. The standard defines the way real numbers can be represented from the bit level including the results of operations, and exceptions.</p><p>A full discussion of the standard is beyond the scope of this document we refer the interested reader to <a href="http://www.mathworks.com/help/techdoc/matlab_prog/f2-12135.html">Matlab's documentation</a> as well as the <a href="http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4610935&amp;tag=1">standard documentation</a></p><h2>Proving tables with floating point numbers<a name="2"></a></h2><p>The toolbox has support for proving tables with floating point inputs. Currently only PVS is supported for this feature, and in general manual intervention with the prover will likely be required.</p><p>Several new types are provided which can be used as anyother type in the input and output fields.</p><div><ul><li>single - a finite or infinite single precision number</li><li>single_finite - a finite single precision number</li><li>double - a finite or infinite double precision number</li><li>double_finite - a finite double precision number</li></ul></div><p>A sample input string might be "x:double_finite, y:double_finite". The same rules for subtyping still apply, as it may be necessary to subtype inputs in order to get them to typecheck properly.</p><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Working with floating point numbers
%
%% Floating point numbers
% One of the limitations with computers is the way that we have to
% represent real numbers. In a theoretical sense the real numbers has
% infinite range and infinite precision, however when we want to represent
% these numbers in a machine using the standard numerical representation
% for a variety of reasons we
% lose these properties.
%
% Matlab and most computers use the IEEE 754 floating point standard. The
% standard defines the way real numbers can be represented from the bit
% level including the results of operations, and exceptions.
%
% A full discussion of the standard is beyond the scope of this document we
% refer the interested reader to <http://www.mathworks.com/help/techdoc/matlab_prog/f2-12135.html Matlab's documentation> as well as the
% <http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4610935&tag=1
% standard documentation>
%
%% Proving tables with floating point numbers
%
% The toolbox has support for proving tables with floating point inputs.
% Currently only PVS is supported for this feature, and in general manual
% intervention with the prover will likely be required.
%
% Several new types are provided which can be used as anyother type in the input and output fields.
%
%
% * single - a finite or infinite single precision number
% * single_finite - a finite single precision number
% * double - a finite or infinite double precision number
% * double_finite - a finite double precision number
%
% A sample input string might be "x:double_finite, y:double_finite". The
% same rules for subtyping still apply, as it may be necessary to subtype
% inputs in order to get them to typecheck properly.
%
##### SOURCE END #####
--></body></html>
\ No newline at end of file
......@@ -4,66 +4,68 @@
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML is auto-generated from an M-file.
To make changes, update the M-file and republish this document.
--><title>Creating a new Tabular Expression</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-09-13"><meta name="m-file" content="TT_ug_opening"><style type="text/css">
body {
background-color: white;
margin:10px;
}
h1 {
color: #990000;
font-size: x-large;
}
h2 {
color: #990000;
font-size: medium;
}
/* Make the text shrink to fit narrow windows, but not stretch too far in
wide windows. */
p,h1,h2,div.content div {
max-width: 600px;
/* Hack for IE6 */
width: auto !important; width: 600px;
}
pre.codeinput {
background: #EEEEEE;
padding: 10px;
}
@media print {
pre.codeinput {word-wrap:break-word; width:100%;}
}
span.keyword {color: #0000FF}
span.comment {color: #228B22}
span.string {color: #A020F0}
span.untermstring {color: #B20000}
span.syscmd {color: #B28C00}
pre.codeoutput {
color: #666666;
padding: 10px;
}
pre.error {
color: red;
}
p.footer {
text-align: right;
font-size: xx-small;
font-weight: lighter;
font-style: italic;
color: gray;
}
</style></head><body><div class="content"><h1>Creating a new Tabular Expression</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Matlab</a></li><li><a href="#2">Simulink</a></li></ul></div><h2>Matlab<a name="1"></a></h2><p>The table tool can be opened up from the Matlab environment, this allows users to create a table and generate an m-file function representing the tabular expression in the table.</p><p>To open up the Table Tool dialog click Start-&gt;Toolbox-&gt;Table Toolbox-&gt;Table Tool</p><h2>Simulink<a name="2"></a></h2><p>To create a table block in the Simulink environement, open up the block library. Select the Table Toolbox Library. From the Table Toolbox Library you should see A block Called Tabular Expression, Drag this block to a new or existing model to add a Tabular Expression. Double Click on the block in the model to bring up the Tabular Expression Dialog.</p><p class="footer"><br>
Published with MATLAB&reg; 7.10<br></p></div><!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Creating a new Tabular Expression</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_ug_opening.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>Creating a new Tabular Expression</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Matlab</a></li><li><a href="#2">Simulink</a></li></ul></div><h2>Matlab<a name="1"></a></h2><p>The table tool can be opened up from the Matlab environment, this allows users to create a table and generate an m-file function representing the tabular expression in the table.</p><p>To open up the Table Tool dialog click Start-&gt;Toolbox-&gt;Table Toolbox-&gt;Table Tool</p><h2>Simulink<a name="2"></a></h2><p>To create a table block in the Simulink environement, open up the block library. Select the Tabular Expression Toolbox Library. From the Table Toolbox Library you should see A block Called Tabular Expression, Drag this block to a new or existing model to add a Tabular Expression. Double Click on the block in the model to bring up the Tabular Expression Dialog.</p><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Creating a new Tabular Expression
%
......@@ -76,8 +78,9 @@ p.footer {
% To open up the Table Tool dialog click Start->Toolbox->Table
% Toolbox->Table Tool
%% Simulink
%
% To create a table block in the Simulink environement, open up the block
% library. Select the Table Toolbox Library. From the Table Toolbox Library
% library. Select the Tabular Expression Toolbox Library. From the Table Toolbox Library
% you should see A block Called Tabular Expression, Drag this block to a
% new or existing model to add a Tabular Expression. Double Click on the
% block in the model to bring up the Tabular Expression Dialog.
......
<!DOCTYPE html
PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>Saving a Table</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_ug_saving.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><h1>Saving a Table</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Saving to Block</a></li><li><a href="#2">Saving to an M-File</a></li></ul></div><h2>Saving to Block<a name="1"></a></h2><p>Saving to a block will either save to an existing simulink block or create a new simulink block for the current table. Saving to a block is the default save option so if the "Save" button is pressed it will perform this action.</p><p>If changes are made in the table interface they will not be updated in the underlying generated code in the simulink block until saving is performed, it is important to remember to save before closing the interface.</p><h2>Saving to an M-File<a name="2"></a></h2><p>The Tabular Expression Toolbox allows for users to save their table as an m-function. This allows the function to be called from Matlab scripts or functions; users can also run the function from the command line as a quick way of testing functionality.</p><p>To save a table to an m-file select the "save to m-file" command from the file menu as seen in the following screen shot.</p><p><img vspace="5" hspace="5" src="ug_save_1.png" alt=""> </p><p>The toolbox will create a file with the name expression_name.m, where expression_name is the name of your expression. The function can then be called as you would any other function in Matlab, ie. expression_name(arg1,arg2,...)</p><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
%% Saving a Table
%
%% Saving to Block
%
% Saving to a block will either save to an existing simulink block or
% create a new simulink block for the current table. Saving to a block is
% the default save option so if the "Save" button is pressed it will
% perform this action.
%
% If changes are made in the table interface they will not be updated in the
% underlying generated code in
% the simulink block until saving is performed, it is important to remember
% to save before closing the interface.
%
%% Saving to an M-File
%
% The Tabular Expression Toolbox allows for users to save their table as an m-function.
% This allows the function to be called from Matlab scripts or functions;
% users can also run the function from the command line as a quick way of
% testing functionality.
%
% To save a table to an m-file select the "save to m-file" command from the
% file menu as seen in the following screen shot.
%
% <<ug_save_1.png>>
%
% The toolbox will create a file with the name expression_name.m, where
% expression_name is the name of your expression. The function can then be
% called as you would any other function in Matlab, ie.
% expression_name(arg1,arg2,...)
##### SOURCE END #####
--></body></html>
\ No newline at end of file
<!DOCTYPE html
PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<!--
This HTML was auto-generated from MATLAB code.
To make changes, update the MATLAB code and republish this document.
--><title>TT_ug_settings</title><meta name="generator" content="MATLAB 8.1"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2013-07-05"><meta name="DC.source" content="TT_ug_settings.m"><style type="text/css">
html,body,div,span,applet,object,iframe,h1,h2,h3,h4,h5,h6,p,blockquote,pre,a,abbr,acronym,address,big,cite,code,del,dfn,em,font,img,ins,kbd,q,s,samp,small,strike,strong,sub,sup,tt,var,b,u,i,center,dl,dt,dd,ol,ul,li,fieldset,form,label,legend,table,caption,tbody,tfoot,thead,tr,th,td{margin:0;padding:0;border:0;outline:0;font-size:100%;vertical-align:baseline;background:transparent}body{line-height:1}ol,ul{list-style:none}blockquote,q{quotes:none}blockquote:before,blockquote:after,q:before,q:after{content:'';content:none}:focus{outine:0}ins{text-decoration:none}del{text-decoration:line-through}table{border-collapse:collapse;border-spacing:0}
html { min-height:100%; margin-bottom:1px; }
html body { height:100%; margin:0px; font-family:Arial, Helvetica, sans-serif; font-size:10px; color:#000; line-height:140%; background:#fff none; overflow-y:scroll; }
html body td { vertical-align:top; text-align:left; }
h1 { padding:0px; margin:0px 0px 25px; font-family:Arial, Helvetica, sans-serif; font-size:1.5em; color:#d55000; line-height:100%; font-weight:normal; }
h2 { padding:0px; margin:0px 0px 8px; font-family:Arial, Helvetica, sans-serif; font-size:1.2em; color:#000; font-weight:bold; line-height:140%; border-bottom:1px solid #d6d4d4; display:block; }
h3 { padding:0px; margin:0px 0px 5px; font-family:Arial, Helvetica, sans-serif; font-size:1.1em; color:#000; font-weight:bold; line-height:140%; }
a { color:#005fce; text-decoration:none; }
a:hover { color:#005fce; text-decoration:underline; }
a:visited { color:#004aa0; text-decoration:none; }
p { padding:0px; margin:0px 0px 20px; }
img { padding:0px; margin:0px 0px 20px; border:none; }
p img, pre img, tt img, li img { margin-bottom:0px; }
ul { padding:0px; margin:0px 0px 20px 23px; list-style:square; }
ul li { padding:0px; margin:0px 0px 7px 0px; }
ul li ul { padding:5px 0px 0px; margin:0px 0px 7px 23px; }
ul li ol li { list-style:decimal; }
ol { padding:0px; margin:0px 0px 20px 0px; list-style:decimal; }
ol li { padding:0px; margin:0px 0px 7px 23px; list-style-type:decimal; }
ol li ol { padding:5px 0px 0px; margin:0px 0px 7px 0px; }
ol li ol li { list-style-type:lower-alpha; }
ol li ul { padding-top:7px; }
ol li ul li { list-style:square; }
.content { font-size:1.2em; line-height:140%; padding: 20px; }
pre, tt, code { font-size:12px; }
pre { margin:0px 0px 20px; }
pre.error { color:red; }
pre.codeinput { padding:10px; border:1px solid #d3d3d3; background:#f7f7f7; }
pre.codeoutput { padding:10px 11px; margin:0px 0px 20px; color:#4c4c4c; }
@media print { pre.codeinput, pre.codeoutput { word-wrap:break-word; width:100%; } }
span.keyword { color:#0000FF }
span.comment { color:#228B22 }
span.string { color:#A020F0 }
span.untermstring { color:#B20000 }
span.syscmd { color:#B28C00 }
.footer { width:auto; padding:10px 0px; margin:25px 0px 0px; border-top:1px dotted #878787; font-size:0.8em; line-height:140%; font-style:italic; color:#878787; text-align:left; float:none; }
.footer p { margin:0px; }
.footer a { color:#878787; }
.footer a:hover { color:#878787; text-decoration:underline; }
.footer a:visited { color:#878787; }
table th { padding:7px 5px; text-align:left; vertical-align:middle; border: 1px solid #d6d4d4; font-weight:bold; }
table td { padding:7px 5px; text-align:left; vertical-align:top; border:1px solid #d6d4d4; }
</style></head><body><div class="content"><p class="footer"><br><a href="http://www.mathworks.com/products/matlab/">Published with MATLAB&reg; R2013a</a><br></p></div><!--
##### SOURCE BEGIN #####
##### SOURCE END #####
--></body></html>
\ No newline at end of file