How can I work around unbounded loops when proving my model using Simulink Design Verifier 1.1 (R2007b)?
1 view (last 30 days)
Show older comments
I have implemented a for-loop in a Stateflow chart and I get the following error when trying to use property proving in Simulink Design Verifier:
"This model contains potentially unbounded loops. Unbounded loops are
not supported in Property Proving mode"
Accepted Answer
MathWorks Support Team
on 27 Jun 2009
Simulink Design Verifier must be able to infer a loop bound in order to translate the loop correctly for property proving. If you have a loop as shown below:
for idx=1:n
...
end
Simulink Design Verifier will not be able to translate the loop to a specific limit because it does not have any knowledge about n. If you know that n is normally bounded by some value, say 100, you can recode your design as shown below:
for idx=1:100
if idx<=n
...
end
end
You can also do this type of rewriting to get proof results based on the assumption that n<=100.
Also R2008a supports Embedded MATLAB scripts which will make the rewrite easier.
0 Comments
More 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!