Go backward to Reasoning about Composed Systems
Go up to Top
Go forward to Interleaving Representations

TLA

Canconical TLA specification form:
- exists $x$ : $Init$ and always [A]_v and $L$ .
- Initialization predicate $Init$ .
- Variable vector $v$ .
- Fairness conditions $L$ .
- There exists a sequence of values for $x$ such that Init is true in the initial state, every step of the behavior is an A step or leaves state function $v$ unchanged and $L$ holds.
Example: GCD
- $Init$ $<=>$ ( $a = 233344$ ) and ( $b = 233577899$ )
  A $<=>$ (( $a>b$ ) and ( $a'=a-b$ ) and ( $b'=b$ ))
  or (( $b>a$ ) and ( $b'=b-a$ ) and ( $a'=a$ ))
  $v$ $<=>$ < $a$ , $b$ >
  $L$ $<=>$ WF_v(A)

Wolfgang.Schreiner@risc.uni-linz.ac.at

Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine

Prev

Next