Задание нескольких шагов с использованием TLA+ (временная логика действий)

Question

Просмотр здесь в основном показывает простые примеры спецификаций действий, где вы ссылаетесь на следующее состояние, используя ', как в:

UponV1(self) ==                                 
  /\ pc[self] = "V1"                        
  /\ pc' = [pc EXCEPT ![self] = "AC"]       
  /\ sent' = sent \cup { <<self, "ECHO">> } 
  /\ nCrashed' = nCrashed
  /\ Corr' = Corr

Например, /\ nCrashed' = nCrashed это логическое утверждение, говорящее "... И далее (nCrashed) == this(nCrashed)`. Таким образом, в основном, вышеупомянутая функция устанавливает несколько переменных "в следующем состоянии". Но все это происходит по существу за один шаг (логически в наименее).

Что мне интересно, так это как определить то, что происходит за несколько шагов. Скажи 10 шагов.

UpdateWithTenSteps(self) ==                                 
  /\ foo' = foo + 1
  /\ bar'' = foo' + 1
  /\ baz''' = bar'' + 1
  /\ ...
  ....

Так что "в третьем состоянии впереди baz будет установлен как bar во втором состоянии плюс один". Что-то вроде того. Но это не имеет смысла. На императивном языке вы бы просто сделали что-то вроде этого:

function updateInTenSteps() {
  incFoo()
  incBar()
  incBaz()
}

Но это имеет смысл, потому что каждый вызов функции происходит после предыдущего. Но я не вижу, как представить это в TLA+.

Хотите знать, как вы должны выполнить вещи, которые занимают более одного шага во временной логике действий +. Другим примером будет цикл while.

Answer 1

TLA разработан так, что он учитывает только текущее состояние и состояние преемника (или все поведение). Вы всегда можете разделить несколько шагов, которые зависят друг от друга, введя явную переменную, которая сообщит вам, какие назначения уже выполнены:

EXTENDS Naturals

Labels == { "foo", "bar", "baz", "fin" } (* just for documentation purposes *)
VARIABLE currstate, foo, baz, bar

Init == /\ currstate = "foo"
        /\ foo = 0
        /\ bar = 0
        /\ baz = 0

Next == \/ (currstate = "foo" /\ currstate' = "bar" /\ foo' = foo +1 /\ UNCHANGED <<bar,baz>>)       
        \/ (currstate = "bar" /\ currstate' = "baz" /\ bar' = foo +1 /\ UNCHANGED <<foo,baz>>)
        \/ (currstate = "baz" /\ currstate' = "fin" /\ baz' = bar +1 /\ UNCHANGED <<foo,bar>>)
        \/ (currstate = "fin" /\ UNCHANGED <<foo,bar,baz,currstate>>

Если вы создаете модель для этого, установите поведение, как определено Init а также Next, а затем проверить инвариант baz = 0, вы получите трассировку, которая показывает вам состояния, которые приводят к изменению baz (вашего последнего назначения). Цикл просто назначает метку преемника как уже существующую (например, вместо определения baz' = "foo").

Преобразование Pluscal в TLA работает аналогично: каждая помеченная строка соответствует id, и каждый переход от строки l к строке m изменит счетчик программы в следующем состоянии с l на m.