DIGITAL SEQUENCES

This grammar makes clocks and their scoping explicit.

R ::= @(c)(b)
      | R ##1 R
      | R ##0 R
      | R or R
      | R intersect R
      | R[*0]
      | R[*1:$]


REALTIME SEQUENCES

R ::= b
      | @(c)(b)
      | R ##1 R
      | R ##0 R
      | R or R
      | R intersect R
      | R[*0]
      | R[*1:$]
      | R #0 R
      | R without @(c)
      | b[*\alpha[+]:\beta[-]]
      | b{*\alpha[+]:\beta[-]}


SVA PROPERTIES

P ::= strong(R)
      | weak(R) // need special letters
      | (\tau v[=e]; P) // \tau is a type; if there is an initialization
                        // assignment, then P must be a boolean
                        // combination of subproperties, each of 
                        // which has a single leading clock
      | not P
      | P or P
      | P and P
      | R |-> P
      | R |=> P
      | @(c)(nexttime P)
      | @(c)(P until P)
      | accept_on(b) P  // need special letters
     
. W,t |= strong(R)

  iff

  \exists non-empty, left-closed I s.t. inf(I) = t and W,I |== R

. W,t |= not P

  iff

  W,t |/= P // assuming W has no special letters

. W,t |= P or P'

  iff

  either W,t |= P or W,t |= P' 

. W,t |= P and P'

  iff

  both W,t |= P and W,t |= P' 

. [Dejan's proposed definition]

  W,t |= R |-> P
 
  iff

  \forall non-empty, left-closed I s.t. inf(I) = t and W,I |== R:
  - if I is right-closed, then W,sup(I) |= P
  - if I is right-open, then there exists t', inf(I) <= t' < sup(I), 
    such that W,u |= P for all t' < u < sup(I)

  [??? Do we want to require W,sup(I) |= P in the second case above?]

  [A weaker definition]

  W,t |= R |-> P
 
  iff

  \forall non-empty, closed I s.t. inf(I) = t and W,I |== R:  W,sup(I) |= P

. W,t |= @(c)(nexttime P)

  iff

  W,t |= c[->1] ##1 c[->1] |-> P


=========================
SANITY

General definition:

.  W,I |== R ##1 R'
   
   iff
 
   \exists J, J' :
      1. I = J \cup J'
      2. J < J'
      3. W,J |== R and W,J' |== R'

Specialize to:

.  W,I |== R ##1 R'
   
   iff
 
   \exists J, J' :
      1. I = J \cup J'
      2. J < J'
      3. W,J |== R and W,J' |== R'

General definition

.  W,I |== R[*1:$]

   iff

   \exists n >= 1 and J_1,...,J_n such that 
   1. \forall 1 <= i < j <= n:  J_i < J_j
   2. I = J_1 \cup ... \cup J_n
   3. \forall 1 <= i <= n:  W,J_i |== R

Specialize to:

.  W,I |== R[*2]

   iff

   \exist J_1,J_2 such that 
   1. J_1 < J_2
   2. I = J_1 \cup J_2
   3. W,J_1 |== R and W,J_2 |== R

=========================
SANITY

[Dejan's proposed definition]

. W,t |= R |-> P
 
  iff

  \forall non-empty, left-closed I s.t. inf(I) = t and W,I |== R,
  - if I is right-closed, then W,sup(I) |= P
  - if I is right-open, then there exists t', inf(I) <= t' < sup(I), 
    such that W,u |= P for all t' < u < sup(I)

. W,t |= R |-> R' |-> P
 
  iff

  \forall non-empty, left-closed I s.t. inf(I) = t and W,I |== R,
  - if I is right-closed, then W,sup(I) |= R' |-> P
  - if I is right-open, then there exists t', inf(I) <= t' < sup(I), 
    such that W,u |= R' |-> P for all t' < u < sup(I)

  iff

  \forall non-empty, left-closed I s.t. inf(I) = t and W,I |== R,
  - if I is right-closed, then \forall non-empty, left-closed I' s.t.
    inf(I') = sup(I) and W,I' |== R',
    . if I' is right-closed, then W,sup(I') |= P
    . if I' is right-open, then there exists t'', inf(I') <= t'' < sup(I'),
      such that W,u |= P for all t'' < u < sup(I')
  - if I is right-open, then there exists t', inf(I) <= t' < sup(I), 
    such that W,u |= R' |-> P for all t' < u < sup(I)

It does not seem that this will give adjoint associativity in the second
case because there is no realtime sequence operator that slides the left 
endpoint of the second interval in the way that u slides above.

[Weaker proposed definition]

. W,t |= R |-> P
 
  iff

  \forall non-empty, closed I s.t. inf(I) = t and W,I |== R:  W,sup(I) |= P

. (Adjoint Associativity)

  W,t |= R ##0 R' |-> P

  iff

  \forall non-empty closed J s.t. inf(J) = t and W,J |== R ##0 R':  W,sup(J) |= P

  iff

  \forall non-empty, closed J s.t. inf(J) = t and s.t. \exists I,I',a s.t.
     1. J = I \cup I' and I \cap I' = [a,a]
     2. I <= [a,a]
     3. [a,a] <= I'
     4. W,I |== R and W,I' |== R'
  W,sup(J) |= P

  iff 

  [ 

     (=>) Assume the statement above.  Let I, I' be non-empty, closed
     s.t. inf(I) = t, inf(I') = sup(I), W,I |== R, and W,I' |== R'.
     Let J = I \cup I', a = inf(I') = sup(I).  Then I <= [a,a] <= I'.
     Since I,I' are closed, I \cap I' = [a,a].  Then 1.-4. above hold,
     so W,sup(J) |= P.  sup(J) = sup(I'), so the statement below
     holds.

     (<=) Assume the statement below.   Let J be non-empty, closed s.t.
     inf(J) = t and s.t. \exists I,I',a s.t. 1.-4. above hold.  From
     1.-3. and the fact that J is closed, it follows that I and I' are
     non-empty and closed.  Also, inf(I) = inf(J) = t, sup(I') = sup(J),
     and sup(I) = inf(I') = a.  From below, W,sup(I') |= P, which proves
     the statement above.

  ]

  \forall non-empty, closed I s.t. inf(I) = t and W,I |== R:
  \forall non-empty, closed I' s.t. inf(I') = sup(I) and W,I' |== R': W,sup(I') |= P

  iff

  \forall non-empty, closed I s.t. inf(I) = t and W,I |== R:  W,sup(I) |= R' |-> P

  iff

  W,t |= R |-> R' |-> P


=========================
EXPLORE

. R |=> P  
  \equiv 
  R #0 (1[*0.0+:$] without @(leading_clocks(P))) #0 1 |-> P

. R |=> R' |=> P
  \equiv R #0 (1[*0.0+:$] without @(leading_clocks(P))) #0 1 |-> R' |=> P
  \equiv R #0 (1[*0.0+:$] without @(leading_clocks(R' |=> P))) #0 1 |-> 
         R' #0 (1[*0.0+:$] without @(leading_clocks(P))) #0 1 |-> P
  \equiv R #0 (1[*0.0+:$] without @(leading_clocks(R' |=> P))) #0 1 ##0 
         R' #0 (1[*0.0+:$] without @(leading_clocks(P))) #0 1 |-> P