1.8.0

decyphir · Sep 24, 2020 · 6843cff · 6843cff
1 parent 178fd96
commit 6843cff
Show file tree

Hide file tree

Showing 93 changed files with 1,058 additions and 271 deletions.
diff --git a/@STL_Formula/STL_Break.m b/@STL_Formula/STL_Break.m
@@ -1,4 +1,4 @@
-function out = STL_Break(phi, n)
+function [out, num_op, num_nested_temp_op]  = STL_Break(phi, n)
 % STL_BREAK breaks a formula into subformulas
 %
 %  Synopsys:  out = STL_Break(phi, [n])
@@ -33,12 +33,14 @@
 %          [ ev ((x1[t]<1.0) and (not (x2[t]<3.0))) ]
 
 out = [];
+num_op=0; 
+num_nested_temp_op=0;
 
 if nargin==1
     n = inf;
 end
 
-if n <= 0;
+if n <= 0
     return;
 end
 
@@ -47,12 +49,36 @@
     case 'predicate'
         out = phi;
 
-    case {'not', 'always', 'eventually'}
+    case 'not' 
+        [out1, num_op1, num_nested_temp_op1]  = STL_Break(phi.phi, n-1);
 
-        out = [STL_Break(phi.phi, n-1) phi] ;
+        out = [out1 phi] ;
+        num_op = num_op1+1;
+        num_nested_temp_op= num_nested_temp_op1;
+
+    case{'always', 'eventually', 'historically', 'once'}
+        [out1, num_op1, num_nested_temp_op1]  = STL_Break(phi.phi, n-1);
+
+        out = [out1 phi] ;
+        num_op = num_op1+1;
+        num_nested_temp_op= num_nested_temp_op1+1;        
+
+    case {'and', 'or', '=>'}
+        [out1, num_op1, num_nested_temp_op1]  = STL_Break(phi.phi1, n-1);
+        [out2, num_op2, num_nested_temp_op2]  = STL_Break(phi.phi2, n-1);
+
+        out = [out1 out2 phi] ;
+        num_op = num_op1+num_op2+1;
+        num_nested_temp_op= max(num_nested_temp_op1, num_nested_temp_op2);        
+
+    case 'until'
+
+        [out1, num_op1, num_nested_temp_op1]  = STL_Break(phi.phi1, n-1);
+        [out2, num_op2, num_nested_temp_op2]  = STL_Break(phi.phi2, n-1);
 
-    case {'and', 'or', '=>', 'until'}
-        out = [STL_Break(phi.phi1, n-1) STL_Break(phi.phi2, n-1) phi];
+        out = [out1 out2 phi] ;
+        num_op = num_op1+num_op2+1;
+        num_nested_temp_op= max(num_nested_temp_op1, num_nested_temp_op2)+1;        
 end
 
 % parameters 

diff --git a/@STL_Formula/STL_EvalThom.m b/@STL_Formula/STL_EvalThom.m
@@ -52,7 +52,7 @@
 end
 
 ii=1;
-num_dim = size(P_.pts,1); 
+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);
@@ -96,15 +96,15 @@
         [val, time_values] = GetValues(Sys_, phi_, Pii, traj, interval);
 
         try
-            if(numel(t)==1) % we handle singular times
-                val__{ii} = val(1);
-            else
+ %           if(numel(t)==1) % we handle singular times
+ %               val__{ii} = val(1);
+ %           else
                 if isfield(BreachGlobOpt, 'disable_robust_linear_interpolation')&&BreachGlobOpt.disable_robust_linear_interpolation
                     val__{ii} = interp1(time_values, val, t, 'previous');
                 else
                     val__{ii} = interp1(time_values, val, t);
                 end
-            end
+ %           end
         catch % if val is empty
             val__{ii} = NaN(1,numel(t));
         end
@@ -220,7 +220,50 @@
             valarray1 = [valarray1 valarray1(end)];
         end
         [time_values, valarray] = RobustEv(time_values1, valarray1, I___);
+
+    case 'once'
+        I___ = eval(phi.interval);
+        I___ = max([I___; 0 0]);
+        I___(1) = min(I___(1), I___(2));
+
+        next_interval = interval-[I___(1)+I___(2), I___(1)];
+        next_interval(1) = max(0, next_interval(1));        
+        [valarray1, time_values1] = GetValues(Sys, phi.phi, P, traj, next_interval);
 
+        % Flipping time, taking into account constant interpolation with
+        % previous 
+        Tend__ =  time_values1(end)+1; 
+        past_time_values1 = fliplr(Tend__-[time_values1 Tend__]);
+        past_valarray1 =    fliplr([valarray1(1) valarray1]);
+
+        [past_time_values, past_valarray] = RobustEv(past_time_values1, past_valarray1, I___);    
+
+        % Flipping back
+        time_values = fliplr(Tend__-[past_time_values Tend__]);
+        valarray = fliplr([past_valarray(1) past_valarray]);        
+
+    case 'historically'
+        I___ = eval(phi.interval);
+        I___ = max([I___; 0 0]);
+        I___(1) = min(I___(1), I___(2));
+
+        next_interval = interval-[I___(1)+I___(2), I___(1)];
+        next_interval(1) = max(0, next_interval(1));        
+        [valarray1, time_values1] = GetValues(Sys, phi.phi, P, traj, next_interval);        
+
+        % Flipping time, taking into account constant interpolation with
+        % previous 
+        Tend__ =  time_values1(end)+1; 
+        past_time_values1 = fliplr(Tend__-[time_values1 Tend__]);
+        past_valarray1 =    fliplr([valarray1(1) valarray1]);
+
+        [past_time_values, past_valarray] = RobustEv(past_time_values1, -past_valarray1, I___);    
+
+        % Flipping back
+        time_values = fliplr(Tend__-[past_time_values Tend__]);
+        valarray = -fliplr([past_valarray(1) past_valarray]);        
+
+
     case 'until'
         I___ = eval(phi.interval);
         I___ = max([I___; 0 0]);
@@ -256,14 +299,14 @@
     time_ok = time_values(~ibof);
     if ~isempty(val_ok)
         warning('STL_Eval:Inf_or_Nan', 'Some values are NaN or inf for property %s (use warning(''off'', ''STL_Eval:Inf_or_Nan'') to disable warning)', disp(phi));
-    if numel(val_ok)==1
-        valarray(1,:) = val_ok;
-    else
-        valarray = interp1(time_ok, val_ok, time_values, 'nearest');
-    end
+        if numel(val_ok)==1
+            valarray(1,:) = val_ok;
+        else
+            valarray = interp1(time_ok, val_ok, time_values, 'nearest');
+        end
     else
         warning('STL_Eval:Inf_or_Nan', 'All values are NaN or inf for property %s', disp(phi));
-    end     
+    end
 end
 
 
@@ -306,7 +349,7 @@
 
 % Last time instant
 if(interval(end)==inf)
-        time_values = [time_values traj.time(1,ind_ti:end)];
+    time_values = [time_values traj.time(1,ind_ti:end)];
 else
     ind_tf = find(traj.time >= interval(end),1);
     if isempty(ind_tf)

diff --git a/@STL_Formula/STL_EvalThom_Gen.m b/@STL_Formula/STL_EvalThom_Gen.m
@@ -100,15 +100,15 @@
         [val, time_values] = GetValues(Sys, phi, Pii, traj, partition, relabs, interval);
 
         try
-            if(numel(t)==1) % we handle singular times
-                val__{ii} = val(1);
-            else
+ %           if(numel(t)==1) % we handle singular times
+ %               val__{ii} = val(1);
+ %           else
                 if isfield(BreachGlobOpt, 'disable_robust_linear_interpolation')&&BreachGlobOpt.disable_robust_linear_interpolation
                     val__{ii} = interp1(time_values, val, t, 'previous');
                 else
                     val__{ii} = interp1(time_values, val, t);
                 end
-            end
+%            end
         catch % if val is empty
             val__{ii} = NaN(1,numel(t));
         end
@@ -251,6 +251,49 @@
         end
         [time_values, valarray] = RobustEv(time_values1, valarray1, I___);
 
+    case 'once'
+        I___ = eval(phi.interval);
+        I___ = max([I___; 0 0]);
+        I___(1) = min(I___(1), I___(2));
+
+        next_interval = interval-[I___(1)+I___(2), I___(1)];
+        next_interval(1) = max(0, next_interval(1));        
+
+        [valarray1, time_values1] = GetValues(Sys, phi.phi, P, traj, partition, relabs, next_interval);
+
+        % Flipping time, taking into account constant interpolation with
+        % previous 
+        Tend__ =  time_values1(end)+1; 
+        past_time_values1 = fliplr(Tend__-[time_values1 Tend__]);
+        past_valarray1 =    fliplr([valarray1(1) valarray1]);
+
+        [past_time_values, past_valarray] = RobustEv(past_time_values1, past_valarray1, I___);
+
+        % Flipping back 
+        time_values = fliplr(Tend__-[past_time_values Tend__]);
+        valarray = fliplr([past_valarray(1) past_valarray]);        
+
+    case 'historically'
+        I___ = eval(phi.interval);
+        I___ = max([I___; 0 0]);
+        I___(1) = min(I___(1), I___(2));
+
+        next_interval = interval-[I___(1)+I___(2), I___(1)];
+        next_interval(1) = max(0, next_interval(1));        
+
+        [valarray1, time_values1] = GetValues(Sys, phi.phi, P, traj, partition, relabs, next_interval);   
+
+        % Flipping time, taking into account constant interpolation with
+        % previous 
+        Tend__ =  time_values1(end)+1; 
+        past_time_values1 = fliplr(Tend__-[time_values1 Tend__]);
+        past_valarray1 =    fliplr([valarray1(1) valarray1]);        
+
+        [past_time_values, past_valarray] = RobustEv(past_time_values1, -past_valarray1, I___);
+        % Flipping back
+        time_values = fliplr(Tend__-[past_time_values Tend__]);
+        valarray = -fliplr([past_valarray(1) past_valarray]);        
+
     case 'until'
         I___ = eval(phi.interval);
         I___ = max([I___; 0 0]);
@@ -310,7 +353,11 @@
 % first time instant
 ind_ti = find(traj.time>=interval(1),1);
 if isempty(ind_ti)
-    time_values = [traj.time(1,end) traj.time(1,end)+1];
+    if ~isempty(traj.time)
+        time_values = [traj.time(1,end) traj.time(1,end)+1];
+    else
+        time_values = [];
+    end
     return
 end
 

diff --git a/@STL_Formula/STL_EvalThom_Gen_Rob.m b/@STL_Formula/STL_EvalThom_Gen_Rob.m
@@ -106,15 +106,15 @@
         [val, time_values, robustness_map] = GetValues(Sys, phi, Pii, traj, partition, relabs, interval, robustness_map);
 
         try
-            if(numel(t)==1) % we handle singular times
-                val__{ii} = val(1);
-            else
+%            if(numel(t)==1) % we handle singular times
+%                val__{ii} = val(1);
+%            else
                 if isfield(BreachGlobOpt, 'disable_robust_linear_interpolation')&&BreachGlobOpt.disable_robust_linear_interpolation
                     val__{ii} = interp1(time_values, val, t, 'previous');
                 else
                     val__{ii} = interp1(time_values, val, t);
                 end
-            end
+%            end
         catch % if val is empty
             val__{ii} = NaN(1,numel(t));
         end
@@ -274,6 +274,50 @@
         end
         [time_values, valarray] = RobustEv(time_values1, valarray1, I___);
 
+    case 'once'
+        I___ = eval(phi.interval);
+        I___ = max([I___; 0 0]);
+        I___(1) = min(I___(1), I___(2));
+
+        next_interval = interval-[I___(1)+I___(2), I___(1)];
+        next_interval(1) = max(0, next_interval(1));                
+        [valarray1, time_values1] = GetValues(Sys, phi.phi, P, traj, partition, relabs, next_interval, robustness_map);           
+
+        % Flipping time, taking into account constant interpolation with
+        % previous 
+        Tend__ =  time_values1(end)+1; 
+        past_time_values1 = fliplr(Tend__-[time_values1 Tend__]);
+        past_valarray1 =    fliplr([valarray1(1) valarray1]);        
+
+        [past_time_values, past_valarray] = RobustEv(past_time_values1, past_valarray1, I___);
+
+        % Flipping back
+        time_values = fliplr(Tend__-[past_time_values Tend__]);
+        valarray = fliplr([past_valarray(1) past_valarray]);        
+
+
+
+    case 'historically'
+        I___ = eval(phi.interval);
+        I___ = max([I___; 0 0]);
+        I___(1) = min(I___(1), I___(2));
+
+        next_interval = interval-[I___(1)+I___(2), I___(1)];
+        next_interval(1) = max(0, next_interval(1));                
+        [valarray1, time_values1] = GetValues(Sys, phi.phi, P, traj, partition, relabs, next_interval, robustness_map);   
+
+        % Flipping time, taking into account constant interpolation with
+        % previous 
+        Tend__ =  time_values1(end)+1; 
+        past_time_values1 = fliplr(Tend__-[time_values1 Tend__]);
+        past_valarray1 =    fliplr([valarray1(1) valarray1]);                
+
+        [past_time_values, past_valarray] = RobustEv(past_time_values1, -past_valarray1, I___);
+
+        % Flipping back
+        time_values = fliplr(Tend__-[past_time_values Tend__]);
+        valarray = -fliplr([past_valarray(1) past_valarray]);        
+
     case 'until'
         I___ = eval(phi.interval);
         I___ = max([I___; 0 0]);
@@ -341,7 +385,11 @@
 % first time instant
 ind_ti = find(traj.time>=interval(1),1);
 if isempty(ind_ti)
-    time_values = [traj.time(1,end) traj.time(1,end)+1];
+    if ~isempty(traj.time)
+        time_values = [traj.time(1,end) traj.time(1,end)+1];
+    else
+        time_values = [];
+    end    
     return
 end
 

diff --git a/@STL_Formula/STL_ExtractSignals.m b/@STL_Formula/STL_ExtractSignals.m
@@ -18,7 +18,7 @@
 for im=1:numel(matches)
     signals{end+1} = tokens{im}{1};
 end
-sreserved = {'alw_', 'ev_','until_'};
+sreserved = {'alw_', 'ev_','until_', 'once_', 'hist_'};
 signals = setdiff(signals, sreserved);
 
 
@@ -35,7 +35,7 @@
         end
     end
 
-    reserved = [ sreserved signals  {'alw', 'ev', 'and', 'or', '=>', 'not', 'until', 't', ...
+    reserved = [ sreserved signals  {'alw', 'ev','once', 'hist','and', 'or', '=>', 'not', 'until', 't', ...
         'abs', 'sin', 'cos', 'exp','tan', 'norm','sqrt'}];
     params = setdiff(params, reserved);
     params = unique(params);