UPPAAL モデル チェッカーを使用してゲート レベルで同期回路をモデル化しています。クロックをモデル化する方法について混乱しています。私の目標は、セットアップ タイムとホールド タイムに違反していないことを確認することです。appal モデル チェッカーでクロックをテスト ベクトルとして指定するモデルをいくつか見つけました。たとえば、at=10 は立ち上がりエッジに相当し、at=20 は立ち下がりエッジであり、テスト ベクトルのように見えます。UPAAL で同期回路をモデル化する方法に関する基本的な例を誰かが提案できますか?
ありがとうございました