[model-checking] Комментарий к первому заданию

Дорогие студенты,

Обратите внимание, что изменение оператором значения переменной (например, в случае присваивания) происходит _после_ выполнения данного оператора.

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

С уважением, Константин Савенков.