Не удалось проверить свойства UPPAAL

Я проверяю очень маленькую модель. Но я получаю сообщение об исчерпании памяти. Я несколько раз менял модель, но с той же проблемой. Я думал, что эта проблема будет связана с использованием определяемой пользователем функции или с использованием опции выбора для получения случайного числа. Затем я изменил модель и не вызывал функцию и не использовал параметр «Выбор», но все же... Мне интересно, либо это проблема UPPAAL, либо моя модель. Никаких ошибок, кроме нехватки памяти, нет. После того, как значение «r1» и «r2» изменено после того, как это свойство ctl не работает. изменить адрес CTL работает для всех значений r1 и r2 до приращения.


out-of-memory deadlock memory verification uppaal
person Muhammad Abdul Basit    schedule 27.11.2018    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Модель инкрементирует несколько переменных (r1, r2 и cntr): если для них нет верхней границы (а вроде и нет, но я не вижу всех функций), то пространство состояний будет огромным (все значения умноженное на количество локаций, умноженное на часовые зоны) и, таким образом, исчерпав всю память.

Либо сделайте эти переменные ограниченными (не позволяйте приращениям передавать какое-либо значение), либо объявите их как мета (не делайте этого, если не понимаете последствий).

person mariusm    schedule 28.11.2018
comment
r1 и r2 используются для запуска часов между диапазонами. Когда часы приближаются к r2, я присваиваю адресам случайные числа (используя функцию assign()). Значение r1 и r2 предназначено только для итерации. Я не хочу сохранять прошлые значения. Как я могу показать вам полную модель. Пожалуйста, мне ссылку, я поделюсь подробной моделью. - person Muhammad Abdul Basit; 29.11.2018