1.11.0

.gitignore

@@ -41,3 +41,7 @@ docrun_backup.mat
 *_ert_rtw
 *.7z
 *.slxc
+/Online/onlineMonitorlib.a
+AbstractFuelControl_breach_acc.*
+Examples/Wordgen/driving_TA.pcmp
+Examples/Wordgen/res.txt

@STL_Formula/STL_Break.m

@@ -1,4 +1,4 @@
-function [out, num_op, num_nested_temp_op]  = STL_Break(phi, n)
+function [out, num_op, num_nested_temp_op]  = STL_Break(phi, n, skip_params)
 % STL_BREAK breaks a formula into subformulas
 %
 %  Synopsys:  out = STL_Break(phi, [n])
@@ -38,6 +38,7 @@
 
 if nargin==1
     n = inf;
+    skip_params = false;
 end
 
 if n <= 0

@STL_Formula/STL_Culprit.m

@@ -88,7 +88,7 @@
     t = tau*ones(1,numParamSet);
     [mu{:}] = deal(phi); % fill mu with phi
     for ii = 1:numParamSet
-        traj_time = P.traj{P.traj_ref(ii}).time;
+        traj_time = P.traj{P.traj_ref(ii)}.time;
         idx(ii) = find(traj_time>=tau,1,'first'); % index of tau if tau belong in traj_time
         if isempty(idx(ii))
             idx(ii) = traj_time(end); % there is no time point higher than tau
@@ -107,7 +107,7 @@
     %
     mus = STL_ExtractPredicates(phi);
     for ii = 1:numParamSet % for each param set
-        traj = P.traj{P.traj_ref(ii});
+        traj = P.traj{P.traj_ref(ii)};
         Pi = Sselect(P,ii);
         found = false;
         jj = 1;

CHANGELOG.md

@@ -1,3 +1,8 @@
+# Release 1.11.0
+- Coverage features, to be documented
+- GUI stuff, tbdocu itou
+- Fixes and stuff, tbdocu too but less
+
 # Release 1.10.0
 - updated README.md
 - **really** updated README.md

Core/Algos/@BreachProblem/BreachProblem.m

@@ -73,7 +73,7 @@
     end
 
     % properties related to the function to minimize
-    properties
+    properties 
         BrSet
         BrSys         % BreachSystem - reset for each objective evaluation
         BrSet_Best    
@@ -133,8 +133,6 @@
         display = 'on'        
         use_parallel = 0
         max_time = inf
-        time_start = tic
-        time_spent = 0
         nb_obj_eval = 0
         max_obj_eval = 300
         num_constraints_failed = 0
@@ -143,6 +141,11 @@
         mixed_integer_optim_solvers = {'ga'};
     end
 
+    properties (Hidden=true)
+        time_start = tic
+        time_spent = 0        
+    end
+
     %% Static Methods
     methods (Static)
 
@@ -537,6 +540,20 @@ function set_stochastic_params(this, sparams, sdomains)
             this.solver_options = solver_opt;
         end
 
+        function solver_opt = setup_turbo(this, varargin)
+            this.solver = 'turbo';
+            %this.solver_options.num_corners = length(this.ub);
+            solver_opt.lb = this.lb;
+            solver_opt.ub = this.ub;
+            solver_opt.start_sample = [];
+            solver_opt.start_function_values = [];
+            solver_opt.use_java_runtime_call = 1;
+            solver_opt= varargin2struct_breach(solver_opt, varargin{:});   
+
+            this.display = 'on';
+            this.solver_options = solver_opt;
+        end
+
         function solver_opt = setup_gnmLausen(this)
             %disp('Setting options for GNM Lausen solver - use help gnm for details');
 %             solver_opt = saoptimset('Display', 'off');
@@ -719,21 +736,18 @@ function set_stochastic_params(this, sparams, sdomains)
                     res = struct('x',x, 'fval',fval, 'counteval', counteval,  'stopflag', stopflag, 'out', out, 'bestever', bestever);
                     this.add_res(res);
 
-                 case 'gnmLausen'
-                    [x, fval, output, used_options] = gbnm(this.objective,this.lb,this.ub,this.solver_options);     
+                case 'turbo'
+                    res = this.solve_turbo();
+
+                case 'gnmLausen'
+                    [x, fval, output, used_options] = gbnm(this.objective,this.lb,this.ub,this.solver_options);
                     res = struct('x', output.usedPoints, 'fval', output.usedVals,...
                         'counteval', output.nEval, 'output', output, 'used_options', used_options);
-%                     === example of output for 2D problem:
-%                     usedPoints: [2×30 double]
-%                     usedVals: [1×30 double]
-%                     usedSimplex: {1×30 cell}
-%                     reason: {1×15 cell}
-%                     nEval: 831
                     this.add_res(res);
 
-
+                    
                 case 'meta'
-                    res = this.solve_meta();        
+                    res = this.solve_meta();
 
                 case 'ga'
                     res = solve_ga(this, problem);
@@ -784,16 +798,6 @@ function set_stochastic_params(this, sparams, sdomains)
                         [x,fval,exitflag,output] = feval(this.solver, problem);
                         res = struct('x',x,'fval',fval, 'exitflag', exitflag, 'output', output);                        
 
-%                         num_works = this.BrSys.Sys.Parallel;
-%                         for idx = 1:num_works
-%                             F(idx) = parfeval(this.solver, 4, problem);
-%                         end
-%                         res = cell(1,num_works);
-%                         for idx = 1:num_works
-%                             [completedIdx, x, fval,exitflag,output] = fetchNext(F);
-%                             this.nb_obj_eval = this.nb_obj_eval + output.funccount;
-%                             res{completedIdx} = struct('x',x,'fval',fval, 'exitflag', exitflag, 'output', output);
-%                         end
                     else
                         [x,fval,exitflag,output] = feval(this.solver, problem);
                         res = struct('x',x,'fval',fval, 'exitflag', exitflag, 'output', output);                        
@@ -832,8 +836,6 @@ function set_stochastic_params(this, sparams, sdomains)
                             end
                         end
 
-
-
                         % Store if it's best
                         if min(rob) < fbest
                             xbest = x;
@@ -849,9 +851,13 @@ function set_stochastic_params(this, sparams, sdomains)
                         end
 
                         % Exit if robustness negative
-                        if this.StopAtFalse && min(rob) < 0 
-                            disp(['FALSIFIED at sample ' num2str(iterationCounter) '!']);
-                            break
+
+                        if min(rob)<0 
+                            this.StopAtFalse = this.StopAtFalse-1;                        
+                            if this.StopAtFalse==1 && min(rob) < 0
+                                disp(['FALSIFIED at sample ' num2str(iterationCounter) '!']);
+                                break
+                            end
                         end
                     end
                     res = struct('bestRob',[],'bestSample',[],'nTests',[],'bestCost',[],'paramVal',[],'falsified',[],'time',[]);
@@ -866,9 +872,7 @@ function set_stochastic_params(this, sparams, sdomains)
                     this.add_res(res);
 
             end
-            % TESTRON: Mute these outputs
             this.DispResultMsg(); 
-            %this.Display_Best_Results(this.obj_best, this.x_best);
 
             %% Saving run in cache folder
             this.SaveInCache();
@@ -1048,8 +1052,7 @@ function SetupDiskCaching(this, varargin)
             this.BrSys.SetupDiskCaching(varargin{:});
         end
 
-        %% Objective function and wrapper        
-
+        %% Objective function and wrapper                
         function [obj, cval, x_stoch] = objective_fn(this,x)
 
             % reset this.Spec
@@ -1354,6 +1357,25 @@ function Display_Best_Results(this, best_fval, param_values)
             end
         end
 
+
+%% Display function
+
+         function varargout = disp_variables(this)
+            variables = list_manip.to_string(this.params);
+
+
+
+            st = sprintf('Variables:  %s. \n',variables);
+
+            if nargout == 0
+                varargout = {};
+                fprintf(st);
+            else
+                varargout{1} = st;
+            end                      
+
+        end
+
     end
 
     methods (Access=protected)

Core/Algos/@BreachProblem/solve_binsearch.m

@@ -39,5 +39,5 @@
 this.X_log = p;
 this.obj_log = rob;
 this.BrSet.SetParam(this.params, p, true);
-this.BrSet.CheckSpec(phi);
+%this.BrSet.CheckSpec(phi);
 end

Core/Algos/@BreachProblem/solve_turbo.m

@@ -0,0 +1,129 @@
+function res = solve_turbo(this)
+
+%% Initialization of the parameters
+fcn = 'turbo_wrapper';
+numberOfIterations = 1; % Counter to count the number of iterations
+maxNumberOfIterations = this.max_obj_eval ;   % limit on the number of iterations
+lower_bound = this.lb;  % lower bound
+upper_bound = this.ub;  % upper bound
+lengthOfInputVector = length(upper_bound);
+xbest = [];
+fbest = [];
+
+%% Saving the necessary data in a json file, "scenarion.json", by calling SavingAllDataInJsonFolderTurbo.m
+SavingAllDataInJsonFolderTurbo(lower_bound, upper_bound, maxNumberOfIterations)
+
+% Share files between MATLAB and turbo
+nameOfInputFile = 'turboToMatlab.csv';
+nameOfFileToWaitFor = 'turboFinishedWriting.dummy';
+nameOfOutputFile = 'matlabToTurbo.csv'; % The name to save objective value values in a csv file
+nameOfTurboWaitFile = 'matlabFinishedWriting.dummy';
+nameOfMatlabInitDataFile = 'initDataFromMatlabToTurbo.csv';
+
+% Make sure the files don't exist to begin with
+if exist(nameOfInputFile, 'file')
+    delete(nameOfInputFile);
+end
+if exist(nameOfFileToWaitFor, 'file')
+    delete(nameOfFileToWaitFor);
+end
+if exist(nameOfOutputFile, 'file')
+    delete(nameOfOutputFile);
+end
+if exist(nameOfTurboWaitFile, 'file')
+    delete(nameOfTurboWaitFile);
+end
+if exist(nameOfMatlabInitDataFile, 'file')
+    delete(nameOfMatlabInitDataFile);
+end
+
+% Write initial data to .csv file
+M = [this.solver_options.start_sample' , ...
+    this.solver_options.start_function_values'];
+csvwrite(nameOfMatlabInitDataFile, M);
+
+%% Main loop:
+% Running main turbo_optimization.py file in python that runs the turbo in the background
+
+turboPythonFileLocation = which('turbo_optimization.py');
+if isempty(turboPythonFileLocation)
+    error('Cannot find turbo_optimization.py. Make sure to add turbo_optimization.py to MATLAB path');
+end
+
+% Note: Using java runtime to run turbo will not open up a command window,
+% which is cleaner, but we also don't access the output from turbo.
+% To access output from turbo, use system() to call the python script
+% instead.
+if this.solver_options.use_java_runtime_call
+    runtime = java.lang.Runtime.getRuntime();
+    process = runtime.exec(sprintf('python %s', ...
+        turboPythonFileLocation));
+else
+    [status, commandOut] = system(sprintf('python %s &', ...
+        turboPythonFileLocation));
+end
+
+%% Main loop to calculate the objective function value in Breach
+while (numberOfIterations <= maxNumberOfIterations)  % While loop over the number of iteration to search falsified point
+
+    while ~exist(nameOfFileToWaitFor, 'file') % While loop to wait until that input value be generated from Turbo and saved in a csv file
+        pause(1);
+    end
+
+    inputValue = csvread(nameOfInputFile);    % Reading input values saved in a csv file
+    delete(nameOfInputFile);
+    delete(nameOfFileToWaitFor);
+
+    if length(inputValue) ~= lengthOfInputVector  % Make sure that the number of dimensions is true
+        error('Wrong number of dimensions in input file %s', nameOfInputFile);
+    end
+
+    objectValue = feval(fcn, inputValue, this); % Calculating the objective function value for the current input value
+
+     % Check to see that objective value is negative or not
+    if objectValue < 0
+        xbest  = inputValue ;
+        fbest = objectValue;
+        break;
+    end
+
+    % saving the objective value in a csv file
+    fileIdOut = fopen(nameOfOutputFile, 'w'); 
+    fprintf(fileIdOut,'%4.4f\n', objectValue);
+    fclose(fileIdOut); % Closing the csv file
+
+    % Write file to tell Turbo that MATLAB is finished writing
+    fclose(fopen(nameOfTurboWaitFile, 'w'));
+
+    %disp("The number of evaluation is:  " + numberOfIterations) % Displaying the number of evaluation
+    numberOfIterations = numberOfIterations + 1; %Increasing the number of iterations
+
+end
+
+% Saving the point with lowest objective value 
+if isempty(xbest)
+    xbest = this.x_best;
+    fbest = this.obj_best;
+end
+
+res = struct('bestRob',[],'bestSample',[],'nTests',[],'bestCost',[],'paramVal',[],'falsified',[],'time',[]);
+res.bestSample = xbest;
+res.bestRob = fbest;
+
+% Clean up files
+if exist(nameOfInputFile, 'file')
+    delete(nameOfInputFile);
+end
+if exist(nameOfFileToWaitFor, 'file')
+    delete(nameOfFileToWaitFor);
+end
+if exist(nameOfMatlabInitDataFile, 'file')
+    delete(nameOfMatlabInitDataFile);
+end
+
+if this.solver_options.use_java_runtime_call
+    % Kill python process
+    process.destroy();
+end
+
+end

Core/Algos/FalsificationProblem.m

@@ -5,8 +5,8 @@
     %    BrSet_False -  BreachSet updated with falsifying parameter vectors
     %                   and traces whenever some are found
     %    X_false     -  parameter values found falsifying the formula
-    %    StopAtFalse - (default: true) if true, will stop as soon as a falsifying
-    %                   parameter is found.
+    %    StopAtFalse - (default: 1)  number of counter example to find
+    %    before stopping. If not a finite integer, never stop 
     %
     %  FalsificationProblem Methods
     %    GetBrSet_False - returns BrSet_False
@@ -17,7 +17,7 @@
         BrSet_False
         X_false
         obj_false
-        StopAtFalse=true
+        StopAtFalse=1
         Rio_Mode
         Rio_Mode_log=[]
         val_max=inf
@@ -180,7 +180,13 @@ function LogX(this, x, fval, cval, x_stoch)
 
         function b = stopping(this)
             b =  this.stopping@BreachProblem();
-            b= b||(this.StopAtFalse&&any(this.obj_best<0));        
+
+            if this.StopAtFalse~=0 && ... % StopAtFalse is not false
+                rem(this.StopAtFalse,1)==0 &&...  % StopAtFalse is integer                    
+                this.StopAtFalse<=sum(this.obj_log<0) % found enough
+                b = true;
+            end
+
         end
 
         function [BrFalse, BrFalse_Err, BrFalse_badU] = GetFalse(this)