Added functionality to annotate model with generated CoCoSpec

README.md

@@ -2,7 +2,12 @@
 
 # CoCoSim
 
-CoCoSim is an automated analysis framework for Simulink and Stateflow models. CoCoSim is currently under development. We welcome any feedback and bug report.
+CoCoSim is an automated analysis and code generation framework for
+Simulink and Stateflow models. Specifically, CoCoSim can be used to
+verify automatically user-supplied safety requirements. Moreover,
+CoCoSim can be used to generate C and/or Rust code. CoCoSim uses
+Lustre as its intermediate language. CoCoSim is currently under
+development. We welcome any feedback and bug report.
 
 [![ScreenCast of CoCoSim](http://i.imgur.com/itLte0X.png)](https://youtu.be/iqwVCiU46Y4)
 
@@ -12,7 +17,6 @@ The CoCoSim toolbox contains linux and osx binariers for the backend solvers.
 Download the [CoCoSim ToolBox](https://github.com/coco-team/cocoSim/releases)
 
 
-
 ## Installation
 
 CoCoSim can be installed and used as follows:
@@ -61,14 +65,20 @@ More information about CoCoSim can be found [here](https://github.com/coco-team/
 
 * Lead Developer: [Temesghen Kahsai](http://www.lememta.info/)
 
-## Current Contributors
+* Current Contributors: Hamza Bourbouh (SGT - USA), Pierre-Loic
+  Garoche (Onera - France), Claire Pagetti (Onera - France), Eric
+  Noulard (Onera - France), Thomas Loquen (Onera - France)
+
+* Past Contributors: Arnaud Dieumegard (Fabruary - August 2015)
+
+
+## Acknowledgments and Disclaimers
 
-* [Hamza Bourbouh] (https://hbourbouh.github.io/)
-* Pierre-Loic Garoche (Onera - France)
-* Claire Pagetti (Onera - France)
-* Eric Noulard (Onera - France)
-* Thomas Loquen (Onera - France)
+CoCoSim is partially funded by:
 
-## Past Contributors
+   * NASA NRA NNX14AI09G
+   * NSF award 1136008
 
-* Arnaud Dieumegard (Fabruary - August 2015)
+Any opinions, findings and conclusions or recommendations expressed in
+this material are those of the author(s) do not necessarily
+reflect the views of NASA and NSF.

sl_customization.m

@@ -19,9 +19,9 @@ function sl_customization(cm)
   schema.statustip = 'Automated Analysis Framework';
   schema.autoDisableWhen = 'Busy';
 
-  schema.childrenFcns = {@getVerify,@getValidate,...
-      @getCheckBlocks, @viewContract, @getProps, ...
-                        @getPP,  @getCompiler};
+  schema.childrenFcns = {@getVerify,@getValidate, ...
+      @getCheckBlocks, @viewContract, @annotateContract, ...
+			@getProps, @getPP,  @getCompiler};
  end
 
 function schema = getCheckBlocks(callbackInfo)     
@@ -143,6 +143,24 @@ function viewContractCallback(callbackInfo)
           display_msg(ME.getReport(),Constants.DEBUG,'viewContract','');
       end
     end
+
+% Function to annotate the Simulink model with the generated CoCoSpec
+function schema = annotateContract(callbackInfo)     
+  schema = sl_action_schema;
+  schema.label = 'Annotate with generated CoCoSpec (Experimental)'; 
+  schema.callback = @annotateContractCallback;
+ end
+
+  function annotateContractCallback(callbackInfo)
+  try 
+      [prog_path, fname, ext] = fileparts(mfilename('fullpath'));
+      simulink_name = gcs;
+      annotate_cocospec(simulink_name);
+
+  catch ME
+      disp(ME.message)
+  end
+ end
 
  function schema = getProps(callbackInfo)     
   schema = sl_action_schema;

src/annotate_cocospec.m

@@ -0,0 +1,86 @@
+function insert_embedded( model_full_path )
+	% Load the system
+	open_system(char(model_full_path));
+	[model_path, file_name, ext] = fileparts(model_full_path);
+	lus_path = [fileparts(which(file_name)) '/lustre_files/src_' file_name '/' file_name '.lus.coco'];
+
+	% Create CoCoSpec block
+	create_cocospec_block(file_name);
+
+	S = sfroot;
+	B = S.find('Name', 'CoCoSpec', '-isa', 'Stateflow.EMChart');
+
+	current_code = strread(B.Script, '%s', 'delimiter', sprintf('\n'));
+
+	fid = fopen(lus_path);
+
+	% Add CoCoSpec to code in Matlab function block
+	code = sprintf([current_code{1} '\n\n']);
+	while true
+		line = [fgets(fid)];
+		if ~ischar(line); break; end;
+		code = [code '% ' line];
+	end
+	code = [code sprintf('\n') current_code{numel(current_code)}];
+
+	% Write code to Matlab function block
+	B.Script = code;
+
+	fclose(fid);
+end
+
+%% Creates the CoCoSpec block object
+function cocospec = create_cocospec_block(file_name)
+	% Create block
+	observer_path = [file_name '/CoCoSpec'];
+	observer = add_block('simulink/User-Defined Functions/MATLAB Function', observer_path);
+	% Set block position
+	obs_pos = get_obs_position(file_name);
+	set_param(observer_path, 'Position', obs_pos);
+end
+
+%% Get the Position value according to the type of block
+function[out] = pos(offset_x, offset_y, port_type)
+% Block position settings
+y = 30;
+w = 30;
+if strcmp(port_type, 'Inport')
+	x = 30;
+	h = 15;
+elseif strcmp(port_type, 'Outport')
+	x = 400;
+	h = 15;
+elseif strcmp(port_type, 'Terminator')
+	x = 100;
+	h = 20;
+	w = 20;
+else
+	x = 30;
+	h = 30;
+end
+
+offset = 60;
+out = [x+offset*offset_x y+offset*offset_y x+offset*offset_x+w y+offset*offset_y+h];
+
+end
+
+%% Returns the Position parameter value for the Observer to be generated
+function [obs_pos] = get_obs_position(parent_subsystem)
+	blocks = find_system(parent_subsystem, 'SearchDepth', 1, 'FindAll', 'on', 'Type', 'Block');
+	positions = get_param(blocks, 'Position');
+	max_x = 0;
+	min_x = 0;
+	max_y = 0;
+	min_y = 0;
+	for idx_pos=1:numel(positions)
+		max_x = max(max_x, positions{idx_pos}(1));
+		if idx_pos == 1
+			min_x = positions{idx_pos}(1);
+			min_y = positions{idx_pos}(2);
+		else
+			min_x = min(min_x, positions{idx_pos}(1));
+			min_y = min(min_y, positions{idx_pos}(2));
+		end
+	end
+	obs_pos = [max_x max_y (max_x + 150) (max_y + 60)];
+end