@GUI/smtlib_ext_call.m

+function [] = cvc_ext_call( object,src,event )
+%CVC_EXT_CALL Summary of this function goes here
+%   Detailed explanation goes here
+
+
+object.save_call([],[]);
+object.save_data;
+if (object.validation_report_handle ~= 0)
+    delete(object.validation_report_handle);
+    object.validation_report_handle = 0;
+end
+error = object.check_call([],2);
+
+
+if (~error)
+    
+    inputs = TET.getInstance.getVariableParser.parseVariables(object.Data.function_inputs);
+    vars = inputs.getVariables().values();
+
+    HGrid = ca.mcscert.jtet.tablularexpression.HierarchicalGrid
+    TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid2.cells, HGrid.getSubHiearchy());
+
+    res = ca.mcscert.jtet.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);
+
+    if object.Data.multi_mode == 0 && size(object.Data.Grid1.cells,2) > 1
+        HGrid = ca.mcscert.jtet.tablularexpression.HierarchicalGrid
+        TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid1.cells, HGrid.getSubHiearchy());
+
+        res2 = ca.mcscert.jtet.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);
+        res.addAll(res2);
+    end   
+    
+    if (res.isEmpty())
+        check = 1;
+        msgbox('table is valid');
+    else
+        check = 0;
+        result = [];
+        for i=0:res.size()-1
+            r = res.get(i)
+            var_out = {}
+            % It is possible not sample values are present.  Just use an
+            % empty cell array in this case.
+            if ~isempty(r.SampleValues)
+                var_it = vars.iterator()
+                j = 0;
+                while var_it.hasNext()
+                    var = var_it.next()
+                    var = var.name()
+                    var_out(j*2+1:j*2+2) = {char(var), r.SampleValues.get(var)};
+                    j = j+1;
+                end
+                var_out
+            end
+            result = [result struct('id', '1234a', 'TCC', 'TCC', 'seq', r.Query, 'ce', {var_out})]
+        end
+        Valid_Report = ValidationReport(object);
+        Valid_Report.set_results(result);
+        Valid_Report.set_mode(1);
+        Valid_Report.init();
+    end
+    object.pvs_checked = check;
+    object.update_Statusbar;
+    if (object.mode == 1)
+        
+        TableBlock.set_block_display(object.block_handle,object.pvs_checked);
+    end
+    
+end
+end
+
+

@GUI/typecheck_call.m

@@ -3,8 +3,9 @@ function [ output_args ] = typecheck_call( object,src,event )
 %   Detailed explanation goes here
 
 if object.default_prover == object.CVC_const
-    
     cvc_ext_call(object,src,event);
+elseif object.default_prover == object.SMTLIB_const
+    smtlib_ext_call(object,src,event);
 else
     pvs_ext_call(object,src,event);
 end

@GUI/update_prover_check_status.m

@@ -11,9 +11,15 @@ function update_prover_check_status( object )
 
 
 if object.default_prover == object.CVC_const
+    set(object.prover_opt_smtlib,'Checked','off');
     set(object.prover_opt_cvc,'Checked','on');
     set(object.prover_opt_pvs,'Checked','off');
+elseif object.default_prover == object.SMTLIB_const
+    set(object.prover_opt_smtlib,'Checked','on');
+    set(object.prover_opt_cvc,'Checked','off');
+    set(object.prover_opt_pvs,'Checked','off');
 else
+    set(object.prover_opt_smtlib,'Checked','off');
     set(object.prover_opt_cvc,'Checked','off');
     set(object.prover_opt_pvs,'Checked','on');
 end

LICENCE

+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in
+      the documentation and/or other materials provided with the distribution
+    * Neither the name of the McMaster Centre for Software Certification nor the names
+      of its contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.

TET.m

+classdef (Sealed) TET < handle
+    %TET provides the global settings for the Tabular Expression Toolbox
+    %   TET provides the system through which all global settings are
+    %   accssed and changed.  It also provides a convient place for some
+    %   globals used in the TET.
+
+    properties (Access = private)
+        variableParser = ca.mcscert.jtet.parsers.VariableParser
+    end
+
+    methods
+        function variableParser = getVariableParser(obj)
+                variableParser = obj.variableParser;
+        end
+
+        %% Register an enumeration type with the TET.
+        %
+        %  This function registers a Simulink compatibile enumeration type
+        %  with the TET.  This allows the enumerated value to be used in
+        %  tables.
+        %  Note: the enumeration must derive from Simulink.IntEnumType
+        %  to be used in the Simulink model.
+        %  Note: each enumerated value must have a distinct value,
+        %  otherwise the type checker may allow invalid tables.
+        %
+        %  obj - This object
+        %  enum - A string representing the enumeration type name.
+        function type = registerEnumeration(obj, enum)
+            enumValues = enumeration(enum);
+            [~, enumConstants] = enumeration(enum);
+            if size(enumValues, 1) ~= size(enumConstants, 1)
+                throw(MException('TET:registerEnumeration', ...
+                  'Enumeration constants share the same concrete value'));
+            end
+
+            type = ca.mcscert.jtet.expression.EnumerationVariableType(enum);
+            typeEnumConstants = type.enumerationValues;
+            for i=1:size(enumConstants, 1)
+                java.lang.String(enumConstants{i})
+                typeEnumConstants.add(java.lang.String(enumConstants{i}));
+            end
+            obj.variableParser.addCustomType(enum, type);
+        end
+    end
+
+    methods (Access = private)
+        function obj = TET
+        end
+    end
+    methods (Static)
+      function singleObj = getInstance
+         persistent localObj
+         if isempty(localObj) || ~isvalid(localObj)
+            localObj = TET;
+         end
+         singleObj = localObj;
+      end
+   end
+
+end
+

TETLoadjTET.m

+function TETLoadjTET()
+%TETLOADJTET Loads jTET for use by the TET
+%   This loads the jTET library into MATLAB, so TET can use it.
+
+% First find the path.
+path = mfilename('fullpath');
+path = [path(1:size(path, 2)-11) 'jTET/jtet-1.0-SNAPSHOT-jar-with-dependencies.jar'];
+
+% Verify the jar isn't already in the classpath.
+classpath = javaclasspath;
+exists = 0;
+for i=1:size(classpath,1)
+    if strcmp(classpath{i}, path) == 1
+        exists = 1;
+    end
+end
+if exists == 0
+    % Not added yet, thus add it.
+    javaaddpath(path);
+end
+
+end

TTdiag.m

 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 function TTdiag(varargin)
+% Java needs to be loaded here.  Thus load it.
+TETLoadjTET();
+
 
 orig_gcbh = gcbh;
 

Tests/BaseConversionTest.m

+classdef BaseConversionTest < matlab.unittest.TestCase
+    %BASECONVERSIONTEST Base test class for conversion to jTET format
+    %   This contains all the common code for doing jTET conversion tests.
+
+    properties (Abstract)
+        File
+        TableName
+    end
+
+    properties
+        ConvertedTable = []
+    end
+
+    methods (TestClassSetup)
+        function setupOnce(testcase)
+            data = load(testcase.File);
+            testcase.ConvertedTable = TableBlock.convert_table_to_java_table(data.data);
+        end
+    end
+
+    methods (Test)
+        function testTableName(testcase)
+            testcase.assertEqual(char(testcase.ConvertedTable.getTableName()), testcase.TableName);
+        end
+    end
+end
+

Tests/ConversionTest1.m

+classdef ConversionTest1 < BaseConversionTest
+    %CONVERSIONTEST1 Summary of this class goes here
+    %   Detailed explanation goes here
+
+    properties
+        File = 'data/test1data.mat'
+        TableName = 'Startup_Limiter'
+    end
+
+    methods (Test)
+        function testVariableParsing(testcase)
+            vc = testcase.ConvertedTable.getVariables();
+
+            inVar = vc.getInputVariables();
+            testcase.assertEqual(inVar.size(), 2);
+            testcase.assertEqual(char(inVar.get('Start').name()), 'Start');
+            testcase.assertEqual(char(inVar.get('Input').name()), 'Input');
+
+            outVar = vc.getOutputVariables();
+            testcase.assertEqual(outVar.size(), 1);
+            testcase.assertEqual(char(outVar.get('output').name()), 'output');
+        end
+
+        function testTopGridConversion(testcase)
+            testcase.assertEqual(testcase.ConvertedTable.getTopGrid().getSubHierarchy().size(), 0)
+        end
+    end
+end
+

Tests/DataTest.m

+classdef DataTest < matlab.unittest.TestCase
+
+    methods (Test)
+        function testInit(testcase)
+            d = Data;
+            d.init;
+            testcase.assertEqual(size(d.Grid2.cells,2),1);
+            testcase.assertEqual(size(d.Grid1.cells,2),1);
+            testcase.assertEqual(size(d.Grid0.Cells,2),1);
+        end
+
+        function testClone(testcase)
+            d = Data;
+            d.init;
+            d.function_name = 'test_name';
+            d.function_inputs = 'input_test';
+            d.checked = 1;
+            d.Grid1.cells(1).cond_text = 'test_cond';
+            d2 = d.clone([]);
+            testcase.assertEqual(d2.function_name,'');
+            testcase.assertEqual(d2.function_inputs,d.function_inputs);
+            testcase.assertEqual(d2.Grid1.cells(1).cond_text,'test_cond');
+        end
+
+        function testClone2(testcase)
+            d = Data;
+            d2 = d.clone;
+            testcase.assertEqual(d2,[]);
+        end
+
+        function testSave(testcase)
+            d = Data;
+            d.init;
+            d.function_name = 'test_file';
+            d.save;
+            testcase.assertEqual(exist('test_file.table'),2);
+            delete('test_file.table');
+        end
+    end
+end

Tests/EMLGeneratorTest.m

+classdef EMLGeneratorTest < matlab.unittest.TestCase
+
+    methods (Test)
+        function testparse_inputs(testcase)
+            input_string = 'x';
+
+            ri = EMLGenerator.parse_inputs(input_string);
+            testcase.assertEqual(char(ri{1}(1)),'x');
+
+            input_string = 'x:boolean';
+            ri = EMLGenerator.parse_inputs(input_string);
+            testcase.assertEqual(char(ri{1}(1)),'x');
+            testcase.assertEqual(char(ri{1}(2)),'boolean');
+
+            input_string = 'a:boolean,c,d:{x:real|x<2}';
+            ri = EMLGenerator.parse_inputs(input_string);
+            testcase.assertEqual(char(ri{1}(1)),'a');
+            testcase.assertEqual(char(ri{1}(2)),'boolean');
+            testcase.assertEqual(char(ri{2}(1)),'c');
+            testcase.assertEqual(char(ri{3}(1)),'d');
+            testcase.assertEqual(char(ri{3}(2)),'{x:real|x<2}');
+
+            input_string = 'rewq$32:fwer';
+            ri = EMLGenerator.parse_inputs(input_string);
+            testcase.assertEqual(char(ri{1}(2)),'error');
+
+            input_string = ',,,,';
+            ri = EMLGenerator.parse_inputs(input_string);
+            testcase.assertEqual(char(ri{1}(2)),'error');
+
+        end
+
+        function testpreamble(testcase)
+            d = Data;
+            d.init;
+            d.function_name  = 'test';
+            d.function_inputs = 'x';
+            d.Grid1.cells(1).cond_text = 'x>1';
+            d.Grid1.new_Cell;
+            d.Grid1.cells(2).cond_text = 'x<=1';
+            d.Grid0.Cells(1).result_text = '1';
+            d.Grid0.Cells(2).result_text = '2';
+            d.settings.except = 0;
+
+            E = EMLGenerator(d);
+            pre = E.generate_preamble;
+            testcase.assertEqual(pre,sprintf('function [output] = test(x)\n%%%%#eml\noutput=1;\n'));
+
+            d.function_name = 'test2';
+            pre = E.generate_preamble;
+            testcase.assertEqual(pre,sprintf('function [output] = test2(x)\n%%%%#eml\noutput=1;\n'));
+
+            d.function_name = 'test3';
+            E.set_datatype({'output', 'logical'});
+            pre = E.generate_preamble;
+            testcase.assertEqual(pre,sprintf('function [output] = test3(x)\n%%%%#eml\noutput=logical(1);\n'));
+
+
+        end
+
+        function testcode_gen(testcase)
+            d = Data;
+            d.init;
+            d.function_name  = 'test';
+            d.function_inputs = 'x';
+            d.Grid1.cells(1).cond_text = 'x>1';
+            d.Grid1.new_Cell;
+            d.Grid1.cells(2).cond_text = 'x<=1';
+            d.Grid0.Cells(1).result_text = '1';
+            d.Grid0.Cells(2).result_text = '2';
+            d.settings.except = 0;
+
+            E = EMLGenerator(d);
+            code = E.generate_eml_code;
+            testcase.assertEqual(code,sprintf('function [output] = test(x)\n%%%%#eml\noutput=1;\nif(x>1)\n  output = 1;\nelseif(x<=1)\n  output = 2;\nend\n'));
+
+            d.Grid1.cells(1).cond_text = 'x+1<2';
+            d.Grid1.cells(2).cond_text = 'x-1>6';
+            code = E.generate_eml_code;
+            testcase.assertEqual(code,sprintf('function [output] = test(x)\n%%%%#eml\noutput=1;\nif(x+1<2)\n  output = 1;\nelseif(x-1>6)\n  output = 2;\nend\n'));
+
+
+            d.Grid2.new_Cell;
+            d.Grid2.cells(1).cond_text = 'x+1<2';
+            d.Grid2.cells(2).cond_text = 'x-1>6';
+            d.Grid1.cells(1).cond_text = 'y<1';
+            d.Grid1.cells(2).cond_text = 'y>=1';
+            d.Grid0.Cells(3).result_text = '3';
+            d.Grid0.Cells(4).result_text = '4';
+            code = E.generate_eml_code;
+            testcase.assertEqual(code,sprintf('function [output] = test(x)\n%%%%#eml\noutput=1;\nif(x+1<2)\n  if(y<1)\n    output = 1;\n  elseif(y>=1)\n    output = 2;\n  end\nelseif(x-1>6)\n  if(y<1)\n    output = 3;\n  elseif(y>=1)\n    output = 4;\n  end\nend\n'));
+        end
+    end
+end

Tests/Untitled.m

-function [ output_args ] = Untitled( input_args )
-%UNTITLED Summary of this function goes here
-%   Detailed explanation goes here
-
-
-end
-

Tests/testData.m

-function test_suite = testData
-initTestSuite;
-end
-
-function testConstructor
-    d = Data;
-    assertEqual(class(d),'Data');
-end
-
-function testInit
-    d = Data;
-    d.init;
-    assertEqual(size(d.Grid2.cells,2),1);
-    assertEqual(size(d.Grid1.cells,2),1);
-    assertEqual(size(d.Grid0.Cells,2),1);
-end
-
-function testClone
-    d = Data;
-    d.init;
-    d.function_name = 'test_name';
-    d.function_inputs = 'input_test';
-    d.checked = 1;
-    d.Grid1.cells(1).cond_text = 'test_cond';
-    d2 = d.clone([]);
-    assertEqual(d2.function_name,'');
-    assertEqual(d2.function_inputs,d.function_inputs);
-    assertEqual(d2.Grid1.cells(1).cond_text,'test_cond');
-end
-
-function testClone2
-    d = Data;
-    d2 = d.clone;
-    assertEqual(d2,[]);
-end
-
-function testSave
-    d = Data;
-    d.init;
-    d.function_name = 'test_file';
-    d.save;
-    assertEqual(exist('test_file.table'),2);
-    delete('test_file.table');
-end
-        
\ No newline at end of file

Tests/testEMLGenerator.m

-
-function test_suite = testEMLGenerator
-initTestSuite;
-end
-
-
-function testparse_inputs
-    input_string = 'x';
-    ri = EMLGenerator.parse_inputs(input_string);
-    
-    assertEqual(char(ri{1}(1)),'x');
-    input_string = 'x:boolean';
-    ri = EMLGenerator.parse_inputs(input_string);
-    assertEqual(char(ri{1}(1)),'x');
-    assertEqual(char(ri{1}(2)),'boolean');
-    input_string = 'a:boolean,c,d:{x:real|x<2}';
-        ri = EMLGenerator.parse_inputs(input_string);
-        assertEqual(char(ri{1}(1)),'a');
-        assertEqual(char(ri{1}(2)),'boolean');
-        assertEqual(char(ri{2}(1)),'c');
-        assertEqual(char(ri{3}(1)),'d');
-        assertEqual(char(ri{3}(2)),'{x:real|x<2}');
-    
-        input_string = 'rewq$32:fwer';
-        ri = EMLGenerator.parse_inputs(input_string);
-        assertEqual(char(ri{1}(2)),'error');
-
-         input_string = ',,,,';
-        ri = EMLGenerator.parse_inputs(input_string);
-        assertEqual(char(ri{1}(2)),'error');
-
-end
-
-function testpreamble
-    d = Data;
-    d.init;
-    d.function_name  = 'test';
-    d.function_inputs = 'x';
-    d.Grid1.cells(1).cond_text = 'x>1';
-    d.Grid1.new_Cell;
-    d.Grid1.cells(2).cond_text = 'x<=1';
-    d.Grid0.Cells(1).result_text = '1';
-    d.Grid0.Cells(2).result_text = '2';
-    E = EMLGenerator(d);
-    pre = E.generate_preamble;
-    assertEqual(pre,sprintf('function output = test(x)\n%%%%#eml\noutput=(1);\n'));
-    
-    d.function_name = 'test2';
-    pre = E.generate_preamble;
-    assertEqual(pre,sprintf('function output = test2(x)\n%%%%#eml\noutput=(1);\n'));
-    
-     d.function_name = 'test3';
-    E.set_datatype('logical');
-        pre = E.generate_preamble;
-
-    assertEqual(pre,sprintf('function output = test3(x)\n%%%%#eml\noutput=logical(1);\n'));
-    
-    
-end
-
-function testcode_gen
-    d = Data;
-    d.init;
-    d.function_name  = 'test';
-    d.function_inputs = 'x';
-    d.Grid1.cells(1).cond_text = 'x>1';
-    d.Grid1.new_Cell;
-    d.Grid1.cells(2).cond_text = 'x<=1';
-    d.Grid0.Cells(1).result_text = '1';
-    d.Grid0.Cells(2).result_text = '2';
-    E = EMLGenerator(d);
-    code = E.generate_eml_code;
-    assertEqual(code,sprintf('function output = test(x)\n%%%%#eml\noutput=(1);\nif(x>1)\n  output = (1);\nelseif(x<=1)\n  output = (2);\nend\n'));
-    
-    
-    d.Grid1.cells(1).cond_text = 'x+1<2';
-    d.Grid1.cells(2).cond_text = 'x-1>6';
-        code = E.generate_eml_code;
-    assertEqual(code,sprintf('function output = test(x)\n%%%%#eml\noutput=(1);\nif(x+1<2)\n  output = (1);\nelseif(x-1>6)\n  output = (2);\nend\n'));
-
-    
-    d.Grid2.new_Cell;
-    d.Grid2.cells(1).cond_text = 'x+1<2';
-    d.Grid2.cells(2).cond_text = 'x-1>6';
-    d.Grid1.cells(1).cond_text = 'y<1';
-    d.Grid1.cells(2).cond_text = 'y>=1';
-    d.Grid0.Cells(3).result_text = '3';
-    d.Grid0.Cells(4).result_text = '4';
-    code = E.generate_eml_code;
-    assertEqual(code,sprintf('function output = test(x)\n%%%%#eml\noutput=(1);\nif(x+1<2)\n  if(y<1)\n    output = (1);\n  elseif(y>=1)\n    output = (2);\n  end\nelseif(x-1>6)\n  if(y<1)\n    output = (3);\n  elseif(y>=1)\n    output = (4);\n  end\nend\n'));
-
-
-%     d.function_name = 'test2';
-%     pre = E.generate_preamble;
-%     assertEqual(pre,sprintf('function output = test2(x)\n%%%%#eml\noutput=(1);\n'));
-%     
-%      d.function_name = 'test3';
-%     E.set_datatype('logical');
-%         pre = E.generate_preamble;
-% 
-%     assertEqual(pre,sprintf('function output = test3(x)\n%%%%#eml\noutput=logical(1);\n'));
-    
-    
-end
-

Tests/testGUI.m

-function test_suite = testGUI
-initTestSuite;
\ No newline at end of file

jTET/README

+This folder needs a copy of the jTET library, currently available at:
+https://groke.mcmaster.ca/gitlab/tables/jtet/
+Place the target/jtet-1.0-SNAPSHOT-jar-with-dependencies.jar file in this
+directory and the TET will automatically pick it up.