How can I work around unbounded loops when proving my model using Simulink Design Verifier 1.1 (R2007b)?
1 Ansicht (letzte 30 Tage)
Ältere Kommentare anzeigen
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"
Akzeptierte Antwort
MathWorks Support Team
am 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 Kommentare
Weitere Antworten (0)
Siehe auch
Kategorien
Mehr zu Specify and Verify Design Requirements finden Sie in Help Center und File Exchange
Community Treasure Hunt
Find the treasures in MATLAB Central and discover how the community can help you!
Start Hunting!