Simulink design verifier verify conditions at the end of execution
3 views (last 30 days)
Show older comments
Hi everyone.
I created this system that simply forwards a constant =1 to a design verifier module that should prove that the constant is equal to 1, but it fails.
How is it possible that it tries to falsify it? the property constant = 1 should be always verified, or am i wrong? This simple question is related to a larger (and real) project in which i have to verify some liveness properties of a robot swarm simulation.
I tried to follow the documentation but it starts with some far complicated models and i really missed the principle.
How can i fix this? thanks.
5 Comments
Pat Canny
on 7 Dec 2021
Edited: Pat Canny
on 7 Dec 2021
Hi Alessandro,
Did you change the solver settings to Fixed-step before trying to prove properties? The model you sent usesd Variable-step, which would cause an incompatibility error.
In general, your workflow does not seem like a property proving use case, but I coud be wrong. My concern is your requirement that it be checked at the end of simulation. I'd be curious to learn more - I'm always happy to talk about property proving! Feel free to reach out using the "Contact the Simulink Design Verifier technical team" link on the Simulink Design Verifier product page.
Have you considered "grabbing" the last value using simout and adding an assertion using MATLAB Unit Test?
Answers (0)
See Also
Categories
Find more on Verification, Validation, and Test 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!