Theory Views

(*<*)
theory Views
imports
  ClockView
  SPRViewDet
  SPRViewNonDet
  SPRViewNonDetIndInit
  SPRViewSingle
begin
(*>*)

section‹Concrete views›

text‹

\label{sec:kbps-theory-views}

Following \<^citet>‹"Ron:1996"›, we provide two concrete synchronous views
that illustrate how the theory works. For each view we give  a
simulation and a representation that satisfy the requirements of the
‹Algorithm› locale in Figure~\ref{fig:kbps-alg-alg-locale}.

›

(*<*)
end
(*>*)