Typechecking a Table
Contents
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 System Requirements in the 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.
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 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.
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.
- 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>
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.
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
