Понимание рекурсивно определенной ошибки в NuSMV - PullRequest
Новая
       40

Понимание рекурсивно определенной ошибки в NuSMV

0 голосов
/ 01 сентября 2018

У меня есть фрагмент кода в NuSMV, который вызвал ошибку. Код: - 

MODULE main
VAR
    x1: {a,b,c,d,e};
    x2: {a,b,c,d,e};
ASSIGN

    next(x1) := case
        x1=a & x2=c: e;

        x1=d & next(x2)=c : a;
        TRUE : x1;
    esac;
    next(x2) := case
            x1=b & x2=b: c;

            x2=d & next(x1)=e : e;
            TRUE : x2;
        esac;

Поэтому, когда я компилирую это в NuSMV, выдается ошибка: recursively defined: x1

Теперь я легко могу устранить эту ошибку, удалив следующие операторы, связанные с x2, для правила перехода x1, что означает замену x1=d & next(x2)=c : a; на x1=d : a; или x1=d & x2=d : a;

Я хочу понять механику программного обеспечения NuSMV, которая вызывает ошибку, и почему вышеуказанное исправление устраняет ошибку. Я думаю, что это связано с синхронной реализацией бла-бла-бла, чего я не понимаю. Может кто-нибудь дать точное подробное техническое объяснение?

А также объясните, почему нет ошибки с переменной x2. Его правила перехода также определены с использованием следующего оператора.

1 Ответ

0 голосов
/ 02 сентября 2018

Это намного проще, чем это.

У вас круговая зависимость, и программное обеспечение не может разрешить ее для вас. 

next(x1) := case
     ... & next(x2) : ...
esac;

next(x2) := case
     ... & next(x1) : ...
esac;

Каким образом компьютер (или человек) должен определять значения x1 и x2 в следующем состоянии, когда для принятия решения о таких назначениях необходимо знать ответы заранее?

Вы нарушили так называемое правило циклической зависимости , как указано в документах , раздел 2.3.8

Правила выполнения заданий

Задания описывают систему уравнений, которая сказать, как ФСМ развивается во времени. С произвольным набором Уравнения нет никакой гарантии, что решение существует или что оно уникальный. Мы решаем эту проблему, устанавливая определенные ограничительные синтаксические правила по структуре заданий, гарантирующие тем самым что программа реализуема.

Правила ограничения для присвоений:

  • Правило одиночного присваивания - каждая переменная может быть назначается только один раз.

  • Правило круговой зависимости - набор уравнения не должны иметь «циклов» в графе зависимостей, не нарушенных задержки.

[...]

Если у нас есть назначение типа x := y ;, то мы говорим, что x зависит от у . комбинаторный цикл - это цикл зависимостей, не нарушенный задержки. Например, задания: 

x := y;
y := x;

образуют комбинаторную петлю. Действительно, не существует фиксированного порядка, в котором мы можем вычислить x и y, поскольку в каждый момент времени значение x зависит от значение y и наоборот Мы можем ввести «единицу задержки» , используя оператор next(). 

      x := y;
next(y) := x;

В этом случае существует зависимость задержки на единицу между x и y. Комбинаторный цикл - это цикл зависимостей, общая задержка равна нулю. В НУСМВ комбинаторные петли являются незаконными. это гарантирует, что для любого набора уравнений, описывающих поведение переменная, есть хотя бы одно решение.

[...]

Вы спрашиваете:

[...] почему вышеуказанное исправление устраняет ошибку.

Исправляет ошибку, потому что разрывает комбинаторный цикл . После изменения программное обеспечение все еще должно вычислить будущее значение x1, чтобы вычислить будущее значение x2. Однако для вычисления будущего значения x1 теперь ему больше не нужно знать будущее значение x2 (или любую другую недоступную информацию, для всего, что имеет значение), поэтому он может разрешить оба назначения.

Вы спрашиваете:

А также объясните, почему нет ошибки с переменной x2. Его правила перехода также определены с помощью оператора next.

Оба задания на x1 и x2, взятые независимо, абсолютно законны. Однако ошибка не в одном назначении, а в комбинации этих двух назначений. Поскольку существует только одна циклическая зависимость , включающая две переменные , ошибка сообщается только один раз, как только она обнаружена. Так что на самом деле не имеет значения, исправляете ли вы это, изменяя присваивание на x1 или на x2, если в графе зависимостей больше нет цикла.

...