removed any references to gui from pvs_checker so that it can be run independantly of the gui (9939ab3b) · Commits · Abdulrahman elgendy / tet

GUI.m

+14 −3

Original line number	Diff line number	Diff line
		@@ -242,7 +242,7 @@ classdef GUI < handle

		obj.update_Statusbar;

		obj.PVS = PVS_checker(obj,obj.settings);
		obj.PVS = PVS_checker(obj.Data);

		obj.initialized = 1;
		obj.Data.open = 1;
		@@ -253,6 +253,7 @@ classdef GUI < handle


		function [] = set_block_display(object)
		if (object.mode == 1)
		%if object.pvs_checked == 1
		mask_string = [];
		code_block = sprintf('%s/code',getfullname(object.block_handle));
		@@ -268,7 +269,7 @@ classdef GUI < handle

		end
		set_param(getfullname(object.block_handle),'MaskDisplay',mask_string);
		%end
		end


		end
		@@ -396,11 +397,17 @@ classdef GUI < handle
		end
		%% pvs_ext_call
		function [] = pvs_ext_call(object,src,event)
		object.save_data;
		error = object.check_call;

		if (~error)
		check = object.PVS.pvs_check;
		[check,result] = object.PVS.pvs_check;
		if (check == 1)
		msgbox('table is valid')
		else
		Valid_Report = ValidationReport(object);
		Valid_Report.set_results(result);
		Valid_Report.init();
		end
		object.pvs_checked = check;
		object.update_Statusbar;
		@@ -1818,8 +1825,12 @@ classdef GUI < handle
		%%

		function [] = textbox_callback(object,src,event)
		if object.pvs_checked == 1
		object.pvs_checked = 0;
		object.update_Statusbar
		object.set_block_display;
		end

		end

		%% clone

PVS_checker.m

+70 −27

Original line number	Diff line number	Diff line
		@@ -3,29 +3,30 @@ classdef PVS_checker < handle
		% prover

		properties
		gui = [];
		counter_examples = 10000;
		counter_size = 100;
		default_type = 'real';
		pvs_version = 4.2;
		settings

		data = [];
		mode = []; % 0 - graphical, 1 - command
		end

		methods

		%% constructor
		function obj = PVS_checker(gui_new,settings)
		obj.gui = gui_new;
		obj.settings = settings;
		function obj = PVS_checker(data)
		obj.data = data;
		end

		%% pvs_ext_call
		function check = pvs_check(obj)
		function [check,output] = pvs_check(obj)
		check = 0;
		output = [];
		% file name will be expression_name.m
		fileid = fopen([get(obj.gui.function_name_control,'String') '.pvs'],'w');
		fileid = fopen([obj.data.function_name '.pvs'],'w');
		code = [];
		code = sprintf('%s:THEORY\nBEGIN\n',get(obj.gui.function_name_control,'String'));
		code = sprintf('%s:THEORY\nBEGIN\n',obj.data.function_name);

		code = [code obj.pvs_check_for_imports];

		@@ -34,7 +35,7 @@ classdef PVS_checker < handle

		%inputs = get(obj.gui.function_inputs_control,'String');
		%inputs = regexp(inputs,',','split');
		parsed_inputs = obj.gui.parse_inputs(get(obj.gui.function_inputs_control,'string'));
		parsed_inputs = obj.parse_inputs(obj.data.function_inputs);

		% initialize inputs to zero
		% functions are assumed to be total, so 0 is just for
		@@ -56,26 +57,26 @@ classdef PVS_checker < handle
		end
		end

		code = [code sprintf('%s(%s):real = \n',get(obj.gui.function_name_control,'String'),inputs_new)];
		code = [code obj.generate_pvs(obj.gui.Grid1,obj.gui.Grid2,0)];
		code = [code sprintf('\nEND %s',get(obj.gui.function_name_control,'String'))];
		code = [code sprintf('%s(%s):real = \n',obj.data.function_name,inputs_new)];
		code = [code obj.generate_pvs(obj.data.Grid1,obj.data.Grid2,0)];
		code = [code sprintf('\nEND %s',obj.data.function_name)];
		fprintf(fileid,code);

		fclose(fileid);

		% generate the proof script
		obj.generate_pvs_script(get(obj.gui.function_name_control,'String'))
		obj.generate_pvs_script(obj.data.function_name)


		% THIS SECTION NEEDS SOME WORK
		%-------------
		% delete the existing proof

		delete([get(obj.gui.function_name_control,'String') '.prf'])
		delete([obj.data.function_name '.prf'])
		%---------
		% call pvs in batch mode with script
		% ADD check that pvs actually exists in system
		[status, result] = system(['pvs -batch -v 3 -l ' get(obj.gui.function_name_control,'String') '.el'])
		[status, result] = system(['pvs -batch -v 3 -l ' obj.data.function_name '.el'])
		%object.msgbox_scroll(result);
		[parsed error] = obj.parse_pvs_result(result);
		if (error == 1)
		@@ -84,18 +85,60 @@ classdef PVS_checker < handle

		if (isempty(parsed))
		check = 1;
		output = [];
		else
		output = parsed;
		%Valid_Report = ValidationReport(obj.gui);
		%Valid_Report.set_results(parsed);
		%Valid_Report.init();
		end
		end
		end

		function revised_input = parse_inputs(obj,input_string)
		revised_input = [];
		input_string2 = reshape(input_string',1,size(input_string,1)*size(input_string,2));
		inputs = regexprep(input_string2,'\s','');
		inputs = regexp(inputs,',','split');

		% need to be careful here because pvs dependant types can have
		% :'s in them

		% find the first :, any thing before this is considered the
		% variable any thing following is considered the type
		c_locations = regexp(inputs,':','start');
		for i= 1:size(inputs,2)
		if size(c_locations{i},2) == 0
		sub_input{1} = inputs{i};
		new_inputs{i} = sub_input;
		else
		Valid_Report = ValidationReport(obj.gui);
		Valid_Report.set_results(parsed);
		Valid_Report.init();
		sub_input{1} = inputs{i}(1:c_locations{i}(1)-1);
		sub_input{2} = inputs{i}(c_locations{i}(1)+1:end);
		new_inputs{i} = sub_input;
		%new_inputs{i}(1) = inputs{i}(1:c_locations{i}(1))
		%new_inputs{i}(2) = inputs{i}(c_locations{i}(1):end)
		end

		end

		%inputs = regexp(inputs,':','split')

		for i=1:size(new_inputs,2)
		valid = regexp(new_inputs{i}(1),'[a-zA-Z][_a-zA-Z0-9]*','match');
		if ~strcmp(new_inputs{i}(1),valid{1})
		new_inputs{i}(2) = {'error'};
		%revised_input = cat(2,revised_input,[char(inputs{i}(1)); 'error'])
		end
		end
		if isempty(revised_input)
		revised_input = new_inputs;
		end
		end

		function [string] = user_imports(obj)
		string = [];
		if ~isempty(obj.settings.pvs_includes)
		files = regexp(obj.settings.pvs_includes,',','split');
		if ~isempty(obj.data.settings.inputs)
		files = regexp(obj.data.settings.inputs,',','split');

		for i=1:size(files,2)
		file_no_ext = regexp(files{i},'\w(?=\.\w)','match');
		@@ -176,7 +219,7 @@ classdef PVS_checker < handle
		continue
		end
		code = [code sprintf('%s->',obj.matlab_to_pvs_syntax_translation(strtrim(char(get(g1.cells(i).cond,'String')))))];
		resultcell = obj.gui.Grid0.search_return(g1.cells(i),g2_cell);
		resultcell = obj.data.Grid0.search_return(g1.cells(i),g2_cell);
		if(~isempty(resultcell))
		code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))];

		@@ -193,7 +236,7 @@ classdef PVS_checker < handle
		end
		end
		if(~isempty(elsecell))
		resultcell = obj.gui.Grid0.search_return(elsecell,g2_cell);
		resultcell = obj.data.Grid0.search_return(elsecell,g2_cell);
		code = [code sprintf('ELSE->%s\n',obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String')))))];

		end
		@@ -237,7 +280,7 @@ classdef PVS_checker < handle
		code = [code obj.generate_pvs_horizontal(g1,g2.cells(i),depth)];
		else

		resultcell = obj.gui.Grid0.search_return(g1.cells(1),g2.cells(i));
		resultcell = obj.data.Grid0.search_return(g1.cells(1),g2.cells(i));
		if(~isempty(resultcell))
		code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))];

		@@ -270,7 +313,7 @@ classdef PVS_checker < handle
		code = [code obj.generate_pvs_horizontal(g1,elsecell,depth) sprintf('\n')];
		else

		resultcell = obj.gui.Grid0.search_return(g1.cells(1),elsecell);
		resultcell = obj.data.Grid0.search_return(g1.cells(1),elsecell);
		if(~isempty(resultcell))
		code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String')))) sprintf('\n')];

		@@ -293,8 +336,8 @@ classdef PVS_checker < handle

		%% pvs_check_for_imports
		function string = pvs_check_for_imports(obj)
		[string,found] = obj.pvs_check_for_imports_g(obj.gui.Grid2,{});
		[string2,found2] = obj.pvs_check_for_imports_g(obj.gui.Grid1,found);
		[string,found] = obj.pvs_check_for_imports_g(obj.data.Grid2,{});
		[string2,found2] = obj.pvs_check_for_imports_g(obj.data.Grid1,found);
		string = [string string2];
		end

		@@ -330,7 +373,7 @@ classdef PVS_checker < handle
		%% generate_pvs_script
		function [] = generate_pvs_script(obj,filename)
		fileid = fopen([filename '.el'],'w');
		code = ['(prove-tccs-pvs-file "' filename '" "(try (try (tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',obj.settings.counter_trials) ' :size ' sprintf('%d',obj.settings.counter_range) '))" )' sprintf('\n')];
		code = ['(prove-tccs-pvs-file "' filename '" "(try (try (tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',obj.data.settings.count) ' :size ' sprintf('%d',obj.data.settings.range) '))" )' sprintf('\n')];

		fprintf(fileid,code);
		fclose(fileid);

ValidationReport.m

+0 −1

Original line number	Diff line number	Diff line
		@@ -48,7 +48,6 @@ classdef ValidationReport < handle
		function [] = init(obj)

		if size(obj.PVS_results,2) == 0
		msgbox('table is proper')

		else