Regenerate the docs and include an easy to use script. (5b38c971) · Commits · Abdulrahman elgendy / tet

html/generation_doc.m

0 → 100644

+8 −0

Original line number	Diff line number	Diff line
		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

html/html/TT_gs_over.html

+59 −61

Original line number	Diff line number	Diff line
		@@ -6,38 +6,45 @@
		<!--
		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 7.12"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2011-08-23"><meta name="DC.source" content="TT_gs_over.m"><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%;}
		}
		--><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 }
		@@ -45,22 +52,18 @@ span.string {color: #A020F0}
		span.untermstring { color:#B20000 }
		span.syscmd { color:#B28C00 }

		pre.codeoutput {
		color: #666666;
		padding: 10px;
		}
		.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; }



		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>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,12 +94,7 @@ p.footer {
		output = 8;
		<span class="keyword">end</span>
		<span class="keyword">end</span>
		</pre><pre class="codeoutput">Input argument "x" is undefined.

		Error in ==> TT_gs_over at 35
		if(x>0)
		</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>
		Published with MATLAB® 7.12<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® R2013a</a><br></p></div><!--
		##### SOURCE BEGIN #####
		%% Product Overview
		% This product allows users to interactively design a tabular expression.

html/html/TT_gs_ref.html

+60 −58

Original line number	Diff line number	Diff line
		@@ -6,38 +6,45 @@
		<!--
		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 7.12"><link rel="schema.DC" href="http://purl.org/dc/elements/1.1/"><meta name="DC.date" content="2011-08-23"><meta name="DC.source" content="TT_gs_ref.m"><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%;}
		}
		--><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 }
		@@ -45,25 +52,20 @@ 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">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>
		Published with MATLAB® 7.12<br></p></div><!--
		.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® R2013a</a><br></p></div><!--
		##### SOURCE BEGIN #####
		%% Tabular Expressions References
		%% Tabular Expression Toolbox Publications

html/html/TT_gs_req.html

+60 −58

File changed.

Preview size limit exceeded, changes collapsed.

html/html/TT_gs_top.html

+60 −58

File changed.

Preview size limit exceeded, changes collapsed.