1.3.3

decyphir · Jul 2, 2018 · 9f1bf01 · 9f1bf01
1 parent a496a4c
commit 9f1bf01
Show file tree

Hide file tree

Showing 21 changed files with 183 additions and 118 deletions.
diff --git a/@STL_Formula/STL_EvalThom.m b/@STL_Formula/STL_EvalThom.m
@@ -52,7 +52,8 @@
 end
 
 ii=1;
-eval_str = [P.ParamList;num2cell(1:numel(P.ParamList))];
+num_dim = size(P.pts,1); 
+eval_str = [P.ParamList(1:num_dim);num2cell(1:num_dim)];
 eval_str = sprintf('%s=P.pts(%d,ii);',eval_str{:});
 eval(eval_str);
 

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,3 +1,13 @@
+# Release 1.3.3
+
+- Fixed violation signals for alw (A => ev_[] B) types of requirements
+- BrDemo are now all working with BreachRequirement class
+- BreachProblem supports pre-conditions of BreachRequirement, treated
+  as hard constraint for optimization
+- Simulation is correctly skipped when pre-conditions on inputs only are not
+  satisfied 
+- overshoot requirement example added as alw (A=> ev_[] B) example for AFC
+
 # Release 1.3.2
 
 - plot_diagnosis now considers alw (A => ev_[] B) types of formulas 

diff --git a/Core/Algos/@BreachProblem/BreachProblem.m b/Core/Algos/@BreachProblem/BreachProblem.m
@@ -60,7 +60,7 @@
         Spec
         T_Spec=0
         constraints_fn    % constraints function
-        robust_fn   % base robustness function - typically the robust satisfaction of some property by some trace
+        robust_fn           % base robustness function - typically the robust satisfaction of some property by some trace
     end
 
     % properties related to the function to minimize
@@ -234,7 +234,7 @@ function ResetObjective(this, BrSet)
             rfprintf_reset();
 
             % robustness
-            this.BrSys = this.BrSet.copy(); 
+            this.BrSys = BrSet.copy(); 
             this.robust_fn = @(x) (this.Spec.Eval(this.BrSys, this.params, x));
 
             this.BrSet_Best = [];
@@ -583,7 +583,6 @@ function SetupDiskCaching(this, varargin)
              if size(x,1) ~= numel(this.params)
                 x = x';
              end
-
 
             nb_eval =  size(x,2);
             fval = inf*ones(1, nb_eval);
@@ -657,7 +656,7 @@ function SetupDiskCaching(this, varargin)
 
         function b = stopping(this)
             b =  (this.time_spent > this.max_time) ||...
-                    (this.nb_obj_eval> this.max_obj_eval) ;
+                    (this.nb_obj_eval> this.max_obj_eval);
         end
 
         %% Misc methods
@@ -766,26 +765,45 @@ function Display_Best_Results(this, best_fval, param_values)
          function summary = SaveResults(this, varargin)
             BLog = this.GetBrSet_Logged();   
             summary = BLog.SaveResults(varargin{:});
+         end
+
+        function Rlog = GetLog(this,varargin)
+            Rlog = this.GetBrSet_Logged(varargin{:});
         end
-            
+
     end
 
     methods (Access=protected)
 
         function display_status_header(this)
-            fprintf(  '#calls (max:%5d)           time spent (max: %g)           best                         obj\n',...
-                this.max_obj_eval, this.max_time);
+            if ~isempty(this.Spec.precond_monitors)
+                fprintf(  '#calls (max:%5d)           time spent (max: %g)           best                         obj                    constraint\n',...
+                    this.max_obj_eval, this.max_time);
+            else
+                fprintf(  '#calls (max:%5d)           time spent (max: %g)           best                         obj\n',...
+                    this.max_obj_eval, this.max_time);
+            end
         end
 
-        function display_status(this,fval)
+        function display_status(this,fval, const_val)
 
             if ~strcmp(this.display,'off')
                 if nargin==1
                     fval = this.obj_log(end); % bof bof
+                    if ~isempty(this.Spec.precond_monitors)
+                        const_val = min(min(this.Spec.traces_vals_precond));
+                    end
                 end
 
-                st__= sprintf('    %5d                   %7.1f                            %+5.5e             %+5.5e\n', ...
+                st__= sprintf('    %5d                        %7.1f                            %+5.5e             %+5.5e', ...
                     this.nb_obj_eval, this.time_spent, this.obj_best, fval);
+                if exist('const_val', 'var')
+                    st__ = sprintf([st__ '          %+5.5e\n'], const_val);
+                else
+                    st__ = [st__ '\n'];  
+                end
+
+
                 switch this.display
                     case 'on'
                         fprintf(st__);
@@ -798,9 +816,14 @@ function display_status(this,fval)
         function [BrOut, Berr,  BbadU] = ExportBrSet(this,B)
             % ExportBrSet prepares a BreachSet such as best, logged, etc to be
             % returned
-            B.Sys.Verbose=1;
             Berr = [];
             BbadU = [];
+            if isempty(B)
+                BrOut = [];
+                return;
+            end
+             B.Sys.Verbose=1;
+
             [idx_ok, idx_sim_error, idx_invalid_input, st_status]  = B.GetTraceStatus();
 
             if ~isempty(idx_sim_error)||~isempty(idx_invalid_input)

diff --git a/Core/Algos/@BreachProblem/solve_binsearch.m b/Core/Algos/@BreachProblem/solve_binsearch.m
@@ -1,7 +1,7 @@
 function res = solve_binsearch(this)
 
 Sys = this.BrSys.Sys;
-phi = this.Spec;
+phi = STL_Formula(this.Spec.req_monitors{1}.formula_id);
 P = this.BrSet.P;
 opt = this.solver_options;
 

diff --git a/Core/Algos/@BreachProblem/solve_global_nelder_mead.m b/Core/Algos/@BreachProblem/solve_global_nelder_mead.m
@@ -43,7 +43,7 @@
                 % update the nb_obj_eval
                 this.nb_obj_eval = this.nb_obj_eval + output.funcCount;
                 this.X_log = [this.X_log output.logs];
-                if fval < 0 || this.nb_obj_val > this.max_obj_val
+                if fval < 0 || this.nb_obj_eval > this.max_obj_eval
                     cancel(F);
                     flag_Cont = false;
                     break;

diff --git a/Core/Algos/BreachCEGIS.m b/Core/Algos/BreachCEGIS.m
@@ -27,14 +27,12 @@ function solve(this)
                 fprintf('Synthesis step\n');
                 fprintf('--------------\n');
                 this.synth_pb.solve();
-                %BrSynth = this.synth_pb.GetBrSet_Best();
 
                 if isempty(this.synth_pb.obj_best<0)
                     fprintf('Couldn''t synthesize parameters.\n');
                     return
                 end
 
-
                 %% Falsification step
                 fprintf('Counter-Example step\n');
                 fprintf('--------------------\n');
@@ -47,7 +45,7 @@ function solve(this)
                 end
 
                 %% Update parameter synthesis problem
-                this.synth_pb.BrSet.Concat(BrFalse);
+                this.synth_pb.BrSet.Concat(BrFalse.BrSet);
                 this.synth_pb.ResetObjective();
                 this.synth_pb.BrSys.Sys.Verbose=0;
 

diff --git a/Core/Algos/FalsificationProblem.m b/Core/Algos/FalsificationProblem.m
@@ -126,22 +126,17 @@ function LogX(this, x, fval)
         end
 
         function [BrFalse, BrFalse_Err, BrFalse_badU] = GetBrSet_False(this)
-            BrFalse = [];
-            if this.log_traces&&~this.use_parallel 
-                BrFalse = this.BrSet_False;
-            else
+            BrFalse = this.BrSet_False;
+            if isempty(BrFalse)
                 [~, i_false] = find(this.obj_log<0);
                 if ~isempty(i_false)
                     BrFalse = this.BrSys.copy();
                     BrFalse.SetParam(this.params, this.X_log(:, i_false));
-                    if this.BrSys.UseDiskCaching
-                        BrFalse.Sim();
-                    end
+                    BrFalse.Sim();
                 end
-
-                [BrFalse, BrFalse_Err, BrFalse_badU] = this.ExportBrSet(BrFalse);
-
             end
+
+            [BrFalse, BrFalse_Err, BrFalse_badU] = this.ExportBrSet(BrFalse);
         end
 
         function DispResultMsg(this)

diff --git a/Core/Algos/MaxSatProblem.m b/Core/Algos/MaxSatProblem.m
@@ -4,7 +4,7 @@
     %  FalsificationProblem Properties
     %    BrSet_True -  BreachSet updated with falsifying parameter vectors
     %                   and traces whenever some are found
-    %    X_True     -  parameter values found falsifying the formula
+    %    X_true     -  parameter values found falsifying the formula
     %    StopAtTrue - (default: true) if true, will stop as soon as a falsifying
     %                   parameter is found.
     %
@@ -15,7 +15,7 @@
 
     properties
         BrSet_True
-        X_True
+        X_true
         StopAtTrue=false
     end
 
@@ -45,7 +45,7 @@
 
         function ResetObjective(this)
             ResetObjective@BreachProblem(this);
-            this.X_True = [];
+            this.X_true = [];
             this.BrSet_True = [];
         end
 
@@ -54,7 +54,7 @@ function ResetObjective(this)
         % if found.
         function [XTrue, res] = solve(this)
             res = solve@BreachProblem(this);
-            XTrue = this.X_True;
+            XTrue = this.X_true;
         end
 
         % Logging

diff --git a/Core/BreachOpenSystem.m b/Core/BreachOpenSystem.m
@@ -69,8 +69,10 @@ function Sim(this,tspan,U)
             this.P = ComputeTraj(Sys, this.P, tspan);
 
             this.CheckinDomainTraj();
-            this.dispTraceStatus();
-         end
+            if this.verbose>=1
+                this.dispTraceStatus();
+            end
+        end
 
         % we merge parameters of the input generator with those of the
         % system, but keep both BreachObjects
@@ -277,12 +279,15 @@ function SetInputSpec(this, varargin)
 
                 % if an inputspec is violated, sabotage U into NaN
                 if ~isempty(this.InputGenerator.Specs)
-                    rob = this.InputGenerator.CheckSpec();
-                    if rob<0
-                        this.InputGenerator.addStatus(1,'input_spec_false', 'A specification on inputs is not satisfied.')
-                        U.t=NaN;
-                        U.u=NaN;
-                        return;
+                    Uspecs = this.InputGenerator.Specs.values();
+                    for ip = 1:numel(Uspecs)
+                        rob = this.InputGenerator.CheckSpec(Uspecs{ip});
+                        if rob<0
+                            this.InputGenerator.addStatus(1,'input_spec_false', 'A specification on inputs is not satisfied.')
+                            U.t=NaN;
+                            U.u=NaN;
+                            return;
+                        end
                     end
                 end