TLA +: Почему честный алгоритм все еще заикается? - PullRequest
Новая
       13

TLA +: Почему честный алгоритм все еще заикается?

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

Я использовал PlusCal для моделирования тривиального конечного автомата, который принимает строки, соответствующие регулярному выражению (X*)(Y). 

(*--fair algorithm stateMachine
variables
    state = "start";

begin

Loop:    
while state /= "end" do
    either
        \* we got an X, keep going
        state := "reading"
    or
        \* we got a Y, terminate
        state := "end"
    end either;
end while;


end algorithm;*)

Несмотря на то, что я пометил алгоритм fair, следующее временное условиедает сбой из-за заикания ... средство проверки модели учитывает случай, когда конечный автомат поглощает X, а затем просто останавливается на Loop, не делая ничего больше. 

MachineTerminates == <>[](state = "end")

Что означает справедливостьна самом деле означает в контексте простого процесса, как этот?Есть ли способ сообщить контролеру модели, что конечный автомат никогда не исчерпает входы и, следовательно, всегда завершит работу?

1 Ответ

2 голосов
/ 13 марта 2019

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

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

  1. Цикл может выбрать «конец», но не.
  2. Цикл может выбрать «конец», но этого не происходит.Это случается произвольное количество раз.
  3. Поскольку цикл верен *, он вынужден выбрать "конец".
  4. Мы закончили.

Ноэто не тот случай.Честность, в плюсе, на уровне лейбла.О том, что происходит на этикетке, ничего не говорится, просто должен произойти сам ярлык .Так что это совершенно правильное поведение:

  1. Поскольку цикл никогда не отключается, это в конечном итоге происходит.Он выбирает «чтение».
  2. Поскольку цикл никогда не отключается, это в конечном итоге происходит.Он выбирает «чтение».
  3. Поскольку цикл никогда не отключается, это в конечном итоге происходит.Он выбирает «чтение».
  4. Это продолжается вечно.

Это соответствует вводу строки бесконечной длины, состоящей только из X.Если вам нужны только конечные строки, вы должны явно выразить это либо как часть спецификации, либо как одно из предварительных условий для желаемого временного свойства.Например, вы могли бы сделать ваше временное свойство state = "end" ~> Termination, вы могли бы смоделировать входную строку, вы могли бы добавить счетчик «сколько х перед y» и т. Д. Это позволяет понять, что на самом деле неправильно, и в том, что является хорошим дизайном спецификацииХотя

Это нормальный случай.Но это очень, очень конкретное исключение из правила.Это из-за того, как «справедливость определяется».Формально WF_vars(A) == <>[](Enabled <<A>>_v) => []<><<A>>_v.Обычно мы переводим это как

Если система всегда может выполнить A, то она будет продолжать выполнять A.

Это интерпретация, которую я использовал до сих пор,Но это неправильно в одном очень большом смысле.<<A>>_vars == A /\ (vars' /= vars), или "А происходит, и vars изменяется. Таким образом, наше определение на самом деле:

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

Если у вас есть pc = "Loop" /\ state = "reading", выполнение state := "reading" делает не изменить состояние системы, чтобы она не учитывалась как <<Next>>_vars. Так что <<Next>>_vars на самом деле не произошло, но из-за слабой справедливости это в конечном итоге должно произойти. Единственный способ для <<Next>>_vars - это если циклустанавливает state := "reading, что позволяет завершить цикл while.

Это довольно нестабильная ситуация. Любое небольшое изменение, которое мы вносим в спецификацию, может подтолкнуть нас обратно на более знакомую территорию. Например, следующееспецификация не будет завершена, как ожидалось: 

variables
    state = "start";
    foo = TRUE;        
begin
Loop:    
while state /= "end" do
    foo := ~foo;
    either
        \* we got an X, keep going
        state := "reading"
    or
        \* we got a Y, terminate
        state := "end"
    end either;
end while;
end algorithm;*)

Даже если foo не влияет на остальную часть кода, это позволяет нам иметь vars' /= vars без необходимости обновления state.замена WF_vars(Next) на WF_pc(Next) приводит к сбою спецификации, так как мы можем достичь состояниягде <<Next>>_pc отключено (иначе любое состояние, где state = "reading").

* Цикл не честен, общий алгоритм.Это может иметь большое значение в некоторых случаях, именно поэтому мы спец.Но в этом случае проще говорить о цикле, так как это единственное действие.

...