\documentclass[landscape]{seminar}

\usepackage{alltt,graphicx,fixseminar,latexsym,color}
%
\def\ttlb{\(\{\)}
\def\ttrb{\(\}\)}

\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}\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.1 Demo}
\begin{center}
\vspace{0.5in}
WRLA 2004
%M. Clavel\ \ \ \ F. Dur\'{a}n\ \ \ \ S. Eker\ \ \ \ P. Lincoln\\
%\vspace{.2in}
%N. Mart\'{\i}-Oliet\ \ \ \ J. Meseguer\ \ \ \ C. Talcott
\end{center}
\end{Slide}


\begin{Slide}{Overview}
\begin{enumerate}
\item New features in 2.1
\begin{itemize}
\item Module expressions.
\item Explicit lightweight polymorphism.
\item upTerm/downTerm functions.
\item More ascent functions.
\item Minor enhancements.
\end{itemize}
\item Projects using Maude.
\begin{itemize}
\item JavaFAN.
\item Pathway Logic.
\end{itemize}
\end{enumerate}
\end{Slide}


\begin{Slide}{Module expressions}
\begin{itemize}
\item Only allowed for imports.
\item Supports arbitrary nesting of renaming and summation.
\item Renaming respects import structure - only modules affected by
renaming get copied.
\item Sorts, operators and labels can be renamed; renamed operators
may change their syntactic attributes.
\item Modules created for module expressions are ``virtual'' - only
parts of their contents is generated to save memory.
\item Caching of module expressions ensures that a given module is
only imported once.
\end{itemize}
\end{Slide}


\begin{Slide}{Renamed natural numbers}
\vspace{.1in}
\begin{Maude}{3.3in}
fmod 2NAT is
  including NAT + NAT *
   (sort Zero to Zero',
    sort Nat to Nat',
    sort NzNat to NzNat',
    op 0 : -> Zero to z) .
endfm

red 6 * 7 .
red 6 * (7).Nat .
red (6 * 7).Nat' .
red z + 42 .
red 0 + 42 .
\end{Maude}
\end{Slide}


\begin{Slide}{Explicit lightweight polymorphism}
\begin{itemize}
\item Introduced to make the lightweight polymorphism implicit in certain
builtin operators such as {\tt if\_then\_else\_fi} and {\tt \_==\_} explicit:
{\scriptsize
\begin{Maude}{3.3in}
op if_then_else_fi : Bool Universal Universal -> Universal 
      [poly (2 3 0)
       special (id-hook BranchSymbol
                term-hook 1 (true)
                term-hook 2 (false))] .

op _==_ : Universal Universal -> Bool 
      [prec 51 poly (1 2)
       special (id-hook EqualitySymbol
                term-hook equalTerm (true)
                term-hook notEqualTerm (false))] .
\end{Maude}
}
\item However it is available for user defined constructors.
\item Instances of polymorphic operators are created on demand on a
per kind basis.
\end{itemize}
\end{Slide}


\begin{Slide}{Polymorphic lists}
{\scriptsize
\begin{Maude}{3.3in}
fmod POLY-LIST is
  sort List .
  op nil : -> List [ctor] .
  op __ : Universal List -> List [ctor poly (1)] .
endfm

fmod POLY-LIST-TEST is
  pr POLY-LIST + CONVERSION + QID .
  op list2string : List -> String .

var L : List . var S : String . var Q : Qid .
var R : Rat . var F : Float . 
  eq list2string(nil) = "" .
  eq list2string(S L) = S + list2string(L) .
  eq list2string(Q L) = "'" + string(Q) + list2string(L) .
  eq list2string(R L) = string(R, 10) + list2string(L) .
  eq list2string(F L) = string(F) + list2string(L) .
endfm

red list2string("The answer is " 42.0 " but that is only "
1/2 " of the " 'problem "." nil) .
\end{Maude}
}
\end{Slide}


\begin{Slide}{upTerm/downTerm builtin functions}
\begin{itemize}
\item Move terms from the object level to the metalevel and back.
\item Module must include the {\em object signature} as well as the
metalevel signature.
\item Typing is solved by the lightweight polymorphism:
\begin{Maude}{3.3in}
op upTerm : Universal -> Term
    [poly (1) special (...)] .

op downTerm : Term Universal -> Universal
    [poly (2 0) special (...)] .
\end{Maude}
\item Second argument of downTerm provides both the object level kind
and the object level return value if the metaterm does not represent a
term in that kind.
\end{itemize}
\end{Slide}


\begin{Slide}{Remaining ascent functions}
\begin{itemize}
\item All parts of modules in the module database and whole modules
can be lifted to the metalevel:
\begin{Maude}{3.3in}
op upModule : Qid Bool ~> Module [...] .
op upImports : Qid ~> ImportList [...] .
op upSorts : Qid Bool ~> SortSet [...] .
op upSubsortDecls : Qid Bool ~> SubsortDeclSet
    [...] .
op upOpDecls : Qid Bool ~> OpDeclSet [...] .
\end{Maude}
\item Hooks for builtin operators are correctly handled and resulting metamodules can be
passed to descent functions.
\end{itemize}
\end{Slide}
 
\begin{Slide}{Up and down example}
{\scriptsize
\begin{Maude}{3.3in}
red in META-LEVEL : upModule('META-LEVEL, true) .
red in META-LEVEL : upModule('NAT, true) .

red in META-LEVEL :
downTerm(getTerm(metaReduce(upModule('NAT, true),
                            '_*_[upTerm(6), upTerm(7)])),
         undef:Nat) .

red in META-LEVEL :
downTerm(getTerm(metaReduce(upModule('META-LEVEL, true),
          'metaReduce[upTerm(upModule('NAT, true)), 
                      upTerm('_*_[upTerm(6), upTerm(7)])])),
         undef:Term) .
\end{Maude}
}
\end{Slide}


\begin{Slide}{Minor enhancements}
\begin{itemize}
\item Source tree now includes a test suite.
\item Standard prelude quo/rem/gcd/lcm/divides functions extended to
rationals.
\item show module/show all commands now handle specials/hooks.
\item Constructor coloring now supported for iter operators.
\item Many bug fixes!
\end{itemize}
\end{Slide}


\begin{Slide}{JavaFAN (Java Formal ANalyzer)}
\begin{itemize}
\item Work by Azadeh Farzan, Jos\'{e} Meseguer and Grigore Ro\,{c}u at
Urbana.
\item Tool for the formal analysis of Java Virtual Machine (JVM) bytecode
produced by compiling Java programs.
\item Executable specification of the 150 most commonly used JVM
bytecode instructions.
\item Deterministic JVM features specified by 300 equations.
\item Concurrent JVM features specified by 40 rewrite rules.
\item Analysis methods include symbolic execution, safely property
checking by proof search and model checking using Maudes LTL model checker.
\end{itemize}
\end{Slide}


\begin{Slide}{JavaFAN - Dining Philosophers}
\begin{itemize}
\item The example uses the Maude LTL model checker to find a deadlock for
4 (naive) philosophers.
\item JavaFAN can find a deadlock for version with 9 philosophers.
\item It can also prove deadlock freeness for fixed version with
7 philosophers.
\item Java PathFinder chokes on 4 philosophers.
\end{itemize}
\end{Slide}


\begin{Slide}{JavaFAN - Thread Game}
\begin{itemize}
\item Thread Game (J. S. Moore) consists of two process accessing a
common variable $c$.
\item Each thread reads $c$ twice and writes the sum of the two values
back to $c$.
\item The problem is to find an interleaving of executions that leaves
$c$ with a given value $n$.
\item The example uses the Maude seach command to solve this for $n = 50$.
\end{itemize}
\end{Slide}

\begin{Slide}{Pathway Logic - Protein Domain Modules}
\begin{itemize}
\item Proteins are sequences of amino acids; biologists refer to
certain subsequences as \textcolor{red}{domains} or
\textcolor{red}{motifs}.
\item In the domain level Maude model, a protein is a pair consisting of a
name and a multiset of domains (e.g. SBM) and amino acid sites
(e.g. (S 43)).
\item Both domains and amino acid sites can take modifiers to
indicate that they are bound or phosphorylated.
\item The overall system state is a multiset of protein and edges between
specific domains or amino acid sites.
\item Rules encode possible interactions that change peices of the
system state.
\end{itemize}
\end{Slide}



\begin{Slide}{Pathway Logic - phosphorylation of Raf}
\begin{center}
\includegraphics[scale=0.3]{raf10}
\end{center}
\end{Slide}

\begin{Slide}{Pathway Logic - example rule}
\begin{center}
{\scriptsize\begin{alltt}
rl[Raf1#3.PS.PA]:
 \ttlb{}CM | cm PS PA
   \ttlb{}cyto [Raf1 | (S 43), (S 259), (S 338), (Y 341),
                 (S 621 - phos - bound), \textcolor{ForestGreen}{C1, PABM}, raf:Atts]
       [14-3-3a | (SBD - bound), (DMD - bound), 1a:Atts]
       [14-3-3b | SBD, (DMD - bound), (T 141 - phos)]
       e((14-3-3a, DMD), (14-3-3b,DMD))
       e((Raf1, (S 621)), (14-3-3a,SBD))\ttrb\ttrb
  =>
 \ttlb{}CM | cm PS PA
       [Raf1 | (S 43), (S 259), (S 338), (Y 341),
               (S 621 - phos - bound), \textcolor{ForestGreen}{(C1 - bound), (PABM - bound)}, raf:Atts]
       [14-3-3a | (SBD - bound), (DMD - bound), 1a:Atts]
       [14-3-3b | SBD, (DMD - bound), (T 141 - phos)]
       e((14-3-3a,DMD), (14-3-3b,DMD))
       e((Raf1, (S 621)), (14-3-3a,SBD))
       \textcolor{Emerald}{e((Raf1, C1), b(PS)) e((Raf1,PABM), b(PA))}
      \ttlb{}cyto\ttrb\ttrb .
  [ metadata "21278045(R-20)  20379031(D) for PA  99426181(D) for PS"] .
\end{alltt}}
\end{center}
\end{Slide}

\begin{Slide}{Pathway Logic - execution}
\begin{itemize}
\item findPath runs the model checker and extracts a simple path (list of
rule labels and the final state) from the counterexample.
\item Look for the desired final state:
\begin{Maude}{3.3in}
red findPath(qraf, praf0) .
\end{Maude}
\item Look for an expected intermediate state
\begin{Maude}{3.3in}
red findPath(qraf, praf1) .
\end{Maude}
\item Look for an undesired intermediate state
\begin{Maude}{3.3in}
red findPath(qraf, praf2) .
\end{Maude}
\end{itemize}
\end{Slide}

\end{document}
