decyphir / breach Goto Github PK

To Run the tutorial in the Readme file, I got a dependency error when running

Rphi.Eval(Bdata)

Invalid MEX-file 'C:\Users\test\breach@STL_Formula\private\RobustEv.mexw64': The specified module
could not be found.

Error in STL_Formula/STL_EvalThom_Gen>GetValues (line 306)
[time_values, valarray] = RobustEv(time_values, -valarray, I___);

Error in STL_Formula/STL_EvalThom_Gen>GetValues (line 216)
[valarray1, time_values1] = GetValues(Sys, phi.phi1, P, traj, partition, relabs, interval);

Error in STL_Formula/STL_EvalThom_Gen (line 100)
[val, time_values] = GetValues(Sys, phi, Pii, traj, partition, relabs, interval);

Error in STL_Formula/STL_Eval_IO (line 90)
[val, tau] = STL_EvalThom_Gen(Sys, phi, P, trajs, partition, relabs, taus);

Error in stl_monitor/get_standard_rob (line 260)
[rob, time] = STL_Eval_IO(this.Sys, phi, this.P0, this.P.traj{1}, this.inout, this.relabs,
time);

Error in stl_monitor/computeSignals (line 95)
[time, Xout] = this.get_standard_rob(this.formula, 0);

Error in stl_monitor/eval (line 99)
[t, Xout] = this.computeSignals(t, X,p);

Error in BreachRequirement/evalRequirement (line 1351)
[val, time, Xout] = req.eval(time, Xin, pin);

Error in BreachRequirement/eval_req (line 1338)
[val, ~, ~, val_vac] = this.evalRequirement(req, time, Xin, p_in);

Error in BreachRequirement/evalAllTraces (line 284)
traces_vals_vac(it, ipre)] = eval_req(this,req,it);

Error in BreachRequirement/Eval (line 240)
[traces_vals, traces_vals_precond, traces_vals_vac] = this.evalAllTraces(varargin{:});

Error in demo1 (line 13)
Rphi.Eval(Bdata)

I am wondering if there is a quick fix to it?

Matlab version: 2021a and 2021b
OS: Windows 10

When I start the BrDemo.AFC_6_Analysis, several errors occurs:

"Index exceeds the number of array elements (1).

Error in QuickMesh (line 5)
yrange= min(y):epsi(2)/2:max(y);

Error in QuickMeshSf (line 29)
[XI, YI, ZI] = QuickMesh(x,y,Z,epsi);

Error in SplotProp (line 62)
[XI, YI, ZI] = QuickMeshSf(Pf,Z);

Error in BreachSystem/PlotRobustMap (line 869)
SplotProp(Pf, phi, options);

Error in BrDemo.AFC_6_Analysis (line 20)
BrMap.PlotRobustMap(AF_alw_ok, {'Pedal_Angle_pulse_amp', 'Pedal_Angle_pulse_period'}, [0 80; 10 20]);"

Hi,
I read the BrDemo 5_2. It seems that the parameter synthesis action is upon a STL variable. Is it possible to do so on a simulink variable?

And how should I represent 'P' the original set of parameters as a polytope?
(P was described in Donz´e, A., Krogh, B., Rajhans, A.: Parameter synthesis for hybrid systems with an application to simulink models)

Do you have a reference manual for this library?

Best
Huaiyuan

any one knows how to fix the problem?

Error using BreachSimulinkSystem/CreateInterface
Problem creating Accelerator MEX file for model 'AbstractFuelControl_breach'.
To see the build output, use set_param('AbstractFuelControl_breach','AccelVerboseBuild','on')

Error in BreachSimulinkSystem (line 104)
this.CreateInterface(mdl_name);

Error in BrDemo.AFC_1_Interface (line 37)
BrAFC = BreachSimulinkSystem(mdl) - Show complete stack trace
Caused by:
Error using BreachSimulinkSystem/CreateInterface
Error(s) encountered while building "AbstractFuelControl_breach_acc" - Show complete stack trace

QuasiRandomSample(1) does something unexpected. Instead of generating one random point in the parameter space, it assigns a constant value to all parameters. For a MWE, construct two signals with 3 control points each, and give them some ranges, and run QuasiRandomSample

Given a Simulink model, I initialize its parameters like

a = 1;
b = 2;

before interfacing with Breach. It seems like Breach will create a new model with _breach.slx suffix. However, if I change the value of these parameters, Breach seems to use the previously generated model with the old values.

So how can I let Breach simulate the model with the new parameter assignments?

Thank you!

In addition to QuasiRandomSample(n), can Breach provide a UniformRandomSample(n)? This could utilize the Matlab-internal rand. The reason is that QuasiRandomSample gives signals that look too "not random" if you have a small sample. E.g. First few signals I get are always monotonically decreasing.

Dears, Mr.Donze
I found propositional logic judgement(P=>Q) that I don't understand why it occurred.
Please refer summary result in attach file(QA.xlsx)
(Although I tried to check in source code STL_EvalThom.m line:172 but I don't know purpose of logic yet)

So, I don't sure that I misunderstand something or the script that I use for test have something wrong.
But in case of this issue is classified as need to revise. I wonder if you could fix this issue.
Thanks for your consideration.

                        Best Regards,
                          Nattawut K.

Reference file

1. Summary result(xlsx)
   QA.xlsx
2. Trial Script(.zip)
   check_ev.zip

Error in STL_Formula/STL_EvalThom>GetValues (line 194)
[time_values, valarray] = RobustAnd(time_values1, valarray1, time_values2, valarray2);

Error in STL_Formula/STL_EvalThom>GetValues (line 252)
[valarray, time_values] = GetValues(Sys, phi.phi, P, traj, next_interval);

Error in STL_Formula/STL_EvalThom (line 96)
[val, time_values] = GetValues(Sys_, phi_, Pii, traj, interval);

Error in STL_Formula/STL_Eval (line 93)
[val, tau] = STL_EvalThom(Sys, phi, P, trajs, varargin{1});

Error in SEvalProp (line 164)
[props_values(i_pt).val, props_values(i_pt).tau] = STL_Eval(Sys, phi, Ptmp, traj_tmp, taus{np}, method);

Error in BreachSystem/CheckSpec (line 347)
[this.P, val] = SEvalProp(this.Sys,this.P,spec, t_spec);

Error in MyOwnProject/calRob (line 134)
rob = Br.CheckSpec(phi);

Hello,
I am working on the fault localization of Matlab/Simulink models and your toolbox is very important for my work, So I want to ask you how can I change the STL property for which I want to generate a violation trace. And if possible, how can I use this toolbox to generate a violation trace to another model.

I don't have an MWE for this, but BreachSimulinkSystem throws an error when there are logged signals in the model with no name (empty string). (I think in one case it threw an error when it had different logged signals with the same name).

Error in S-function 'AFC_Online_breach/STL Monitor/STL Monitor ': S-Function 'onlineMonitorWrapper' does not exist
Component:Simulink | Category:Model error

Error in S-function 'AFC_Online_breach/STL stops when false/STL Monitor ': S-Function 'onlineMonitorWrapper' does not exist
Component:Simulink | Category:Model error