% 

\newcommand{\seqcircuit}[3]{% #1=S, #2=r, #3=A
\begin{tikzpicture}[shorten >=0.8pt,node distance=2cm,on grid,auto,
    double distance=1.5pt,
    every state/.style={
      semithick,
      fill=gray!10,
      shape=rectangle
    },
    every edge/.style={
      draw,->,
      >={Stealth[length=2.8mm,width=3.6mm,inset=2.3mm]},
      semithick,
      auto
    },
    every loop/.style={looseness=8}]
   \node (s) {#1}; 
   \node[state] (r) [right=of s] {#2};
   \node (a) [above=of r] {#3}; 
   \path [->] (s) edge node {} (r);
   \path [->] (a) edge node {} (r);
   \draw [->] (r) edge[out=270,in=270] node{} (s);
\end{tikzpicture}
}

\begin{document}

\begin{frame}
  \frametitle{Exercise: Snack Dispenser}

  Snack dispenser has 6 levels with 4 slots each. Each slot can hold 10 items.
  Each item costs 2 CHF. The only way to operate a machine is to insert 1 CHF coin into temporary storage (one step), 
  which must be done two times,
  then select the refreshment (in one step), which immediately dispenses the snack or cancels and returns coins
  if none is available in the slot, or if the stable coin storage is full.
  The machine can hold up to 500 CHF in its stable coin storage. 
  It starts full with items but with no coins. Describe this transition system and 
  estimate the cardinality of the set of all of its states. Can the stable storage ever hold 99 coins? 100 coins?
  490 coins?

  \ \\

  \Ovalbox{
  \begin{tabular}{|r|r|r|r||l} \hline
    10 & 10 & 10 & 10 \\ \hline
    10 & 10 & 10 & 10 \\ \hline 
    10 & 10 & 10 & 10 \\ \hline 
    10 & 10 & 10 & 10 \\ \hline 
    10 & 10 & 10 & 10 \\ \hline 
    10 & 10 & 10 & 10 & 0 coins \\ \hline 
  \end{tabular}
  } 
  \begin{tabular}{l}
  \pause
    states: $10^{4\cdot 6} \cdot 501 \cdot 2 = 10^{24} \cdot 1002 > 10^{27}$ \\
  \pause  
    coins: $0 \to 2 \to \ldots \to 98 \to 100 \to 240 \cdot 2 = 480$ \\
  \end{tabular}
\end{frame}

\begin{frame}
  \frametitle{Sets of States (Reachable, Invariants) are Too Large to Store Explicitly}

  Approach: use formulas and data structure to represent them compactly

  Use general formulas as in Stainless: expressive, but not very automated

  \  

  For finite state systems: can get much more automation.

  \  

  Two important algorithms:
  \begin{itemize}
    \item bounded model checking using SAT solvers
    \item (reachability) model checking using binary decision diagrams (BDDs)
  \end{itemize}
  
  \ 

  These algorithms play important role in model checking hardware designs and are basis
  for tools and more complex algorithms.
\end{frame}

\begin{frame}
  \frametitle{Encoding Finite Transition Systems with Bits: Sequential Circuit}

  Consider a deterministic 
  finite-state transition system: $M = (S, I, r, A)$ 

  If we pick $n \ge \log_2 |S|$ and $m \ge \log_2 |A|$, we can represent the finite-state
  transition system using boolean functions:
  \begin{itemize}
  \item each element of $S$ as $\bar s \in \{0,1\}^n$, so $S = \{0,1\}^n$
  \item each element of $A$ as $\bar a \in \{0,1\}^m$, so $A = \{0,1\}^m$
  \item initial states $I \subseteq S$ by the characteristic function $\{0,1\}^n \to \{0,1\}$
  \item deterministic transition relation $r \subseteq S \times A \times S$ as function 
  $(S \times A) \to S$, that is, $\{0,1\}^n \times \{0,1\}^m \to \{0,1\}^n$
  \end{itemize}

  \vspace*{-0.5cm}
  \begin{center}
    \scalebox{0.9}{\seqcircuit{$\bar s \in \{0,1\}^n$}{$r$}{$\bar a \in \{0,1\}^m$}}
  \end{center}
  
  \vspace*{-0.5cm}
  (For non-deterministic systems, we represent $r$ as $(S \times A \times S) \to \{0,1\}$)
\end{frame}

\begin{frame}
  \frametitle{Example: Blinking Lights}
  \begin{minipage}{7cm}
  \begin{itemize}
    \item $S = \{0,1\}$ ($1$ = ``light on'')
    \item $A = \{0,1\}$ ($1$ = ``toggle light'')
    \item $I(s) = (s = 0)$
    \item $r(s,a) = s \oplus a$
  \end{itemize}   
  \end{minipage}
  \begin{minipage}{4cm}
    \seqcircuit{$\{0,1\}$}{$\oplus$}{$\{0,1\}$}
  \end{minipage}

  Example trace:
  \input{trace-blinking.tex}

\end{frame}

\begin{frame}
  \frametitle{Example: Accumulator with Add and Clear Commands}
  \begin{minipage}{9cm}
  \begin{itemize}
    \item $S = \{0,1\}^n$ (value of accumulator)
    \item $A = \{0,1\}^n \times \{0,1\}$ (number to add, clear signal)
    \item $I(s) = (s = 0^n)$
    \item $r(s,(i,c)) = $ \mbox{if (c) then 0 else} $s +_{n}\, i$ \\ 
          ($+_{n}$ is addition modulo $2^n$)
  \end{itemize}   
  \end{minipage}
  \begin{minipage}{4cm}
    \seqcircuit{$\{0,1\}^n$}{$r$}{$\{0,1\}^n \times \{0,1\}$}
  \end{minipage}

  Example trace:
  \begin{center}
  \input{trace-accum.tex}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Encoding Finite Transition Systems with Bits: Sequential Circuit}

  Consider a deterministic 
  finite-state transition system: $M = (S, I, r, A)$ 

  If we pick $n \ge \log_2 |S|$ and $m \ge \log_2 |A|$, we can represent the finite-state
  transition system using boolean functions:
  \begin{itemize}
  \item each element of $S$ as $\bar s \in \{0,1\}^n$, so $S = \{0,1\}^n$
  \item each element of $A$ as $\bar a \in \{0,1\}^m$, so $A = \{0,1\}^m$
  \item initial states $I \subseteq S$ by the characteristic function $\{0,1\}^n \to \{0,1\}$
  \item deterministic transition relation $r \subseteq S \times A \times S$ as function 
  $(S \times A \times S) \to S$, that is, $\{0,1\}^n \times \{0,1\}^m \to \{0,1\}^n$
  \end{itemize}

  \begin{flushright}
  \begin{minipage}{4cm}
    \seqcircuit{$\bar s \in \{0,1\}^n$}{$r$}{$\bar a \in \{0,1\}^m$}
  \end{minipage}
  \textbf{How to represent boolean functions, like $r$, efficiently?}
  \end{flushright}
\end{frame}


\begin{frame}
  \frametitle{Boolean Function Representation: Table}
    
    Let $r: \{0,1\}^n \times \{0,1\}^m \to \{0,1\}^n$

    List each of the $\{0,1\}^{n+m}$ inputs and specify the result

    When $s,a \in \{0,1\}^4$ and represent addition of 4-bit non-negative integers modulo $16$:

    $\begin{array}{c|c|c}
      s    & a    & r(s,a) \\ \hline
      0000 & 0000 & 0000 \\
      0000 & 0001 & 0001 \\
      0000 & 0010 & 0010 \\
      \multicolumn{3}{c}{\cdots} \\
      0001 & 0000 & 0001 \\
      0001 & 0001 & 0010 \\
      \multicolumn{3}{c}{\cdots} \\
      1111 & 1111 & 1110 \\
    \end{array}$    
    \raisebox{-7pt}{$\left.\rule{0pt}{56pt}\right\}$ $2^{4 + 4} = 256$ columns}

    In general, we cannot do better than truth table (there are that many different functions), but truth table always has bad representation size, even for functions like $+_4$.
\end{frame}

\begin{frame}
    \frametitle{Boolean Function Representation: Formulas}

    Let $r \subseteq \{0,1\}^n \times \{0,1\}^m \times \{0,1\}^n$

    We represent the condition
    \[
      ((s_1,\ldots,s_n),(a_1,\ldots,a_m),(s'_1,\ldots,s'_n)) \in r
    \]
    by writing a propositional formula with variables 
    $s_1,\ldots,s_n$, $a_1,\ldots,a_m$, $s'_1,\ldots,s'_n$ that is true
    precisely when the tuple belongs to $r$.
    
    If $p$ is a propositional variable and $v \in \{0,1\}$ then we define
    $p^v$ by $p^1 = p$ and $p^0 = \lnot p$.

    We can always represent $r$ by a propositional formula in disjunctive normal form:
    \[
        \bigvee_{((v_1,\ldots,v_n),(u_1,\ldots,u_m),(v'_1,\ldots,v'_n)) \in r}
          \left( 
            \bigwedge_{1 \le i \le n} s_i^{v_i} \land
            \bigwedge_{1 \le i \le m} a_i^{u_i} \land
            \bigwedge_{1 \le i \le n} ({s'}_i)^{v'_i} 
          \right)
    \]
   so we do not lose on generality. Moreover, for many boolean 
   functions, we can write down smaller formulas.
\end{frame}

\begin{frame}
  \frametitle{Example Formula for Blinking Lights}

  \begin{minipage}{7cm}
  \begin{itemize}
    \item $S = \{0,1\}$ ($1$ = ``light on'')
    \item $A = \{0,1\}$ ($1$ = ``toggle light'')
    \item $I(s) = (s = 0)$
    \item $r(s,a) = s \oplus a$
  \end{itemize}   
  \end{minipage}
  \begin{minipage}{4cm}
    \seqcircuit{$\{0,1\}$}{$\oplus$}{$\{0,1\}$}
  \end{minipage}

  Formula $R$ represents condition $(s,a,s') \in r$:
  \[\begin{array}{l|l}
  r \ (\mbox{relation}) & R \ (\mbox{formula}) \\ \hline
  \{ (0,0,0), & (\lnot s \land \lnot a \land \lnot s')\ \lor \\
  (0,1,1),    & (\lnot s \land a \land s')\ \lor \\
  (1,0,1),    & (s \land \lnot a \land s')\ \lor \\
  (1,1,0) \}  & (s \land a \land \lnot s')
  \end{array}\]  
\end{frame}

\begin{frame}[fragile]
  \frametitle{Propositional (Boolean) Logic}

  Propositional logic is a language for representing Boolean functions
  $f : \{0,1\}^n \to \{0,1\}$.
  \begin{itemize}
    \item sometimes we write $\bot$ for $0$ and $\top$ for $1$
  \end{itemize}

  Grammar of formulas:
  \[
     P ::= x \mid 0 \mid 1 \mid P \land P \mid \lnot P  \mid P \lor P \mid P \oplus P \mid
           P \rightarrow P \mid P \leftrightarrow P
  \]
  where $x$ denotes variables (identifiers). Corresponding Scala trees:

  \lstinputlisting{expr-syntax.scala}
\end{frame}

\begin{frame}
  \frametitle{Environment and Truth of a Formula}
  An environment $e$ is a partial map from propositional variables to $\{0,1\}$   

  For vector of $n$ boolean variables $\bar p = (p_1,\ldots,p_n)$ and $\bar v = (v_1,\ldots,v_n) \in \{0,1\}^n$, we denote
  $[\bar p \mapsto \bar v]$ the environment $e$ given by $e(p_i) = v_i$ for $1 \le i \le n$.
  
  We write $e \models F$, and define $\interp{F}{e}=1$, to denote that $F$ is true in environment $e$, otherwise define 
  $\interp{F}{e}=0$

  Let $e = \{ (a,1), (b, 1), (c, 0) \}$ and $F$ be $a \land (\lnot b \lor c)$. Then:
  \[
      \interp{a \land (\lnot b \lor c)}{e} \ =\ e(a) \land (\lnot e(b) \lor e(c)) 
                                  \ =\ 1 \land (\lnot 1 \lor 0)
                                  \ =\ 0
  \]
  The general definition is recursive:
  \[\begin{array}{rcl}
    \interp{x}{e} & = & e(x) \\
    \interp{0}{e} & = & 0 \\
    \interp{1}{e} & = & 1 \\
    \interp{F_1 \land F_2}{e} &=& \interp{F_1}{e} \land \interp{F_2}{e} \\
    \interp{\lnot F_1}{e} &=& \lnot \interp{F_1}{e}
  \end{array}\]
  Note: $\land$ and $\lnot$ on left and right are different things
\end{frame}

\begin{frame}
    \frametitle{Truth of a Formula in Scala}

    We can define it as \lstinline|interpret| method on propositional expressions class:

    \ 

    \lstinputlisting{expr-interpret.scala}
\end{frame}

\begin{frame}
  \frametitle{Satisfiability Problem}

    Formula $F$ is \emph{satisfiable}, iff there \textbf{exists} $e$ such that 
    $\interp{F}{e}=1$. 
    
    Otherwise we call $F$ \emph{unsatisfiable}: when there does not exist $e$
    such that $\interp{F}{e}=1$, that is, for all $e$, $\interp{F}{e}=0$.
    
    Example: let $F$ be $a \land (\lnot b \lor c)$. Then $F$ is satisfiable, 
    with e.g. $e = \{(a,1),(b,0),(c,0)\}$

    Its negation of $\lnot F$, is also satisfiable, 
    with e.g. $e = \{(a,0),(b,0),(c,0)\}$

   \

    SAT is a problem: given a propositional formula, determine whether it is satisfiable.

  \

  The problem is decidable because given $F$ we can compute its variables
  $FV(F)$ and it suffices to look at the $2^{n}$ environments for $n = FV(F)$.
  The problem is NP-complete, but useful heristics exist.

  \

    A SAT solver is a program that, given boolean formula $F$, either:
    \begin{itemize}
    \item returns \textbf{sat}, and, optionally, 
    returns one environment $e$ such that $\interp{F}{e}=1$, or
    \item returns \textbf{unsat} and, optionally, returns a \textbf{proof} that
    no satisfying assignment exists 
    \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Observation about Eliminating Variables}

    Let $F,G$ be propositional formulas and $c$ a propositional variable

    Let $F[c:=G]$ denote the result of replacing in $F$ \emph{each} occurrence of $c$ by $G$:
    \[\begin{array}{rcl}
        c[c:=G] &=& G \\
        (F_1 \land F_2)[c:=G] &=& F_1[c:=G] \land F_2[c:=G] \\
        (F_1 \lor F_2)[c:=G] &=& F_1[c:=G] \lor F_2[c:=G] \\
        (\lnot F_1)[c:=G] &=& \lnot (F_1[c:=G])
    \end{array}
    \]
    We also generalize to simultaneous replacement of many variables, $F[\bar c:=\bar G]$

    Then following formulas are equivalent (have same truth for all free variables):
    \begin{itemize}
      \item $F[c:=G]$
      \item $\exists c. ((c = G) \land F)$
      \item $\forall c. ((c = G) \rightarrow F)$
    \end{itemize}
    Note: free variables are the variables occurring in the formula minus quantified ones ($c$)
\end{frame}

\begin{frame}
    \frametitle{Free Variables for Quantified Boolean Formulas}

    Quantified boolan formulas (QBF) are build from propositional variables and constants
    $0,1$ using
    $\land,\lor,\lnot,\rightarrow,\leftrightarrow,\exists,\forall$

    (We also write $=$ for $\leftrightarrow$.)
    A boolean formula is a QBF without quantifiers $\forall,\exists$.

    Definition of free variables of a formula:
    \[\begin{array}{rcl}
      FV(v) &=& \{v\} \mbox{ when $v$ is a propositional variable} \\
      FV(F_1 \land F_2) &=& FV(F_1) \cup FV(F_2) \\
      FV(F_1 \lor F_2) &=& FV(F_1) \cup FV(F_2) \\
      FV(F_1 \rightarrow F_2) &=& FV(F_1) \cup FV(F_2) \\
      FV(\lnot F_1) &=& FV(F_1) \\
      FV(\exists v. F_1) &=& FV(F_1) \setminus \{v\} \\
      FV(\forall v. F_1) &=& FV(F_1) \setminus \{v\} 
    \end{array}\]

    An environment $e$ maps propositional variables to $\{0,1\}$ 
    (sometimes written $\{\bot,\top\}$)

%    For vector of $n$ boolean variables $\bar p = (p_1,\ldots,p_n)$ and $\bar v = (v_1,\ldots,v_n) \in \{0,1\}^n$, we denote
%    $[\bar p \mapsto \bar v]$ the environment $e$ given by $e(p_i) = v_i$ for $1 \le i \le n$.
    
%    We write $e \models F$ to denote that $F$ is true in environment $e$.
\end{frame}


\begin{frame}
  \frametitle{Validity and Equivalence}


    Definition: Formula $F$ is valid, iff for all $e$, $e \models F$.

    \
    
    \textbf{Observation: $F$ is valid iff $\lnot F$ is unsatisfiable.} 

    \ 

    Definition: Formulas $F$ and $G$ are equivalent iff for every $e$ that defines all variables
    in $FV(F) \cup FV(G)$, we have: $e \models F$ iff $e \models G$.

    \ 

    Observation: $F$ and $G$ are equivalent iff $F \leftrightarrow G$ is valid.

    \ 

    $\exists p. F$ is equivalent to $F[p:=0] \lor F[p:=1]$ whereas
    $\forall p. F$ to $F[p:=0] \land F[p:=1]$
\end{frame}

\begin{frame}
    \frametitle{Boolean Function Representation: Circuits}

    Formulas correspond to \emph{trees}: variables are leaves, operations internal nodes.

    More efficient representation that exploits sharing: directed acyclic graphs (DAGs).

    We can view DAGs as formulas with \emph{auxiliary variable} definitions.

    Example for simple (ripple-carry) $n$-bit adder: 
    \begin{itemize}
    \item input numbers: $s_1\ldots s_n$ and $a_1 \ldots a_n$
    \item output: $s'_1\ldots s'_n$
    \end{itemize}
    The formula with auxiliary variables $c_1,\ldots, c_{n+1}$:
    \[
        c_1 =0 \land 
        \bigwedge_{i=1}^n (s'_i = s_i \oplus a_i \oplus c_i) \land
                          (c_{i+1} = (s_i \land a_i) \lor (s_i \land c_i) \lor (a_i \land c_i))
    \]
    We can implement such definitions in hardware: route an output
    of one gate to multiple other gates.
    
    To get back a tree: substitute all auxiliary variables $c_i$, but we get much
    bigger formula. Or, existentially quantify all auxiliary variables.
\end{frame}


%{\setbeamercolor{background canvas}{bg=yellow!20}
  \begin{frame}
    \frametitle{Formula Representation of Sequential Circuits}
    
    We represent sequential circuit as $C = (\bar s,Init,R,\bar x,\bar a)$ where:
    \begin{itemize}
    \item $\bar s = (s_1,\ldots,s_n)$ is the vector of state variables
    \item $Init$ is a boolean formula with $FV(Init) \subseteq \{s_1,\ldots,s_n\}$
    \item $\bar a = (a_1,\ldots,a_m)$ is the vector of input variables
    \item $\bar x = (x_1,\ldots,x_k)$ is the vector of auxiliary variables (for $R$)
    \item $R$ is a boolean formula called transition formula, for which
     \[
        FV(R) \subseteq \{s_1,\ldots,s_n,a_1,\ldots,a_m,x_1,\ldots,x_k,s'_1,\ldots,s'_n\}
     \]
    \end{itemize}
    Transition system for $C$ is $(S,I,r,A)$ where $S = \{0,1\}^n$, $A= \{0,1\}^m$,
    \begin{itemize}
    \item $I = \{ \bar v \in \{0,1\}^n \mid [\bar s \mapsto \bar v] \models Init \}$
    \item $r = \{ (\bar v,\bar u,\bar v') \in \{0,1\}^{n+m+n} \ \mid \        
         [(\bar s,\bar a,\bar s') \mapsto (\bar v,\bar u,\bar v')] \models \exists \bar x. R \}$
    \end{itemize}
    Auxiliary variables $\bar x$ are treated as existentially quantified, 
    can use conjucts $x_i = E(\bar s,\bar a,\bar x)$ to express intermediate values.
  \end{frame}
%}

\begin{frame}
    \frametitle{Checking Inductive Invariant using SAT Queries}

    Given sequential circuit representation $C = (\bar s,Init,R,\bar x,\bar a)$
    and a formala $Inv$ with $FV(Inv) \subseteq \{s_1,\ldots,s_n\}$, how do we check that 
    $Inv$ is an inductive invariant?

    \pause
    Let us write \emph{negations} of conditions ``$Init \subseteq Inv$'' and ``$r[Inv] \subseteq Inv$''
    \begin{itemize}
      \item An initial state is not included in invariant: 
      \[ 
         Init \land \lnot Inv
      \]           
      \item \pause There is a state satisfying invariant, leading to a state that breaks invariant: 
      \[ 
          \underbrace{Inv}_{\bar s} \land 
          \underbrace{R}_{\bar s,\bar a,\bar x,\bar s'} \land 
          \underbrace{\lnot Inv[\bar s:= \bar s']}_{\bar s'}
      \] 
      Note that $\bar a,\bar x$ variables are also existentially quantified, as they should be.
    \end{itemize}

    \

    We can check if a formula is an inductive invariant using two queries to a SAT solver
    and making sure that they both return \textbf{unsat}.
\end{frame}

%{\setbeamercolor{background canvas}{bg=green!20}
\begin{frame}
    \frametitle{Bounded Model Checking for Reachability}

    We construct a propositional formula $T_j$ such that formula is satisfiable if and only if
    there exist a trace of length $j$ starting from initial state that satisfies error formula $E$
    where $FV(E) \subseteq \{s_1,\ldots,s_n\}$.

    $\bar s^i$ denotes state variables in step $i$.

    $\bar a^i$ denotes inputs in step $i$.

    \begin{center}
      \input{trace-general.tex}
    \end{center}
    
    \[ T_j \ \ \equiv \ \
      Init[\bar s := \bar s^0] \ \land \ \left( \bigwedge_{i=0}^{j-1} R_i \right) \ 
      \land \ E[\bar s := \bar s^j]
    \]
    where $R_i$ is our transition formula, with variables renamed:
    \[  
       R_i \ \equiv \
        R[(\bar s,\bar a,\bar x,\bar s'):=(\bar s^i,\bar a^i,\bar x^i,\bar s^{i+1})]
    \]

\end{frame}
%}


