Простые примеры програм на TLA+ и +Cal

Данные язык и его расширение инструменты для верификации программ. Под капотом там находится машина генерирующая граф и полученной модели программы. С какой-то стороны код здесь становиться частью данных. Важной частью является модель и её свойства которые задаются отдельно. Свойства модели могут описываться более богатым языком, чем сама программа.

Так как самое главное это понять окно Model Overview и Model Checking result.

Вывод графа

На маленьких моделях можно видеть весь граф исполнения, и это очень полезно на начальных этапах понимания языка. Для включения вывода графа необходимо в Model Overview нажать на кнопку Additional TLC Options и выбрать Features, а там Visualize state after graph compilation.

Минимальная программа

Как мне сейчас кажется минимальной программой-моделью показывающей хотя бы начало может быть что-то такое:

(*--algorithm noproblem
variables
    x = 0;
begin
    START:
        x := 1;
end algorithm;**)

Программа просто присваевает x значение 1 и заканчивается. После того как произойдет трансляция из +Cal В TLA+ можно запустить программу и увидеть что она верифицируется.Но это не очень интересно. Для нас интерес представляет когда модель показывает несостоятельность нашей программы. Для начала проверим что наша модель проверяется на Deadlock. Для этого в What to check? проверим что галочка Deadlock проставлена. Изменим код на вот такой:

EXTENDS TLC, Sequences, Integers, FiniteSets

(*--algorithm noproblem
variables
    x \in 0..3
begin    
    START:
        await x = 1;
    ATOMIC_OPERATION:
        x := 1;
end algorithm;**)

Команда await ожидает условия, так как наше условие не выполняется никогда, мы получаем ошибку о том что Deadlock достигнут. Самой важной панелькой теперь становиться Error Trace он показывает как мы достигли ошибочного состояния. В данном случае тупика. У нас это произошло очень легко, чекер выбрал для x не то состояние (0,2,3) и программа пришла в тупик.

Свойства и инварианты

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

Изменим нашу модель таким образом:

(*--algorithm noproblem
variables
    x = 1;
begin    
    START:
        await x = 1;
    ATOMIC_OPERATION:
        x := 1;
end algorithm;**)

\* BEGIN TRANSLATION 
..
\* END TRANSLATION 

XAlwaysOne == [](x = 1)

Свойства

XAlwaysOne это свойство, что x = 1. Добавляем его в What to check  Propertes и видим что оно выполняется всегда.

Но мы можем поменять нашу атомную операцию сделать x := 2 и увидеть, что это свойство не выполняется когда мы исполняем атомную операцию.

Свойства проверяют именно поведение.

Инвариант

Добавим бросок кубика и сложение к одному

(*--algorithm noproblem
variables
    x = 1,
    dice \in 1..6;
begin    
    START:
        await x = 1;
    ATOMIC_OPERATION:
        x := 1;
    INT_OPERATION:
        dice := dice + 1;
end algorithm;**)

Количество состояний нашей модели увеличилось.

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

DiceRightVariant == dice > 0 /\ dice < 7

И допишем его в модель What to check  Invariants.

После запуска видно, что такой вариант достижим если выпало 6 на кубике.

Инварианты лучше проверять как параметры, которые не допустимы для системы всегда.

Свойства

Изменим нашу модель таким образом:

(*--algorithm noproblem
variables
    x = 1,
    dice \in 1..6;
begin    
    START:
        await x = 1;
    ATOMIC_OPERATION:
        x := 1;
    INT_OPERATION:
        dice := dice + 1;
        if (dice > 3) then
            x := x + dice
        end if
end algorithm;**)

Если на кубике больше трёх, то прибавляем его к x, сделаем свойство которое проверяет что никогда наш x не может стать цифрой 8.

XProp == ~<>(x = 8)

После рекомпиляции и запуска видим, что если на кубике выпало 6, то наше свойство не выполнится если на кубике выпало 6.

Основной цикл верификации

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