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

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

0 голосов
/ 01 марта 2019

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

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 будет установлензапретить во втором состоянии плюс один. ". Нечто подобное. Но это не имеет никакого смысла. На императивном языке вы бы просто сделали что-то вроде этого: 

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

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

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

1 Ответ

0 голосов
/ 02 марта 2019

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 работает аналогично: каждая помеченная строка соответствует идентификатору и каждому переходу из строки lстрока m изменит счетчик программы в следующем состоянии с l на m.

...