latest update to help files (0c1d4058) · Commits · Abdulrahman elgendy / tet

html/TT_help.m

+1 −0

Original line number	Diff line number	Diff line
		@@ -3,5 +3,6 @@
		% Available Documentation
		%
		% * <TT_gs_top.html Getting Started>
		% * <TT_ug.html User Guide>
		%
		% Copyright 2010 Colin Eles

html/TT_ug_checking.m

+52 −0

Original line number	Diff line number	Diff line
		@@ -26,11 +26,34 @@
		%
		% <<ug_check_3.png>>
		%
		%% Syntax Check
		%
		% Pressing the "Syntax" button or seleting "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 are proper matlab syntax. The syntax check will
		% highlight the problem cells in red as seen in the example below.
		%
		% <<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 where as 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 deveoped at NYU.
		%
		% * CVC3 Typecheck
		%
		% Typecheck the current table using CVC3, will call the syntax check
		% first.
		%
		% * 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.
		@@ -84,6 +107,35 @@
		% 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 also
		% 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. 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
		%

html/html/TT_help.html

+4 −2

Original line number	Diff line number	Diff line
		@@ -6,7 +6,7 @@
		<!--
		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">
		--><title>Table Toolbox</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-11-26"><meta name="m-file" content="TT_help"><style type="text/css">

		body {
		background-color: white;
		@@ -62,7 +62,7 @@ p.footer {
		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>
		</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><li><a href="TT_ug.html">User Guide</a></li></ul></div><p>Copyright 2010 Colin Eles</p><p class="footer"><br>
		Published with MATLAB® 7.10<br></p></div><!--
		##### SOURCE BEGIN #####
		%% Table Toolbox
		@@ -70,7 +70,9 @@ p.footer {
		% 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

html/html/TT_ug_checking.html

+53 −1

Original line number	Diff line number	Diff line
		@@ -62,7 +62,7 @@ p.footer {
		color: gray;
		}

		</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">CVC3</a></li><li><a href="#3">PVS</a></li><li><a href="#4">Typechecking Report</a></li></ul></div><h2>Overview<a name="1"></a></h2><p>The main feature of tabular expressions is the facilitation of the inspection of completness and disjointness conditions. This tool has support for external tools to automate this process. currerntly two different tools based on seperate 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 System Requirements in the Getting Started Guide.</p><p>It is recommened that both systems be installed as they have different advantages and disadvantages, additionaly 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 opperate the same way to the user. 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>CVC3<a name="2"></a></h2><p>CVC3 is the third iteration of a SMT solver deveoped at NYU.</p><h2>PVS<a name="3"></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 call the syntax check first.</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 counter example.</li><li><b>Test Range:</b> Used to adjust the range of possible counterexamples found. 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 counter example.</li></ul></div><p><b>PVS Check Status</b></p><p>Check if the current file has already been typechecked, used when a table has had to be manually proven in pvs rather than being automatically proven using the tool. If the tool fails to generate a counter example it is possible that the theorem is true but the automatic strategies were not sufficient to prove the table, in this case it may be neccessary to prove the table manually using the pvs interface.</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>Typechecking Report<a name="4"></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, it will also display a counter example should one be generated. The report will also highlight on the table the cells which are either true or false for the given 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>non-disjoint tables</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>incomplete tables</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>
		</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>The main feature of tabular expressions is the facilitation of the inspection of completness and disjointness conditions. This tool has support for external tools to automate this process. currerntly two different tools based on seperate 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 System Requirements in the Getting Started Guide.</p><p>It is recommened that both systems be installed as they have different advantages and disadvantages, additionaly 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 opperate the same way to the user. 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 seleting "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 are proper matlab syntax. The syntax check will highlight the problem cells in red as seen in the example below.</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 where as 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 deveoped at NYU.</p><div><ul><li>CVC3 Typecheck</li></ul></div><p>Typecheck the current table using CVC3, will call the syntax check first.</p><div><ul><li>Generate CVC File</li></ul></div><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 call the syntax check first.</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 counter example.</li><li><b>Test Range:</b> Used to adjust the range of possible counterexamples found. 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 counter example.</li></ul></div><p><b>PVS Check Status</b></p><p>Check if the current file has already been typechecked, used when a table has had to be manually proven in pvs rather than being automatically proven using the tool. If the tool fails to generate a counter example it is possible that the theorem is true but the automatic strategies were not sufficient to prove the table, in this case it may be neccessary to prove the table manually using the pvs interface.</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 also 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. 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/"><http://pvs.csl.sri.com/</a>></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, it will also display a counter example should one be generated. The report will also highlight on the table the cells which are either true or false for the given 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>non-disjoint tables</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>incomplete tables</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>
		Published with MATLAB® 7.10<br></p></div><!--
		##### SOURCE BEGIN #####
		%% Typechecking a Table
		@@ -93,11 +93,34 @@ p.footer {
		%
		% <<ug_check_3.png>>
		%
		%% Syntax Check
		%
		% Pressing the "Syntax" button or seleting "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 are proper matlab syntax. The syntax check will
		% highlight the problem cells in red as seen in the example below.
		%
		% <<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 where as 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 deveoped at NYU.
		%
		% * CVC3 Typecheck
		%
		% Typecheck the current table using CVC3, will call the syntax check
		% first.
		%
		% * 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.
		@@ -151,6 +174,35 @@ p.footer {
		% 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 also
		% 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. 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
		%

html/html/ug_check_10.png

0 → 100644

+50 KiB

Loading image diff...