\documentclass{article}
\setlength{\textwidth}{7in}
\setlength{\textheight}{9.25in}
\setlength{\oddsidemargin}{-.25in}
\setlength{\evensidemargin}{-.25in}
\setlength{\topmargin}{-.75in}
\setlength{\unitlength}{1.01mm}

\usepackage{amsmath,amssymb}

\begin{document}
\title{CS476 Last Comprehensive Homework \\ Due at 11:59pm  on Monday 12/12}


\date{}
\maketitle

\noindent {\bf Important Notes:}
 (1) In consideration of the fact that you may be involved
in various final exams, you are given a full week to solve this 
Comprehensive Homework.  Given the very ample time you have available,
except for a major, verifiable emergency, like a grave
illness, there will be no  extensions possible:
any solutions emailed after 11:59pm  on Monday 12/12 will get 0 points.
Your solutions, as well as all Maude code
for exercises requiring it, should be emailed to
\texttt{nishant2@illinois.edu}.  In addition, your screenshots for
interactions with tools \emph{should be present in the same pdf containing your answers
to the homework's problems}.
(2) All Maude code for the different
exercises can be obtained from the Latex file for this Comprehensive
Homework, also available in the CS 476 web page.



\begin{enumerate}
\item Let $h: \mathbb{A} \longrightarrow \mathbb{B}$ be a
$\Sigma$-isomorphism, and $u=v$ a
$\Sigma$-equation.  Prove that
\[\mathbb{A} \models u=v \;\;\; \Leftrightarrow \;\;\; 
\mathbb{B}\models u=v.\]

\vspace{2ex}

\noindent {\bf For Extra Credit}.  You can earn 10 more points (out of
the total of 10 for this exercise) if you also prove that
the above equivalence generalizes to one of the form:
\[\mathbb{A} \models \varphi \;\;\; \Leftrightarrow \;\;\; 
\mathbb{B}\models \varphi.\]
for $\varphi$ a \emph{quantifier-free} $\Sigma$-formula
(recall the Appendix on First-Order Logic to Lecture 14).


\item Consider the definition of binary trees with natural numbers
  on the leaves given in Lecture 16.  Complete the module
  \texttt{NAT-TREE+AC} given below
  by defining with confluent and
  terminating equations the two functions called \texttt{leaves} and
  \texttt{inner}, that count, respectively, the number of leaf nodes of
  a tree, and the number of nodes in a tree that are \emph{not} leaf
  nodes.  For example, for the tree \verb+((0 ^ s(0)) ^ 0) ^ s(0)+
  there are 4 leaf nodes (namely \texttt{0}, \texttt{s(0)},
  \texttt{0}, and \texttt{s(0)}, and 3 inner nodes (corresponding to
  the 3 different occurrences of the \texttt{\^} operator).

\begin{verbatim}
set include BOOL off .

fmod PEANO+AC is sort Nat .
    op 0 : -> Nat [ctor metadata "0"] .
    op s : Nat -> Nat [ctor metadata "4"] .
    op _+_ : Nat Nat -> Nat [assoc comm metadata "8"] .
    vars N M : Nat .
    eq N + 0 = N .
    eq N + s(M) = s(N + M) .
endfm


fmod NAT-TREE+AC is protecting PEANO+AC .
    sort  Tree .  subsort Nat < Tree .
    op _^_ : Tree Tree -> Tree [ctor metadata "6"] .
    op inner : Tree -> Nat [metadata "10"] .  *** counts inner nodes
    op leaves : Tree -> Nat [metadata "12"] . *** counts tree leaves
    vars N M : Nat .  vars T1 T2 : Tree .
    *** add equations for leaves and inner here
endfm
\end{verbatim}

Once you have defined and tested your definitions for 
\texttt{leaves} and  \texttt{inner} do the following, \emph{including screenshots
for each tool used} in your solutions for this homework:

\begin{itemize}
\item check that \texttt{NAT-TREE+AC} is confluent using the Church-Rosser
Checker
\item check that \texttt{NAT-TREE+AC} is terminating using the MTA with the RPO
  order specified by the \texttt{metadata} annotations
\item check that \texttt{NAT-TREE+AC} is sufficiently complete using the SCC tool
\item state a theorem, in the form of an
equation, that gives a general
law stating, for any tree \texttt{T}, the exact
relation between the numbers 
\texttt{leaves(T)} and  \texttt{inner(T)} 
\item give a mechanical proof of that theorem using Maude's NuITP.
\end{itemize}

\item The asynchronous and unordered communication protocol between
sender and receiver objects in the \texttt{COMM} module below
 is a  variant of the example protocol
in Lecture 17.  

\begin{verbatim}
fmod NAT-LIST is protecting NAT .
 sort List .
 subsorts Nat < List .
 op nil : -> List .
 op _;_ : List List -> List [assoc id: nil] .
 op length : List -> Nat .
 var L : List .
 var N : Nat .
 eq length(nil) = 0 .
 eq length(N ; L) = s(length(L)) . 
endfm

mod COMM is protecting NAT-LIST . protecting  QID .
 sorts Oid Class Object Msg Msgs Att Atts Configuration State .
 subsort Qid < Oid .  
 subsort Att < Atts .     *** Atts is set of attribute-value pairs
 subsort Object < Configuration .
 subsorts Msg < Msgs < Configuration .
 op none : -> Msgs [ctor] .
 op __ : Configuration Configuration -> Configuration
                       [ctor config assoc comm id: none] .
 op __ : Msgs Msgs -> Msgs
                       [ctor config assoc comm id: none] .
 op null : -> Atts .		       
 op _,_ : Atts Atts -> Atts [ctor assoc comm id: null] .
 op buff:_ : List -> Att [ctor] .
 op snd:_ : Oid -> Att [ctor] .
 op rec:_ : Oid -> Att [ctor] .
 op cnt:_ : Nat -> Att [ctor] .
 op ack-w:_ : Bool -> Att [ctor] .
 ops Sender Receiver : -> Class [ctor] .
 op <_:_|_> : Oid Class Atts -> Object [ctor] .
 msg to_from_val_cnt_ : Oid Oid Nat Nat -> Msg [ctor] .
 msg to_from_ack_ : Oid Oid Nat -> Msg [ctor] .  
 op {_} : Configuration -> State [ctor] . 
 op init : Oid Oid List -> State .

 vars N M : Nat . var L : List .  vars A B : Oid .  var C : Configuration .
 
 rl [snd] : {< A : Sender | buff: (N ; L), rec: B, cnt: M, ack-w: false > C}
   => 
    {(to B from A val N cnt M)
    < A : Sender | buff: L, rec: B, cnt: M, ack-w: true > C} .
  
 rl [rec] : {< B : Receiver | buff: L, snd: A, cnt: M >
      (to B from A val N cnt M) C}
    =>
      {< B : Receiver | buff: (L ; N), snd: A, cnt: s(M) >
      (to A from B ack M) C} .

 rl [ack-rec] : {< A : Sender | buff: L, rec: B, cnt: M, ack-w: true >
    (to A from B ack M) C}
    =>
    {< A : Sender | buff: L, rec: B, cnt: s(M), ack-w: false > C} .

 eq init(A,B,L) = {< A : Sender | buff: L, rec: B, cnt: 0, ack-w: false > 
                   < B : Receiver | buff: nil, snd: A, cnt: 0 >} .
endm

rew init('a,'b,(1 ; 2 ; 3)) .

rew init('a,'b,(1 ; 2 ; 3 ; 4)) .

rew init('a,'b,(1 ; 2 ; 3 ; 4 ; 5)) .
\end{verbatim}

The only differences are: (1) the buffers
now are not separate objects: they are attributes of sender and receiver
objects;  (2) the sender,  before sending the next item in its
buffer,  awaits until after  receiving an \texttt{ack} from the
receiver for the previous item; and (3) to facilitate the definition
of state predicates, the entire configuration of objects
and messages in enclosed in curly braces as a term of sort 
\texttt{State}.
You may want to run a few tests
cases.  For example, those given in the rewrite commands after the
\texttt{COMM} module, to get a better feeling for how this protocol works.
If you wish to see a detailed trace of the executions, you can type in Maude:

\begin{verbatim}
Maude> set trace on . 
\end{verbatim}

The point about this exercise is to increase your familiarity with
\emph{parametric} state predicates and their model checking
verification.  Parametric state predicates are very useful for
both verifying invariants with the \texttt{search} command
(the case in this exercise), and to perform LTL model checking
of parametric properties.
The key idea is that
 we may be interested in verifying properties
\emph{that depend on the initial state}; but
not for a single initial state \texttt{init}, but, instead, for a \emph{parametric
  family of initial states}, defined using and operator:
\begin{verbatim}
op init : S1 ... Sn -> State . 
\end{verbatim}
and giving appropriate equations,
were the sorts \verb+S1 ... Sn+ are its \emph{parameter sorts}.
But then, some property \verb+P+, which we want to verify is
an invariant for all these initial states, may also be itself \emph{parametric}
in the exact same sense, i.e., be a Boolean-valued  state predicate
of the form:
\begin{verbatim}
op P : State S1 ... Sn -> Bool . 
\end{verbatim}
If \verb+u1 ... un+ are ground terms of the parameter sorts \verb+S1 ... Sn+,
then we can model check property \verb+P+ as an invariant
from the initial state \verb+init(u1 ... un)+
by failing to get any solutions for the \texttt{search} command:
\begin{verbatim}
search  init(u1 ... un) =>* X:State s.t.  P(X:State,u1,...,un) =/= true . 
\end{verbatim}

Specifically, you are asked to correctly define
an (unparametric) state predicate [which is not an invariant],
and two parametric state predicates
[corresponding to two invariants],
 whose
operator declarations are given in the \texttt{COMM-PREDS} module below.
The state predicates are the following:

\begin{itemize}
\item {\bf Enabled}: a state is not a deadlock state and can therefore
transition to some other state.

\vspace{2ex}

\item {\bf In-Order} (Communication).
Any initial state of the form \texttt{init(A,B,L)} satisfies
the parametric
state predicate \texttt{In-Order(X:State,A,B,L)} (which you are asked to define)
as an \emph{invariant},
where \\ \texttt{In-Order(X:State,A,B,L)} essentially states that 
if in state \texttt{X:State}  \texttt{L1} is the list in the buffer of the receiver \texttt{B}, 
then the list
 \texttt{L1}  is  a \emph{prefix sublist} of the list \texttt{L}.
This  means that the protocol achieves \emph{in-order-communication} in
spite of being asynchronous.

\vspace{2ex}

\item {\bf Succcess} (of the Communication).
Any initial state of the form \texttt{init(A,B,L)} satisfies
the parametric
state predicate \texttt{Success(X:State,A,B,L)} (which you are asked to define)
as an \emph{invariant},
where \texttt{Success(X:State,A,B,L)} essentially states that
either \texttt{X:State} is  {\bf Enabled}, or
\texttt{B} holds \texttt{L} in its buffer.  Since this protocol is
\emph{terminating}, this invariant ensures that, not only it delivers 
data in order, but the protocol does indeed \emph{succeed}
 in always delivering \emph{all
  the data} initially stored in the sender's buffer.
\end{itemize}

You can define these predicates by giving your definition
[and that of any auxiliary functions you may need] in the
following module importing \texttt{COMM}.  You can make use the
the \verb+[owise]+ feature in Maude to define the \verb+false+ case for
each predicate. 


\begin{verbatim}
mod COMM-PREDS is 
 protecting COMM . 

 op Enabled : State -> Bool .
 ops In-Order Success : State Oid Oid List -> Bool .
 
 var MS : Msgs . var C : Configuration .  vars L L1 L2 : List .
 vars A B : Oid .  vars N M : Nat .  var T : Bool .  var S : State .

*** include here your equational definition of Enabled(S) 

*** include here your equational definition of In-Order(S,A,B,L) 

*** include here your equational definition of Success(S,A,B,L)

endm
\end{verbatim}

After you have defined [hopefully correctly] the above state
predicates, you are asked to verify in Maude the two parametric
invariants \verb+In-Order(S,A,B,L)+  and
\verb+Success(S,A,B,L)+ 
for three initial states of the form \texttt{init(A,B,L)} 
where \texttt{A} is \texttt{'a}, \texttt{B} is \texttt{'b},
and \texttt{L} is, respectively:  \texttt{(1 ; 2 ; 3)}, \texttt{(1 ; 2 ; 3 ; 4)},
and \texttt{(1 ; 2 ; 3 ; 4 ; 5)}.

\vspace{2ex}

The entire \emph{template} to be filled in, containing
all the modules for this problem is, therefore:
\begin{verbatim}
fmod NAT-LIST is protecting NAT .
 sort List .
 subsorts Nat < List .
 op nil : -> List .
 op _;_ : List List -> List [assoc id: nil] .
 op length : List -> Nat .
 var L : List .
 var N : Nat .
 eq length(nil) = 0 .
 eq length(N ; L) = s(length(L)) . 
endfm

mod COMM is protecting NAT-LIST . protecting  QID .
 sorts Oid Class Object Msg Msgs Att Atts Configuration State .
 subsort Qid < Oid .  
 subsort Att < Atts .     *** Atts is set of attribute-value pairs
 subsort Object < Configuration .
 subsorts Msg < Msgs < Configuration .
 op none : -> Msgs [ctor] .
 op __ : Configuration Configuration -> Configuration
                       [ctor config assoc comm id: none] .
 op __ : Msgs Msgs -> Msgs
                       [ctor config assoc comm id: none] .
 op null : -> Atts .		       
 op _,_ : Atts Atts -> Atts [ctor assoc comm id: null] .
 op buff:_ : List -> Att [ctor] .
 op snd:_ : Oid -> Att [ctor] .
 op rec:_ : Oid -> Att [ctor] .
 op cnt:_ : Nat -> Att [ctor] .
 op ack-w:_ : Bool -> Att [ctor] .
 ops Sender Receiver : -> Class [ctor] .
 op <_:_|_> : Oid Class Atts -> Object [ctor] .
 msg to_from_val_cnt_ : Oid Oid Nat Nat -> Msg [ctor] .
 msg to_from_ack_ : Oid Oid Nat -> Msg [ctor] .  
 op {_} : Configuration -> State [ctor] . 
 op init : Oid Oid List -> State .

 vars N M : Nat . var L : List .  vars A B : Oid .  var C : Configuration .
 
 rl [snd] : {< A : Sender | buff: (N ; L), rec: B, cnt: M, ack-w: false > C}
   => 
    {(to B from A val N cnt M)
    < A : Sender | buff: L, rec: B, cnt: M, ack-w: true > C} .
  
 rl [rec] : {< B : Receiver | buff: L, snd: A, cnt: M >
      (to B from A val N cnt M) C}
    =>
      {< B : Receiver | buff: (L ; N), snd: A, cnt: s(M) >
      (to A from B ack M) C} .

 rl [ack-rec] : {< A : Sender | buff: L, rec: B, cnt: M, ack-w: true >
    (to A from B ack M) C}
    =>
    {< A : Sender | buff: L, rec: B, cnt: s(M), ack-w: false > C} .

 eq init(A,B,L) = {< A : Sender | buff: L, rec: B, cnt: 0, ack-w: false > 
                   < B : Receiver | buff: nil, snd: A, cnt: 0 >} .
endm

rew init('a,'b,(1 ; 2 ; 3)) .

rew init('a,'b,(1 ; 2 ; 3 ; 4)) .

rew init('a,'b,(1 ; 2 ; 3 ; 4 ; 5)) .

mod COMM-PREDS is 
 protecting COMM . 

 op Enabled : State -> Bool .
 ops In-Order Success : State Oid Oid List -> Bool .
 
 var MS : Msgs . var C : Configuration .  vars L L1 L2 : List .
 vars A B : Oid .  vars N M : Nat .  var T : Bool .  var S : State .

*** include here your equational definition of Enabled(S) 

*** include here your equational definition of In-Order(S,A,B,L) 

*** include here your equational definition of Success(S,A,B,L)

endm
\end{verbatim}



\item The following example is a simplified version of Lamport's
  bakery protocol, of which several versions have been  presented in
  CS 476 lectures.
  A simple Maude specification for the case of two processes is as follows:

\begin{verbatim}
set include BOOL off .

fmod NAT-ACU is
  sort Nat .
  ops 0 1 : -> Nat [ctor] .
  op _+'_ : Nat Nat -> Nat [ctor assoc comm id: 0] .
endfm

mod BAKERY is
  protecting NAT-ACU .

  sorts Mode BState .

  ops sleep wait crit : -> Mode [ctor] .
  op <_,_,_,_> : Mode Nat Mode Nat -> BState [ctor] .
  op initial : -> BState .

  vars P Q : Mode .
  vars X Y : Nat .

  eq initial = < sleep, 0, sleep, 0 > .
  
  rl [p1_sleep] : < sleep, X, Q, Y > => < wait, Y +' 1, Q, Y > .
  rl [p1_wait] : < wait, X, Q, 0 > => < crit, X, Q, 0 > .
  rl [p1_wait] : < wait, X, Q, X +' Y > => < crit, X, Q, Y +' X > .
  rl [p1_crit] : < crit, X, Q, Y > => < sleep, 0, Q, Y > .
  
  rl [p2_sleep] : < P, X, sleep, Y > => < P, X, wait, X +' 1  > .
  rl [p2_wait] : < P, 0, wait, Y > => < P, 0, crit, Y > .
  rl [p2_wait] : < P, X +' Y +' 1, wait, Y > => < P, X +' Y +' 1, crit, Y > .
  rl [p2_crit] : < P, X, crit, Y > => < P, X, sleep, 0 > .
endm
\end{verbatim}
In this module, states are represented by terms of sort \texttt{BState}, 
which are constructed by a 4-tuple operator \verb+<_,_,_,_>+\,;
the first two components describe the status of the first process 
(the mode it is currently in, and its priority as given by the number 
according to which it will be served), and the last two
components the status of the second process.
The rules describe how each process passes from being sleeping to waiting, 
from waiting to its critical section, and then back to sleeping.

\vspace{2ex}

The problem, of course, is that, even in this simpler version,
\texttt{BAKERY} is infinite-state.

We would like to verify three LTL properties  about this protocol, namely:
\begin{itemize}
\item \emph{mutual exclusion}, that is, the two processes are
never simultaneously in their critical mode
\item
\emph{non-starvation of process 1}.  If process 1 is in its waiting 
mode infinitely often, then it will be in its critical mode infinitely often
\item \emph{non-starvation of process 2}.  If process 2 is in its waiting 
mode infinitely often, then it will be in its critical mode infinitely often.
\end{itemize}
Since the set of states reachable from \texttt{initial} is
\emph{infinite},  we cannot use Maude's explicit-state LTL model
checker to verify these
properties.  We can, however, use Maude's \emph{Logical LTL Model
  Checker} to verify that these three properties hold from an
\emph{even more general symbolic initial state of the form}:
\begin{verbatim}
 < sleep , X:Nat , sleep, X:Nat >
\end{verbatim}
To perform this verification, you first need to equationally define state predicates
\texttt{1wait},  \texttt{2wait}, \texttt{1crit} and \texttt{2crit},
corresponding to the case when process 1 (resp. process 2) is in its
\texttt{wait}, resp. \texttt{crit} mode.  Of course, the equations $D$
defining these predicates should be FVP.  But if the righthand sides
of all equations are either \texttt{true} or \texttt{false} and you
have specified the equations $D$ correctly, so that they are
confluent ad sufficiently complete, they \emph{will} be FVP.

\vspace{2ex}

\noindent To facilitate your work and the use of Maude's Logical LTL Model
Checker you just need to: (1) fill in the remaining equations
to \emph{fully define} the above for predicates in an FVP manner
in the template below; (2) enter the full template into the special
version of Maude running the Maude's Logical LTL Model
Checker; and (3) give three commands of the form:
\begin{verbatim}
( lfmc < sleep , X:Nat , sleep, X:Nat > |= formula1 ) .)

( lfmc < sleep , X:Nat , sleep, X:Nat > |= formula2 ) .)

( lfmc < sleep , X:Nat , sleep, X:Nat > |= formula3 ) .)
\end{verbatim}
where \texttt{formulai} expresses in LTL property \texttt{i}
for \texttt{i} = 1,2,3.
\begin{verbatim}
set include BOOL off .

fmod NAT-ACU is
  sort Nat .
  ops 0 1 : -> Nat [ctor] .
  op _+'_ : Nat Nat -> Nat [ctor assoc comm id: 0] .
endfm

mod BAKERY is
  protecting NAT-ACU .

  sorts Mode BState .

  ops sleep wait crit : -> Mode [ctor] .
  op <_,_,_,_> : Mode Nat Mode Nat -> BState [ctor] .
  op initial : -> BState .

  vars P Q : Mode .
  vars X Y : Nat .

  eq initial = < sleep, 0, sleep, 0 > .
  
  rl [p1_sleep] : < sleep, X, Q, Y > => < wait, Y +' 1, Q, Y > .
  rl [p1_wait] : < wait, X, Q, 0 > => < crit, X, Q, 0 > .
  rl [p1_wait] : < wait, X, Q, X +' Y > => < crit, X, Q, Y +' X > .
  rl [p1_crit] : < crit, X, Q, Y > => < sleep, 0, Q, Y > .
  
  rl [p2_sleep] : < P, X, sleep, Y > => < P, X, wait, X +' 1  > .
  rl [p2_wait] : < P, 0, wait, Y > => < P, 0, crit, Y > .
  rl [p2_wait] : < P, X +' Y +' 1, wait, Y > => < P, X +' Y +' 1, crit, Y > .
  rl [p2_crit] : < P, X, crit, Y > => < P, X, sleep, 0 > .
endm


load symbolic-checker

( mod BAKERY-PREDS is
  extending SYMBOLIC-CHECKER .
  protecting BAKERY .

  subsort BState < State .
  ops 1wait 2wait 1crit 2crit : -> Prop [ctor] .

  vars P Q : Mode .
  vars X Y : Nat .

  eq < wait, X, Q, Y > |= 1wait = true  [variant] .
 
  *** give here the remaining equations fully defining
  *** 1wait, 2wait, 1crit, and 2crit
  *** remember to include the [variant] attribute in all equations

endm )
\end{verbatim}

\noindent Detailed instructions on how to run the Maude LTL Logical
Model Checker can be found in the CS 476 web page.  Furthermore,
a tool tutorial/manual can be found in:

\vspace{2ex}

\texttt{https://maude.cs.uiuc.edu/tools/lmc/manual.pdf}

\vspace{2ex}

\noindent The tutorial uses various examples available in:

\vspace{2ex}

\texttt{https://maude.cs.uiuc.edu/tools/lmc/}


\end{enumerate}
\end{document}
