%% genereate_cvc_grid % generate the queries for cvc for the inputted grid. % % inputs: % grid:Grid - grid to generate conditions for. % level:int - count of the queries generated. % % outputs; % code:string - string representing code to generate including comments % query:cell array - contains string representing both the disjoint and % complete without the comments, used for validation report. % Author: Colin Eles elesc@mcmaster.ca % Organization: McMaster Centre for Software Certification function [ code , query] = generate_cvc_grid( grid , level) % generate the formulas for the main grid parents = CVC_checker.find_parents(grid.cells(1)); if isempty(parents); disjoint = 'QUERY ('; complete = 'QUERY ('; else disjoint = ['QUERY ' parents ' => (']; complete = ['QUERY ' parents ' => (']; end for i=1:size(grid.cells,2) for j = i+1:size(grid.cells,2) % compare i to j disjoint = [disjoint 'NOT ( (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ') AND (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(j).cond_text)) ') )']; if j~= size(grid.cells,2) disjoint = [disjoint ' AND ' char(10)]; end end % need to do pairwise disjointness % otherwise doesn't work complete = [complete '(' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ')']; if i < size(grid.cells,2) - 1 disjoint = [disjoint ' AND ' char(10)]; end if i < size(grid.cells,2) complete = [complete ' OR ']; end end disjoint = [disjoint ');']; complete = [complete ');']; query = [{disjoint} {complete}]; code = ['ECHO "begin' num2str(level+1) '";' char(10) 'PUSH;' char(10) disjoint char(10) 'POP;' char(10) 'ECHO "end' num2str(level+1) '";' char(10)]; code = [code 'ECHO "begin' num2str(level+2) '";' char(10) 'PUSH;' char(10) complete char(10) 'POP;' char(10) 'ECHO "end' num2str(level+2) '";' char(10)]; for i=1:size(grid.cells,2) if ~isempty(grid.cells(i).subgrid) [new_code,new_queries] = CVC_checker.generate_cvc_grid(grid.cells(i).subgrid,level+2); code = [code new_code]; query = [query new_queries]; level = size(query,2) - 2; end end end