Design verifier generates additional objectives
1 view (last 30 days)
Show older comments
I built a model on Simulink using Stateflow and I'm trying to verify one property using Design Verifier.
The analysis starts correctly, but the engine tries to verify 27 objectives instead of my only 1.
It seems that it generates an objective for each output port of my statecharts of type message .
Is there a way of using messages over datas and prove only my property?
1 Comment
Pat Canny
on 10 Mar 2019
Hi Lorenzo,
This requires more details on your model. If you are able to share your model or your approach, I suggest contacting MathWorks Support. https://www.mathworks.com/help/matlab/matlab_env/contact-technical-support.html
Answers (0)
See Also
Categories
Find more on Specify and Verify Design Requirements in Help Center and File Exchange
Community Treasure Hunt
Find the treasures in MATLAB Central and discover how the community can help you!
Start Hunting!