Модель проверки синхронной схемы в UPPAAL

Question

Я использую модель проверки UPPAAL для моделирования синхронной схемы на уровне затвора, у меня есть некоторая путаница в том, как я могу смоделировать часы, моя цель - убедиться, что время установки и время удержания не нарушены. Я нашел некоторые модели, дающие часы в качестве тестового вектора в апплере проверки модели, например, при =10, например, эквивалент для нарастающего фронта, а при =20 - это падающий фронт, что делает его больше похожим на тестовый вектор. Может кто-нибудь предложить базовый пример о том, как моделировать синхронную схему в УПААЛ?

Спасибо

Answer 1

В декларациях напишите это:

clock t;
broadcast chan rise, fall;

Тогда синхронные часы в Уппале будут выглядеть так:

Тогда другие подключенные компоненты должны слушать с rise? а также fall? как синхронизация по краям.