Проверить выполнение веток

Программа может перейти от СТАРТа к ЛЕВОЙ или ПРАВОЙ ветви. Как я могу проверить, есть ли путь выполнения для ЛЕВОЙ ветки и другой путь выполнения для ПРАВОЙ ветки?

------------------------------ MODULE WFBranch ------------------------------

VARIABLE state

START == "start"
LEFT == "left"
RIGHT == "right"

Init == state = START

Next ==
    \/  /\ state = START
        /\  \/ state' = LEFT
            \/ state' = RIGHT
    \/  /\ state \in {LEFT, RIGHT}
        /\ state' = START

Spec ==
    /\ Init
    /\ [][Next]_<<state>>
    /\ WF_<<state>>(Next) \* Avoid stuttering at start

(*
This passes, but it does not ensure that there exist different paths covering both
branches - e.g. state might never be LEFT.
*)
CheckEventualStates == \/ (state = START) ~> (state = RIGHT)
                       \/ (state = START) ~> (state = LEFT)

=============================================================================

formal-verification tla+
person Jakub M.    schedule 10.12.2017    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

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

Left == 
  /\ state = START
  /\ state' = LEFT

Right ==
  /\ state = START
  /\ state' = RIGHT

Next ==
    \/  /\ state = START
        /\  \/ Left
            \/ Right
    \/  /\ state \in {LEFT, RIGHT}
        /\ state' = START

Затем вы можете проверить, есть ли две ветки с

CheckEventualStates ==
    /\ <>(ENABLED Left)
    /\ <>(ENABLED Right)
person Hovercouch    schedule 10.12.2017
comment
FTR, ENABLED описан в Спецификации систем 8.4 Слабая справедливость - person Jakub M.; 11.12.2017