editing help files

%% Typechecking a Table

%% Overview

%

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

% 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 System Requirements in the Getting

% Started Guide.

% installed on the system, see the <TT_gs_req.html System Requirements> in the <TT_gs_top.html Getting

% Started Guide>.

%

% It is recommened that both systems be installed as they have different

% advantages and disadvantages, additionaly with both installed a single

% 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

%

% <<ug_check_1.png>>

%

% Both tools will appear to opperate the same way to the user. If a table

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

%

%% Syntax Check

%

% Pressing the "Syntax" button or seleting "Syntax Check" from the

% 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 are proper matlab syntax. The syntax check will

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

% 

% 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 is the third iteration of a SMT solver developed at NYU.

%

% * CVC3 Typecheck

% *CVC3 Typecheck*

% 

% Typecheck the current table using CVC3, will call the syntax check

%   first.

% Typecheck the current table using CVC3, will perform a syntax check

%   prior to running the typecheck operation.

%

% * Generate CVC File

% *Generate CVC File*

%

% generate a CVC file with the required proof obligations. Calling the typecheck

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

%

% typecheck the current table using pvs, will call the syntax check

%   first.

% 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

% A few settings for running the pvs commands can be adjusted using the pvs

% settings window. See the screenshot below.

%

% <<ug_check_2.png>>

% finding a counterexample but will also increase the time taken to find a

% counterexample.

% * *Test Range:* Used to adjust the range of possible counterexamples

% found. the range of numbers to test will be in the range (-size..size). 

% 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 has had to be manually proven in pvs rather than being

% 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

% strategies were not sufficient to prove the table, in this case it may be

% neccessary to prove the table manually using the pvs interface.

% 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

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

% 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. In this case the tool allows you to go into pvs to

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

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

%

% 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

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

%

% Ideally you want one and only one green cell in each grid. Some examples follow:

%

% non-disjoint tables

% *Non-disjoint tables*

%

% <<ug_check_7.png>>

%

% <<ug_check_8.png>>

%

% incomplete tables

% *Incomplete tables*

% 

% <<ug_check_6.png>>

%