The Is Boxed Algorithm

In order to determine if a certain sequent or a formula is in an Always scope, we apply the following mutually recursive algorithms is_box and is_diamond (note: we refer to both using is_?):

We first fully expand TLA operators such as fairness, actions, etc.
  • is_?(A,B,... |- F) -> is_?(F)
  • is_?(F) -> True if F is constant
  • is_?(True | False) -> True
  • is_box([]F) -> True
  • is_diamond(<>F) -> True
  • is_?([]F | <>F | F') -> is_?(F)
  • is_box(~F) -> is_diamond(F)
  • is_diamond(~F) -> is_box(F)
  • is_?(F /\ G | F \/ G) -> is_?(F) /\ is_?(G) and similarly for lists
  • is_box(F -> G) -> is_diamond(F) /\ is_box(G) and similarly for {{is_diamond(F -> G)} | is_?(F <-> G)}
  • is_?(op(a,b,...)) -> is_?(a) /\ is_?(b) /\ ...
  • else False

Proof of Soundness (i.e. if is_box(F) and F, then []F)

Note, since none of the proofs is using assumptions, the algorithm is not used within its own proof.

------------------------------ MODULE isboxed ------------------------------

EXTENDS TLAPS 

VARIABLE A,B

IsBox(C) == [](C <=> []C)
IsDmd(C) == [](C <=> <>C)

THEOREM ASSUME NEW CONSTANT C
        PROVE  IsBox(C) /\ IsDmd(C)

THEOREM IsBox([]A)
BY PTL DEF IsBox, IsDmd

THEOREM IsBox(A) /\ IsBox(B) => IsBox(A /\ B) /\ IsBox(A \/ B)
BY PTL DEF IsBox, IsDmd

THEOREM IsBox(A) => IsBox([]A)
BY PTL DEF IsBox, IsDmd

THEOREM IsBox(A) => IsBox(<>A)
BY PTL DEF IsBox, IsDmd

THEOREM IsDmd(A) => IsBox(~A)
BY PTL DEF IsBox, IsDmd

THEOREM IsDmd(<>A)
BY PTL DEF IsBox, IsDmd

THEOREM IsDmd(A) /\ IsDmd(B) => IsDmd(A /\ B) /\ IsDmd(A \/ B)
BY PTL DEF IsBox, IsDmd

THEOREM IsDmd(A) => IsDmd([]A)
BY PTL DEF IsBox, IsDmd

THEOREM IsBox(A) => IsDmd(~A)
BY PTL DEF IsBox, IsDmd

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

Last edited Dec 10, 2013 at 3:44 PM by libal, version 13