From 0c1d40586ffb4588ca2befd983dd7f790a0ac31e Mon Sep 17 00:00:00 2001 From: Colin Eles Date: Fri, 26 Nov 2010 20:49:16 +0000 Subject: [PATCH] latest update to help files git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6594 57e6efec-57d4-0310-aeb1-a6c144bb1a8b --- html/TT_help.m | 1 + html/TT_ug_checking.m | 52 ++++++++++++++++++++++++++++++++ html/html/TT_help.html | 6 ++-- html/html/TT_ug_checking.html | 54 +++++++++++++++++++++++++++++++++- html/html/ug_check_10.png | Bin 0 -> 51221 bytes html/html/ug_layout_6.png | Bin 0 -> 105765 bytes html/html/ug_layout_7.png | Bin 0 -> 60220 bytes 7 files changed, 110 insertions(+), 3 deletions(-) create mode 100644 html/html/ug_check_10.png create mode 100644 html/html/ug_layout_6.png create mode 100644 html/html/ug_layout_7.png diff --git a/html/TT_help.m b/html/TT_help.m index 51ef8dd..2bc6354 100644 --- a/html/TT_help.m +++ b/html/TT_help.m @@ -3,5 +3,6 @@ % *Available Documentation* % % * +% * % % Copyright 2010 Colin Eles diff --git a/html/TT_ug_checking.m b/html/TT_ug_checking.m index a573bfd..893e377 100644 --- a/html/TT_ug_checking.m +++ b/html/TT_ug_checking.m @@ -26,11 +26,34 @@ % % <> % +%% 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. +% +% <> +% +% 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 +% +% +% 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 % diff --git a/html/html/TT_help.html b/html/html/TT_help.html index 1414496..12bec53 100644 --- a/html/html/TT_help.html +++ b/html/html/TT_help.html @@ -6,7 +6,7 @@ Table Toolbox

Table Toolbox

Available Documentation


+

Table Toolbox

Available Documentation

Copyright 2010 Colin Eles


Published with MATLAB® 7.10

\ No newline at end of file diff --git a/html/html/TT_ug_checking.html b/html/html/TT_ug_checking.html index 3846b8d..d38b814 100644 --- a/html/html/TT_ug_checking.html +++ b/html/html/TT_ug_checking.html @@ -62,7 +62,7 @@ p.footer { color: gray; } -

Typechecking a Table

Contents

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

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.

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.

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.

CVC3

CVC3 is the third iteration of a SMT solver deveoped at NYU.

PVS

PVS is a general purpose theorem prover developed by SRI.

PVS Typecehck

typecheck the current table using pvs, will call the syntax check first.

PVS Settings

a few settings for running the pvs commands can be adjusted using the pvs settings window. See the screenshot below.

  • 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 counter example.
  • Test Range: 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.

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

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.

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

Below is the report for a CVC3 typecheck then for a PVS typecheck.

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

incomplete tables


+

Typechecking a Table

Contents

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

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.

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.

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.

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.

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.

PVS Typecehck

typecheck the current table using pvs, will call the syntax check first.

PVS Settings

a few settings for running the pvs commands can be adjusted using the pvs settings window. See the screenshot below.

  • 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 counter example.
  • Test Range: 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.

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

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

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

Below is the report for a CVC3 typecheck then for a PVS typecheck.

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

incomplete tables


Published with MATLAB® 7.10