Commit 1d21ee1f authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Completely replace CVC generation into the java side. 

Now the full contents of the CVC3 file are generated inside of Java, but the
actual saving and running of CVC3 still happen inside of matlab.  For now.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10651 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 4d5ae5bc

+TableBlock/convert_hierarchical_grid_to_java.m

0 → 100644
+28 −0
Original line number Diff line number Diff line 
%% convert_hierarchical_grid_to_java

% generates a java version fo the hiearchcial grid

%

% inputs:

%   grid:Grid - grid to convert

%   java_grid:List<HierarchicalCell> - place to put changed cells.

%

% outputs;

%   none

% Author: Matthew Dawson matthew@mjdsystems.ca

% Organization: McMaster Centre for Software Certification



function convert_hierarchical_grid_to_java(grid, java_grid)



for i=1:size(grid,2)

    new_cell = ca.mcmaster.cas.tablularexpression.HierarchicalCell;

    

    old_cell = grid(i)

    new_cell.setContents(old_cell.cond_text)

    

    if ~isempty(old_cell.subgrid)

        TableBlock.convert_hierarchical_grid_to_java(old_cell.subgrid.cells, new_cell.getSubHiearchy())

    end

    java_grid.add(new_cell)

end



end

@CVC_checker/CVC_checker.m

+0 −8
Original line number Diff line number Diff line
@@ -11,14 +11,6 @@ classdef CVC_checker 
        

    end

    

    

    methods(Static)

        

        [ code ] = find_parents( grid );

        [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type );

        

    end

    

    methods

        

        %% CVC_checker

@CVC_checker/cvc_check.m

+2 −2
Original line number Diff line number Diff line
@@ -56,7 +56,7 @@ if ~isempty(fatal_exception) 
end





for i = 1:size(queries,2)

for i = 1:queries.size()

    asserts = [];



    % find results of individual queries, using regexp and notations in
@@ -77,7 +77,7 @@ for i = 1:size(queries,2) 
        name = [filename '_' num2str(i) '_COM'];

    end    



        seqs = [seqs struct('id', '1234a', 'TCC', name, 'seq', queries(i), 'ce', {asserts})];

        seqs = [seqs struct('id', '1234a', 'TCC', name, 'seq', queries.get(i-1), 'ce', {asserts})];

    end

@CVC_checker/cvc_parse_result.m

deleted100644 → 0
+0 −7
Original line number Diff line number Diff line 
function [ output_args ] = cvc_parse_result( input_args )

%CVC_PARSE_RESULT Summary of this function goes here

%   Detailed explanation goes here





end

@CVC_checker/find_parents.m

deleted100644 → 0
+0 −47
Original line number Diff line number Diff line 
%% find_parents

% function will find all the parents of a cell, used to determine what

% preconditions must be true.

%

% inputs:

%   cell:Cell - cell to find the parents of

%

% outputs;

%   code:string - string of conjunction of all parent cells.

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification



function [ code ] = find_parents( cell )

% assumption, initial input will be grid we want to find parents for not

%  cell itself



code = '';

if isempty(cell)

    % current cell is empty

    code = '';

else

    if isempty(cell.parent_grid.parent_cell)

        % no parent cell

        

    else

        % there is a parent cell

        top = char(CVC_checker.find_parents(cell.parent_grid.parent_cell));

        code = char(cell.parent_grid.parent_cell.cond_text);

        if isempty(top);

            % there were no more above this cell

            

        else

            % there were more above this cell

            code = [code ' AND ' top];

        end

        

        

    end

    

    

end









end