\documentclass[landscape]{seminar}

\usepackage{alltt,graphicx,fixseminar,latexsym,color}

\definecolor{GreenYellow}{cmyk}{0.15,0,0.69,0}
\definecolor{Yellow}{cmyk}{0,0,1.,0}
\definecolor{Goldenrod}{cmyk}{0,0.10,0.84,0}
\definecolor{Dandelion}{cmyk}{0,0.29,0.84,0}
\definecolor{Apricot}{cmyk}{0,0.32,0.52,0}
\definecolor{Peach}{cmyk}{0,0.50,0.70,0}
\definecolor{Melon}{cmyk}{0,0.46,0.50,0}
\definecolor{YellowOrange}{cmyk}{0,0.42,1.,0}
\definecolor{Orange}{cmyk}{0,0.61,0.87,0}
\definecolor{BurntOrange}{cmyk}{0,0.51,1.,0}
\definecolor{Bittersweet}{cmyk}{0,0.75,1.,0.24}
\definecolor{RedOrange}{cmyk}{0,0.77,0.87,0}
\definecolor{Mahogany}{cmyk}{0,0.85,0.87,0.35}
\definecolor{Maroon}{cmyk}{0,0.87,0.68,0.32}
\definecolor{BrickRed}{cmyk}{0,0.89,0.94,0.28}
\definecolor{Red}{cmyk}{0,1.,1.,0.3}
\definecolor{OrangeRed}{cmyk}{0,1.,0.50,0}
\definecolor{RubineRed}{cmyk}{0,1.,0.13,0}
\definecolor{WildStrawberry}{cmyk}{0,0.96,0.39,0}
\definecolor{Salmon}{cmyk}{0,0.53,0.38,0}
\definecolor{CarnationPink}{cmyk}{0,0.63,0,0}
\definecolor{Magenta}{cmyk}{0,1.,0,0}
\definecolor{VioletRed}{cmyk}{0,0.81,0,0}
\definecolor{Rhodamine}{cmyk}{0,0.82,0,0}
\definecolor{Mulberry}{cmyk}{0.34,0.90,0,0.02}
\definecolor{RedViolet}{cmyk}{0.07,0.90,0,0.34}
\definecolor{Fuchsia}{cmyk}{0.6,1,0,0.2}
\definecolor{Lavender}{cmyk}{0,0.48,0,0}
\definecolor{Thistle}{cmyk}{0.12,0.59,0,0}
\definecolor{Orchid}{cmyk}{0.32,0.64,0,0}
\definecolor{DarkOrchid}{cmyk}{0.40,0.80,0.20,0}
\definecolor{Purple}{cmyk}{0.45,0.86,0,0}
\definecolor{Plum}{cmyk}{0.50,1.,0,0}
\definecolor{Violet}{cmyk}{0.79,0.88,0,0}
\definecolor{RoyalPurple}{cmyk}{0.75,0.90,0,0}
\definecolor{BlueViolet}{cmyk}{0.86,0.91,0,0.04}
\definecolor{Periwinkle}{cmyk}{0.57,0.55,0,0}
\definecolor{CadetBlue}{cmyk}{0.62,0.57,0.23,0}
\definecolor{CornflowerBlue}{cmyk}{0.65,0.13,0,0}
\definecolor{MidnightBlue}{cmyk}{0.98,0.13,0,0.43}
\definecolor{NavyBlue}{cmyk}{0.94,0.54,0,0}
\definecolor{RoyalBlue}{cmyk}{1.,0.50,0,0}
\definecolor{Blue}{cmyk}{1.,1.,0,0.3}
\definecolor{Cerulean}{cmyk}{0.94,0.11,0,0}
\definecolor{Cyan}{cmyk}{1.,0,0,0}
\definecolor{ProcessBlue}{cmyk}{0.96,0,0,0}
\definecolor{SkyBlue}{cmyk}{0.62,0,0.12,0}
\definecolor{Turquoise}{cmyk}{0.85,0,0.20,0}
\definecolor{TealBlue}{cmyk}{0.86,0,0.34,0.02}
\definecolor{Aquamarine}{cmyk}{0.82,0,0.30,0}
\definecolor{BlueGreen}{cmyk}{0.85,0,0.33,0}
\definecolor{Emerald}{cmyk}{1.,0,0.50,0}
\definecolor{JungleGreen}{cmyk}{0.99,0,0.52,0}
\definecolor{SeaGreen}{cmyk}{0.69,0,0.50,0}
\definecolor{Green}{cmyk}{1.,0,1.,0}
\definecolor{ForestGreen}{cmyk}{0.91,0,0.88,0.12}
\definecolor{PineGreen}{cmyk}{0.92,0,0.59,0.25}
\definecolor{LimeGreen}{cmyk}{0.50,0,1.,0}
\definecolor{YellowGreen}{cmyk}{0.44,0,0.74,0}
\definecolor{SpringGreen}{cmyk}{0.26,0,0.76,0}
\definecolor{OliveGreen}{cmyk}{0.64,0,0.95,0.40}
\definecolor{RawSienna}{cmyk}{0,0.72,1.,0.45}
\definecolor{Sepia}{cmyk}{0,0.83,1.,0.70}
\definecolor{Brown}{cmyk}{0,0.81,1.,0.60}
\definecolor{Tan}{cmyk}{0.14,0.42,0.56,0}
\definecolor{Gray}{cmyk}{0,0,0,0.50}
\definecolor{Black}{cmyk}{0,0,0,1.}
\definecolor{White}{cmyk}{0,0,0,0}

\newenvironment{Maude}[1]
{\begin{center}\vspace{-2.5ex}\begin{minipage}{#1}\begin{alltt}}
{\end{alltt}\end{minipage}\end{center}}

\newenvironment{Slide}[1]
{
\begin{slide}
\sf
\begin{center}
\textcolor{cyan}{\Large\em #1}
\end{center}
}
{
\end{slide}
}

\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\EM}[1]{\textcolor{red}{\em #1}}

\begin{document}

\begin{Slide}{\huge Maude 2.2 Demo}
\begin{center}
\vspace{0.5in}
WRLA 2006
\end{center}
\end{Slide}


\begin{Slide}{Overview}
\begin{itemize}
\item New features in 2.2
\begin{itemize}
\item Random numbers
\item Counters
\item External objects
\item Parameterization
\item Predefined container modules
\item Linear Diophantine solver
\end{itemize}
\item Work in progress
\begin{itemize}
\item Builtin strategy language
\end{itemize}
\end{itemize}
\end{Slide}


\begin{Slide}{Random numbers}
\begin{itemize}
\item We use the Mersenne Twister as a source of high quality random
  numbers.
\item The sequence of numbers generated from a particular seed is
  viewed as a function \EM{random} from the natural numbers into
  $[0,\ldots, 2^{32} -1]$.
\item Internally, the state of the Mersenne Twister is cached so that
  if \EM{random} was last called on $n$, calling it on $n+k$ requires
  $k$ steps of the twister; usually $k=1$.
\item The seed is set at startup time with the command line flag
  -random-seed=$\la \it{int} \ra$ so the sequence is constant for any
  given run of Maude.
\end{itemize}
\end{Slide}


\begin{Slide}{Counters}
\begin{itemize}
\item It is often useful to have implicitly stored state, especially
  when working with random numbers.
\item Such state cannot be functional but is available in system
  modules via counters.
\item \EM{counter} is a special constant of kind [Nat] that each time
  it is rewritten (by rules) generates the next larger natural number.
\item It can be viewed as a special builtin strategy for executing
  the otherwise nonexecutable rule:
\begin{Maude}{5in}
  rl counter => N:Nat [nonexec] .
\end{Maude}
\item Additional counters can be created using renamed
  copies. Reseting of counters between commands is avoided by
\begin{Maude}{5in}
  set clear rules off .
\end{Maude}
\
\end{itemize}
\end{Slide}

\begin{Slide}{External objects}
\begin{itemize}
\item Maude 2.2 supports external objects to represent entities in the
  external world.
\item Configurations that want to communicate with external objects
  must contain at least one portal.
\begin{Maude}{5in}
  sort Portal .
  subsort Portal < Configuration .
  op <> : -> Portal [ctor] .
\end{Maude}
\item \EM{erewrite } is used to start rewrite sequences that may
  involve external objects.
\item \EM{erewrite } may not terminate even if no rewrites are
  possible; this is because there may be incomplete transactions with
  external objects and more rewriting may be possible once they
  complete.
\end{itemize}
\end{Slide}


\begin{Slide}{Internet sockets}
\begin{itemize}
\item Maude 2.2 supports IPv4 TCP client and server sockets.
\item Sockets are created by sending a message to a special external
  object called:
\begin{Maude}{5in}
  op socketManager : -> Oid [special (...)] .
\end{Maude}
\item The created socket external objects are named using the constructor
\begin{Maude}{5in}
  op socket : Nat -> Oid [ctor] .
\end{Maude}
\item \EM{send} and \EM{receive} messages can then be sent to the
  newly created socket objects.
\item Message are usually paired - a user object sends a message to
  an external object and waits for a reply message. This enforces
  sequentialization in the otherwise concurrent Maude
  configuation.
\end{itemize}
\end{Slide}


\begin{Slide}{Parameterization}
\begin{itemize}
\item Core Maude now supports a subset of Full Maude module
parameterization.
\item Modules may now take a list of parameters:
\begin{Maude}{5in}
fmod MAP\{X :: TRIV, Y :: TRIV\} is
\end{Maude}
\item Sorts may be parameterized:
\begin{Maude}{5in}
sorts Entry\{X,Y\} Map\{X,Y\} .
\end{Maude}
\item Instances of parameterized modules must be fully instantiated
  before they can be imported.
\item Instantiating by a module-view removes the parameter.
\item Instantiation by a theory-view changes the theory of a
  parameter.
\item The final instantiation in a module may instantiate using
  parameters from the enclosing module.
\end{itemize}
\end{Slide}


\begin{Slide}{Predefined Parameterized Modules 1}
\begin{itemize}
\item The predefined module LIST provides associative lists over TRIV
\item Adding or removing elements from either end is amortized constant time
  except for pathological cases.
\item Concatenation and reversal is linear time.
\item The predefined module SET provides sets over TRIV.
\item Insertion and deletion of elements is $O(\log n)$ time.
\item Union, intersection and difference are $O(n \log n)$ time where
  $n$ is the size of the largest set involved.
\item Views from TRIV are provided for all the standard builtin data
  types.
\end{itemize}
\end{Slide}


\begin{Slide}{Predefined Parameterized Modules 2}
\begin{itemize}
\item The theory TAO-SET decribes transitive, antisymmetric orderings
  (reflexivity is unspecified).
\item This structure is just strong enough for merge and sorting to
  work correctly.
\item The predefined module SORTABLE-LIST builds on top of LIST and
  provides an $O(n \log n)$ time sorting operation for lists over
  TAO-SET.
\item Views from TAO-SET are provided for the standard builtin data
  types where it makes sense.
\item The predefined module LIST-AND-SET provides conversion between
  lists and sets and allows a list to be filtered by a set.
\end{itemize}
\end{Slide}


\begin{Slide}{Predefined Parameterized Modules 3}
\begin{itemize}
\item The predefined module MAP provides maps from TRIV to TRIV with
  $O(\log n)$ time lookup and updating.
\item The theory DEFAULT describes data types with a distinguished
  element.
\item The predefined module ARRAY closely resembles MAP but has
  DEFAULT as its target theory.
\item Mapppings to the distinguished element are not stored, and
  missing entries are assumed to map to the distinguished element.
\item Views from DEFAULT are provided for the standard builtin data
  types where it makes sense.
\item Nestable versions of lists and sets are provided by LIST* and
  SET*.
\end{itemize}
\end{Slide}

\begin{Slide}{Linear Diophantine solver}
\begin{itemize}
\item Integer vectors and matricies are implemented as instantiations
  of module ARRAY.
\item The predefined module DIOPHANTINE contains a solver for
  non-negative solutions of (homogenous and inhomogenous) linear Diophantine equations.
\item The solution is a pair of sets of integer vectors $A$ and $B$.
\item The non-negative solutions are formed by adding a vector from
  $A$ to a non-negative linear combination of vectors from $B$.
\item Two algorithms are currently implemented - Contejean-Devie and a
  method based on Gaussian elimination and extended gcd.
\end{itemize}
\end{Slide}


\begin{Slide}{Builtin strategy language 1}
\begin{itemize}
\item Rewritng with a strategy is invoked by:
\begin{Maude}{5in}
srewrite [<nat>] in <module> :
    <term> using <strategy> .
\end{Maude}
\item Leaf strategies implemented so far:
\begin{tabular}{ll}
fail &	   produce the empty set of successors \\
idle &	   produce the identity rewrite\\
all &	   apply any rule\\
l &	   apply a rule with label l \\
l[s] &	   apply a rule with label l and substitution s
\end{tabular}
\end{itemize}
\end{Slide}


\begin{Slide}{Builtin strategy language 2}
\begin{itemize}
\item Combinators implemented so far:
\begin{tabular}{ll}
s * &	   do s 0 or more times\\
s + &	   do s 1 or more times\\
s ; s' &	   do s and then s'\\
s $\mid$ s' &	   do s or s'\\
t ? s : f &  do t, if it produces results, do s on them; \\
 & else do f on the original term
\end{tabular}
\end{itemize}
\end{Slide}

\end{document}
