text:
\section{Introduction}
Detecting software errors and vulnerabilities is becoming increasingly important in a world where the demand for code development is soaring, often leading to incomplete specifications. Building tools to help achieve this goal is crucial as testing and manual revisions have proven to be insufficient to guarantee software correctness.

Indeed, a carefully designed test suite may detect the presence of many bugs, but it does not guarantee their absence~\cite{dijkstra1972humble}. A widespread practice is the use of programming languages with type systems~\cite{cardelli1996type}. These ensure that programs do not present errors for executing invalid operations, but the type of detected errors is quite limited. Day-to-day programmers have to deal with problems that arise from not checking the correct usage of an object. For example, a type system would prevent one from using an undefined method, but not from trying to write on a file prior to opening it.

Stateful objects are non-uniform~\cite{nierstrasz1993regular}, i.e., their methods' availability depends on their internal state. Behavioral types~\cite{huttel2016foundations} are notions of types for programming languages representing the possible behavior of an entity, such as an automaton or a state machine. These notions allow us to declare behavioral specifications capturing the availability of methods. For example, a file should first be opened (once), then it could be written (multiple times, as long as there is space), or read (provided it is not empty), and when its use is finished, it should be closed (once), and cannot be used until opened again.

Textual behavioral specifications, however, can be long and cumbersome. Furthermore, not only does the existing code not use the concept of behavioral types, but it is also quite difficult to define these notions for more elaborate programs. To deal with legacy code, automatic inference tools are needed. Our goal is to enhance the support in the definition of behavioral types in programming languages like Java. We chose the Mungo tool~\cite{mungo_article}, which associates
behavioral specifications -- \textit{Mungo protocols} or \textit{typestates} -- to Java classes and verifies if objects are used correctly.

Given how helpful automata are in abstracting system behavior and assisting developers in understanding the underlying relation between operations, and how useful Mungo typestates are in specifying object behavior and making sure Java code respects such specification, we developed a tool that assists programmers in the (naturally iterative) process of designing
an application. The key idea is to support the conception and visualization of (Mungo) typestates as automata.

Specifically, our main contributions are the following
\begin{enumerate}
    \item \textbf{An automaton model equivalent to Mungo typestates:} we defined
    a specific automaton model to Mungo protocols; besides allowing a more detailed and accurate graphical representation of the behavioral specification, it simplifies the conversion between typestate and automaton.
    \item \textbf{A grammar for Mungo typestates:} we defined the full Mungo typestates grammar,

    providing a formal basis for constructing Mungo protocols. This detailed definition also simplifies the task of describing terms generated by the grammar as automata, given that formal grammars generally have a corresponding abstract machine
    \item \textbf{Bi-directional translation between typestates and automata:} we have defined two algorithms that, respectively, translate Mungo protocols into automata by following the productions of the Mungo Typestate Grammar, and produce a Mungo protocol (a term of the grammar) by following all possible execution paths of an automaton.
    \item \textbf{Implementation and web-based tool:} lastly, we developed a functional implementation of the algorithms, as well as an interactive web-based tool, which allows developers to obtain an automaton from their Mungo protocol, and, conversely, obtain a Mungo typestate from an automaton.
\end{enumerate}

\section{How to model an entity as a Mungo protocol?}\label{motivation}
Suppose we want to build a program describing the behavior of a drone that should be able to take off, move, and land. To describe such system, we have first to understand the ordering between these actions, as it is obvious that the drone must take off prior to moving somewhere, or that it can only land if it is not yet on the ground. We can easily represent this behavior through an automaton
(Figure \ref{fig:model1}), where each state represents those of the drone, and each transition its operations.

\begin{figure}[htbp]
    \centering
    \includegraphics[scale=0.5]{model1}
    \caption{Automaton 1}
    \label{fig:model1}
\end{figure}

We now realize the drone should be able to move to a specified destination, but the current specification does not allow this behavior.
We change the automaton to include a \texttt{moveTo} method instead of \texttt{move}, where \texttt{x} and \texttt{y} specify the coordinates of the desired destination (Figure \ref{fig:model2}). Additionally, we also add a method \texttt{hasArrived} that allows us to check if the drone has arrived at the specified destination.

\begin{figure}[htbp]
    \centering
    \includegraphics[scale=0.5]{model2}
    \caption{Automaton 2}
    \label{fig:model2}
\end{figure}

Notice that state Decision is different from the other states: transitions from this node depend on the result of method \texttt{hasArrived}, whereas transitions from other nodes are performed by executing methods. On that account, we would like to define a new kind of automaton that correctly renders this idea of states offering \textit{method-call transitions}, and states or \textit{internal-choice states} offering \textit{result-based transitions}. We call \textit{Deterministic Object Automata} (DOA) to this new type of automata, which we will be formalizing in Sec.~\ref{a:doa}. We tweak the previous automaton in order to make these changes apparent, resulting in what you see in Figure~\ref{fig:model3}.

\begin{figure}[htbp]
    \centering
    \includegraphics[scale=0.5]{model3}
    \caption{Automaton 3}
    \label{fig:model3}
\end{figure}

However easy and intuitive may the representation of system behavior through state machines be, when it comes to implementation, we would be interested in having protocols that verify if, indeed, our code
respects the behavioral model we have just designed as an automaton. To do so, one may resort to Mungo~\cite{mungo_article}, a tool used for associating automata-like specifications -- \textit{typestates} -- with Java classes. These \textit{typestate specifications} abstract the available operations on an object, by defining the sequence of permitted method-calls, which depend on the state of the object~\cite{typestate, typestate_oriented}.

Mungo protocols are defined through a grammar generating DOAs, which can then be associated to a class. It is possible to check if the associated classes are used correctly (according to the typestate), since Mungo has a typechecker. If the typestate is violated, Mungo reports the errors, otherwise we can securely compile and run the Java code using the standard Java tools.

In Listing~\ref{lst:typestate1}, we present a Mungo protocol in an attempt to define our automaton representation as a typestate that we can use to check if our code respects the intended behavior of the drone.

\newpage
\begin{lstlisting}[language=Java, label={lst:typestate1}, caption={Mungo typestate specifying the drone's behavior.}]
typestate DroneProtocol {
    Idle = { void takeOff(): Hovering }
    Hovering = { void land(): Idle,
                 void moveTo(double, double): Flying }
    Flying = { Boolean hasArrived(): <True: Hovering, False: Flying> }
}
\end{lstlisting}

Similarly to the automaton we have previously defined, since \texttt{Idle} is the first state in our Mungo typestate, a new drone object starts in this state. From here, the only method available is \texttt{takeOff}. Calling this method changes the object's state to \texttt{Hovering}, where we can invoke method \texttt{land} and go back to state \texttt{Idle}, or invoke method \texttt{moveTo} and change to state \texttt{Flying}. In that state, executing method \texttt{hasArrived} has two possible outcomes: if the result is \texttt{True}, we change to state \texttt{Hovering}; otherwise, we stay in the same state. This mimics the idea of internal-choice states we have previously mentioned. The execution of \texttt{hasArrived} takes us to a state that evaluates the result of this method and consequently changes states according to that result.

After drafting the typestate and developing the code for the drone (see appendix~\ref{a:code1}), we now realize that this specification is quite restrictive, as it does not allow changing the drone's destination nor stop its movement mid-flight.
We made the appropriate changes, rewriting the Mungo typestate as in Listing~\ref{lst:typestate2}.
\begin{lstlisting}[language=Java, label={lst:typestate2}, caption={Mungo typestate after changes.}]
typestate DroneProtocol {
    Idle = { void takeOff(): Hovering }
    Hovering = { void land(): Idle,
                 void moveTo(double, double): Flying }
    Flying = { void moveTo(double, double): Flying,
               void stop(): Hovering,
               Boolean hasArrived(): <True: Hovering, False: Flying> }
}
\end{lstlisting}

To better understand these changes, it would be helpful
to visualize
the resulting automaton. By following each step of the Mungo protocol, we are able to draw
it (Figure 4). Naturally, it could also be
obtained from the previous automaton
by adding the corresponding transitions. The code with these modifications can be seen in appendix~\ref{a:code2}.
\begin{figure}[htbp]
    \centering
    \includegraphics[scale=0.5]{model4}
    \caption{Automaton 4}
    \label{fig:model4}
\end{figure}

The process of describing an automaton model as a Mungo typestate, and \textit{vice versa}, can be hard and error-prone, specially when describing complex systems. In the following sections we present the work leading to the development of a tool does this transformation automatically and further allows one to directly change either the automaton or the typestate, and obtain the converse representation, by formalizing the translation between typestate and automaton.

\section{Bi-directional conversion between Mungo Typestates and Deterministic Object Automata}
One way of looking at the problem of obtaining a Deterministic Object Automaton from a Mungo typestate (and \textit{vice versa}) is to understand similarities with typical properties regarding Formal Languages and Automata, specifically, translating a finite state automaton from a regular expression (and \textit{vice versa}). Generally, formal grammars have a corresponding state machine, for example, we can abstract regular grammars as finite automata or unrestricted grammars as Turing machines
~\cite{chomsky,hopcroft}. Therefore, formalizing a grammar for Mungo typestates naturally simplifies the task of describing these typestates as abstract machines, helping us better understand the possible behavior of an object.

Having this in mind, the first steps towards defining a conversion algorithm are the formalization of DOA, the automaton model to be equivalent to Mungo typestates, which we have highlighted in the previous section, and the formalization of a grammar for Mungo typestates. Finally, we take these two elements and, by studying their structure, define two algorithms that allow for the bi-directional translation of between both grammar and automata.

Since the end goal was to develop a tool that automates the process of translation between typestate and DOA, one of our concerns while designing such algorithms was to test that they produce the intended results
\footnote{(Mechanized) Formal proofs are work in progress.}.
For this reason, their definition was accompanied by the implementation of equivalent OCaml code~\footnote{\url{https://github.com/draexlar/compile_doa}}, a natural choice given how simple it is to represent mathematical definitions of recursive functions as functional code.

\subsection{Deterministic Object Automata}\label{a:doa}
Communicating automata have been used in the past to model binary session types~\cite{communicating_automata, heaps_and_hops}. However, the model does not fit Mungo usages perfectly, namely it does not distinguish external from internal-choice states, as clearly as DOA do. To have an automata model adequate to Mungo typestates, namely leading to an equivalence result, we defined the novel approach introduced in Sec.~\ref{motivation}. The definition of a new model allows us to have a finer control over its righteous representation of a Mungo typestate, which in the end is far easier than adapting existing models.
\medskip

\begin{definition}[\textbf{Deterministic Object Automata}]
    A DOA is an octuple $\langle S, T, M, L, s, F, D, E\rangle$ where:
    \begin{itemize}
        \item S is a set of (external choice) states;
        \item T is a set of (internal choice) states (disjoint from S);
        \item M is a set of method identifiers;
        \item L is a set of label identifiers;
        \item $s \in S$ is the initial state;
        \item $F \subseteq S$ are the final states;
        \item $D \subseteq S \times M \times (S \cup T)$ contains the method-call transitions (external);
        \item $E \subseteq T \times L \times S$ contains all the result transitions (internal).
    \end{itemize}
\end{definition}
\newpage

\begin{definition}[\textbf{Transition function}]
    Let $\Delta = D \cup E$ be the set of transitions, with D ranged over by $\delta$ and E
    ranged over by $\tau$. Consider $x, y \in (S \cup T)$, $a \in (M \cup L)$ and $w \in (M \cup L)^*$.

    The function $\Delta^* \subseteq (S \cup T) \times (M \cup L)^* \times (S \cup T)$ is inductively
    defined by the rules:

    \begin{itemize}
        \item $\Delta^*(x, \varepsilon) = x$;
        \item $\Delta^*(x, aw) = \Delta^*(\delta(x, a), w)$, if $a \in M$;
        \item $\Delta^*(x, aw) = \Delta^*(\tau(x, a), w)$, if $a \in L$.
    \end{itemize}
\end{definition}

\subsection{Mungo Typestate Grammar}\label{grammar}
\begin{definition}[\textbf{Mungo Typestate Grammar}]
    A Mungo Typestate Grammar, $G_{Mungo}$, is a quadruple $\langle V, \Sigma, P, T \rangle$, where:
    \begin{itemize}
        \item V is a finite set of non-terminal symbols;
        \item $\Sigma$ is a finite set of terminal symbols (alphabet), disjoint from V;
        \item P is a finite set of production rules;
        \item $T \in V$ is the start symbol.
    \end{itemize}

    \medskip
    \vspace{1mm}
    Let $N$ be a set of strings one can use to name a Mungo protocol, $K$ be a set of all possible state names, $R$ be a set of all possible data types, $Y$ be a set
    of all possible method names, and $Z$ be a set of all possible label names. Moreover, let $name \in N$ be the name of a typestate, $state \in K$ be any valid Java identifier, $type \in R$ be any Java identifier
    that points to a Java data type, $method \in Y$ be any valid Java identifier for a method name, and $label \in Z$ be any valid Java identifier.

    \medskip
    $V$ = \{ T, TB SDN, SD, S, SN, M, A, AN, W, O, ON, L, LT \}

    \medskip
    $\Sigma$ = \{ \texttt{typestate}, \texttt{end}, \texttt{<}, \texttt{>}, \texttt{(}, \texttt{)}, \texttt{:}, \texttt{\{}, \texttt{\}}, \texttt{,} , \texttt{=} \} $ \cup \ \{name\} \ \cup \ K \ \cup \ R \ \cup \
    Y \ \cup \ Z$

    \medskip
    \begin{table}[h!]
    \begin{tabular}{llll}
    P = \{ & \text{T $\rightarrow$ \texttt{typestate} } $name$ \text{\{TB\} }; & \text{SN $\rightarrow$ $\varepsilon$ $\mid$ , M SN };                  & \text{O $\rightarrow$ L ON };                             \\
           & \text{TB $\rightarrow$ $\varepsilon$ $\mid$ SDN TB };     & \text{M $\rightarrow$ $type$ $method$ (A) : W };                     & \text{ON $\rightarrow$ $\varepsilon$ $\mid$ , O };        \\
           & \text{SDN $\rightarrow$ $state$ = SD };                   & \text{A $\rightarrow$ $\varepsilon$ $\mid$ $type$ AN };                & \text{L $\rightarrow$ $label$: LT };                      \\
           & \text{SD $\rightarrow$ \{S\} };                         & \text{AN $\rightarrow$ $\varepsilon$ $\mid$ , $type$ AN };             & \text{LT $\rightarrow$ \texttt{end} $\mid$ $state$ $\mid$ SD }\ \} \\
           & \text{S $\rightarrow$ $\varepsilon$ $\mid$ M SN };        & \text{W $\rightarrow$ \texttt{end} $\mid$ SD $\mid$ \texttt{<} O \texttt{>} $\mid$ $state$ }; &
    \end{tabular}
    \vspace{-4mm}
    \end{table}
\end{definition}

\paragraph{Properties}
Notice that the grammar's production rules are neither left-regular nor right-regular, since their right-hand side accepts an arbitrary sequence of terminal and non-terminal symbols -- $P \subseteq V \times (V \cup \Sigma)^*$ -- as seen in the first rule of our grammar. Therefore, this is a context-free grammar.

One of our concerns while defining the grammar we present, was to ensure it to be LL(1) deterministic. This means, it is not ambiguous (produces one leftmost derivation), scans the input from left to right, and is not left-recursive. Furthermore, at each step of a derivation, there is only one applicable rule. It is simple to verify the result was achieved.

\medskip
\subsection{Translating Mungo Typestates into Deterministic Object Automata}
Now that we have formalized a grammar for Mungo protocols, we can move on to the task of defining an algorithm for translating Mungo Typestates into Deterministic Object Automata.
To this purpose, we have defined a recursive function, $Compile$, which, given a typestate specification, infers the automaton's states and transitions by following the production rules of the Mungo Typestate Grammar, returning a DOA (as defined in Sec.~\ref{a:doa}).

\paragraph{Compile Function.}
    Please recall the sets defined in Sect.\,\ref{grammar}: $K$, the set of all possible state names; $R$, the set of all possible data types; $Y$, the set of all possible method names; and $Z$, the set of all possible label names. Let $start, next \in K$, $type \in R$, $m \in Y$, $label \in Z$, and let $G$ be the set of available states defined in the typestate\footnote{For the example given in Sect.\,\ref{motivation}, $G$ = \{\texttt{Idle}, \texttt{Hovering}, \texttt{Flying}\}. }.

    As previously noted, the $Compile$ function parses a given typestate by following the production rules of the defined Mungo Typestate Grammar. To avoid ambiguity, in cases where there is a recursive production rule, we use an apostrophe (') to distinguish symbols. For example, we denote TB~$\rightarrow$~SDN~TB as TB = SDN TB'.

    \medskip
    We begin with the start symbol in our grammar, T, which represents a typestate. When parsing the typestate, some symbols may be ignored since they are not relevant for constructing a DOA. For example, even though T contains more information than TB (T $\rightarrow$ \texttt{typestate} $name$ \{TB\}), we can ignore the symbols \texttt{typestate}, $name$, \{, and \}, because we are only interested in states and their respective transitions to build an automaton.
    \begin{align*}
        &Compile_G(\text{T}) = \hfill Compile_G(\text{TB})\\[6pt]
        &Compile_G(\text{TB}) =
        \left \{
            \begin{array}{ll}
            \langle \{\texttt{end}\}, \{\}, \{\}, \{\}, \texttt{end}, \{\texttt{end}\}, \{\}, \{\}\rangle & \textit{ if } \ \text{TB} = \varepsilon \\[6pt]
            Union\big(Compile_G(\text{SDN}), \ Compile_G(\text{TB'})\big) & \textit{ if } \ \text{TB = SDN\ TB'}
            \end{array}
        \right.
    \end{align*}

    If the typestate's body is empty -- no states are defined -- the object is idle, and therefore the resulting automaton is characterized by having just one initial and final state: \texttt{end}, which is defined by default in any Mungo protocol. Otherwise, there is at least one defined state, thus the resulting DOA is the union (which we will define later in this section) of the automaton generated by the state SDN and the remainder of the typestate (TB').

    \medskip
    As an example, consider Listing~\ref{ml:ext} where we define a Mungo typestate with just two states, one initial and the final state \texttt{end}, and with only one method-call transition.
\begin{lstlisting}[language=ML, label={ml:ext}, caption={Example typestate.}]
typestate basic {
    begin = { void terminate(): end }
}
\end{lstlisting}

According to the algorithm, since the typestate's body is not empty, we would now have to compute $Union\big(Compile_G(\texttt{begin=\string{void terminate():end\string}}), \ Compile_G(\emptyset)\big)$, with $G = \{\texttt{begin}\}$. Since the typestate's body only has one state definition, the remainder of the typestate is empty. For this reason, we already know that the final union will be with an automaton with just one initial and final state, \texttt{end}: $\big\langle \{\texttt{end}\}, \{\}, \{\}, \{\}, \texttt{end}, \{\texttt{end}\}, \{\}, \{\}\big\rangle$, resulting from the computation of $Compile_G(\emptyset)$.

    \medskip
    Moving on with the definition of \textit{Compile}, when translating a state, if the state's body is empty (S~$= \varepsilon$) -- no transitions to other states are defined -- the resulting DOA only has one state, which is both initial and final. Otherwise, it is necessary to translate the state's transitions, as defined below.
    \begin{align*}
        &Compile_G(\text{SDN}) = Compile_G(start, \text{SD}) = Compile_G(start, \text{S}) \\[6pt]
        &Compile_G(start, \text{S}) =
        \left \{
            \begin{array}{ll}
            \langle \{start\}, \{\}, \{\}, \{\}, start, \{start\}, \{\}, \{\}\rangle & \textit{ if } \text{S} = \varepsilon \\[6pt]
            Compile_G(start, \text{M, SN}) & \textit{ if } \text{S = M\ SN}
            \end{array}
        \right.
    \end{align*}

    Notice the use of $start$ instead of the name $state$ used in the grammar definition. Further on this document, we will see why this change is helpful but, since $start \in K$, it plays the same role in this instance, being $start$ the name of the current state.

    Since the state definition from our example is not empty, the next step in the computation of our example would be to compute the result of $Compile_G(\texttt{begin=\string{void terminate():end\string}})$, thus, according to the new step of the algorithm, we now have \[Union\big(Compile_G(\texttt{begin},\ \texttt{void terminate()},\ \texttt{end}), \ \big\langle \{\texttt{end}\}, \{\}, \{\}, \{\}, \texttt{end}, \{\texttt{end}\}, \{\}, \{\}\big\rangle\big).\]

    Continuing where we left off, in the instance of a non-empty state definition, we consider the event of only one transition being allowed -- only one method is defined in the current state (SN = $\varepsilon$) -- and the event of multiple transitions being allowed (SN = , M' SN'). In the latter, the resulting DOA is the union of the automaton generated by the first method transition (M) of the current state, and the one generated by the remainder method transitions (M' SN').
    \begin{align*}
        Compile_G(start, \text{M, SN}) =
        \left \{
            \begin{array}{ll}
            Compile_G(start, \text{M}) & \textit{ if } \text{SN} = \varepsilon \\[6pt]
            Union\big(Compile_D(start, \text{M}), \\\qquad\quad Compile_G(start, \text{M', SN'})\big) & \textit{ if } \text{SN = , M' SN'}
            \end{array}
        \right.
    \end{align*}

    To compile a method transition, we need only focus on the current state, the method allowing the transition, and the resulting state, ignoring all other symbols:
    \begin{align*}
        &Compile_G(start, \text{M}) = Compile_G(start, type\ m(\text{A}), \text{W}) \\[6pt]
        &Compile_G(start, type\ m(\text{A}), \text{W}) = \\
        & \quad
        \left \{
            \begin{array}{ll}
            \big\langle \{start, \mathtt{end}\}, \{\}, \{type \ m(\text{A})\}, \{\}, start, \{\mathtt{end}\}, \{\delta(start, \ type \ m(\text{A})) = \mathtt{end}\}, \{\}\big\rangle &\\\quad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \textit{ if } \text{W} = \mathtt{end} \ or \text{ W = \texttt{\string{\string}}}\\[6pt]
            \big\langle \{start, next\}, \{\}, \{type \ m(\text{A})\}, \{\}, start, \{\}, \{\delta(start, \ type \ m(\text{A})) = next\}, \{\}\big\rangle &\\\quad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \textit{ if } \text{W} = next \\[6pt]
            Union\big(\ Compile_{G \cup \{inner\}}(start,\ type\ m(\text{A}),\ inner), Compile_{G \cup \{inner\}}(inner,\ \text{SD})\ \big) &\\\quad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \textit{ if } \text{W = SD},\ inner \notin G,\ inner \in K \\[6pt]
            Compile_G(start,\ type\ m(\text{A}),\ \text{O})
            \qquad\qquad\qquad\qquad\qquad\qquad\textit{ if } \text{W} = \ \texttt{<}\text{ O }\texttt{>}
            \end{array}
        \right.
    \end{align*}

    Once again, notice how we use $start$ instead of $state$, but also $m$ instead of $method$ and $next$ instead of $state$ which, respectively, stand for the current state, the method allowing the transition, and the resulting state. The use of $state$ would force us to work with $state =\{ type \ method$(A) : $state \}$, which is ambiguous, hence, the use of $start$ and $next$, both elements of $K$. Bear in mind that we are not concerned with which or how many arguments a method accepts, and thus we assume A is well defined.

    When the resulting state is the \texttt{end} state -- which can be denoted by \texttt{end} or \texttt{\string{\string}} in Mungo protocols -- the resulting automaton has: two external-choice states, $start$ and \texttt{end}; one method, $m$; an initial state, $start$; a final state, \texttt{end}; and a (\textit{method-call}) transition from $start$ to \texttt{end}, through $m$. As you can see, we follow the same reasoning when the resulting state is $next$.

    Mungo protocols also allow states to be defined inside other states, similar to an inlining. These ``inner'' states do not have names, so we need to assign them one. The assigned name must be unique, and thus, before assigning it, one must first check if the name is already in use, by checking if it is in $G$~\footnote{Recall that $G$ is the set of defined states in the typestate.}. We will be referring to the assigned name as $inner$ and we may see it as an element of $K$. Now, we need to update $G$ to include the newly defined inner state, so that, in the future, it will not be possible to create a state with that same name. Consequently, the generated automaton of a transition to an inner state (W = SD), is the union of ``compiling'' the current state with a resulting state $inner$, along with the resulting automaton of compiling the inner state.

    Lastly, Mungo protocols allow a state to transition to an \textit{internal-choice state} with a set of options (W~=~\texttt{<}~O~\texttt{>}), through a method $m$.

    \medskip
    According to the last few steps, we can understand that, from where we left off our example, since our state has only one defined transition, and this transition leads to state \texttt{end}, our computation results in solving:
    \vspace{-2mm}
    \begin{align*}
        Union\Big(\ &\big\langle \{\texttt{begin}, \mathtt{end}\}, \{\}, \{\texttt{void terminate()}\}, \{\}, \texttt{begin}, \{\mathtt{end}\},\\
        &\ \ \{\delta(\texttt{begin}, \texttt{ void terminate()}) = \mathtt{end}\}, \{\}\big\rangle,\ \big\langle \{\texttt{end}\}, \{\}, \{\}, \{\}, \texttt{end}, \{\texttt{end}\}, \{\}, \{\}\big\rangle\ \Big).
    \end{align*}

    Continuing with the definition of \textit{Compile}, we have still to define the translation of transitions to internal-choice states.
    \begin{align*}
        &Compile_G(start,\ type\ m(\text{A}),\ \text{O}) = \\
        &\qquad
        Union\Big(\big\langle \{start\}, \{choice\}, \{type \ m(\text{A})\}, \{\}, start, \{\},\ \{\delta(start, \ type \ m(\text{A})) = choice\}, \{\}\big\rangle,\\
        &\ \ \quad\qquad\qquad Compile_{G \cup \{choice\}}(choice, \text{ O})\Big),\
        \text{where } \ choice \notin G, \ choice \in K
    \end{align*}

    To translate a transition to an internal-choice state, we must first assign a name to that state, which we will be referring to as $choice$, and we may see it as an element of $K$. Although $S$ (the set of external-choice states) and $T$ (the set of internal-choice states) are disjoint, $choice$ should be unique to avoid ambiguity. So, similarly to what was done for the inner states, we check if $choice$ is in $G$, and then update this set. The resulting DOA is the union of an automaton with: one external-choice state, $start$; one internal-choice state, $choice$; a method, $m$; an initial state; and an (method-call) transition from $start$ to $choice$; along with the resulting automaton of translating the set of options (O) offered by $choice$.
    \begin{align*}
        &Compile_G(choice, \text{ O}) = Compile_G(choice, \text{L, ON})\\[6pt]
        &Compile_G(choice, \text{L, ON}) =
        \left \{
            \begin{array}{ll}
            Compile_G(choice,\ \text{L}) & \textit{ if } \text{ON} = \varepsilon \\[6pt]
            Union(Compile_G(choice,\ \text{L}), \ Compile_G(choice,\ \text{O})) & \textit{ if } \text{ON = , O}
            \end{array}
        \right.
    \end{align*}

    Notice that, our grammar does not accept an internal-choice state -- a decision state -- without options. Hence, we consider the instances of only one option being defined in the current decision state (ON~=~$\varepsilon$), and the instance of having multiple options (ON = , O). We then "compile" the decision state with its first option (or only option). By performing its union with the automaton generated by the the remainder options in $choice$, we satisfy the latter instance.

    \medskip
    To compile an option, we focus on the current internal-choice state, $choice$, the option's label identifier, $label$, and the option's resulting (external-choice) state for the label in consideration, LT:
    \begin{align*}
        &Compile_G(choice, \ \text{L}) = Compile_G(choice,\ label, \text{ LT}) \\[6pt]
        &Compile_G(choice,\ label, \text{ LT}) = \\
        &\quad
        \left \{
            \begin{array}{ll}
            \langle \{\mathtt{end}\}, \{choice\}, \{\}, \{label\}, \epsilon, \{\mathtt{end}\}, \{\}, \{\tau(choice, label) = \mathtt{end}\}\rangle \quad \textit{if } \text{LT} = \texttt{end} \ or \text{ LT = } \texttt{\string{\string}}\\[6pt]
            \langle \{next\}, \{choice\}, \{\}, \{label\}, \epsilon, \{\}, \{\}, \{\tau(choice, label) = next\}\rangle \ \quad\quad
            \textit{if } \text{LT} = next\\[6pt]
            Union\big(Compile_{G \cup \{inner\}}(choice,\ label,\ inner), \ Compile_{G \cup \{inner\}}(inner,\ \text{SD})\big) \\ \ \ \ \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\
            \textit{if } \text{LT} = \text{SD}, \ inner \notin G,\ inner \in K
            \end{array}
        \right.
    \end{align*}

    Similarly to what was done for translating method-call transitions, when our resulting state is the \texttt{end} state, the resulting automaton has: one external-choice state, \texttt{end}; one internal-choice state, $choice$; one label; a final state; and a (\textit{result-based}) transition from $choice$ to \texttt{end}, through $label$. Otherwise, when the resulting state is $next$, the resulting automaton has: one external-choice state, $next$; one internal-choice state, $choice$; one label; and a (result-based) transition from $choice$ to $next$, through $label$.

    Mungo typestates also allow states to be defined inside internal-choice states (LT = SD). Therefore, the resulting automaton is the union of translating the current internal-choice state with a resulting state $inner$ ($inner \in K$ and $inner \notin G$) through $label$, along with the resulting automaton of compiling the inner state. Recall that we then need to update $G$ to include the new state $inner$, so that, in the future, no other state can have the same name.

\paragraph{Union of Deterministic Object Automata.}
At many steps in our $Compile$ function we made use of a $Union$ function. This is because simply performing the union ($\cup$) of two Deterministic Object Automata is not right. Although it would be valid for almost every set in our octuple, notice that, in the definition of DOA, there is only one initial state, which is assumed to be the first state defined in a Mungo typestate. Addressing this issue, a function $Union(a, b)$ is defined.

\medskip
\begin{definition}[\textbf{Union Function}]
    Let $a$ and $b$ be two DOA, where $a$ is the automaton with the initial state considered to be the start:
    \begin{equation*}
        Union(a, b) = \big\langle \ S_a \cup S_b,\ T_a \cup T_b,\ M_a \cup M_b,\ L_a \cup L_b,\ s_a, F_a \cup F_b,\ D_a \cup D_b,\ E_a \cup E_b \ \big\rangle
    \end{equation*}
\end{definition}

\noindent
Now that the \textit{Union} function is defined, we can now complete the last computation from our example, which we recall bellow.
\begin{align*}
    Union\Big(\ &\big\langle \{\texttt{begin}, \mathtt{end}\}, \{\}, \{\texttt{void terminate()}\}, \{\}, \texttt{begin}, \{\mathtt{end}\},\\
    &\ \ \{\delta(\texttt{begin}, \texttt{ void terminate()}) = \mathtt{end}\}, \{\}\big\rangle,\ \big\langle \{\texttt{end}\}, \{\}, \{\}, \{\}, \texttt{end}, \{\texttt{end}\}, \{\}, \{\}\big\rangle\ \Big)
\end{align*}

Notice that, in this particular case, the first automaton already has a transition to \texttt{end}, therefore the resulting sets will be equal to those of this DOA. Furthermore, by definition, the initial state of the first automaton is the initial state of the resulting automaton, thus we obtain the DOA: $\big\langle \{\texttt{begin}, \mathtt{end}\}, \{\},$ $\{\texttt{void terminate()}\}, \{\}, \texttt{begin}, \{\mathtt{end}\}, \{\delta(\texttt{begin}, \texttt{ void terminate()}) = \mathtt{end}\}, \{\}\big\rangle$.

\subsection{Translating Deterministic Object Automata into Mungo Typestates}
We now define the converse translation. By describing the behavior of an entity as a state machine, one should be able to infer its corresponding Mungo protocol. This would be helpful since describing an automaton can be easier and more intuitive than writing a typestate specification.

In this section, we propose a method for translating Deterministic Object Automata into Mungo typestates by defining a function, $Decompile$, that, given a DOA, infers a corresponding Mungo typestate by following the automaton's transitions.

\paragraph{Decompile function.}
    Let $name$ be the name one wants to give the resulting Mungo typestate, and $doa = \langle S, T, M, L, s, F, D, E\rangle$ be a Deterministic Object Automaton. And let $G$ be the set of already defined states in the typestate. Initially, $G = \{\texttt{end}\}$ given that the \texttt{end} state is predefined for every Mungo typestate.

    The $Decompile$ function returns a string corresponding to the Mungo protocol described by \textit{doa}.

    We start by giving the typestate's name and the automaton \textit{doa} representing the typestate as arguments of our \textit{Decompile} function, in order to obtain the protocol's header, followed by the definition of its body.
    \begin{align*}
        &Decompile(name, doa) = \texttt{typestate} \ name \ \{ \ Decompile_G(doa) \ \}\\[6pt]
        &Decompile_G(doa) =
        \left \{
            \begin{array}{ll}
                \varepsilon \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\
                \textit{ if} \ S = \emptyset \ or \ S = \{\texttt{end}\} \\[6pt]
                s = \{ \ Decompile_{G \cup \{s\}}(s, doa, A) \ \} \\\quad
                Decompile_{G \cup \{s\}}\big(\langle S \setminus \{s\}, T, M, L, n, F, D \setminus A, E \rangle\big),\\\qquad\ \
                \text{with } A = \{ \delta(x, y)=z \in D \mid x=s \} \text{ and } n \in S \setminus \{s, \text{end}\}
                \qquad\quad \textit{ otherwise }
            \end{array}
        \right.
    \end{align*}

    Looking at the Mungo Typestate Grammar definition, we see that the typestate's body can be empty (TB $\rightarrow$ $\varepsilon$ $\mid$ SDN TB). Therefore, if the set of external-choice states, $S$, of the given DOA is empty or its only element is \texttt{end}, there are no (more) states to be defined in the typestate, and this instance of $Decompile$ returns the empty string. Otherwise, we define state $s$ in the typestate.

    Recall that the first state defined in a Mungo protocol is the initial state of the typestate and, naturally, the initial state of the $doa$, $s$. For this instance, we also need to define the remaining states of the given automaton. Thus, we make the recursive call of $Decompile$ with a DOA where: the set of external-choice states, $S$, no longer includes $s$; its initial state can be any state in $S \setminus \{s, \text{end}\}$; and the set of method-call transitions, $D$, does not include any transition where the initial state is $s$. Lastly, it is important that we update the set of defined states in the protocol, $G$, to include the newly defined state $s$.

    \medskip
    As an example, consider a DOA with just two states, one initial and one final with only one method-call transition:
    \[d = \big\langle \{begin\},\ \emptyset,\ \{\texttt{void terminate()}\},\ \emptyset,\ begin,\ \{\texttt{end}\},\ \{(begin, \texttt{ void terminate()}, \texttt{ end})\},\ \emptyset \big \rangle.\]

According to the first steps of \textit{Decompile}, if we called $Decompile(\texttt{basic}, d)$, we would have $s = begin$, $A=\{(begin, \texttt{ void terminate()}, \texttt{ end})\}$, and $G=\{\texttt{end},\ begin\}$, given that $begin$ is the initial state and the only transition beginning in $begin$ is that of calling method \texttt{terminate}.

\medskip
Continuing with the formalization of \textit{Decompile}, the body of an external-choice state is the state's method-call transitions. For this reason, besides the current state, $c$, and $doa$, we also receive the set of all the current state's method-call transitions, $A$, as follows.

\begin{align*}
    &Decompile_G(c, doa, A) =\\&\qquad
    \left \{
        \begin{array}{ll}
            \varepsilon & \textit{ if } A = \emptyset \\[6pt]
            m:\ Decompile_G(n, doa) & \textit{ if } A = \{\delta(c, m) = n\},\ m \in M \\[6pt]
            m:\ Decompile_G(n, doa), \\\quad\ \ \ Decompile_G\big(c, doa, A \setminus \{\delta(c, m) = n\}\big) & \textit{ if } \#A \neq 1,\ \{\delta(c, m) = n\} \subset A,\ m \in M
        \end{array}
    \right.
\end{align*}

If the set of method-call transitions from $c$ is empty, there are no (more) transitions to be defined for the current state. If the set of method-call transitions from $c$ only has one element, then we need to define the transition relative to that element. Taking a look at our grammar definition, we define a transition by writing the method allowing it, followed by colon (:) and the resulting (external-choice) state or a series of choices (internal-choice state).

Otherwise, the set of method-call transitions has multiple elements. We start by choosing one of its elements and defining it, similarly to what was explained in the prior instance, followed by a comma (,) and the definition of the remaining transitions allowed in the current state, $c$. This is done by recursively calling $Decompile$ with a set of method-call transitions excluding the one we have just defined.

To finish defining a transition, we need to decide whether the state we are transitioning to, $n$, is external or internal.
    \begin{align*}
        Decompile_G(n, doa) =
        \left \{
            \begin{array}{ll}
                n & \textit{ if } n \in S \cup G \\[6pt]
                \texttt{< } Decompile_G\big(n, doa,\{\tau(x, y) =z \in E \mid x = n\}\big) \texttt{ >} & \textit{ if } n \in T
            \end{array}
        \right.
    \end{align*}

    To do so, we need only check if $n$ is in $S$, the set of external-choice states, or in $G$, the set of already defined states; or otherwise check if $n$ is in $T$, the set of internal-choice states. In which case, we start by writing \texttt{<}, which identifies the choice; call $Decompile$ with the state we are transitioning to, $n$, the automaton $doa$, and the set of all result transitions starting in $n$, which we will be calling $B$; followed by closing the choice with \texttt{>}.
    \begin{align*}
        &Decompile_G(c, doa, B) =\\&\quad
        \left \{
            \begin{array}{ll}
                l: n & \textit{ if } B = \{\tau(c, l) = n\}, \ l \in L,\ n \in S \cup G \\[6pt]
                l: n,\ Decompile_G\big(c, doa, B \setminus \{\tau(c, l) = n\}\big) & \textit{ if } \#B > 1,\ \{\tau(c, l) = n\} \subset B,\ l \in L, \ n \in S \cup G
            \end{array}
        \right.
    \end{align*}

    In the Mungo Typestate Grammar definition, you can see there must be at least one choice in an internal-choice state (O $\rightarrow$ L ON). Therefore, we consider the instance of $B$ (the set of result transitions starting in $c$) having only one element, and the instance of $B$ having multiple elements.

    Taking a look at the grammar definition, in a Mungo typestate, we define a result transition by writing a label, $l$, followed by colon (:), and the resulting external-choice state, $n$. Since $n$ is an external-choice state, it must be an element of $S$ or an element of $G$. When having multiple result transitions for $c$, we start by choosing one of its elements and defining it, as explained above, followed by a comma (,), and the definition of the remaining result transitions allowed in the current state. This is done by recursively calling $Decompile$ with a set of result transitions excluding the one we have just defined.

    \medskip
    From these lasts few steps of \textit{Decompile} we can see that, given that set $A$ is the singleton $A=\{(begin, \texttt{ void terminate()}, \texttt{ end})\}$ and that, indeed, $\texttt{end} \in S \cup G$, the resulting typestate from our previous example is the following.
\begin{lstlisting}[language=ML, label={ml:exa3}, caption={Typestate obtained from $d$.}]
typestate basic {
    begin = { void terminate(): end }
}
\end{lstlisting}
\vspace{-4mm}

\section{The Web Tool}
\vspace{-2mm}
The work presented in the previous section gave us the formal basis to what we sought out to do from the beginning: build a tool~\footnote{\url{http://typestate-editor.github.io/}} that helps developers describe behavioral specifications by automating the process of converting Mungo typestates into automata and \textit{vice versa}.
This tool allows any user to write a Mungo protocol and preview a visual representation of the corresponding automaton.

The implementation was done using \texttt{TypeScript}~\footnote{\url{https://www.typescriptlang.org/}}, a static type checker for JavaScript. Although we tried to stick to the functional approach, discussed in the previous section, as to follow the \textit{Compile} and \textit{Decompile} function definitions, some parts of the implementation are imperative in nature, since they work with mutable structures for performance sake. Lastly, to help us with handling the data and the graphical representation of typestates as automata, we used the \texttt{vis.js}~\footnote{\url{https://visjs.org/}} library.

Figure~\ref{fig:typestate_to_preview} presents the tool's interface when converting a Mungo protocol into an Deterministic Object Automata. On the left, one can type the typestate specification and click the ``Do'' button to produce a corresponding visual representation -- a DOA -- which can be observed on the right. Each element of the image has a meaning: the gray arrow points to the initial state; blue arrows represent transitions; external-choice states are represented as circles; and internal-choice states are represented as diamonds. Finally, one can also download the automaton as a \texttt{PNG} file or copy the automaton in \texttt{JSON} to the clipboard.
\begin{figure}[H]
    \centering
    \includegraphics[scale=0.45]{typestate_to_preview}
    \vspace{-2mm}
    \caption{Web tool interface: Mungo typestate to DOA.}
    \label{fig:typestate_to_preview}
\end{figure}

Additionally, the user may view the internal representations and intermediate transformations to understand how the tool works. Namely, the user may transform the typestate into an abstract syntax tree (and \textit{vice versa}), and transform an abstract syntax tree into an automaton (and \textit{vice versa}), both represented in \texttt{JSON}. Figure~\ref{fig:automaton_to_ast} shows an example of a transformation from an automaton to the abstract syntax tree, which can then be used to obtain the corresponding typestate, as illustrated in Figure~\ref{fig:ast_to_typestate}. Notice how the inverse transformation produced the same typestate initially presented in Figure~\ref{fig:typestate_to_preview}.
\begin{figure}[htbp]
    \centering
    \includegraphics[scale=0.45]{automaton_to_ast}
    \vspace{-2mm}
    \caption{Web tool interface: DOA to AST.}
    \label{fig:automaton_to_ast}
\end{figure}
\vspace{-2mm}
\begin{figure}[H]
    \centering
    \includegraphics[scale=0.45]{ast_to_typestate}
    \vspace{-2mm}
    \caption{Web tool interface: AST to Mungo typestate.}
    \label{fig:ast_to_typestate}
\end{figure}

Lastly, we would like to add that the tool also checks for errors. In the written typestates, it detects syntax errors and errors related to the structure of the typestate, such as: states with the reserved name \texttt{end}; references to states that are not defined; duplicate states, transitions (for the same state) or labels (in internal-choice states); and internal-choice states without options. When performing the converse translation, we look for errors regarding transitions to undefined states, internal-choice states without result transitions, or even transitions from internal-choice states to internal-choice states.

\section{Conclusions and Further work}
Nowadays, programming languages
rely heavily on type systems to avoid non-trivial errors such as the execution of
operations on invalid states,
as trying to access a non-existent position of an array or trying to read from a file that is not yet opened. Behavioral types
are useful methods to prevent errors resulting from applying operations in wrong order.

In this paper we focus on
how tools such as Mungo allow us to describe the behavior of entities through its typestates.
By presenting a formal grammar description of Mungo protocols, we define a norm for building Mungo typestates, and by designing a new automata model that can soundly portray a Mungo typestate, we give a concrete way of visualizing the described object's behavior. The formalization of a function for translating Mungo typestates into Deterministic Object Automata, as well as a function that computes the reverse translation, grants mathematical grounds for developing tools to represent and manipulate behavioral descriptions of computational entities. Such is the web-based tool we have developed, which, through an easy to use graphical interface, allows any developer to obtain a Mungo typestate from an automaton, or even get a better sense of how their Mungo typestate is structured, by displaying an equivalent automaton graph. Allied with the Mungo tool, one can associate the protocols designed or obtained through our tool with corresponding Java class implementations, and Mungo's typechecker will verify if the code follows the revised protocols.

Nonetheless, as many have said, \textit{a work of art is never finished}, and so is true for the work herein presented. A common theme throughout this paper, and the motivation driving the use of behavioral types is, in its core, the same as for using other formal methods: the necessity of systems that ensure correct behavior. Therefore, the next step in our work is to ensure the correct specification of our algorithms, by using deductive program verification to prove that the behavior and properties we expect from them are correct. Concretely, the formal proof is based on the typical properties regarding Formal Languages and Automata: the conversion between grammar and automaton preserve the language. This is, to prove the correction of the algorithm that converts Mungo typestates into DOA is to prove that the \textit{language} of the (resulting) DOA is the same as the \textit{language} of the Mungo typestate. Similarly, to prove the correction of the translation from DOA to Mungo typestate is to prove that the \textit{language} of the (resulting) Mungo typestate is the same as the \textit{language} of the DOA. The result of this work will contribute to the development of a mechanically verified version of the tool that developers can use with the assurance of correct results. Following this step, we intend on improving the usability of the tool, by allowing the users to construct and manipulate the graphical representation of the automaton, rather than having to work with the formal, more complex, textual representation.

\bibliographystyle{eptcs}

redpajama_set_name: RedPajamaArXiv


Everyone on social media calls themselves a "content creator". Brian lives it 24/7. He travels the world talking, teaching, and streaming. While he was in Atlanta for The Social Shakeup, I caught him for great chat about all the social channels and much more. Enjoy.


text:
In 2016, as part of the federal government's efforts to conserve Colorado River water, the U.S. Bureau of Reclamation funded rebates in the district to encourage growers to convert flood-irrigated fields to drip irrigation.
The rebates of up to $1,500 per acre made only a small dent: In the past two years, three farms converted about 71 acres to drip irrigation. Three other farms initially applied but later withdrew when they calculated the costs of electricity necessary to run the drip systems, as well as the costs of building new reservoirs for them.
The economic incentives for farms, golf courses and private well owners have been relatively minuscule compared to the incentives for domestic water customers, who've been able to take advantage of millions of dollars in rebates to convert grass to desert landscaping.
CVWD is the largest of the valley's water suppliers, with about 108,000 customers. The district has long had relatively high per-capita water use because of the hot climate and the history of building resort communities filled with big lawns, pools and ponds. But between 2009 and 2017, the district's annual deliveries of domestic water fell nearly 25 percent — a trend that's also emerged to varying degrees in other cities across the Southwest, from Las Vegas to Phoenix.
People who get their drinking water from CVWD, unlike farmers and golf course managers, pay tiered rates that reward those who conserve and penalize those who use more.
The fees for canal water use and pumping from private wells, in contrast, are flat charges. And the district's managers say that under California water law, they can't switch those fees to a tiered pricing system.
Katie Evans, director of communications and conservation, said under the state Water Code, "conservation pricing" isn't allowed for the fees that agencies charge private well owners or users of canal-delivered Colorado River water.
For drinking water customers, the system of tiered rates has been in place since 2009. And it's generated funds to pay for the rebates that have helped homeowners replace their lawns.
The water district has spent $17.9 million on rebates to encourage conservation since 2012. Much of the money has gone to help residents and homeowners' associations replace grass with desert landscaping, converting a total of 390 acres.
Though the acreage converted is still a small portion of the area's water-intensive grass, the effort has been one of several changes helping to boost the levels of the aquifer.
Over the past half-century, as subdivisions, resorts and golf courses expanded across the desert, the water table declined beneath much of the Coachella Valley. Water agencies have combated the problem by importing water from the Colorado River to replenish the aquifer at three sites: near Palm Springs, near Desert Hot Springs and in south La Quinta.
The largest declines in the aquifer have occurred away from those replenishment ponds in the middle of the valley. In parts of Palm Desert, Indian Wells and Rancho Mirage, records show water levels in wells have declined by 90-100 feet or more since the 1950s and 60s.
But the aquifer's levels have risen significantly near the groundwater recharge ponds in La Quinta since the facility began receiving water deliveries in 2009. In some areas of the east valley where the aquifer previously had been depleted, the water district says there are now artesian wells where water flows out of the ground.
Next to Windy Point in the desert north of Palm Springs, Colorado River water has also been pouring into the Whitewater River groundwater replenishment facility. Water agencies have been sending imported water to the ponds since 1973.
During the 2012-2016 drought, the ponds in the desert next to Palm Springs' windmills often sat mostly empty and dry. But after California's wet winter in 2017, a record amount of water — 385,995 acre-feet in all — flowed into the Whitewater Groundwater Replenishment Facility, filling the ponds to the brim.
The aquifer took in more imported water last year than was pumped out by all the wells in the valley.
The area's agencies rely on multiple sources of imported water, including the State Water Project, which runs from the Sacramento-San Joaquin River Delta to Southern California. Because the canals and pipelines of that system don't reach the valley, local agencies trade their allotments to the Los Angeles-based Metropolitan Water District for equivalent amounts from the Colorado River Aqueduct.
Metropolitan also has a water-banking arrangement with the valley's agencies, and a large portion of the water that soaked into the soil last year belongs to Met. That portion is to be repaid by the Coachella Valley through reduced deliveries in future years. The area's districts now owe Met about 229,489 acre-feet — which is nearly 75 billion gallons, or about 80 percent of the water that's pumped from the ground in the valley each year.
That influx of imported water has helped boost groundwater levels in many areas.
To examine trends in the aquifer, The Desert Sun obtained measurements of water levels in wells from the Coachella Valley Water District and the Desert Water Agency. An analysis of that data shows the aquifer has risen in large portions of the valley in recent years, helped by the large quantities of imported water.
Of 269 wells for which measurements were available in 2007 and 2017, 70 percent of those wells saw increases in average annual groundwater levels, while others declined.
On average, the data showed that groundwater levels across the valley were lower last year than they were 20 years earlier in 1997. In the middle of the valley around Palm Desert, some wells are down more than 40 feet compared to two decades ago. But many of those wells have stabilized or risen. And the rising water levels in a majority of wells during the past several years reveal a significant shift.
Researchers say the trend is also helping to fight another related problem: sinking ground.
Michelle Sneed, a hydrologist with the U.S. Geological Survey, has been studying the problem of land subsidence for years, and she said her latest research in the Coachella Valley shows major improvement.
The last USGS study of land subsidence in the area, published in 2014, found that the ground sank by between nine inches and 2 feet from 1995 to 2010 in parts of Indian Wells, La Quinta and Palm Desert where groundwater levels were declining. Sinking ground has caused damage in other parts of the Coachella Valley in the past few decades, cracking the foundations of some homes and damaging swimming pools, roads and other infrastructure.
Aquifer at Risk:Heavy pumping strains desert water supply
More:Regulators ordered Californians to use 25% less water. Desert golf courses cut back 8%.
But Sneed said the increasing amounts of water flowing into the replenishment ponds in La Quinta since 2009 have made a big difference in boosting aquifer levels in many areas and preventing the ground from sinking.
"Mostly, I don't bring good news to anybody. So, this is a nice case. This is the one study that I've worked on personally where the trends are improving," said Sneed, whose research has yet to be published. "I'm really very surprised, pleasantly surprised, that they have really turned it around."
She said the adoption of tiered rates, lawn-removal rebates and the use of imported water have all helped the aquifer after decades of declines.
"I can't obviously predict the future or when they're going to be sustainable or any of that," Sneed said. "But I can say that they're headed in the right direction."
CVWD is also moving ahead with a $9.8-million plan to recharge the aquifer in the middle of the valley, where the long-term declines have been the largest.
In the past month, workers have been constructing a new cluster of replenishment ponds on a plot of land between the district's Palm Desert offices and a sewage treatment plant.
The first ponds are due to be finished by February, and more ponds will be built later in the Whitewater River stormwater channel. They'll soon be filled with water from the Colorado River.
The district is getting increasing deliveries of water through the All-American Canal, and is set to take even more in the coming years.
Under a 2003 water transfer deal called the Quantification Settlement Agreement, the Imperial Irrigation District is selling growing amounts to CVWD and San Diego County. As the deal sends more water away from Imperial Valley farmlands, California officials are starting to grapple with the effects at the Salton Sea, where the inflow of agricultural runoff is shrinking.
The sea's retreating shorelines are leaving stretches of dry lakebed exposed to the winds, sending more lung-damaging dust into communities that already suffer from high asthma rates.
In an effort to control dust and revitalize deteriorating bird habitats, state officials are working on a $410 million plan to build thousands of acres of ponds and wetlands on portions of the exposed lakebed around the sea.
As the district gets escalating amounts under the water transfer deal, putting the water to use has required some planning — especially in light of the recent conservation success and population growth that has been slower than once projected before the Great Recession.
In addition to building the Palm Desert groundwater replenishment ponds, the agency has also been hooking up more golf courses to Colorado River water, enabling them to rely less on groundwater.
In the past several years, though, the district hasn't used all the available Colorado River water, and has sent some unused water to the Metropolitan Water District.
Johnson recently wrote a blog post criticizing the district for relinquishing the water instead of using it locally. He cited figures showing that over the past five years, CVWD has sent 52,171 acre-feet of unused water to Met. That's enough to supply about 60 percent of CVWD's domestic customers for a year.
"It's water that we should keep right here in the Coachella Valley. Or they should come up with some arrangement, if they can't use it here, to store it somewhere and get it when they can use it," Johnson said. "It's water that belongs to all the inhabitants of the Coachella Valley, and it should be used here now or sometime in the future, instead of transferring it to Los Angeles."
The district's managers disagree. They say they're complying with the terms of the water transfer agreement and taking steps to put the water to use as more becomes available each year. They plan to start replenishing the aquifer in Palm Desert as soon as the ponds are completed.
In the meantime, they say, the arrangement is helping the region alleviate pressure on the Colorado River by enabling Met to rely a bit less on its own withdrawals from Lake Mead, where the declining water levels have been approaching a threshold that would trigger shortage measures.
The Coachella Valley has a total of 121 golf courses, one of the biggest concentrations of courses in the country.
In an effort to reduce groundwater pumping, CVWD has been gradually hooking up more of them to pipes carrying recycled wastewater, Colorado River water or a blend of the two. A total of 15 courses have started receiving those alternative water supplies since 2010, and others are in the works.
A tally provided by the district shows a total of 59 and a half golf courses are now getting recycled water, canal water or a mix. The remaining 61 and a half courses continue to rely on groundwater.
Climate Point:Sign up for USA TODAY's climate change and environment newsletter
Several years ago, it was easier to track how much groundwater was being pumped by individual golf courses, farms, housing developments and resorts. CVWD used to include detailed information about groundwater pumping by private well owners in its annual reports. But the district stopped releasing that information in 2014 after The Desert Sun published a list of some of the area's biggest water users.
This year, CVWD provided data on total water use by the 106 golf courses within its boundaries between 2010 and 2017 — including groundwater, Colorado River water and recycled water.
The figures show those golf courses used a total of 99,870 acre-feet last year — 6.6 percent more water than in 2010, and about the same amount as in 2013. The average amount of water used by a single golf course last year was about 307 million gallons.
Representatives of the valley's golf courses pledged in 2014 to work toward a goal of cutting water use by 10 percent, and the latest figures show they're falling short of the target.
Managers at some courses say they've taken significant steps to shrink their water footprint, but that higher temperatures have made it tougher to conserve the past few years.
Jim Schmid, director of operations at The Lakes Country Club in Palm Desert, said conservation has been a priority and his club has cut water use by 14 percent since 2014.
Those savings have been achieved by replacing sprinklers with more efficient heads and nozzles, and by installing new irrigation controllers in homeowners' association common areas that are connected to a central system, which adjusts watering depending on the weather.
Hotter temperatures increase the amount of water that grass and other plants need. And the past few years have been some of the hottest on record in the desert, reflecting the influence of climate change.
"We're seeing it in front of us every day," Schmid said. "Even in the face of conditions that are increasingly hot, we have managed to reduce water usage."
The Lakes, which has 212 acres of grass and 30 acres of lakes, uses recycled water.
In the past five years, the country club has removed more than seven acres of grass, replacing it with artificial turf and desert landscaping. The club also replaced the liners in six of its lakes to prevent leakage.
The costs for those projects totaled more than $3 million, Schmid said.
Converting each acre of grass to low-water landscaping cost more than $100,000, he said, and the country club took advantage of a federally funded rebate through CVWD, which offered $15,000 per acre.
So far, golf courses have used more than $1.6 million in the rebates to help take out more than 155 acres of grass.
Schmid and other golf course managers have been participating in a water task force, holding regular meetings to review their water-saving efforts.
"I think we'd all like to see a point where we were a little bit further along in conservation, but I think what we've seen so far is very positive," Schmid said. "It's going a little slower than everyone would hope, but some of these things are longer-term propositions."
Among other things, the golf industry has been donating to support research at the University of California, Riverside, on new varieties of grasses that are capable of staying green through the winter to eliminate the need for the annual practice of over-seeding, which consumes more water. That research is supported by the United States Golf Association as well as a local group, the Hi-Lo Desert Golf Course Superintendents Association.
Representatives of the golf business say the research holds promise for dramatically reducing the amount of watering.
"While the research is of value to all of the game in the arid and hot southwest, its benefits are particularly impactful in the Coachella Valley, where many of the 'snowbirds' who elect to spend their winters in the valley have high expectations of wall-to-wall green during winter," said Craig Kessler, director of governmental affairs for the Southern California Golf Association. "Eliminating the need to overseed would save a substantial amount of water in the Coachella Valley."
Managers of golf clubs have also been talking over other approaches that would create greater economic incentives to help drive conservation.
"One of the things we've asked the water district to look at is water budgets for each course," Schmid said. "We've all seen that tiered rates work and they do help to ensure efficient water usage."
The individualized water budgets would be calculated for each course based on acreage and other factors, similar to the budgets that now exist for residential customers.
"I do think over the long term, the golf industry will support tiered rates," he said. "Most people are in favor of higher costs for wasteful users."
Many areas of California face a daunting task in trying to stop declines in groundwater levels after decades of overpumping.
The state's Sustainable Groundwater Management Act, which was approved in 2014, focuses on groundwater basins deemed to be "high" or "medium" priority and calls for local agencies to adopt plans for moving toward sustainability.
In the Coachella Valley, the ground is fragmented by the San Andreas Fault and a web of other faults running through the desert. In places, the faults act as underground barriers, dividing the valley's groundwater basin into several distinct subbasins.
State water regulators initially listed the Indio subbasin as medium priority. But more recently, in a draft released in May, they described the area as high priority.* Two other subbasins — Mission Creek and San Gorgonio Pass — are classified as medium priority, and the Desert Hot Springs subbasin, which has warm water filled with dissolved minerals, is considered "very low" priority.
The law requires the creation of local "groundwater sustainability agencies."
Forming these new entities to draft management plans might seem like a relatively straightforward and noncontroversial task. But the boundaries of the subbasins don't line up with the agencies' jurisdictional boundaries, and a dispute has flared between the water suppliers.
Mission Springs Water District is suing Desert Water Agency and CVWD to challenge its exclusion from taking part in the management of the Mission Creek and Indio aquifer subbasins. Officials at Mission Springs filed the suit in 2016 and say they're prepared to keep fighting in court.
"We want a seat at the table," said Arden Wallum, general manager of Mission Springs. "Everyone that provides water to people in this valley should be a part of the management of that water."
Desert Water Agency has responsibility for replenishing the aquifer with imported water in a zone that includes the territory where Mission Springs supplies water to customers. Mission Springs pays a replenishment assessment fee to DWA for the water it pumps from wells. Under state law, DWA was designated as the sole groundwater sustainability agency for its area. The agency's officials say they believe they should be in charge.
"We were in mediation and at one point we thought that we had an agreement, and ultimately Mission Springs decided not to sign that agreement," said Ashley Metzger, DWA's outreach and conservation manager. "We were certainly working toward compromise, and it's our prerogative that we are designated as the exclusive GSA (groundwater sustainability agency) for the area."
While the case continues in Riverside County Superior Court, another battle is pending in federal court.
The Agua Caliente Band of Cahuilla Indians sued DWA and CVWD in 2013, seeking to assert rights to groundwater and gain greater influence in decisions about how the aquifer is managed.
The Ninth Circuit Court of Appeals ruled in March 2017 that the tribe has a right to groundwater dating back to the federal government's creation of the reservation in the 1870s. The Supreme Court declined to hear an appeal by the water districts, effectively handing the tribe legal backing for its claim to groundwater rights.
The tribe has about 485 members, and its reservation spreads across more than 31,000 acres in a checkerboard pattern that includes parts of Palm Springs, Cathedral City, Rancho Mirage and surrounding areas. Its initial victory in the case will likely change how decisions are made about managing groundwater.
Many details have yet to be worked out in court. In upcoming phases, District Court Judge Jesus Bernal will consider how much groundwater the tribe is entitled to, whether it owns storage space within the aquifer and whether its groundwater rights include a water-quality component.
The tribe has accused the water agencies of imperiling the aquifer by allowing its levels to decline over the years and by using saltier, less pure Colorado River water to offset the amounts drawn out.
The Colorado River has a higher concentration of salts and minerals — called total dissolved solids — than the valley's aquifer. And higher concentrations of dissolved salts can affect the taste of tap water. The levels in the groundwater have increased over the decades in areas where imported water has seeped underground.
The agencies, however, defend their efforts to manage water supplies and insist that water from the Colorado River meets all drinking water standards.
These disputes are playing out as water supplies are under mounting strains in the Southwest. The Colorado River has been dwindling during what scientists say is one of the driest 19-year periods in the past 1,200 years.
Climate change is contributing to the pressures, diminishing the flow of rivers and streams. Scientists have projected that warming will likely cause the Colorado River's flow to decrease by 35 percent or more this century.
Lake Mead near Las Vegas now stands at just 37 percent full, and federal water managers have been pressing for California, Arizona and Nevada to finish negotiating a "drought contingency plan," under which all sides would agree to temporarily take less water to keep the reservoir from falling to disastrously low levels.
Representatives of the Coachella Valley Water District have been involved in discussions about the proposed plan and have signaled they're willing to participate. It's not yet clear how much water CVWD might end up leaving in Lake Mead to contribute to the effort.
Managers of the valley's water districts have also voiced support for California's controversial $17 billion plan to build two giant water tunnels beneath the Sacramento-San Joaquin Delta to carry water southward — a project intended to boost the reliability of water deliveries. It's not clear how much the project might end up costing ratepayers.
While the agencies look outward to try to secure their imported water supplies, they're also going to be required to look inward to find ways to conserve more.
New legislation signed this year by Gov. Brown will set water-efficiency goals for cities and agencies statewide, and will require water suppliers to develop annual water budgets. The legislation also includes requirements aimed at encouraging more conservation in agriculture.
More of the state's agricultural water suppliers — including those that irrigate at least 10,000 acres — will be required to measure how much water is delivered to farms, adopt a pricing structure for water customers "based at least in part on quantity delivered," and take other steps to encourage efficiency.
Farming districts will be required to submit agricultural water management plans that include information on "which efficient water management practices have been implemented," and what other improvements are planned to dial back water use.
Depending on how those requirements are implemented in the Coachella Valley, the new legislation might help drive more water-savings on farms.
Whether the area ultimately succeeds in bringing its water supplies into a long-term balance will depend on many factors, including how well local water districts prepare for the possibility of getting less water in the future.
For now, the agencies are working on a new version of their regional water management plan.
*Editor's note: This sentence was edited to clarify that the listing of the Indio subbasin as "high" priority was included in a draft document.
Ian James writes about water for The Desert Sun. Reach him at ian.james@desertsun.com or @ByIanJames.
Evan Wyloge is the Data/Investigations Editor at The Desert Sun. He can be reached at Evan.Wyloge@desertsun.com, (760) 218-5154 and @EvanWyloge.
Got ideas to share about water in the Coachella Valley? Send us your thoughts in 200 words or less, together with a headshot, and we'll publish a selection of submissions. Email your contribution, with the subject line "CV water" to letters@desertsun.com.
Contact Us Support Local Businesses Advertise Your Business Advertising Terms and Conditions Place An Ad Licensing & Reprints Help Center Subscriber Guide My Account Give Feedback
© 2021 www.desertsun.com. All rights reserved.

redpajama_set_name: RedPajamaCommonCrawl


By Aggie Hurst, telling her own story in Aggie: The Inspiring Story of A Girl Without A Country, Springfield, MO: Gospel Publishing House, 1986.
Aggie was not to be deterred. She walked into the squalid apartment, with liquor bottles everywhere, and approached the seventy-three-year-old man lying in a rumpled bed.
The man instantly stiffened. The tears stopped. "God forgot all of us," he said. "Our lives have been like this because of Him." He turned his face back to the wall.
Over the next few days, father and daughter enjoyed warm moments together. Aggie and her husband soon had to return to America— and within a few weeks, David Flood had gone into eternity.
A few years later, the Hursts were attending a high-level evangelism conference in London, England, where a report was given from the nation of Zaire (the former Belgian Congo). The superintendent of the national church, representing some 110,000 baptized believers, spoke eloquently of the gospel's spread in his nation. Aggie could not help going to ask him afterward if he had ever heard of David and Svea Flood.
In time that is exactly what Aggie Hurst and her husband did. They were welcomed by cheering throngs of villagers. She even met the man who had been hired by her father many years before to carry her back down the mountain in a hammock-cradle.
Psalm 126:3-6 — The Lord has done great things for us, and we are filled with joy. Restore our fortunes, Lord, like streams in the Negev. Those who sow with tears will reap with songs of joy. Those who go out weeping, carrying seed to sow, will return with songs of joy, carrying sheaves with them.


Become one of the leading System Integrators in Vietnam and Southeast Asia.
Provide ICT products and solutions with the optimal technologies and the best quality services to customers.
works with a warm heart and a spirit of continuous learning for making SVTECH be the leading System Integrators in Vietnam and Southeast Asia.
That is a development which focuses on efforts to become the best in any field that we participate in. Therefore, customers' trust is a vital component for us to grow.
SVTECH success depends on the companionship with our customers and the ability to deliver success to them.
All members are bound together on sharing of responsibilities rather than by power system. Company is the sweet-home that career and path of glory of each staff associated with every period of success of the Company.
A perfect service that we supplied to customers can only be achieved by people who have high competency, full responsibility, non-stopped struggle, and characteristics which base on social standards.


Fall prevention is a top priority in acute care, skilled care, and home health. Many outpatient clinics have a fall prevention emphasis also.
The reason: Falls happen. A lot. And the costs are astounding.
Beyond simply being a cost to the healthcare system, falls also frequently result in loss of independence.
Staying active is one of the best fall prevention strategies.
An older adult falls and fractures a bone, maybe a wrist, humerus, hip, or ankle.
After surgery and a brief hospital stay, he or she moves to a skilled facility of some sort. This could be a dedicated rehab facility, skilled care, nursing home, or assisted living.
In many cases, patients don't return to their home to live because of the fear of falling again or lack of help at home.
And once someone assumes official residence in a facility, the chances of living independently again are very minimal.
The PT community debates if falls can truly be prevented and what specifically can be done to help.
While the total effectiveness of specific exercises and activities are uncertain, we know that strength training, balance activities, and education help in fall prevention.
People with chronic and/or progressive diseases like Parkinson's, MS, COPD and many others benefit from these activities for certain.
As a home health professional, I prescribe functional exercises most of time.
Strength training and balance activities help in fall prevention.
Education is key. Practice makes perfect.
The goal of the therapist is always to get patients to a place where they can take ownership of their health and manage their condition as independently as possible.
There is no substitute for working with a patient in person. The ability to guide, correct, and encourage a patient in a balance activity or exercise is one of the quickest paths to building his or her confidence.
These times together are valuable but too short to reach the end goal.
It's clear patients who want more independence must work on their activities and/or exercises on their own to keep progress headed in the right direction.
I typically provide materials for patients to use as reference for these between session times.
In the past, these materials range from printed sheets of information to stick figure drawings for less technical patients. I am currently exploring the In Hand Health system for those who are tech savvy.
This system puts me in a HIPAA-compliant communication environment (texts, videos, images, and audio clips) with a patient and/or a caregiver.
In Hand Health provides narrated videos that clearly explain the movements of an activity (even things like wound management or preparing an ice pack) or exercise. Patients don't have to worry about misplacing printed documents. Very helpful!
There are many fall prevention steps therapists and caregivers can make around a home environment.
Caregivers can help by removing trip hazards from homes and installing grab bars in bathrooms and other logical places.
Despite all these efforts, patients will experience falls.
Perhaps with more awareness, we can lower the rate and empower patients to maintain their independence as long as possible.


text:
Siphunculina intonsa är en tvåvingeart som beskrevs av Lamb 1918. Siphunculina intonsa ingår i släktet Siphunculina och familjen fritflugor.

Artens utbredningsområde är Sri Lanka. Inga underarter finns listade i Catalogue of Life.

Källor

Fritflugor
intonsa

redpajama_set_name: RedPajamaWikipedia


text:
Q: How to automate video editing for streaming Let me describe the problem I am facing:
I would like to record a room with a fixed camera, and put the video live on Twitch. In the room will be present two ore three people talking around a table, wearing hoodies.
Here comes the problem: I would like to obscure the faces of the people in the shot, for example by making the region under the hood black, or by drastically reducing the luminosity of that region in the video. This editing work must be performed live and automatically, by some sort of script, since the video is to be streamed live.
Facing this challenge I came up with the following technique, let me know if it is any good: I though of putting colour markers on the faces of the people in the shot, or maybe colour markers all around the border of the hood, let's say yellow markers. Then I will clean the room of anything else yellow and use the color as reference to tell my script where to perform the video modding. This seems to me like a good plan; I have seen that OBS has a face recognition function, but I fear it will be not completely accurate, leading to faces getting flashed in the live footage.
Problem is I have no idea how to start implementing this functionality! I don't know, in practice, where to start. I need to get the video signal on my machine, somehow pass it to some script, and then pass it to Twitch. How can I do this? What language should I use? For example: is there some sort of python module to handle things like this? Should I somehow just use OBS?

Couple of last notes:
Hiding the faces is not a strict need, is just for mood and aesthetics purpose. So no top security is required.
Also at the table there will be drinks, so the method by which we hide the faces must be resilient to people putting glasses near their faces; for this reason I think colour markers around the borders of the hood is the best bet, but feel free to propose something else.

A: Hi so depending on what streaming software you are using there are different ways of going about it, can you drop a comment letting me know which software you are planning on using, if you haven't got streaming software then I would say that https://obsproject.com/ isn't a bad place to start. I haven't tried blurring my face before but this https://www.youtube.com/watch?v=fQmBs3PRpOA looks like a good place to start. I doubt you will have to use any coding.

redpajama_set_name: RedPajamaStackExchange


Are you looking for Hesperia Bail Bonds? Most Hesperia bail bond companies can bail you (or another person) out anytime anywhere in Hesperia. BailBondsNetwork.com helps you locate and get in touch with a licensed bail bond company in Hesperia, Michigan. At your convenience, many bail bonds agents will come pick you up privately. Installment payment plans are often available depending on case by case basis.
Upon arrest anywhere in Oceana county, a person is usually processed at the Oceana county jail. In order to be released from jail, a few steps must occur, including being "booked in" and posting bail. When the bail bond amount is decided, a bail bonds agent arrives to post the bail bond at the local jail. Now the jail release procedure begins and typically can take anywhere from 1 to 2 hours to complete. Even though cash bonds are permitted, it is normally not a common practice due to it's high expense.


Positioned in the historic Wanamaker creating, Macy's Center City is a single of Philadelphia's leading shopping destinations with more than one hundred years of retail history. I was reading over the weekend about a mall in (I think) NY who had a Tv screen set up displaying the faces of people who have been previously arrested for shoplifting. And your tiny bathroom trick or your fitting area concept will be already booted due to the fact these issues will have already been covered as you stroll your shoplifting self into the store. Notos House has also a retailer at the Golden Hall , whilst at The Mall Athens you can visit the Notos Exclusive shop with brands such as GANT, Lacost, Newman and MURPHY NYE. Other possibilities incorporate charging separately for mileage, an extra fee for choosing up coupons ahead of shopping, or added fees for shopping at more than one shop. Go shopping with a trendy buddy and get their opinion on what you should wear.
To this day, I by no means pass up a chance to go to Oakbrook Center, the famed open-air mall in the west suburbs. Shortlist the sites that are supplying the factors you are searching to acquire and have a excellent amount of variety and selections for the very same. For instance, you could promote a $40 shopping charge, which involves two hours of shopping, delivery, and mileage (cost of groceries not integrated). Under, I have compiled a list of bridesmaid dress designers who give a internet site with the colour altering function. Maintain this on your list of fashion forward places to shop whether or not pregnant or not!!
You'll discover tons of clothes that are going out of season, and it's so significantly less expensive to stock up early than to go on a shopping spree later on. At the finish of this summer season, I headed to Wet Seal's website and got two pairs of shorts for $10, leggings for $eight, and three shirts for $7. My order total was initially $95.86, but right after discounts were applied, it was decreased to $50.


How to use a compass Using the compass alone This is a very easy lesson, First, a quick summary of what you will learn in this lesson: 1. Align the edge of the compass with the starting and finishing point. 2. Rotate the compass housing until the orienting arrow and lines point N on the map. 3. Rotate the map and compass together until the red end of the compass needle points north. 4... EXPLANATION OF COMPASS DRAW . A. When authorized. Compass draws may be used in any tournament provided the entry form states the tournament shall be played using a compass draw format.
Learn to draw a compass. This step-by-step tutorial makes it easy. Kids and beginners alike can now draw a great looking compass. This step-by-step tutorial makes it easy. Kids and beginners alike can now draw a great looking compass.... The Compass Draw is a tennis tournament that takes place over several months. Players get lots of fun, competitive matches in their local area and compete for prizes!
To draw the compass onto an existing Bitmap just modify the method to not use "result" but to use the passed on Bitmap and use the size of the existing bitmap or whichever size you want he compass to be and to modify it's location on the bitmap is easy enough by modifying the xcenterpoint and ycenterpoint.
A compass can help you draw a perfect circle and you can also use it to create one or multiple rectangles. A drawing compass allows you to attach a writing tool on the mobile point of the compass. Always use a pencil in case you need to go back and re-work any of your drawn shapes.
Learn to draw a compass. This step-by-step tutorial makes it easy. Kids and beginners alike can now draw a great looking compass. This step-by-step tutorial makes it easy. Kids and beginners alike can now draw a great looking compass.


text:
DMCV Sharks soccer was established in 1970, and is a community based program that is devoted to teaching and nurturing the development of youth players. It is our mission to offer opportunities for players of all skill levels and experience, and to provide a positive learning environment where players can develop their technical skills and build a passion for the game. We offer all of our players the opportunity for growth and advancement in the sport, because we want each player to reach their highest potential
ABOUT DMCV SHARKSRECREATIONAL PROGRAMS
The DMCV Sharks Recreational program is one of the largest in the country, serving thousands of participant in the Del Mar/Carmel Valley area. The DMCV Sharks Rec program is for everyone regardless of skill set. The Recreational Program consists of a Fall, Winter, and Spring leagues for area youth ranging from under six years old to under nineteen years old. We also conduct a wide variety of camps and clinics throughout the year to help players to have fun and further develop their skills.
VOLUNTEER COACHES
LEARN ABOUT DMCVRECREATIONAL SEASONS
Learn more about our Fall Season, Winter Season (Junior World Cup), and Minor League Soccer (MLS) Spring Season
ANNUAL TIMELINE
DECEMBER/JANUARY JUNIOR WORLD CUP WINTER PROGRAM REGISTRATION BEGINS
FEBRUARY/MARCH JUNIOR WORLD CUP LEAGUE PLAY
MARCH/APRIL MINOR LEAGUE SOCCER SPRING PROGRAM REGISTRATION BEGINS
FEBRUARY/MARCH MINOR LEAGUE SOCCER SPRING PROGRAM REGISTRATION BEGINS
APRIL./JUNE MINOR LEAGUE SOCCER LEAGUE PLAY
APRIL FALL SEASON REGISTRATION BEGINS
APRIL FALL SEASON VIP WALK-UP REGISTRATION (COACHES ONLY)
MAY FALL SEASON WALK-UP REGISTRATION
MARCH SUMMER CAMP REGISTRATION BEGINS
MAY/JUNE FALL SEASON COORDINATING COACHES PAIRS
JUNE/AUGUST SUMMER CAMP 5 WEEKS OF CAMPS, SIGN UP ONLINE
JUNE FALL SEASON DIVISION 3-5 PLAYER DRAFTS
JULY FALL SEASON COLLECT PRACTICE FROM REQUESTS
AUGUST FALL SEASON POST ROSTERS/ SCHEDULES ONLINE
AUGUST 1/SEPTEMBER FALL SEASON PLAYER DROPS/ADD AND CHANGE REQUESTS
AUGUST FALL SEASON PCA COACHING WORKSHOP
AUGUST FALL SEASON EQUIPMENT BAG PICKUP
AUGUST FALL SEASON UNIFORM PICKUP (COACHES ONLY)
SEPTEMBER/OCTOBER FALL SKILLS CLINICS SEE CAMPS & CLINICS PAGES
OCTOBER ALL-STAR TRYOUTS –
NOVEMBER FALL SEASONS INTRA-LEAGUE TOURNAMENT
NOVEMBER FALL SEASON ALL-STAR MEETINGS AND REGISTRATION
DECEMBER FALL SEASON ALL-STAR TOURNAMENT
Under/Age U6 U7 U8 U9-U10 U11-U12 U13-U14 U15-U16 U17-U19
Birth Year 2014 2013 2012 2011-2010 2009-2008 2007-2006 2005-2004 2003-2001
# of Players on Field / Max. Roster Size 4v4
12 4v4
13 11v11
Match Time (Minutes) 2×20 2×20 2×20 2×25 2×30 2×35 2×40 2×45
Ball Size /
Goal Size 3
5×10 3
Offside Called NO NO YES YES YES YES YES YES
Maximum Roster Size 12 12 11 11 13 16 18 18
League DMCV Sharks DMCV Sharks DMCV Sharks DMCV Sharks DMCV Sharks DMCV Sharks Presidio Presidio
The league relies on volunteers to referee Recreational games and tournaments. No experience necessary – sign up to become a Ref today!
TOPSoccer is an outreach soccer program that is designed to meet the needs of children and young adults with physical and/or mental disabilities. The program is designed to foster the physical, mental, and emotional growth of the child and to teach basic soccer skills in a fun and rewarding environment.
During these 5-day camps, players have fun while working on their technical abilities, speed and agility, as well as basic skills including dribbling, passing, trapping and shooting.
SPONSOR A TEAM
Registration fees do not completely cover the costs of running the Rec soccer league, so sponsors are needed to help cover the additional costs to run the league. Team sponsorship is $350.00. Please let your coach know that you are interested in sponsoring the team.
BECOME A VOLUNTEER COACH
Every year we need more coaches, assistants and team parents. The league depends on parents to fill all these positions,and we are always looking to add to our roster of coaches, at all levels of experience. If you would like to volunteer as a coach or assistant coach, or if you know someone who is interested in making a difference in a young soccer player's life, please contact Erin Misaki, Director of Recreational Programs. No experience is necessary, we will train you!
You can also register online as a volunteer at the same time you register your child and let us know which position you would like. For Head and Assistant Coaches, our Division Coordinators will be your source of information. We will only form teams for the number of coaches we have. All other players will be placed on a wait-list until another coach volunteers.
The requirements for coaching are set by our parent organization, Cal South. All Head and Assistant coaches must go through Risk Management (fingerprinting) that is paid for by the league. In addition, coaches are now required to have a coaching license and we offer a minimum or two license classes per season. You will also be asked to attend a coaches meeting in August. For detailed information, contact Erin Misaki, Director of Recreational Programs.
RECREATIONALPROGRAM DIRECTOR
DIRECTOR OF RECREATIONALERIN MISAKI
Erin Misaki begins her third season with the Sharks after two years as the Director of Coaching for Saddleback United where she worked closely with former US National Team star, Joy Fawcett. Prior to that, Erin worked with Velocity Sports in Santa Clarita from 2008 to 2009 where she taught soccer specific speed, agility and strength classes. Erin has been a youth coach since 2000 and she brings a wealth of knowledge and experience to the Sharks.
As a player, Erin played for the U14, U16, U18 and U21 youth national teams. She played her college soccer at the University of Portland where she was the captain of the first National Championship team for the University. After Portland, Erin was drafted into the WUSA where she played professionally for the Philadelphia Charge. Erin then went on to play professionally in Japan with the Tokyo Verdi Team.
Erin graduated from the University of Portland in 2002 with a Bachelor's degree of Art and Social Sciences. She also received an Interdisciplinary Degree, three disciplines combined into one: Sociology, Psychology and Education.


text:
Album Review: Case – The Rose Experience
Nov 22, 2009 | Album Review
The release of Case's fourth album "The Rose Experience" is a great accomplishment. Not only has the album been eight years in the making, but there was a time when it looked like not only his recording career, but also his life, might be over. Shortly after the release of his "Open Letter" album in 2002, Case accidently fired a gun which struck him in the throat and missed his spine by an inch. Miraculously, he was out of the hospital within four hours with no damage to his vocal chords at all.
After gaining his release from Def Soul, he partnered with manager Blue Williams to create an independent label called "Indigo Blue." Now with full creative control, Case is in full control of his destiny, and that is very evident on "The Rose Experience." The signature case sound is still here and as he has done on each of his previous albums, he takes us on his soulful journey through love and relationships. In fact, his sound has not evolved much since he first came on the scene in the early 90's and that is not a bad thing at all.
This is immediately evident upon hearing the first single "Lovely." On this soulful ballad, Case stays true to the formula that landed him some of his other big hits such as "Happily Ever After" and "Missing You." He uses this piano laced ballad as an opportunity to express to his woman how beautiful she is in his eyes. As long as romancing a woman will be in style, Case will always have something to sing about.
In essence, just like all of his previous albums, each song hits on a different point in a relationship; and there aren't many in r&b who can better accentuate this than Case. On "Let Me Down Easy," you almost feel for him as he passionately sings about a woman breaking his heart. Next, on "Me and You," he croons about being caught up between two women and having to choose. Even though everyone may not be able to relate, he is able to make you feel as though you are right there in the situation yourself.
Another highlight of the album is the way he harmonizes which adds feeling to each song. "Déjà Vu" is a great example as he sings about meeting a woman for the first time but remembering her from the past. Case is also at his best on "Smile" where he's so smooth that he can easily convince any woman to do just what the title states. After hearing his silky and soulful vocals throughout the album, I'm convinced he's still in his prime.
Since Case is now independent, he was able to handle most of the production on this album and make it his most personal album to date. From to the sultry slow jams to the bubbly mid tempo tracks, he was able to create the perfect backdrop on just about every song. However, one song that sounds out of place is the Neptunes produced "Should Have Known Better." Whereas most of the production on the album has a retro sounding 90's feel, this song does not fit in.
In my opinion, "The Rose Experience" has many of the qualities of a successful r&b album. From Case's soulful voice, to the very good production, to the content on each song, you can't ask for much else. If you are looking for an album with singles that will end up all over the radio, you came to the wrong place. What we have here is a carefully crafted creation that flows from beginning to end and characterizes the essence of r&b.
Rating: 3.75/5
Case Talks New Album "The Rose Experience", New Outlook on Life, Meeting Michael Jackson (Exclusive…
Album Review: Justin Timberlake - The 20/20 Experience
Album Review: Justin Timberlake "The 20/20 Experience 2 of 2" (4 stars out of 5)
Case Talks New Album, Def Soul Experience & Music Industry Politics (Exclusive Interview)
Album Review: Case, Heaven's Door
Here Are Five Reasons Why "Black Rose" Will NOT Be the Final Album from Tyrese


The image of the Arctic Fox is taken on Dovrefjell in Norway, while all the African wildlife images are taken in Maasai Mara, Kenya, from Oltepesi Tented Safari Camp's specially modified and low-angled safari vehicle for wildlife photography. Thanks to John Siololo and Johnmark Kiss-may for great guiding. The Bison images are taken in Yellowstone National Park in Wyoming, U.S.
Arctic Fox on Dovrefjell, Norway. Highly Commended i Monochrome Photography Awards 2018. Nikon D5, Nikkor 400/2.8E, 1/2000 sec at f/4. ISO 125.
Cheetah and insect in Maasai Mara. Highly Commended i Monochrome Photography Awards 2018. Nikon D5, Nikkor 600/4E, 1/1600 sec at f/4. ISO 50.
Male lion in Maasai Mara. Highly Commended i Monochrome Photography Awards 2018. Nikon D5, Nikkor 600/4E, 1/1000 sec at f/4. ISO 1,100.
Serval Cat in Maasai Mara. Highly Commended i Monochrome Photography Awards 2018. Nikon D5, Nikkor 600/4E, 1/640 sec at f/4. ISO 9,000.
Bison in Yellowstone, U.S. Highly Commended i Monochrome Photography Awards 2018. Nikon D5, Nikkor 600/4E, 1/1600 sec at f/5.6. ISO 3,200.
Bison in the hot spring steam. Yellowstone, U.S. Highly Commended i Monochrome Photography Awards 2018. Nikon D5, Nikkor 600/4E, 1/2000 sec at f/4. ISO 640.