Разработка NuSMV: измените функцию «ИСТИНА» в постановке - PullRequest
Новая
       20

Разработка NuSMV: измените функцию «ИСТИНА» в постановке

0 голосов
/ 24 мая 2018

Недавно я попытался поработать над переводом некоторых моделей в модели Nusmv, но я хочу попытаться изменить функцию ключевого слова «ИСТИНА:».Как мы все знаем, «TRUE:» в «case ... esac;»Можно определить некоторые действия, которые вы хотите, когда условия случая не имеют этого конкретного условия, однако у меня есть требование, чтобы "ИСТИНА" могла выполнять действия в последний раз, например: 

    next(a) := 
                 case 
                       a>0 : -10;
                       a<0 : 10;
                       TRUE : (do the last time actions);
                  esac;

В другомслово, когда 'a' = 0, если в последний раз был назначен 'a' - 10, на этот раз также будет назначено - 10;если в прошлый раз «а» было назначено 10, на этот раз оно также будет назначено 10.

Итак, теперь вопрос в том, можно ли это сделать, изменив исходный код NuSMV, не могли бы вы сказатьme, который является языковым файлом c, который реализует функции "ИСТИНА" в "случае"?

Спасибо за помощь!

1 Ответ

0 голосов
/ 25 мая 2018

Можно использовать несколько подходов.

Решение 1.

Это решение основано на постоянстве значения .Обратите внимание, что его можно использовать для игрушечного примера , который вы указали в своем вопросе, но это никоим образом не является общим решением. 

MODULE main
VAR
    a : -1..1;

ASSIGN
    init(a) := -1;
    next(a) := case
        a < 0 : 1;
        a > 0 : -1;
        TRUE  : a;
    esac;

Значение постоянства равнодостаточно, потому что мы присваиваем постоянное значение переменной.

Решение 2.

В случае, если присваиваемое значение не является constant , значение постоянства не может быть использовано.Вместо этого мы обогащаем модель достаточным количеством памяти , чтобы отслеживать выполняемые действия. 

MODULE main
VAR
    a : -1..1;
    action : { ACTION_1, ACTION_2, NONE };

ASSIGN
    init(action) := NONE;
    next(action) := case
        a < 0 : ACTION_1;
        a > 0 : ACTION_2;
        TRUE  : action;
    esac;
    init(a) := -1;
    next(a) := case
        a < 0 : a + 1;
        a > 0 : a - 1;
        action = ACTION_1 : a + 1;
        action = ACTION_2 : a - 1;
        TRUE              : a;
    esac;

В этом примере action отслеживает последний выбранный вариантвыполняется по переменной a.Всякий раз, когда предварительных условий a case недостаточно для определения, какое действие следует предпринять, мы полагаемся на наше сохраненное значение action и воспроизводим ранее выполненное действие.

Обратите внимание, что этоответственность дизайнера за решение того, что должно произойти в исходном состоянии, если не выполнено ни одно из предварительных условий a.В этом случае мы не можем воспроизвести предыдущее действие (оно не существует) , поэтому спецификация открыта для обработки по-другому.В моем случае я решил оставить a на значении 0 навсегда.

...