How can I work around unbounded loops when proving my model using Simulink Design Verifier 1.1 (R2007b)?
1 回表示 (過去 30 日間)
古いコメントを表示
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"
採用された回答
MathWorks Support Team
2009 年 6 月 27 日
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 件のコメント
その他の回答 (0 件)
参考
カテゴリ
Help Center および File Exchange で Specify and Verify Design Requirements についてさらに検索
Community Treasure Hunt
Find the treasures in MATLAB Central and discover how the community can help you!
Start Hunting!