fix bugs

Author: hbourbouh

Dockerfile

@@ -1,3 +1,5 @@
+# This Dockerfile is not currently used for CoCoSim.
+# It's work in progress to support docker in the future
 FROM ubuntu:18.04 as builder
 
 

RELEASE_NOTES.md

@@ -1,3 +1,20 @@
+CoCoSim version 1.1 release notes
+===================================
+
+Release date
+------------
+
+May 29th, 2020
+
+List of features:
+----------------
+
+* This release contains many bug fixes to v1.0. 
+* Also some improvements on Stateflow compiler. 
+Stateflow flow chart algorithm was modified to speedup the verification time. On one example, we reduced verification time of a Stateflow flow chart from hours to seconds.
+* Add the option to choose which smt solver (Z3 or Yices2) will be used by Kind2.
+* We organized Matlab functions files in packages to avoid any conflicts in function names.
+
 CoCoSim version 1.0 release notes
 ===================================
 

doc/TROUBLESHOOTING.md

@@ -6,7 +6,7 @@ This document covers some common issues with CoCoSim, and how to solve them.
 Contact
 -------
 
-Please contact as at [email protected] with any issue. Or use Github issues reporting system.
+Please contact us at [email protected] with any issue. Or use Github issues reporting system.
 
 Installation issues
 -------------------
@@ -25,8 +25,19 @@ To call the function in Matlab Command Window:
 install_cocosim_lib(true)
 ```
 
+## Install script issues
+### Missing libraries:
 
-**Installing external tools (Kind2, Lustrec, etc ...):**
+**Error: gmb.h Cannot be found**
+
+you need to install libgmp3-dev 
+```
+apt-get install  libgmp3-dev
+```
+
+
+
+### Installing external tools (Kind2, Lustrec, etc ...):
 
 If running the script `cocosim2/scripts/install_cocosim` failed. You can install the tools manually and set their path in `cocosim2/tools/tools_config.m`.
 
@@ -42,3 +53,4 @@ change `osx` by `linux` if your machine is a linux machine.
 
 See [INSTALL.md](../INSTALL.md) 
 
+

src/backEnd/verification/+coco_nasa_verify/@ToLustreVerify/run_kind2.m

@@ -103,7 +103,9 @@
             return;
         end
         export_verif_results(model, verificationResults, xml_trace);
-        VerificationMenu.displayHtmlVerificationResultsCallbackCode(model);
+        VerificationMenu.displayHtmlVerificationResultsCallbackCode(model, ...
+            verificationResults, ...
+            fileparts(nom_lustre_file));
     catch me
         display_msg(me.getReport(), MsgType.DEBUG, 'toLustreVerify.run_kind2', '');
         display_msg('Something went wrong in Verification.', MsgType.ERROR, 'toLustreVerify.run_kind2', '');

src/middleEnd/+nasa_toLustre/+IR_pp/+stateflow_IR_pp/+stateflow_fields/confirm_actions_SFIR_pp.m

@@ -60,14 +60,16 @@
     else
         display_msg(...
             sprintf('To Disable parsing checks of Stateflow State/transition actions, go to: '),...
-            MsgType.WARNING, 'confirm_actions_SFIR_pp', '');
+            MsgType.RESULT, 'confirm_actions_SFIR_pp', '');
         display_msg('tools -> CoCoSim -> Preferences -> NASA Compiler Preferences -> Skip Stateflow parser check. ', ...
-            MsgType.WARNING, 'confirm_actions_SFIR_pp', '');
+            MsgType.RESULT, 'confirm_actions_SFIR_pp', '');
     end
 
     if isfield(new_ir, 'States')
-        new_ir.States = adapt_states(new_ir.States);
-        
+        [new_ir.States, skip] = adapt_states(new_ir.States);
+        if skip
+            return;
+        end
         for i=1:numel(new_ir.States)
             statePath = new_ir.States{i}.Path;
             % default transition
@@ -98,12 +100,12 @@
         end
     end
 end
-function states = adapt_states(states)
+function [states, skip] = adapt_states(states)
     states_keywords = {'en', 'du', 'ex'};
     states_fields = {'Entry', 'During', 'Exit'};
     % 'Bind', 'On', 'OnAfter', ...
     %     'OnBefore', 'OnAt', 'OnEvery'};
-    
+    skip = false;
     for i=1:numel(states)
         statePath = states{i}.Path;
         if isfield(states{i}, 'LabelString')...
@@ -139,9 +141,12 @@
                     fprintf('\n');
                 end
             end
-            prompt = 'Are all the above actions correct? Y/N [Y]: ';
+            prompt = sprintf('Are all the above actions correct?\nY(yes)/N(no)/S(skip all next actions) [Y]: ');
             str = input(prompt,'s');
-            if ~isempty(str) && strcmp(upper(str), 'N')
+            if ~isempty(str) && strcmpi(str, 'S')
+                skip = true;
+                return;
+            elseif ~isempty(str) && strcmpi(str, 'N')
                 for j=1:numel(states_fields)
                     f = states_fields{j};
                     if isfield(states{i}.Actions, f) ...

src/middleEnd/+nasa_toLustre/+utils/@SLX2LusUtils/get_lustre_dt.m

@@ -72,9 +72,17 @@
                 slx_dt = regexprep(slx_dt, 'Enum:\s*', '');
             end
             if isKey(TOLUSTRE_ENUMS_MAP, lower(slx_dt))
+                % Lustrec requires enums to be lower case
                 isEnum = true;
                 hasEnum = true;
                 Lustre_type = lower(slx_dt);
+            elseif isKey(TOLUSTRE_ENUMS_MAP, slx_dt)
+                % Kind2 does not require enums to be lower case
+                % CEX uses enums, therefore the original name should be
+                % respected
+                isEnum = true;
+                hasEnum = true;
+                Lustre_type = slx_dt;
             else 
                 isBus = coco_nasa_utils.SLXUtils.isSimulinkBus(char(slx_dt));
                 if isBus

src/middleEnd/+nasa_toLustre/ToLustreUnsupportedBlocks.m

@@ -149,7 +149,7 @@
     [ir_struct, ir_handle_struct_map, ir_json_path] = nasa_toLustre.IR_pp.internalRep_pp(ir_struct, 1, output_dir);
 
     % add enumeration from Stateflow and from IR
-    add_IR_Enum(ir_struct);
+    add_IR_Enum(ir_struct, lus_backend);
 
     %% Unsupported blocks detection
     if skip_unsupportedblocks
@@ -178,17 +178,20 @@
     end
     %% display report files
     if isempty(unsupportedOptions)
+        msg = sprintf(['The model does not contain unsupported blocks.\n' ...
+            'Some blocks may be partially supported.\n'...
+            'When running verification or code generation, other errors may appear if some blocks are partially supported.']);
         if mode_display == 1
+            
             if exist('success.png', 'file')
                 [icondata,iconcmap] = imread('success.png');
-                msgbox('Your model is compatible with CoCoSim!','Success','custom',icondata,iconcmap);
+                msgbox(msg,'Success','custom',icondata,iconcmap);
             else
-                msgbox('Your model is compatible with CoCoSim!');
+                msgbox(msg);
             end
         end
         % display it too in command window.
-        display_msg('Your model is compatible with CoCoSim!', ...
-            MsgType.RESULT, 'ToLustreUnsupportedBlocks', '');
+        display_msg(msg, MsgType.RESULT, 'ToLustreUnsupportedBlocks', '');
 
     elseif mode_display == 1
         try
@@ -281,14 +284,18 @@
 
 
 %% add enumeration from IR
-function add_IR_Enum(ir)
+function add_IR_Enum(ir, lus_backend)
     global TOLUSTRE_ENUMS_MAP TOLUSTRE_ENUMS_CONV_NODES;
     if isfield(ir, 'meta') && isfield(ir.meta, 'Declarations') ...
             && isfield(ir.meta.Declarations, 'Enumerations')
         enums = ir.meta.Declarations.Enumerations;
         for i=1:numel(enums)
-            % put the type name in LOWER case: Lustrec limitation
-            name = lower(enums{i}.Name);
+            if coco_nasa_utils.LusBackendType.isKIND2(lus_backend)
+                name = enums{i}.Name;
+            else
+                % put the type name in LOWER case: Lustrec limitation
+                name = lower(enums{i}.Name);
+            end
             if isKey(TOLUSTRE_ENUMS_MAP, name)
                 continue;
             end

src/utils/+coco_nasa_utils/@MenuUtils/createHtmlListUsingHTMLITEM.m

@@ -52,7 +52,7 @@
     if ~exist(output_dir, 'dir')
         coco_nasa_utils.MatlabUtils.mkdir(output_dir);
     end
-    cocoSim_path = regexprep(mfilename('fullpath'), 'cocosim2/.+', 'cocosim2');
+    cocoSim_path = fileparts(which('start_cocosim'));
     % read template
     html_text = fileread(fullfile(cocoSim_path, 'src', 'backEnd' , 'html_templates' , 'item_list.html'));