How can I work around unbounded loops when proving my model using Simulink Design Verifier 1.1 (R2007b)?

1 view (last 30 days)
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
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.

More Answers (0)

Products


Release

R2007b

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!