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

Question

У меня есть кусок кода в 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, Его правила перехода также определены с использованием следующего оператора.

Answer 1

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

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

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

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

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

---

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

Правила назначения

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

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

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

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

[...]

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

x := y;
y := x;

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

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

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

[...]

---

Ты спрашиваешь:

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

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

---

Ты спрашиваешь:

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

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