Как сохранить переменные из Uppaal, созданные в процессе моделирования

Я создал модель с Uppaal, в которой несколько целочисленных переменных изменяются с течением времени. Теперь я хотел бы сохранить значения переменных в процессе моделирования куда-нибудь (лучше всего в xml или текстовый файл). В документации Uppaal (https://www.it.uu.se/research/group/darts/uppaal/documentation.shtml) Я нашел метод в пункте 13 (Как экспортировать и интерпретировать трассы из Uppaal?) и попробовал Java Уже через API, в надежде, что он сможет выводить как переменные, так и трассировки. К сожалению, этот метод, по-видимому, ограничен трассировкой. Кто-нибудь знает способ сохранить значения переменных из Uppaal?

Обнадеживающий привет,

Джози


variables save uppaal
person Josi    schedule 09.12.2020    source источник
comment
Если вы хотите сохранить траекторию значений переменных с течением времени, попробуйте смоделировать запрос, затем откройте график, щелкните правой кнопкой мыши и выберите экспорт CSV.   -  person mariusm    schedule 10.12.2020
comment
@mariusm большое спасибо. Кажется, это именно то, что мне нужно. К сожалению, мне не удалось реализовать Ваше предложение: если я правильно понял, то в верификаторе нужно ввести команду симулировать запрос. Я нашел следующую строку, которая, по моему мнению, должна подойти: simulate 1 [‹=300] { Train(0).Cross, Train(5).Cross, Gate.len} . Но когда я ввожу его в запрос, я получаю: Все каналы должны транслироваться. Мне это кажется странным, так как я пытаюсь запустить пример с воротами поезда из uppaal-4.1.19, и симуляция работает нормально. Я что-то неправильно понял в уроке?   -  person Josi    schedule 15.12.2020
comment
попробуйте пример из demo/smc/train-gate-stat.xml -- он был изменен, чтобы соответствовать требованиям SMC, чтобы иметь широковещательные каналы.   -  person mariusm    schedule 16.12.2020
comment
отлично, большое спасибо, что сработало   -  person Josi    schedule 18.12.2020

Ответы (1)


arrow_upward
0
arrow_downward

Решение из комментариев.

чтобы экспортировать значение переменной с течением времени, можно использовать запрос SMC в верификаторе.

Например:

  1. Введите следующий запрос: simulate 1 [<=300] { Gate.len }
  2. Нажмите Check
  3. Щелкните запрос правой кнопкой мыши и во всплывающем меню выберите Simulations (1).
  4. Наблюдайте за новым всплывающим окном с графиком
  5. Щелкните правой кнопкой мыши график и выберите Export Comma Separated Values
  6. Следуйте диалоговому окну save file и убедитесь, что полученный файл содержит время и последовательность значений.

Обратите внимание, что SMC предполагает, что все каналы широковещательные и взаимоблокировок нет.

person mariusm    schedule 23.12.2020