documents/source/henshin_mcrl2/sections/modelchecking-mcrl2.tex

\section{Instance-aware model checking with \mcrl}
\label{sec:modelchecking-mcrl2}

\mcrl~\cite{mcrl2} is a behavioral specification language and associated toolset with support for model checking based on the modal $\mu$-calculus extended with regular expressions, data and time~\cite{GM99}. \mcrl can indirectly model check explicit state spaces as generated by \henshin using the import tool \texttt{lts2lps} which converts a given LTS into \mcrl's own format (so-called \emph{linear process specifications}). 

The \henshin state space tools include an adapter and a front-end for instance-aware model checking of generated state spaces using \mcrl. State spaces are first converted into an LTS format readable by \mcrl. In the mode with node IDs, the adapter extracts all used node IDs from the state space first and generates a data type definition in the format of \mcrl. For the RailCab example, the generated data type specification is shown in Listing~\ref{mcrl2data}. As data types in \mcrl cannot make use of inheritance, the adapter identifies \textsf{Vehicle} as common supertype of \textsf{Shuttle} and \textsf{Train}. The adapter found five node IDs for this type and generates the data type \texttt{\underline{Vehicle}} accordingly as a sum over five different identifiers, modeling the instances. These identifiers are also used in the parameters of the transitions and can be therefore used for the model checking (see also the generated actions and their parameter types in line~2). The adapter also generates the helper predicates \texttt{isShuttle} and \texttt{isTrain} (see line 4--5) which can be used to check for the real data type of instances in formulas. 

Using the generated LTS and data type definition in Listing~\ref{mcrl2data}, we can now directly verify $\mu$-calculus formulas with data using \mcrl. For our running example we check the following two properties:

\lstset{emph={Vehicle,Bool}}

\begin{mcrlcode}[float=t,aboveskip=-1mm,belowskip=-1mm,
  caption={Generated \mcrl data type specification for the RailCab example},label={mcrl2data}]
sort Vehicle = struct s1 | s2 | s3 | t4 | t5;
act move : Vehicle;    createConvoy : Vehicle#Vehicle;    deleteConvoy : Vehicle#Vehicle;
var x : Vehicle;
map isShuttle : Vehicle -> Bool;       eqn isShuttle(x) = (x==s1) || (x==s2) || (x==s3);
map isTrain : Vehicle -> Bool;         eqn isTrain(x) = (x==t4) || (x==t5);
\end{mcrlcode}
\begin{mcrlcode}[float=t,,aboveskip=0mm,belowskip=-2mm,
  caption={Example property \emph{a)}},label={propA}]
forall s:Vehicle.val(isShuttle(s)) => 
 ([true*] (exists t:Vehicle.val(isShuttle(t)) && (<true*.createConvoy(s,t)> true)))
\end{mcrlcode}

%\vspace{-8mm}
%\begin{mcrlcode}[float=h,caption={Example property B},label={propB}]
%forall s:Vehicle.val(isShuttle(s)) => 
% ([true*] (exists t:Vehicle.val(isShuttle(t)) && (<move(s)*.createConvoy(s,t)> true)))
%\end{mcrlcode}

\begin{enumerate}[label=\emph{\alph*})]
  \item For every shuttle it holds in every state that it can eventually form a convoy with another shuttle.
	In \mcrl-syntax, the property can be written as shown in Listing~\ref{propA}.
	This property is satisfied.
  \item For every shuttle it holds in every state that it can eventually form a convoy with another shuttle 
  only by moving itself (meaning that no other vehicle stands in the way). We can adapt the formula in Listing~\ref{propA} by replacing \lstinline!<true*.createConvoy(s,t)>! with \lstinline!<move(s)*.createConvoy(s,t)>!.
  This property is not satisfied, meaning that it is possible that a train blocks a shuttle.
\end{enumerate}
Note that this approach allows us to use existential and forall-quantification over node types in the original graph transition system and to track transitions involving bound node variables.