(*T* \usection{An Abstract Frame}\label{abstract} *T*)

(*T* This section describes the module |abstract| which provides an
abstract frame for the temporal logic library.  This frame is abstract
in the sense that it is a skeleton assuming an arbitray transition
system and includes all library modules which do not require any
specific assumptions about this system. A slightly less abstract
instance of this module will be presented in Section \ref{sect-ssvars},
where we replace the abstract state space by a state space with typed
variables. A more concrete instance of this module will be our
example in Section \ref{chap-example}, where we verify a particular
program specified by a unique transition system.  *T*)

(*T* We begin by including the module |init|, which in turn includes
the libraries discussed in the previous section. *T*)

Load init.

(*T* We now introduce the type |st| of states and the type |act| of
actions.  In this section we are concerned with the most abstract
setting, where we avoid any further assumptions on these types. *T*)

Variable st:Type.
Variable act:Type.

(*T* The ternary transition relation |trans| is declared next.  Given
an action |e| and states |s|, |s'| the proposition |(trans e s s')|
states that there is a state transition from |s| to |s'| with an
action |e|. *T*)

Variable trans : act->st->st->Prop .

(*T* We also need the notion of a view, which is just a set of
actions.  As explained before, a view induces a restriction of the
presupposed transition system and all temporal assertions are defined
relative to a view. For bevity, we often identify a view 
and its induced transition system in informal explanations. *T*)

Definition view := (set act).

(*T* In addition to the transition system we assume a set |wf| of
weakly fair groups of actions, which should at least contain
the empty group by our convention. *T*)

Variable wf : (set (set act)).

Hypothesis wf_contains_empty_set : 
  (In (set act) wf (Empty_set act)).

(*T* For the modules included below we just give some brief
explanations here, since they all will be discussed in more detail in
the subsequent sections.  *T*)

(*T* The module |state_pred| defines the central type |s_prop| of
state predicates and provides a collection of operators lifted from
propositions |Prop| to state predicates |s_prop|. *T*)

Load state_pred. 

(*T* The module |safety| defines temporal logic operators for
specifying safety assertions, in particular |co|, |unless|, |stable|
and |invariant| and contains a variety of theorems relating these
assertions to the system and to each other.  *T*)

Load safety.

(*T* The module |liveness| contains definitions of temporal operators
used to specify liveness assertions. These operators are |transient|,
|ensures| and |leads_to|. Also a collection of theorems relating
safety and liveness assertions are provided. *T*)

Load liveness.

(*T* Finally, we include the module |composition| which provides
support for compositional reasoning. *T*)

Load composition.