Государственный космический взрыв в UPPAAL

Question

Я смоделировал синхронизированную модель с двумя триггерами в UPPAAL, когда я попытался проверить некоторые свойства, я достиг состояния 6M, и на моем ноутбуке не было оперативной памяти, было использовано около 5Go, может кто-нибудь сказать, какое приблизительное число состояний может UPPAAL иметь дело с? и каковы возможные методы борьбы со взрывом состояния в UPPAAL?
Спасибо

Answer 1

Количество штатов зависит от:

1. размер доступной памяти. На 32-битных архитектурах он ограничен 4 ГБ.

2. размер / след отдельных государств.

3. форма государственного пространства и порядок освоения.

4. гранулярность символических состояний (насколько хорошо интервалы ограничения охватывают: если время дискретизируется, символические методы будут плохо масштабироваться).

Вы можете попробовать следующие методы:

1. Примените абстракцию и удалите ненужные переменные: установите переменные const, установите переменные равными нулю, когда они не используются, переменные только для одного перехода могут быть помечены как "мета" (не злоупотребляйте этим! Или вы столкнетесь с проблемами из-за странного поведения),

2. оптимизировать потребление пространства путем установки агрессивного сокращения пространства состояний.

3. применить частичное уменьшение порядка, уменьшение симметрии.

4. применить метод развертки (ищите ключевое слово "progress" в справке Uppaal).

Посмотрите учебник Uppaal для получения дополнительной информации.