starting to update documentation (6df35db4) · Commits · Abdulrahman elgendy / tet

html/TT_gs_over.m

+7 −3

Original line number	Diff line number	Diff line
		@@ -91,7 +91,7 @@ end
		%%
		% 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 PVS button will start the proof and popup a
		% satisfied. Clicking on the Typecheck button will start the proof and popup a
		% process dialog as shown below:
		%
		% <<walk7.png>>
		@@ -99,7 +99,9 @@ end
		% 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.
		%
		% <<walk8.png>>
		% <<walk8_p1.png>>
		%
		% <<walk8_p2.png>>
		%
		% 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.
		@@ -112,7 +114,9 @@ end
		% false for the counter example indicating to the table designer that they
		% failed to consider a case of the input.
		%
		% <<walk9.png>>
		% <<walk9_p1.png>>
		%
		% <<walk9_p2.png>>
		%
		% 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

+16 −1

Original line number	Diff line number	Diff line
		@@ -3,8 +3,23 @@
		%% Matlab/Simulink
		%
		% * Tested with Matlab Simulink 2009b and 2010a
		%
		%% Table Checking
		% * The tool supports checking of table completness and disjointness
		% through the support of external tools
		% * This tool will work with either or both of the tools installed.
		% * It is recommened that both tools be installed, as they are built on
		% different technologies, and have different strengths and weaknesses.
		%
		%% CVC3
		% * CVC3 is supported for checking for completness and disjointness of
		% tables
		% * CVC3 can be downloaded from http://cs.nyu.edu/acsys/cvc3/
		% * Ensure that cvc3 is executable on the shell path.
		% * CVC3 is available for Linux/OS X and Windows.
		%
		%% PVS (Prototype Verification System)
		% * PVS is required to be installed in order to check for completness and
		% * PVS is supported for checking for completness and
		% disjointness of tables.
		% * PVS is downloadable from http://pvs.csl.sri.com/
		% * System has been tested on PVS versions 4.2 and 4.1

+4 −1

Original line number	Diff line number	Diff line
		%% User Guide
		%
		% * <TT_ug_background.html Tabular Expressions>
		% * <TT_ug_opening.html Creating a new Table>
		% * <TT_ug_editing.html Editing a Tabular Expression>
		% * <TT_ug_editing.html Editing a Table>
		% * <TT_ug_settings.html Settings>
		% * <TT_ug_checking.html Typechecking a Table>
		%
		% Copyright 2010 Colin Eles
		No newline at end of file

0 → 100644

+1 −0

Original line number	Diff line number	Diff line
		%% Tabular Expressions

0 → 100644

+2 −0