Empty objectives in Design Verifier

I created a model in Simulink and i wished to prove a property using Design Verifier.

Here is a portion of the model:

The verification system is the following:

Design Verifier analysis starts correctly, but it tries to validate 27 objectives instead of 1 (it seems one for each output message in the chart above)

Also those objectives seem to be empty.

Is there a way to validate only my objective?

[Pat Canny]

Hi Lorenzo,

The images of your model are not showing - perhaps it's my browser.

Can you try inserting the images again?

Thanks.

[Lorenzo Niccolai]

ok, I'll fix that

[Pat Canny]

Does your model have any Assertion blocks or other blocks from the Model Verification library? Design Verifier treats those blocks as proof objectives by default.

To disable this, change the Assertion blocks setting in the Design Verifier Pane: Property Proving: https://www.mathworks.com/help/sldv/ug/design-verifier-pane-property-proving.html

If you want to disable all Assertion blocks, select "Disable all". If you want to manually enable or disable certain blocks, select "Use local settings".

This can also be done via the DVAssertions parameter in the sldvoptions function: https://www.mathworks.com/help/sldv/ug/simulink-design-verifier-configuration-parameters.html

[Lorenzo Niccolai]

I managed to insert an image of a portion of the model.

The particularity is that I have only 1 proof objective in the verification subsystem, but 27 objectives in the verification process.

In the portion of model above you can see 3 + 3 = 6 message outputs; I can count exactly 26 message outputs in my model, it seems that each one causes the spawn of an objective.

I already tryed to play with Design Verifier settings without achieving nothing.

I created another project in which I use datas over messages and the issue is gone. What's up with those messages?

[Pat Canny]

Hi Lorenzo,

This likely requires further digging. I don't know if we'll solve this via MATLAB Answers.

Do you mind contacting MathWorks Support? https://www.mathworks.com/support/contact_us.html?s_tid=sp_ban_cs