Commit f86ce9c2 authored by Markus Klinik's avatar Markus Klinik
Browse files

description of state and actions

parent ffef01a5
......@@ -51,7 +51,7 @@
\usetikzlibrary{arrows.meta}
\usepackage{listings}
%\input{proportioneleListings.tex}
\input{languages.tex}
% proof trees
\usepackage{bussproofs}
......@@ -85,6 +85,7 @@
%BEGIN user-defined commands ===========================
\newcommand{\todo}[1]{\textcolor{red}{\emph{Todo: #1}}}
\newcommand*{\name}[1]{\textit{#1}}
% general math
\newcommand{\set}[1]{\{\,#1\,\}}
......
% !TEX root=../main.tex
%% Styles %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\lstdefinestyle{natural}
{columns=fullflexible
,gobble=2
,breaklines=true
,breakatwhitespace=true
,literate=
%{.}{{$\cdot$}}1
%{.}{{\ }}1
{<<}{{$\<$}}1
{>>}{{$\>$}}1
{->}{{$\to$\ }}2
% {--}{{--}}1
%{_}{{\ }}1
%{\ "}{{\ \textquotedblleft}}2
%{"\ }{{\textquotedblright\ }}2
,basicstyle={\sffamily}
,keywordstyle=[1]{\bfseries}
,keywordstyle=[2]{\scshape}
,keywordstyle=[3]{}
%,commentstyle={\itshape}
%,identifierstyle={\itshape}
,emphstyle={\itshape}
%,stringstyle={\rmfamily}
,showstringspaces=false
,texcl=true
,mathescape=true
%,escapechar=\$
%,escapeinside={\{\}}
,xleftmargin=1\parindent
}
\lstdefinestyle{flexible}
{columns=flexible
,gobble=2
,fontadjust=true
,basicstyle={\ttfamily\small}
,commentstyle={\itshape}
,keywordstyle={\bfseries}
%,identifierstyle={\itshape}
%,stringstyle={\ttfamily}
,emphstyle={\itshape}
,showstringspaces=false
,texcl=true
,mathescape=true
%,escapechar=\$
%,escapeinside={\{\}}
,xleftmargin=1\parindent
}
\lstdefinestyle{literate}
{style=natural
,literate=
{\\}{{$\lambda$}}1
{\\\$}{{\$}}1 %NOTE: otherwise eaten by `\`, NOTE: prevents \$ to be parsed as math escape
{\\/}{{$\vee$}}1
{/\\}{{$\wedge$}}1
{A.}{{$\forall$}}1
{E.}{{$\exist$}}1
{->}{{$\rightarrow$ }}1
{<-}{{$\leftarrow$}}1
{==}{{$\equiv$\ }}1
{/=}{{$\nequiv$\ }}1
{<=}{{$\leq$}}1
{>=}{{$\geq$}}1
{>>=}{{>>=}}3 %NOTE: otherwise eaten by `>=`
{\{|}{{$\{\!|\!$}}1
{|\}}{{$\!|\!\}$}}1
{\{|*|\}}{{$\{\!|\!\!\star\!\!|\!\}$}}3
}
%% Definitions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Tasks %%
\lstdefinelanguage{tasks}
{sensitive=true
,morekeywords=[1]{let,in,if,then,else,case,of,ref,type}
,morekeywords=[2]{Bool,Int,String,Unit,List, Ref,Task, Passenger,Seat,Booking}
,moreemph={a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z as,bs,cs,ds,es,fs,gs,hs,is,js,ks,ls,ms,ns,os,ps,qs,rs,ss,ts,us,vs,ws,xs,ys,zs}
,morestring=[b]"
,morecomment=[l]--
,morecomment=[n]{\{-}{-\}}
}[keywords,strings,comments]
\lstdefinestyle{tasks}
{style=natural
,literate=
{\\}{{$\lambda$}}1
{<<}{{$\<$}}1
{>>}{{$\>$ }}1
{->}{{$\to$ }}1
{==}{{$\equiv$ }}1
{/=}{{$\nequiv$ }}1
{<=}{{$\leq$ }}1
{>=}{{$\geq$ }}1
{*}{{$\times$ }}1
{\\/}{{$\vee$ }}1
{/\\}{{$\wedge$ }}1
{>>=}{{$\Then$ }}1
{>>?}{{$\Next$ }}1
{<&>}{{$\And$ }}1
{<|>}{{$\Or$ }}1
{<?>}{{$\Xor$ }}1
{++}{{$\pp$ }}1
{edit}{{$\Edit$}}1
{enter}{{$\Enter$}}1
{update}{{$\Update$}}1
{fail}{{$\Fail$ }}1
}
\lstnewenvironment{TASK}[1][]
{\lstset{language=tasks,style=tasks,#1}}
{}
%\newmacro{TS}[1][1]
%{\lstinline[language=tasks,style=tasks,#1]}
%\newmacro{includeTASK}[2][]
%{\lstinputlisting[language=tasks,style=tasks,#1]{#2}}
%% Flows %%
\lstdefinelanguage{flows}
{sensitive=true
,morekeywords=[1]{module,where,define,using,as,yielding,share,holding,with,do,for,fork,then,when,next,done,on,and,or,not,readonly,writeonly,readwrite}
,morekeywords=[2]{Bool,Int,String,Shared,List, Date,Document,Photo, Citizen,Company,Declaration}
,morekeywords=[3]{True,False,Just,Nothing,List}
,morestring=[b]"
,morecomment=[l]--
,morecomment=[n]{\{-}{-\}}
}[keywords,strings,comments]
% \lstMakeShortInline[language=flows,style=natural] | % |
\lstnewenvironment{FLOW}[1][]
{\lstset{language=flows,style=natural,#1}}
{}
%\newmacro{FL}[1][1]
%{\lstinline[language=flows,style=natural,#1]}
%\newmacro{includeFLOW}[2][]
%{\lstinputlisting[language=flows,style=natural,#1]{#2}}
%% Clean %%
\lstdefinelanguage{clean}
{sensitive=true
%,alsoletter={ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz_`}
%,alsoletter={~!@\#$\%^\&*-+=?<>:|\\} %$
,morekeywords={from,definition,implementation,import,module,system,code,inline,if,case,of,let,let!,in,where,with,class,instance,generic,derive,dynamic,infix,infixl,infixr}
,morestring=[b]"
,morestring=[b]'
,morecomment=[l]//
,morecomment=[n]{/*}{*/}
}[keywords,strings,comments]
\lstnewenvironment{CLEAN}[1][]
{\lstset{language=clean,style=flexible,#1}}
{}
%\newmacro{CL}[1][1]
%{\lstinline[language=clean,style=flexible,#1]}
%\newmacro{includeCLEAN}[2][1]
%{\lstinputlisting[language=clean,style=flexible,#1]{#2}}
......@@ -98,11 +98,52 @@ Our plan synthesis algorithm uses the ingredients of model-based testing to find
(Making coffee)
The running example throughout this chapter will be the problem domain of preparing coffee.
A coffee machine needs to be filled with beans and water before it can prepare coffee.
There are three actions: \emph{addBeans}, \emph{addWater}, and \emph{makeCoffee}.
There are three actions: \name{addBeans}, \name{addWater}, and \name{makeCoffee}.
The planner should deduce that in order to have coffee, the plan must consist of first adding beans and water, in any order, and then make coffee.
\qed
\end{example}
We use the facilities of Gast in a creative way to let it compute plans in the following way.
We use the facilities of Gast creatively to let it compute plans in the following way.
An \textsc{Action} consists of a guarding \textsc{Expression} and a list of \textsc{Assignment}s to state variables.
Actions are specified in a domain-specific language (DSL) so that they can easily be analyzed.
A pre-processing step translates them to Clean before the synthesis algorithm can be run.
The \textsc{State} is a record whose fields are different for each domain.
\begin{example}
(Making coffee)
The state in the coffee domain is a record with three fields.
They store the amount of beans and water present in the machine, and how many cups of coffee the machine has already dispensed.
The following code is its data type definition in Clean.
\begin{CLEAN}
:: State =
{ beans :: Int
, water :: Int
, haveCoffee :: Int
}
\end{CLEAN}
The three actions are defined as follows, given in pseudo-syntax of our action description DSL.
\begin{CLEAN}
Action addWater amount
(amount > 0 && state.water + amount <= maxWater)
(state.water := state.water + amount)
Action addBeans amount
(amount > 0 && state.beans + amount <= maxBeans)
(state.beans := state.beans + amount)
Action makeCoffee
(state.water >= 2 && state.beans >= 1)
( state.water := state.water - 2
; state.beans := state.beans - 1
; state.haveCoffee := state.haveCoffee + 1
)
\end{CLEAN}
The action \name{addWater} takes one argument, \name{amount}.
The guard expression checks that the amount is greater than zero, and that adding the amount to the water currently held by the machine does not exceed \name{maxWater}, which is a globally defined constant.
The effect of \name{addWater} adds the given amount to the state's water level.
The action \name{addBeans} does the same as \name{addWater}, but for the coffee beans.
The action \name{makeCoffee} does not have arguments.
Its guard expression checks that there are at least two units of water and one unit of beans in the machine.
The effect of \name{makeCoffee} removes those units from the state and adds one coffee.
\qed
\end{example}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment