A PTA modeling a water boiler

water_boiler.tex

\documentclass{standalone}
\usepackage{amssymb,amsmath}
\usepackage{tikz}
\usepackage{mathtools}
\usetikzlibrary{automata,positioning,matrix,shapes.callouts}
\tikzstyle{every node}=[initial text=]
%%% Color setting
\definecolor{coloract}{rgb}{0.50, 0.70, 0.30}
\definecolor{colorclock}{rgb}{0.4, 0.4, 1}
\definecolor{colorloc}{rgb}{0.4, 0.4, 0.65}
\definecolor{colorparam}{rgb}{1, 0.6, 0.0}
%%% Styles
\newcommand{\styleact}[1]{\ensuremath{\textcolor{coloract!80!black}{\mathrm{#1}}}}
\newcommand{\styleclock}[1]{\textcolor{colorclock!80!black}{#1}}
\newcommand{\styleloc}[1]{\ensuremath{\textcolor{colorloc!80!black}{\mathrm{#1}}}}
\newcommand{\styleparam}[1]{\ensuremath{\textcolor{colorparam!80!black}{\mathsf{#1}}}}
\begin{document}
 \begin{tikzpicture}[shorten >=1pt,node distance=5cm,on grid,auto]
  \node[state,initial] (s_0) [align=center] {\styleloc{Locked}\\\styleloc{Light\_off}};
  \node[state] (s_1) [right=of s_0,align=center] {\styleloc{Unlocked}\\\styleloc{Light\_on}};
  \node[rectangle,dashed,draw=black,node distance=1.25cm] (s_1_inv) [above=of s_1] {$\styleclock{c} \leq \styleparam{p}$};
  \node[state] (s_2) [right=of s_1] {\styleloc{Pouring}};
  \path[->]
  (s_0) edge [above,bend left] node[above, align=center] {\styleact{press\_unlock}} node[below, align=center] {$\styleclock{c} \coloneq 0$} (s_1)
  (s_1) edge [below,bend left] node[align=center] {$\styleclock{c} = \styleparam{p}$} (s_0)
  (s_1) edge [below,bend left] node[above,align=center] {\styleact{press\_pour}} node[below, align=center] {$\styleclock{c} \coloneq 0$} (s_2)
  (s_2) edge [above,bend left] node[below, align=center] {$\neg$ \styleact{press\_pour}} (s_1)
  ;
 \end{tikzpicture}
\end{document}