Loading @Cell/flag_cell.m +1 −5 Original line number Diff line number Diff line Loading @@ -19,7 +19,3 @@ end No newline at end of file function new_cell = clone() end end No newline at end of file @Data/Data.m +1 −1 Original line number Diff line number Diff line Loading @@ -28,7 +28,7 @@ classdef Data < handle end end end Loading @GUI/pvs_ext_call.m +2 −0 Original line number Diff line number Diff line Loading @@ -14,6 +14,8 @@ [check,result] = object.PVS.pvs_check; if (check == 1) msgbox('table is valid') elseif (check == 0 && strcmp(result,'canceled')) return; else Valid_Report = ValidationReport(object); Valid_Report.set_results(result); Loading @PVS_checker/pvs_check.m +3 −1 Original line number Diff line number Diff line Loading @@ -31,9 +31,11 @@ end if (exists == 1 && (isempty(button) || strcmp(button,'Cancel'))) % do nothing output = 'canceled'; return; elseif (exists == 1 && (strcmp(button,'Open PVS'))); [status, result] = system(['pvs ' object.data.function_name '.pvs']); output = 'canceled'; elseif (exists == 0 || strcmp(button,'Attempt to prove')) box = waitbar(0,'Generating Proof Script') Loading check_system.m 0 → 100644 +27 −0 Original line number Diff line number Diff line function [ output_args ] = check_system(system) %UNTITLED Summary of this function goes here % Detailed explanation goes here blocks = find_system(system,'MaskDescription','Table Block') msg = []; for i = 1:size(blocks,1) if ~strncmp(blocks(i),'TableLibrary',12) block_data = get_param(char(blocks(i)),'UserData'); if ~isempty(block_data) PVS = PVS_checker(block_data); [check,result] = PVS.pvs_check; if (check == 1) msg = [msg char(blocks(i)) ' is valid' sprintf('\n')] else msg = [msg char(blocks(i)) ' is not valid' sprintf('\n')] end block_data.checked = check; TableBlock.set_block_display(char(blocks(i)),block_data.checked) end end end msgbox(msg); end Loading
@Cell/flag_cell.m +1 −5 Original line number Diff line number Diff line Loading @@ -19,7 +19,3 @@ end No newline at end of file function new_cell = clone() end end No newline at end of file
@Data/Data.m +1 −1 Original line number Diff line number Diff line Loading @@ -28,7 +28,7 @@ classdef Data < handle end end end Loading
@GUI/pvs_ext_call.m +2 −0 Original line number Diff line number Diff line Loading @@ -14,6 +14,8 @@ [check,result] = object.PVS.pvs_check; if (check == 1) msgbox('table is valid') elseif (check == 0 && strcmp(result,'canceled')) return; else Valid_Report = ValidationReport(object); Valid_Report.set_results(result); Loading
@PVS_checker/pvs_check.m +3 −1 Original line number Diff line number Diff line Loading @@ -31,9 +31,11 @@ end if (exists == 1 && (isempty(button) || strcmp(button,'Cancel'))) % do nothing output = 'canceled'; return; elseif (exists == 1 && (strcmp(button,'Open PVS'))); [status, result] = system(['pvs ' object.data.function_name '.pvs']); output = 'canceled'; elseif (exists == 0 || strcmp(button,'Attempt to prove')) box = waitbar(0,'Generating Proof Script') Loading
check_system.m 0 → 100644 +27 −0 Original line number Diff line number Diff line function [ output_args ] = check_system(system) %UNTITLED Summary of this function goes here % Detailed explanation goes here blocks = find_system(system,'MaskDescription','Table Block') msg = []; for i = 1:size(blocks,1) if ~strncmp(blocks(i),'TableLibrary',12) block_data = get_param(char(blocks(i)),'UserData'); if ~isempty(block_data) PVS = PVS_checker(block_data); [check,result] = PVS.pvs_check; if (check == 1) msg = [msg char(blocks(i)) ' is valid' sprintf('\n')] else msg = [msg char(blocks(i)) ' is not valid' sprintf('\n')] end block_data.checked = check; TableBlock.set_block_display(char(blocks(i)),block_data.checked) end end end msgbox(msg); end