Commit 526ae04a authored by Colin Eles's avatar Colin Eles
Browse files

have a mode working where tool will generate a theory using the simulink... 

have a mode working where tool will generate a theory using the simulink types, as well as an constraints expressed in the pvs types. for example if input is x:real, but in simulink diagram input is int8, will create a theory where input is of type int8, copies a pvs theory of the types to the pwd, currently using integer subranges for types, and real for floating pt types, not sure if I should use IEEE754, might lose test case generation with this. Typechecker forces proving that no over/under flow for outputs, this is not always automatic, and grind seems to have trouble with it sometimes.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6318 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 8af291be

@EMLGenerator/parse_inputs.m

+1 −1
Original line number Diff line number Diff line
@@ -16,7 +16,7 @@ input_string2 = reshape(input_string',1,size(input_string,1)*size(input_string,2 
inputs = regexprep(input_string2,'\n','');

inputs = regexp(inputs,',','split');



% need to be careful here because pvs dependant types can have

% need to be careful here because pvs dependant types can have multiple

% :'s in them



% find the first :, any thing before this is considered the

@GUI/compiled_types.m

+4 −4
Original line number Diff line number Diff line 
function [ inputs, outputs ] = compiled_types( object )

inputs = [];

outputs = [];

try

%try

eval([bdroot '([],[],[],''compile'')']);

catch exception

    return;

end

%catch exception

%    return;

%end

if (object.mode == 1)

    S = sfroot;

    code_block = sprintf('%s/code',getfullname(object.block_handle));

@GUI/evaluate_counter.m

+1 −1
Original line number Diff line number Diff line
@@ -12,7 +12,7 @@ 
function [] = evaluate_counter(object,counter)



problem = object.evaluate_counter_grid(object.Grid2, counter);

if(~problem)

if(~problem && object.multi_mode == 0)

    object.evaluate_counter_grid(object.Grid1, counter);

end

end

@GUI/init.m

+1 −0
Original line number Diff line number Diff line
@@ -157,6 +157,7 @@ uimenu(pvsmenu,'Label','Typecheck','Accelerator','t','Callback',@(src,event)pvs_ 
uimenu(pvsmenu,'Label','PVS Settings','Callback',@(src,event)settings_call(object,src,event));

uimenu(pvsmenu,'Label','Check Status','Callback',@(src,event)prf_file_call(object,src,event));

uimenu(pvsmenu,'Label','Generate PVS file','Callback',@(src,event)pvs_file_call(object,src,event));

uimenu(pvsmenu,'Label','Typecheck SimTypes','Callback',@(src,event)pvs_ext_call_sim(object,src,event));



uimenu(helpmenu,'Label','Product Help','Callback',@(src,event)help_call(object,src,event));

uimenu(helpmenu,'Label','About Table Tool','Callback',@(src,event)about_call(object,src,event));

@GUI/pvs_ext_call.m

+5 −0
Original line number Diff line number Diff line
@@ -20,8 +20,13 @@ if(object.multi_mode == 0) 
    object.PVS.output_type = object.output_data_type;

    

    object.PVS.input_type = object.input_data_type;

    

    

    

end



object.PVS.type_mode = 0;



if (~error)

    [check,result] = object.PVS.pvs_check;

    if (check == 1)