Can I do parameter synthesis on model variables about breach HOT 5 OPEN

Hi Huaiyuan,
Yes, it is possible to do parameter synthesis over a Simulink model. Actually, BrDemo 5_3 is doing it on parametrs ki and kp, though it might not be exactly what you are looking for, as it tries to maximize the satisfaction of a formula. If you are looking for a boundary, you should indeed use the ParamSynthProblem class. Note that this class by default will use a binary search, which means some monotonicity is assumed.
P is represented by an hypercube - there is no direct support for general polytope, though there is a mechanism that makes it possible to apply a function to parameter vector prior to simulation. So if you can parameterize your set with variables in a hypercube by some transformation, you can use this to get a non-hypercube initial set. Sorry if this is not clear, also since it is relatively recent code, it is not documented yet (the documentation mostly consists of the examples in BrDemo folder), but if you tell me more about your application/problem, I can help you and/or provide example code.

Best,
Alex

from breach.

from breach.

Your code is correct. I can see why it is not working though. Breach is indeed raising an error when using the ParamSynthProblem class with system (Simulink) parameters, though it should not. Here is a quick fix: change line 41 in solve_binsearch.m into

this.BrSet.SetParam(this.params, p, true);

I will push this fix in future versions.

Sensitivity analysis as described in the paper you mentioned has not been maintained unfortunately. One reason is that it is difficult to make it work for arbitrary Simulink model. The parameter synthesis algorithm implemented (and currently maintained) in Breach is the one from "Mining requirements from closed-loop control models" . Note that for one dimensional problems, the behavior is similar though. The algorithm will try to converge around a value for which the property is true but a small perturbation makes it false.

PS: for easier navigation in the examples, you can generate html using GenDoc() command. This should create a breach/Doc folder with an index.html file. This won't make the documentation more complete but at least more readable...

from breach.

from breach.

Hi Huaiyuan,

Sorry for the late reply. After looking into the issue, it is true that the binsearch solver does not currently work with system parameters. I will fix that eventually, but this is not trivial (reliance on some old legacy code that I need to adapt properly) so I can't suggest a quick fix now. However, using a different solver does work. Here is an example:

BrDemo.InitAutotrans;
phi = STL_Formula('phi', 'alw speed[t]<60');
pb = ParamSynthProblem(B, phi, 'throttle_u0', [0 100]);
pb.display = 'on';
pb.setup_global_nelder_mead();
pb.solve();

Note that this will find the values of throttle for which the formula is true but becomes false with a very small change (tries to get robustness close to 0+). To get positive higher robustness, then use the MaxSatProblem class.

Regarding the paper, all three algorithms are maintained: Algo 2 is demoed in BrDemo 5_1, Algo 3 in BrDemo 5_2 and algo 1 in BrDemo 5_4.
Although clearly algo 2 (i.e. Falsification) is clearly the most used and thus mature.

Best,
Alex

from breach.