Can I do parameter synthesis on model variables

[huaiyuat]

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

[adonze]

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

[huaiyuat]

Thanks for your reply.

I looked into Demo 5_3 but encountered another problem. When I was using ParamSythProblem Class on a model variable, 'Attempt to modify a system parameter - use SetParam instead ' was raised in command line. [image: P1.png] I was trying to synthesis the power of the white noise shown above to see when will it disrupt the linear feed back controller.

Here is my code:

clear Pr.A=[0,1;1,0]; % x, x_dot; x_dotdot=x Pr.B=[0;1]; % controling x_dotdot Pr.init=[0;0]; Pr.C=[1 0]; %looking at x

Pr.K=lqr(Pr.A,Pr.B,diag([1,0]),0.1);

Pw=0.0005; mdl='double_int'; Bss = BreachSimulinkSystem(mdl); Bss.PrintAll()

S1=STL_Formula('S1', 'alw(Out11[t]<1)'); % PF=ParamSynthProblem(Bss, S1, {'Pw'}, [0,0.1]); PF.solver_options.monotony = -1; %PF.setup_cmaes();

a=PF.solve();

Sorry if this is not clear, but I do found it hard to investigate into the demos. Is that the right way do use the class?

Apart from that, is there a way to make the solver work the same way as mentioned in " Parameter Synthesis for Hybrid Systems with anApplication to Simulink Models"?

Best Huaiyuan

[adonze]

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...

[huaiyuat]

Hi, Alex Thanks again for your guidance. I looked into the article "Mining requirements from closed-loop control models" https://cloudfront.escholarship.org/dist/prd/content/qt95q77327/qt95q77327.pdf. It seems that only 'Algorithm 2' is maintained in breach (According to the content of BrDemo 5_2). Is my understanding here correct?

Adding the fixation to solve_binsearch.m did helped me in settling the previous error. But there is a new one when executing '.solve':

Error using SEvalProp (line 116) P has no traj field.

Here is my code(2018b) and the simulink model is unchanged(attached):

clear Pr.A=[0,1;1,0]; % x, x_dot; x_dotdot=x Pr.B=[0;1]; % controling x_dotdot Pr.init=[0;0]; Pr.C=[1 0]; %looking at x

Pr.K=lqr(Pr.A,Pr.B,diag([1,0]),0.1);

Pw=0.0005; mdl='double_int'; Bss = BreachSimulinkSystem(mdl, 'all', [], {}, [], 'Verbose',0,'SimInModelsDataFolder', true);

S1=STL_Formula('S1', 'alw(Out11[t]<1)'); % Bss.Sim() PF=ParamSynthProblem(Bss, S1, {'Pw'}, [0,0.1]); PF.solver_options.monotony = -1; %PF.setup_cmaes();

a=PF.solve();

If I misused something here, please let me know.

And Thanks again for your guidance.

Best Huaiyuan

On Wed, Mar 20, 2019 at 9:14 AM adonze notifications@github.com wrote:

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" https://cloudfront.escholarship.org/dist/prd/content/qt95q77327/qt95q77327.pdf. 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...

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/decyphir/breach/issues/5#issuecomment-474823066, or mute the thread https://github.com/notifications/unsubscribe-auth/Ard7mikKc-DFOVczt22NCgUbvnHN-oRRks5vYjQ9gaJpZM4b6b1f .

[adonze]

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