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

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"

Answer 1

[MathWorks Support Team]

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.