From 42a9118b4d1d700528c209da4515b815c13632a1 Mon Sep 17 00:00:00 2001 From: Alex Date: Wed, 28 Mar 2018 18:26:28 +0200 Subject: [PATCH] 1.2.16 --- @STL_Formula/STL_EvalThom.m | 16 +++- @STL_Formula/private/generic_predicate.m | 10 ++- CHANGELOG.md | 22 ++++++ Contents.m | 2 +- Core/Algos/@BreachProblem/BreachProblem.m | 95 +++++++++++------------ Core/Algos/BreachCEGIS.m | 2 +- Core/Algos/FalsificationProblem.m | 21 +++-- Core/Algos/MaxSatProblem.m | 44 ++++++----- Core/BreachDomain.m | 10 +-- Core/BreachSet.m | 18 +++-- Core/BreachSimulinkSystem.m | 56 ++++++++----- Core/BreachSystem.m | 25 ++++-- Core/BreachTraceSystem.m | 5 ++ Core/ComputeTraj.m | 2 +- Core/CreateExternSystem.m | 3 +- Core/m_src/BreachStatus.m | 10 ++- Examples/+BrDemo/AFC_1_Interface.m | 10 +-- Examples/+BrDemo/AFC_2_Simulation.m | 16 ++-- Examples/+BrDemo/AFC_4_Specifications.m | 4 +- Examples/+BrDemo/Autotrans_tutorial.m | 3 +- Examples/+BrDemo/InitAFC.m | 3 +- Examples/Simulink/vdp/test_vdp.m | 17 +++- InitBreach.m | 5 ++ InstallBreach.m | 61 ++++++--------- Online/m_src/compile_stl_mex.m | 8 +- VERSION | 2 +- 26 files changed, 280 insertions(+), 190 deletions(-) diff --git a/@STL_Formula/STL_EvalThom.m b/@STL_Formula/STL_EvalThom.m index ebaed8bf..1087f261 100644 --- a/@STL_Formula/STL_EvalThom.m +++ b/@STL_Formula/STL_EvalThom.m @@ -44,8 +44,12 @@ % all subsequent computations global BreachGlobOpt; -BreachGlobOpt.GlobVarsDeclare = ['global ', sprintf('%s ',P.ParamList{:})]; % contains parameters and IC values (can remove IC if phi is optimized) -eval(BreachGlobOpt.GlobVarsDeclare); % These values may be used in generic_predicate and GetValues +if ~isempty(P.ParamList) + BreachGlobOpt.GlobVarsDeclare = ['global ', sprintf('%s ',P.ParamList{:})]; % contains parameters and IC values (can remove IC if phi is optimized) + eval(BreachGlobOpt.GlobVarsDeclare); % These values may be used in generic_predicate and GetValues +else + BreachGlobOpt.GlobVarsDeclare = ''; % contains parameters and IC values (can remove IC if phi is optimized) +end ii=1; eval_str = [P.ParamList;num2cell(1:numel(P.ParamList))]; @@ -94,7 +98,11 @@ if(numel(t)==1) % we handle singular times val__{ii} = val(1); else - val__{ii} = interp1(time_values, val, t); + 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 catch % if val is empty val__{ii} = NaN(1,numel(t)); @@ -269,7 +277,7 @@ % first time instant ind_ti = find(traj.time>=interval(1),1); -if isempty(ind_ti) +if isempty(ind_ti) time_values = [traj.time(1,end) traj.time(1,end)+1]; return end diff --git a/@STL_Formula/private/generic_predicate.m b/@STL_Formula/private/generic_predicate.m index cd861507..848c00e7 100644 --- a/@STL_Formula/private/generic_predicate.m +++ b/@STL_Formula/private/generic_predicate.m @@ -28,7 +28,11 @@ global BreachGlobOpt; eval(BreachGlobOpt.GlobVarsDeclare); -dt__ = traj.time(1,2)-traj.time(1,1); +if numel(traj.time)==1 + dt__ = 1; % not sure this makes sense, will see +else + dt__ = traj.time(1,2)-traj.time(1,1); +end Sys = params.Sys; P =params.P; @@ -59,8 +63,8 @@ fn_ = params.fn; % don't like that... But not so trivial to remove -traj.time = [-1e99 traj.time 1e99]; % NM: when fixing that, don't forget to change -traj.X = [traj.X(:,1) traj.X traj.X(:,end)]; % GetTrajSensi. +traj.time = [-1e99 traj.time 1e99]; +traj.X = [traj.X(:,1) traj.X traj.X(:,end)]; if isfield(traj,'XS') traj.XS = [traj.XS(:,1) traj.XS traj.XS(:,end)]; diff --git a/CHANGELOG.md b/CHANGELOG.md index f15a4700..5514e2f4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,25 @@ +# Release 1.2.16 +## Users +- printStatus now prints error message obtained during failed Simulink + simulation +- New SimInModelsDataFolder option, default to false (i.e., by + default, Breach won't change folder for simulalink simulations +- Changed default max_obj_eval to 100 and max_time to inf in BreachProblem + +## Bugfixes +- GetBrSet_Logged, _False, _True methods now works as expected in + serial and parallel (BreachTEMA Issue #33) +- DiskCaching matfiles writable option should improve stability +- Fixed interpolation bug in STL_EvalThom (Issue #62) +- Fixed bug in BreachTraceSystem with useless legacy Xf field +- ModelsData folders properly created at initialization if not + existant (BreachTEMA Issue #30) + +## Developpers +- log_traces field for BreachProblem now consistent with serial and + parallel (BreachTEMA Issue #31) +- StoreTracesOnDisk true by default for DiskCaching (BreachTEMA Issue #21) + # Release 1.2.15 ## Users diff --git a/Contents.m b/Contents.m index 99421b13..1605a853 100644 --- a/Contents.m +++ b/Contents.m @@ -1,4 +1,4 @@ -% Breach Toolbox v1.0-beta1 +% Breach Toolbox % % Files % InitBreach - Initializes Breach, in particular adding paths to Breach directories diff --git a/Core/Algos/@BreachProblem/BreachProblem.m b/Core/Algos/@BreachProblem/BreachProblem.m index 695b5ad7..3a9e112a 100644 --- a/Core/Algos/@BreachProblem/BreachProblem.m +++ b/Core/Algos/@BreachProblem/BreachProblem.m @@ -92,12 +92,12 @@ properties display = 'on' freq_update = 10 - use_parallel =0 - max_time = 60 + use_parallel = 0 + max_time = inf time_start = tic time_spent = 0 nb_obj_eval = 0 - max_obj_eval = inf + max_obj_eval = 100 end %% Static Methods @@ -466,9 +466,10 @@ function SetupParallel(this, varargin) this.BrSys.use_parallel = 0; this.BrSys.Sys.Parallel=0; - % Disable serial logging mechanism and enable DiskCaching - this.log_traces = 0; - this.SetupDiskCaching(); + % Enable DiskCaching + if this.log_traces + this.SetupDiskCaching(); + end end function StopParallel(this) @@ -546,7 +547,6 @@ function SetupDiskCaching(this, varargin) end %% Misc methods - function x = CheckinDomain(this,x) for ip = 1:numel(this.params) x(ip) = this.domains(ip).checkin(x(ip)); @@ -556,11 +556,10 @@ function SetupDiskCaching(this, varargin) function LogX(this, x, fval) % LogX logs values tried by the optimizer - x = this.CheckinDomain(x); this.X_log = [this.X_log x]; this.obj_log = [this.obj_log fval]; - if (this.log_traces) + if (this.log_traces)&&~(this.use_parallel); if isempty(this.BrSet_Logged) this.BrSet_Logged = this.BrSys.copy(); else @@ -609,7 +608,7 @@ function DispResultMsg(this) function [BrOut, Berr, BbadU] = GetBrSet_Logged(this) % GetBrSet_Logged gets BreachSet object containing parameters and traces computed during optimization - if this.log_traces + if this.log_traces&&~this.use_parallel % when this is true, BrSet_Logged is already a BreachSet with traces BrOut = this.BrSet_Logged; else BrOut = this.BrSys.copy(); @@ -619,23 +618,11 @@ function DispResultMsg(this) BrOut.Sim(); end end - BrOut.Sys.Verbose=1; - Berr =[]; - BbadU = []; - [idx_ok, idx_sim_error, idx_invalid_input, st_status] = BrOut.GetTraceStatus(); - - if ~isempty(idx_sim_error)||~isempty(idx_invalid_input) - [Bok, Berr, BbadU] = FilterTraceStatus(BrOut); - BrOut= Bok; - this.disp_msg(['Warning: ' st_status],1); - end - if ~isempty(idx_ok) - BrOut.CheckSpec(this.Spec); - end + [BrOut, Berr, BbadU] = this.ExportBrSet(BrOut); end - + function BrBest = GetBrSet_Best(this) BrBest = this.BrSet_Best; if isempty(BrBest) @@ -643,21 +630,11 @@ function DispResultMsg(this) BrBest.SetParam(this.params, this.x_best, 'spec'); BrBest.Sim(); end - BrBest.Sys.Verbose=1; - if BrBest.hasTraj() - BrBest.CheckSpec(this.Spec); - end - end - - function SetupLogFolder(this, fname) - if nargin<2 - this.BrSys.SetupLogFolder(); - else - this.BrSys.SetupLogFolder(fname); - end - this.log_traces= false; + + BrBest = this.ExportBrSet(BrBest); + end - + function display_status_header(this) fprintf( '#calls (max:%5d) time spent (max: %g) best obj\n',... this.max_obj_eval, this.max_time); @@ -670,11 +647,6 @@ function display_status(this,fval) fval = this.obj_log(end); % bof bof end -% if this.nb_obj_eval==1 -% this.display_status_header(); -% rfprintf_reset(); -% end - st__= sprintf(' %5d %7.1f %+5.5e %+5.5e\n', ... this.nb_obj_eval, this.time_spent, this.obj_best, fval); switch this.display @@ -686,6 +658,35 @@ function display_status(this,fval) end end + function new = copy(this) + % copy operator for BreachSet, works with R2010b or newer. + objByteArray = getByteStreamFromArray(this); + new = getArrayFromByteStream(objByteArray); + end + + end + + methods (Access=protected) + + function [BrOut, Berr, BbadU] = ExportBrSet(this,BrOut) + % ExportBrSet prepares a BreachSet such as best, logged, etc to be + % returned + BrOut.Sys.Verbose=1; + Berr =[]; + BbadU = []; + [idx_ok, idx_sim_error, idx_invalid_input, st_status] = BrOut.GetTraceStatus(); + + if ~isempty(idx_sim_error)||~isempty(idx_invalid_input) + [Bok, Berr, BbadU] = FilterTraceStatus(BrOut); + BrOut= Bok; + this.disp_msg(['Warning: ' st_status],1); + end + + if ~isempty(idx_ok)&&BrOut.hasTraj(); + BrOut.CheckSpec(this.Spec); + end + end + function [cmp, cmpSet, cmpSys, cmpBest, cmpLogged] = compare(this, other) % FIXME broken as per changes in BreachStatus cmp = BreachStatus(); @@ -715,11 +716,7 @@ function display_status(this,fval) end end - function new = copy(this) - % copy operator for BreachSet, works with R2010b or newer. - objByteArray = getByteStreamFromArray(this); - new = getArrayFromByteStream(objByteArray); - end - + end + end diff --git a/Core/Algos/BreachCEGIS.m b/Core/Algos/BreachCEGIS.m index 81939b26..726c968d 100644 --- a/Core/Algos/BreachCEGIS.m +++ b/Core/Algos/BreachCEGIS.m @@ -41,7 +41,7 @@ function solve(this) this.falsif_pb.BrSet.SetParam(this.synth_pb.params, this.synth_pb.x_best, true); this.falsif_pb.ResetObjective(); this.falsif_pb.solve(); - BrFalse = this.falsif_pb.BrSet_False; + BrFalse = this.falsif_pb.GetBrSet_False(); if isempty(BrFalse) return end diff --git a/Core/Algos/FalsificationProblem.m b/Core/Algos/FalsificationProblem.m index e3e971f6..dff7a9eb 100644 --- a/Core/Algos/FalsificationProblem.m +++ b/Core/Algos/FalsificationProblem.m @@ -78,7 +78,8 @@ function ResetObjective(this) % Logging function LogX(this, x, fval) - + % LogX log variable parameter value tested by optimizers + % Logging default stuff this.LogX@BreachProblem(x, fval); @@ -86,7 +87,7 @@ function LogX(this, x, fval) [~, i_false] = find(fval<0); if ~isempty(i_false) this.X_false = [this.X_false x(:,i_false)]; - if (this.log_traces) + if (this.log_traces)&&~this.use_parallel if isempty(this.BrSet_False) this.BrSet_False = this.BrSys.copy(); else @@ -97,14 +98,13 @@ function LogX(this, x, fval) end function b = stopping(this) - b = (this.time_spent >= this.max_time) ||... - (this.nb_obj_eval>= this.max_obj_eval) ||... - (this.StopAtFalse&&this.obj_best<0); + b = this.stopping@BreachProblem(); + b= b||(this.StopAtFalse&&this.obj_best<0); end - function BrFalse = GetBrSet_False(this) + function [BrFalse, BrFalse_Err, BrFalse_badU] = GetBrSet_False(this) BrFalse = []; - if this.log_traces + if this.log_traces&&~this.use_parallel BrFalse = this.BrSet_False; else [~, i_false] = find(this.obj_log<0); @@ -115,10 +115,9 @@ function LogX(this, x, fval) BrFalse.Sim(); end end - BrFalse.Sys.Verbose=1; - if isempty(BrFalse.InputGenerator.Specs)&&BrFalse.hasTraj() % TODO: change this when dealing with Input requirements/constraints - BrFalse.CheckSpec(this.Spec); - end + + [BrFalse, BrFalse_Err, BrFalse_badU] = this.ExportBrSet(BrFalse); + end end diff --git a/Core/Algos/MaxSatProblem.m b/Core/Algos/MaxSatProblem.m index 25e59dad..c2f10e2f 100644 --- a/Core/Algos/MaxSatProblem.m +++ b/Core/Algos/MaxSatProblem.m @@ -64,35 +64,43 @@ function LogX(this, x, fval) this.LogX@BreachProblem(x, fval); % Logging satisfying parameters and traces - if fval < 0 - this.X_True = [this.X_True x]; - if isempty(this.BrSet_True) - this.BrSet_True = this.BrSys.copy(); - else - this.BrSet_True.Concat(this.BrSys); - end - - if this.StopAtTrue == true - this.stopping = true; + [~, i_true] = find(fval>0); + if ~isempty(i_true) + this.X_true = [this.X_true x(:,i_true)]; + if (this.log_traces)&&~this.use_parallel + if isempty(this.BrSet_True) + this.BrSet_True = this.BrSys.copy(); + else + this.BrSet_True.Concat(this.BrSys); + end end end - end - function BrTrue = GetBrSet_True(this) - if this.log_traces - BrTrue = this.BrSet_False; + function b = stopping(this) + b = this.stopping@BreachProblem(); + b= b||(this.StopAtTrue&&this.obj_best>0); + end + + function [BrTrue, BrTrue_Err, BrTrue_badU] = GetBrSet_True(this) + BrTrue = []; + if this.log_traces&&~this.use_parallel + BrTrue = this.BrSet_True; else - [~, i_true] = find(this.obj_log>=0); - if ~isempty(i_true) + [~, i_false] = find(this.obj_log<0); + if ~isempty(i_false) BrTrue = this.BrSys.copy(); - BrTrue.SetParam(this.params, this.X_log(:, i_true)); - if ~isempty(this.BrSys.log_folder) + BrTrue.SetParam(this.params, this.X_log(:, i_false)); + if this.BrSys.UseDiskCaching BrTrue.Sim(); end end + [BrTrue, BrTrue_Err, BrTrue_badU] = this.ExportBrSet(BrTrue); + end + + end diff --git a/Core/BreachDomain.m b/Core/BreachDomain.m index 9d208ee7..59f84732 100644 --- a/Core/BreachDomain.m +++ b/Core/BreachDomain.m @@ -3,13 +3,11 @@ % % TODO error handling when intersection of domain and enum is empty % - - % properties - type='double' % can be 'int', 'bool', 'enum', 'double' + type='double' % can be 'int', 'bool', 'enum', 'double' domain % always be an interval, empty means singleton - enum % only used with type enum and 'bool' + enum % only used with type enum and 'bool' end methods @@ -288,13 +286,15 @@ x{ip} = dom.sample_rand(num_samples{ip}); elseif isequal(method{ip}, 'corners') x{ip} = [dom.domain(1) dom.domain(2)]; + else + error('Unknown sampling method: %s', method{ip}); end end num_x(ip) = numel(x{ip}); end - % Combine new samples + % Combine new samples --> this is where we need some smarts if num_dom>1 if combine_x idx = N2Nn(num_dom, num_x); diff --git a/Core/BreachSet.m b/Core/BreachSet.m index e00035bd..68bc422d 100644 --- a/Core/BreachSet.m +++ b/Core/BreachSet.m @@ -343,7 +343,7 @@ function SetParamRanges(this, params, ranges) % kept for backward compatibility with legacy stuff this.P.dim = i_params; - + this.CheckinDomainParam(); end function ranges = GetParamRanges(this, params) @@ -537,7 +537,15 @@ function dispTraceStatus(this) end if ischar(signals) || iscell(signals) - signals = FindParam(this.P, signals); + [signals_idx, type] = FindParam(this.P, signals); + if any(type==0) + not_found= find(type==0); + error('GetSignalValues:sig_not_found', 'Signal %s not found.',signals{not_found(1)}); + end + elseif isnumeric(signals) + signals_idx=signals; + else + error('GetSignalValues:signals_type', 'signals should be a string or cell of string or numeric array ') end if ~exist('itrajs','var') @@ -549,10 +557,10 @@ function dispTraceStatus(this) X = cell(nb_traj,1); for i_traj = 1:numel(itrajs) if (~exist('t','var')) - X{i_traj} = this.P.traj{itrajs(i_traj)}.X(signals,:); + X{i_traj} = this.P.traj{itrajs(i_traj)}.X(signals_idx,:); else - X{i_traj} = interp1(this.P.traj{itrajs(i_traj)}.time, this.P.traj{itrajs(i_traj)}.X(signals,:)',t)'; - if numel(signals)==1 + X{i_traj} = interp1(this.P.traj{itrajs(i_traj)}.time, this.P.traj{itrajs(i_traj)}.X(signals_idx,:)',t)'; + if numel(signals_idx)==1 X{i_traj} = X{i_traj}'; end end diff --git a/Core/BreachSimulinkSystem.m b/Core/BreachSimulinkSystem.m index d5b779b5..2bb6c092 100644 --- a/Core/BreachSimulinkSystem.m +++ b/Core/BreachSimulinkSystem.m @@ -32,10 +32,11 @@ FindTables = false FindStruct = false MaxNumTabParam - SimCmdArgs = {} % argument list passed to sim command - InputSrc % for each input, we match an input port or base workspace (0) - MdlVars % List of variables used by the model + SimCmdArgs = {} % argument list passed to sim command + InputSrc % for each input, we match an input port or base workspace (0) + MdlVars % List of variables used by the model SimInputsOnly=false % if true, will not run Simulink model + SimInModelsDataFolder=false mdl UseDiskCaching=false DiskCachingRoot @@ -107,6 +108,7 @@ function SetupOptions(this, varargin) options.FindTables = false; options.FindStruct = false; options.FindSignalBuilders = false; % TODO fixme when true + options.SimInModelsDataFolder = false; options.Parallel = 'off'; options.SimCmdArgs = {}; options.Verbose = 1; @@ -125,6 +127,7 @@ function SetupOptions(this, varargin) this.MaxNumTabParam = options.MaxNumTabParam; this.SimCmdArgs = options.SimCmdArgs; this.verbose = options.Verbose; + this.SimInModelsDataFolder = options.SimInModelsDataFolder; if ~isempty(options.InitFn) this.SetInitFn(options.InitFn); @@ -190,7 +193,7 @@ function SetupParallel(this, NumWorkers, varargin) end function StopParallel(this) - + this.StopParallel@BreachSystem(); poolobj = gcp('nocreate'); % If no pool, do not create new one. if ~isempty(poolobj) delete(poolobj); % not sure this is doing anything @@ -474,14 +477,21 @@ function StopParallel(this) assignin('base','t__',0); assignin('base','u__',zeros(1, numel(this.Sys.InputList))); assignin('base','tspan',tspan); - crd = pwd; - cd(crd); - try + if this.SimInModelsDataFolder; + crd = pwd; + cd(breach_data_dir); + end + try simout = sim(mdl_breach, this.SimCmdArgs{:}); catch MException - cd(crd); + if this.SimInModelsDataFolder; + cd(crd); + end rethrow(MException); end + if this.SimInModelsDataFolder; + cd(crd); + end %% find logged signals (including inputs and outputs) this.Sys.mdl= mdl_breach; @@ -735,18 +745,23 @@ function Sim(this, tspan, U) % status = 0; % optimistic default; - cwd = pwd; - if this.use_parallel - worker_id = get(getCurrentTask(), 'ID'); - cd([this.ParallelTempRoot filesep 'Worker' int2str(worker_id)]); - else - cd(this.mdl.mdl_breach_path); + if this.SimInModelsDataFolder + cwd = pwd; + if this.use_parallel + worker_id = get(getCurrentTask(), 'ID'); + if ~isinteger(worker_id) + worker_id = 1; + end + cd([this.ParallelTempRoot filesep 'Worker' int2str(worker_id)]); + else + cd(this.mdl.mdl_breach_path); + end end - mdl = Sys.mdl; load_system(mdl); num_signals = Sys.DimX; params = Sys.ParamList; + for i = 1:numel(params)-num_signals pname = params{i+num_signals}; pval = pts(i+num_signals); @@ -788,8 +803,10 @@ function Sim(this, tspan, U) simout= sim(mdl, this.SimCmdArgs{:}); [tout, X] = GetXFrom_simout(this, simout); end - catch MException + catch MException % TODO keep that in status message + if this.SimInModelsDataFolder cd(cwd); + end if numel(tspan)>1 tout = tspan; else @@ -797,14 +814,17 @@ function Sim(this, tspan, U) end X = zeros(Sys.DimX, numel(tout)); status =-1; + this.addStatus(-1, MException.identifier, MException.message); end % FIXME: the following needs to be reviewed if ~isempty(this.InputGenerator)&&this.use_precomputed_inputs==false this.InputGenerator.Reset(); end - cd(cwd) - + + if this.SimInModelsDataFolder + cd(cwd); + end end function [tout, X] = GetXFrom_simout(this, simout) diff --git a/Core/BreachSystem.m b/Core/BreachSystem.m index 590428f8..cd38f082 100644 --- a/Core/BreachSystem.m +++ b/Core/BreachSystem.m @@ -26,8 +26,8 @@ properties Sys % Legacy Breach system structure Specs % A set (map) of STL formulas - ParamSrc=containers.Map() - use_parallel=0 % the flag to indicate the usage of parallel computing + ParamSrc = containers.Map() + use_parallel = 0 % the flag to indicate the usage of parallel computing ParallelTempRoot = '' % the default temporary folder for parallel computing InitFn = '' % Initialization function end @@ -109,14 +109,29 @@ function SetupParallel(this, NumWorkers) cd(this.ParallelTempRoot) for ii = 1:NumWorkers dirName = ['Worker' int2str(ii)]; - if exist(dirName, 'dir') == 7 - rmdir(dirName,'s'); + if exist(dirName, 'dir') ~= 7 + mkdir(dirName); end - mkdir(dirName); + end cd(cwd) end + % clear up the ModelsData/ParallelTemp folder + function StopParallel(this) + cwd = pwd; + cd(this.ParallelTempRoot) + folders = dir(this.ParallelTempRoot); + names = {folders.name}; + % delete the path for the current folder and parent folder + names(ismember(names,{'.', '..'})) = []; + for ii = 1:length(names) + rmdir(names{ii}, 's'); + end + this.Sys.use_parallel = 0; + cd(cwd) + end + function this = SetInitFn(this,Fn) if isa(Fn, 'function_handle') f = functions(Fn); diff --git a/Core/BreachTraceSystem.m b/Core/BreachTraceSystem.m index 515213a7..548462cc 100644 --- a/Core/BreachTraceSystem.m +++ b/Core/BreachTraceSystem.m @@ -122,6 +122,11 @@ function AddTrace(this, trace) this.P.traj_to_compute = []; this.P.pts(this.P.DimX+1,:) = 1:nb_traces+1; % index traces this.Sys.tspan = traj.time; + if isfield(this.P, 'Xf') + this.P.Xf(:,end)= traj.X(:,end); + else + this.P.Xf= traj.X(:,end); + end end function AddRandomTraces(this,n_traces, n_samples, amp, end_time) diff --git a/Core/ComputeTraj.m b/Core/ComputeTraj.m index 8239acd6..cd0e81a8 100644 --- a/Core/ComputeTraj.m +++ b/Core/ComputeTraj.m @@ -333,7 +333,7 @@ traj.param = P0.pts(1:P0.DimP,ii)'; if use_caching % cache new trace - cache_traj = matfile(cache_traj_filename); + cache_traj = matfile(cache_traj_filename, 'Writable', true); cache_traj.param = traj.param; cache_traj.time = traj.time; cache_traj.status = traj.status; diff --git a/Core/CreateExternSystem.m b/Core/CreateExternSystem.m index 1bb66735..d3dc6d8c 100644 --- a/Core/CreateExternSystem.m +++ b/Core/CreateExternSystem.m @@ -38,8 +38,7 @@ for i=1:nparams params = {params{:} ['x' num2str(i)]}; - - end + end end end diff --git a/Core/m_src/BreachStatus.m b/Core/m_src/BreachStatus.m index f7e1f401..04301c1f 100644 --- a/Core/m_src/BreachStatus.m +++ b/Core/m_src/BreachStatus.m @@ -3,9 +3,12 @@ % of an algorithm properties - status = [] % unique integer id for the status - statusMap = containers.Map() % map with key and msg strings describing the status. verbose = 1 + end + + properties (Hidden) + status = [] % unique integer id for the status + statusMap = containers.Map() % map with key and msg strings describing the status. logged_msg max_logged_msg=100 end @@ -62,7 +65,8 @@ function setStatus(this, status, key, msg) for ist = 1:n_status new_st = ['[' keys{ist} ']']; msg = this.statusMap(keys{ist}); - new_st(24:24+numel(msg)-1) = msg; + %new_st(24:24+numel(msg)-1) = msg; % not sure why I had 24 here... + new_st = [new_st ' ' msg]; st = [st new_st '\n']; end diff --git a/Examples/+BrDemo/AFC_1_Interface.m b/Examples/+BrDemo/AFC_1_Interface.m index b9be84fa..2980670f 100644 --- a/Examples/+BrDemo/AFC_1_Interface.m +++ b/Examples/+BrDemo/AFC_1_Interface.m @@ -27,7 +27,7 @@ %% % They will be discovered automatically and included in the interface. -%% Creating an Interface Object +%% Creating an Interface Object (1) % % Running the following will create a BreachSystem interface with the model: mdl = 'AbstractFuelControl'; @@ -42,7 +42,7 @@ BrAFC.PrintParams() -%% Creating an Interface Object +%% Creating an Interface Object (2) % % Sometimes a model contains many tunable parameters. In that case, we can % explicitly specify those we want to tune, e.g., some PI parameters: @@ -80,11 +80,11 @@ %% Input Signals % Input signals of different types can be generated. They are defined by -% parameters of the form $\mathtt{input1\_u0, input1\_u1}$ etc. +% parameters of the form input1_u0, input1_u1 etc. %% % By default, input signals are simply constant and we have two inputs, -% which are $\mathtt{Engine\_Speed}$ and $\mathtt{Pedal\_Angle}$. Next, +% which are Engine_Speed and Pedal\_Angle. Next, % we set their constant values: BrAFC.SetParam('Engine_Speed_u0',1000) BrAFC.SetParam('Pedal_Angle_u0',30) @@ -101,7 +101,7 @@ AFC_Nominal.PlotSignals(); % plots the signals collected after the simulation -%% Simulation with Nominal Parameters +%% Plotting Nominal Simulation % The plotting methods accepts a number of arguments. The first one and % most useful simply allows to select which signals to plot. diff --git a/Examples/+BrDemo/AFC_2_Simulation.m b/Examples/+BrDemo/AFC_2_Simulation.m index 6dfeba4a..ac20182f 100644 --- a/Examples/+BrDemo/AFC_2_Simulation.m +++ b/Examples/+BrDemo/AFC_2_Simulation.m @@ -7,7 +7,7 @@ BrDemo.InitAFC; BrAFC -%% Using input signals +%% Providing Directly Input Signals % We can provide non-constant inputs to the system by directly giving them % as argument to the Sim command. time_u = 0:.1:30; @@ -18,7 +18,7 @@ BrAFC.Sim(0:.05:30,U); BrAFC.PlotSignals({'Pedal_Angle','Engine_Speed','cyl_air', 'cyl_fuel', 'AF'}); -%% Fixed Step Input Generation +%% Fixed Step Input Generation (1) % % To interact with the system we can also use parameterized input generators. For % instance, parameters can represent control points, and the input generated by @@ -36,7 +36,7 @@ AFC_UniStep3.PrintParams(); -%% Fixed Steps Input Generation +%% Fixed Steps Input Generation (2) % We set values for the control points and plot the result. AFC_UniStep3.SetParam({'Engine_Speed_u0','Engine_Speed_u1','Engine_Speed_u2'}, [ 1000 900 1100]); AFC_UniStep3.SetParam({'Pedal_Angle_u0','Pedal_Angle_u1','Pedal_Angle_u2'}, [ 20 60 30]); @@ -66,7 +66,7 @@ AFC_VarStep.Sim(0:.05:40); figure; AFC_VarStep.PlotSignals({'Pedal_Angle','Engine_Speed','cyl_air', 'cyl_fuel', 'AF'}); -%% Mixing Signal Generators for Inputs +%% Mixing Signal Generators for Inputs (1) % It is possible to mix different ways to generate signals for the % different inputs. To do this, Breach provides a number of classes of % signal generators. For example: @@ -91,20 +91,20 @@ [0 15 30 .5 10]); InputGen.PrintParams(); -%% Mixing Signal Generators for Inputs (ct'd) +%% Mixing Signal Generators for Inputs (2) % We can attach InputGen to the Simulink model and simulate as follows. BrAFC.SetInputGen(InputGen); BrAFC.Sim(0:.05:40); figure; BrAFC.PlotSignals({'Pedal_Angle', 'Engine_Speed','cyl_fuel', 'AF'}); -%% Writing a New Signal Generator +%% Writing a New Signal Generator (1) % If the available signal generators are not enough, it is easy to write a % new one. The idea is to write a simple new class implementing a computeSignals % method. type my_signal_generator; -%% Writing a New Signal Generator (ct'd) +%% Writing a New Signal Generator (2) % We can use the new signal generator as the builtin ones my_input_gen = my_signal_generator(2) % creates an instance with lambda=2 MyInputGen = BreachSignalGen({my_input_gen}); % Makes it a Breach system @@ -115,7 +115,7 @@ BrAFC_MyGen.PrintParams(); % Makes sure the new parameters are visible -%% Writing a New Signal Generator +%% Writing a New Signal Generator (3) % And simulate to see what happens. BrAFC_MyGen.Sim(0:.05:40); figure; BrAFC_MyGen.PlotSignals({'Pedal_Angle', 'Engine_Speed','cyl_fuel', 'AF'}); diff --git a/Examples/+BrDemo/AFC_4_Specifications.m b/Examples/+BrDemo/AFC_4_Specifications.m index dc52342e..e2b12e8e 100644 --- a/Examples/+BrDemo/AFC_4_Specifications.m +++ b/Examples/+BrDemo/AFC_4_Specifications.m @@ -147,7 +147,7 @@ bad_param = Brneg.GetParam({'Pedal_Angle_base_value', 'Pedal_Angle_pulse_period', 'Pedal_Angle_pulse_amp'}) -%% Monitoring a Formula on a Trace +%% Monitoring a Formula on a Trace (1) % To monitor STL formulas on existing traces, one can use the % BreachTraceSystem class. @@ -157,7 +157,7 @@ BrTrace = BreachTraceSystem({'x','y'}, trace); figure; BrTrace.PlotSignals(); -%% Monitoring a Formula on a Trace (ct'd) +%% Monitoring a Formula on a Trace (2) % Checks (plots) some formula on imported trace: figure; BrTrace.PlotRobustSat('alw (x[t] > 0) or alw (y[t]>0)'); diff --git a/Examples/+BrDemo/Autotrans_tutorial.m b/Examples/+BrDemo/Autotrans_tutorial.m index eeb158d6..ef01372e 100644 --- a/Examples/+BrDemo/Autotrans_tutorial.m +++ b/Examples/+BrDemo/Autotrans_tutorial.m @@ -14,7 +14,6 @@ STL_ReadFile('Autotrans_spec.stl'); B.PlotRobustSat(gear3_and_speed_low) - %% Describes and generate driving scenarios % We create an input generator that will alternates between acceleration and braking sg = var_step_signal_gen({'throttle', 'brake'}, 5); @@ -28,7 +27,6 @@ % We don't specify a range for brake_u0 so that it remains constant equal % to 0 (by default). Same for throttle_u1, etc. - B.QuasiRandomSample(10); B.Sim(); %% Plot multiple simaltions result @@ -45,6 +43,7 @@ %% Falsify property B.ResetSampling(); % remove the 10 samples and traces, keep parameter ranges falsif_pb = FalsificationProblem(B, never_gear3_and_speed_low); +falsif_pb.max_obj_eval = 1000; falsif_pb.max_time = 180; % give the solver three minutes to falsify the property falsif_pb.solve(); diff --git a/Examples/+BrDemo/InitAFC.m b/Examples/+BrDemo/InitAFC.m index ae286c71..394f3848 100644 --- a/Examples/+BrDemo/InitAFC.m +++ b/Examples/+BrDemo/InitAFC.m @@ -5,7 +5,8 @@ warning('off', 'Simulink:LoadSave:EncodingMismatch') mdl = 'AbstractFuelControl'; -BrAFC = BreachSimulinkSystem(mdl, 'all', [], {}, [], 'Verbose', 0); + +BrAFC = BreachSimulinkSystem(mdl, 'all', [], {}, [], 'Verbose', 0,'SimInModelsDataFolder', true); pedal_angle_gen = pulse_signal_gen({'Pedal_Angle'}); % Generate a pulse signal for pedal angle diff --git a/Examples/Simulink/vdp/test_vdp.m b/Examples/Simulink/vdp/test_vdp.m index 72155c08..faf7b793 100644 --- a/Examples/Simulink/vdp/test_vdp.m +++ b/Examples/Simulink/vdp/test_vdp.m @@ -1,12 +1,23 @@ -%% +%% +% Set some default parameters x1_0 = 2; x2_0 = 3; Mu = 1; Bvdp = BreachSimulinkSystem('vdp'); %% -Bvdp.SetDomain('Mu','double', [-1 2]); +% Set a domain partly invalid +Bvdp.SetDomain('Mu','double', [-1 2]); % negative values for mu will lead to numerical errors Bvdp.GridSample(4); Bvdp.Sim(); -[Bok, Berr, Binput_err] = Bvdp.FilterTraceStatus(); + +%% +% Error message can be recovered using printStatus +Bvdp.printStatus(); + +%% +% Filtering valid/invalid traces +[Bok, Berr, Binput_err] = Bvdp.FilterTraceStatus() % Binput_err is for input generators with non satisfied contraints + % Not relevant here. + diff --git a/InitBreach.m b/InitBreach.m index 0828ddd1..2a2fb4a8 100644 --- a/InitBreach.m +++ b/InitBreach.m @@ -45,6 +45,11 @@ function InitBreach(br_dir, force_init) mkdir([br_dir filesep 'Ext' filesep 'ModelsData']); end + +%% Make sure ModelsData/ParallelTemp exist for parallel computing +if ~exist( [br_dir filesep 'Ext' filesep 'ModelsData' filesep 'ParallelTemp'], 'dir') + mkdir([br_dir filesep 'Ext' filesep 'ModelsData' filesep 'ParallelTemp']); +end %% Init disp(['Initializing Breach from folder ' br_dir '...']); diff --git a/InstallBreach.m b/InstallBreach.m index 8245bfd5..324b6f90 100644 --- a/InstallBreach.m +++ b/InstallBreach.m @@ -62,29 +62,6 @@ function InstallBreach(varargin) eval(cmd) end -if (0) - fprintf([MEX FLAGS '-outdir .. lemire_engine.c\n']); - mex -outdir .. lemire_engine.c - fprintf([MEX FLAGS '-outdir .. lemire_nd_engine.c\n']); - mex -outdir .. lemire_nd_engine.c - fprintf([MEX FLAGS '-outdir .. lemire_nd_maxengine.c\n']); - mex -outdir .. lemire_nd_maxengine.c - fprintf([MEX FLAGS '-outdir .. lemire_nd_minengine.c\n']); - mex -outdir .. lemire_nd_minengine.c - fprintf([MEX FLAGS '-outdir .. until_inf.c\n']); - mex -outdir .. until_inf.c - fprintf([MEX FLAGS '-outdir .. lim_inf.c\n']); - mex -outdir .. lim_inf.c - fprintf([MEX FLAGS '-outdir .. lim_inf_inv.c\n']); - mex -outdir .. lim_inf_inv.c - fprintf([MEX FLAGS '-outdir .. lim_inf_indx.c\n']); - mex -outdir .. lim_inf_indx.c - fprintf([MEX FLAGS '-outdir ../../../Core/m_src ltr.c\n']); - mex -outdir ../../../Core/m_src/ ltr.c - fprintf([MEX FLAGS '-outdir ../../../Core/m_src rtr.c\n']); - mex -outdir ../../../Core/m_src/ rtr.c -end - cd robusthom; fprintf('Compiling offline STL monitoring functions...\n') @@ -144,25 +121,31 @@ function InstallBreach(varargin) % Compile blitz library blitz_dir = [breach_dir filesep 'Ext' filesep 'Toolboxes' filesep 'blitz']; cd(blitz_dir); -CompileBlitzLib; - -% Compile mydiff -if (0) % TODO move this into a dedicated script - cd([breach_dir filesep 'Toolboxes' filesep 'mydiff']); - fprintf([MEX FLAGS '-lginac mydiff_mex.cpp\n']); - try - mex -lginac mydiff_mex.cpp - catch %#ok - warning('InstallBreach:noMydiffCompilation',... - ['An error occurs when compiling mydiff. Maybe GiNaC not available.\n'... - 'Some functionnalities will not be available.']); - fprintf('\n'); - end +try + CompileBlitzLib; end fprintf('Compiling online monitoring functions...\n') -compile_stl_mex - +try + compile_stl_mex +catch + fprintf(['FAILED: try to run the script compile_stl_mex to get ' ... + 'error information. If you are using Mingw, note ' ... + g 'that it is not supported yet. Try installing Visual ' ... + 'C++. Note that this error only affects online monitoring.' ... + 'Most Breach features will work nonetheless.']); + addpath(breach_dir); + savepath; + + % cd back and clean variable + cd(cdr); + + fprintf('\n'); + disp('-------------------------------------------------------------------'); + disp('- Install mostly successful. --') + disp('-------------------------------------------------------------------'); + return; +end addpath(breach_dir); savepath; diff --git a/Online/m_src/compile_stl_mex.m b/Online/m_src/compile_stl_mex.m index 5da0cd10..3c3b00c8 100644 --- a/Online/m_src/compile_stl_mex.m +++ b/Online/m_src/compile_stl_mex.m @@ -53,7 +53,7 @@ function compile_stl_mex(recomp, debug_level) }; %% Obj files -cxxflags = '-silent -DYYDEBUG=1 CXXFLAGS=''$CXXFLAGS -Wno-write-strings -std=c++11 -std=gnu++0x -Wno-deprecated-register'''; +cxxflags = '-silent -DYYDEBUG=1 CXXFLAGS=''$CXXFLAGS -Wno-write-strings -std=gnu++11 -std=gnu++0x -Wno-deprecated-register'''; includes = ['-I' stlpp_dir filesep 'include']; prefix_cpp = [stlpp_dir filesep 'src' filesep]; prefix_m = [stlpp_dir filesep 'src' filesep]; @@ -87,8 +87,10 @@ function compile_stl_mex(recomp, debug_level) if (compile_obj__) for i_src = 1:numel(src_cpp) cmd= sprintf('mex -c %s %s %s%s -outdir %s', cxxflags, includes,prefix_cpp, src_cpp{i_src}, obj_dir); -% fprintf(cmd); -% fprintf('\n'); + if debug_level>=1 + fprintf(cmd); + fprintf('\n'); + end eval(cmd); end end diff --git a/VERSION b/VERSION index 1fc5b820..f69752ab 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -1.2.15 +1.2.16