как я могу смоделировать несколько синхронизаций в UPPAAL? Например: изменение состояния одновременно вызывает два других изменения состояния в разных шаблонах. В поле синхронизации я могу поставить только один канал (sync1! или sync!). Как я могу объединить sync1! и синхрон2! ?
Спасибо
Самый простой способ сделать это — разделить ребро, представляющее изменение состояния, на два и ввести зафиксированное местоположение посередине. Первое ребро, ведущее от исходного местоположения к зафиксированному местоположению, должно содержать все исходное ребро, кроме второй синхронизации. Второе ребро, ведущее от фиксированного местоположения к целевому местоположению, должно содержать вторую синхронизацию.
Выделенные локации — это виртуальные локации, созданные для помощи в моделировании такого поведения. Когда автомат входит в выделенное место, он должен покинуть его немедленно, без промедления и без чередования с каким-либо другим автоматом. Это также означает, что выделенное место не будет введено, если его нельзя покинуть в соответствии с правилами.
