session.texi

@chapter @arc{} at a glance

In this chapter we present a small session with @arc{}. We do not present all
features of the tool; we refer the reader to next chapters for details.
Here we simply show the basics of commands and interactions with @arc{} while 
studying a game between two opponents. We use @arc{} to compute a 
winning strategy for one of the two players.

@section The game 

We consider a game with two players, say @emph{A} and @emph{B}. Player @emph{A}
has four coins and each coin has two different sides. Player @emph{A} arranges 
 coins 
as a square and chooses which side of each coin is visible. @emph{B} never sees
the current side of coins. Each turn of the play, @emph{B} requests @emph{A} 
to change the side of either
@itemize
@item one coin,
@item one column or one line of coins,
@item or one diagonal.
@end itemize
Each request can be satisfied in different ways by @emph{A}; for instance,
when @emph{B} says ``one coin'', @emph{A} has four possibilities. Since 
@emph{B} does not see coins, he can not know the choice made by its opponent. 
@emph{B} wins the game if all coins are on the same side. Of course @emph{A} 
has to make his possible to prevent @emph{B} to reach one of the two winning 
situations. We assume that @emph{A} is honnest enough to end the game when 
he looses. 

Our goal in this chapter is to use @arc{} to find a strategy for player @emph{B}
that is winning from all configurations of the game. 

@section The model

The board game (i.e. the coins arranged as a square) is easily described with 
an @altarica{} node. 
@itemize
@item First we define a domain @code{SIDE} for values that model sides of 
      coins; Booleans could be a good choice but integers 0 and 1 ease the 
      description of properties.
@item Then we declare a node @code{Board} where:
 @itemize 
 @item the four coins are modeled with a two-dimensional array @code{c} 
       of values in @code{SIDE}.
 @item the three requests of the player @emph{B} are modeled with three 
       events called @code{one}, @code{col_or_line} and @code{diagonal}.
 @item the response of @emph{A} is modeled using transitions. The 
       non-deterministic choices made by @emph{A} is straitghforward since
       @altarica{} allows non-determinism on event occurrences.
 @end itemize
@end itemize

We store the @altarica{} model of the game into a file called @file{game.alt}.
The content of the file is given below. In the following lines @t{$} denotes 
the prompt of the shell program (e.g. @command{bash}).

@smallexample
$ cat game.alt
@include game.alt
$ 
@end smallexample

@altarica{} users should have noticed that the third line of the file is not 
an @altarica{} sentence. Indeed, it is the definition of a macro-function 
@code{FLIP(@i{i},@i{j})} for the C preprocessor. This macro-function is a 
shortcut used in transitions to flip the coin at line @code{@i{i}} and column
@code{@i{j}}. We come back on preprocessing in the next section.

@section Getting started with @arc{}

Now that we have written the model of the game we just have to start @arc{} and
load the file @file{game.alt}. @arc{} accepts several options followed by 
filenames (@pxref{The ARC command}, for details on options). 
We start the program with the file @file{game.alt} as argument (the ellipsis 
below replaces the banner of @arc{}). Inputs of the user are written using a 
@t{typewriter} font and @arc{} outputs are printed using @i{italic}.

@smallexample
$ arc game.alt
@i{@dots{}
Loading file 'game.alt'.
game.alt:3: error: syntax error on symbol '#' (current parser is for any text syntax).
arc>}
@end smallexample

Things does not start very well because the @altarica{} parser founds an error
in the file. The error occurs on the first character of the C preprocessor 
line that defines the macro-function @code{FLIP(@i{i}, @i{j})}. 

By default preprocessing of files is disabled; this yields to a syntax error on
line 3. To enable it we use the @ref{setcmd,,@command{set} 
command}, to specify in the preference variable 
@code{arc.shell.preprocessor.default.command} which preprocessor we want to use by default (here @command{cpp}):

@smallexample
@i{arc>@t{set arc.shell.preprocessor.default.command "/usr/bin/cpp"}
arc>}
@end smallexample

Note that the value of preferences are lost between sessions unless the user
requests @arc{} to store them into its configuration file (i.e. 
@file{~/.arcrc}). To save preferences, use the option @option{-save} of the
@command{set} command. (@xref{User preferences}, for existing customization 
variables.)

Now we can reload @file{game.alt}. If we display the node @code{Board} (using 
the @ref{showcmd,,@command{show} command}) we can see substitutions realized
by the preprocessor:
@smallexample
@i{arc>@t{load game.alt}
Loading file 'game.alt'.
arc>@t{show Board}
@include Board.alt
arc>}
@end smallexample

One can notice the presence of an additional event @code{'$'} and a transition
@code{true |- '$' -> }. This is the well-known @math{@epsilon} event and its
associated transition that are added implicitly by the @altarica{} semantics.

@section First computations

Our goal is to compute a strategy that is winning from all positions of coins. 
The size of the state-space of the game (16 configurations) is reasonable 
enough to be displayed. To do this we use @acheck{} commands (see @ref{Using 
the Acheck specifications}). Rather than 
creating a new file containing these commands we use the @ref{evalcmd,, 
@command{eval} command}, that redirects the standard input of the program to 
the @altarica{} parser (note that @sc{readline} is disabled when using 
@command{eval}). Characters @t{^D} denote the end-of-file character that is
generally @kbd{CTRL-D} on Unix-like systems.

@smallexample
@i{arc>@t{eval}
@t{with Board do
 dot(any_s, any_t) > "game.dot";
done
^D}
arc>}
@end smallexample

The @keyword{with ... do ... done} sentence specifies that @arc{} has to apply 
commands listed between the @keyword{do} and @keyword{done} keywords to 
each nodes listed between @keyword{with} and @keyword{do}. Before executing
 commands @arc{} computes the semantics of the node and then applies 
commands to the semantics. 

Here we apply to @code{Board} the command @command{dot} (@pxref{Commands}).
This latter displays the state graph of the node in the @sc{GraphViz} file
format (i.e. for the @command{dot} tool - @bibcite{GraphViz}). 
The two keywords @keyword{any_s} and @keyword{any_t} simply said that all
states and all transitions have to be displayed (sometimes it is interesting to
restrict these two sets e.g. counterexamples).

The output of the command is redirected into a file called @file{game.dot}. 
Using the @command{dot} tool of @sc{GraphViz} we obtain the following graph:

@center{@image{game,16cm,,,.pdf}}

Despite its small size this graph is not very informative. @arc{} possesses 
another command, called @command{quot}, that outputs the state-graph (yet in 
@code{dot} format) but this time, states are gathered according to the greatest 
auto-bisimulation that respects currently computed properties.

@smallexample
@i{arc>@t{eval
with Board do 
 quot() > "game_q0.dot";
done
^D}
arc>}
@end smallexample

As shown on the following figure the generated graph is not more interesting 
than the previous one. Up to now no properties have been computed and since all
events are possible from all states the greatest auto-bisimulation is the 
identity. 

@center{@image{game_q0,5cm,,,.pdf}}

To refine the result we compute small properties that will label states:
@itemize
@item @var{O} is the set of states where only one coin is either 0 or 1;
@item @var{CL} is the set of states where coins form columns or lines;
@item @var{D} is the set of states where coins form diagonals;
@item and finally, @var{W} is the set of states that are winning for @emph{B}.
@end itemize

These properties are simply written ``@code{@var{X} := @math{@phi}}''
where @var{X} is the name of the set and @math{@phi} is an @acheck{}
formula. In our example properties are related to values of coins. When we have
to talk about the
values of variables one writes the corresponding Boolean expression between
square-brackets. For instance, winning states (the set @var{W}) are those for 
which all coins display the side 0 or all display the side 1; the corresponding
formula for this set can be that the sum of values that label coins is either 
0 or 4.

@smallexample
@i{arc>@t{eval
with Board do 
 W := [c[0][0] + c[0][1] + c[1][0] + c[1][1] = 0 or
       c[0][0] + c[0][1] + c[1][0] + c[1][1] = 4];

 O := [c[0][0] + c[0][1] + c[1][0] + c[1][1] = 1 or
       c[0][0] + c[0][1] + c[1][0] + c[1][1] = 3];

 CL := [c[0][0] + c[1][0] = 2 and c[0][1] + c[1][1] = 0 or 
        c[0][0] + c[1][0] = 0 and c[0][1] + c[1][1] = 2 or
        c[0][0] + c[0][1] = 2 and c[1][0] + c[1][1] = 0 or
        c[0][0] + c[0][1] = 0 and c[1][0] + c[1][1] = 2];

 D := [c[0][0] + c[1][1] = 2 and c[1][0] + c[0][1] = 0 or  
       c[0][0] + c[1][1] = 0 and c[1][0] + c[0][1] = 2];

 show (all);
 quot() > "game_q1.dot";
done
^D}
@include Board.props
arc>}
@end smallexample

Before the output of the @command{quot} command into the file @file{game_q1.dot}
we call the command @command{show} that displays the cardinalities of currently
computed properties. The parameter @keyword{all} indicates that all known 
properties have to be displayed. This keyword can be replaced by a 
coma-separated list of property identifiers.

The reader can notice that some properties that was not specified have been 
computed. In fact, several properties are pre-defined in @acheck{} 
(@pxref{Built-in sets}).
 
The new graph obtained with the @command{quot} command is displayed below. 
@center{@image{game_q1,13cm,,,.pdf}}
This graph shows that the game would have been modeled with only four
configurations. Indeed sides of coins (0 and 1) play symetrical roles and only
arrangements of coins (i.e. lines, columns, @dots{}) are relevant rather than
their actual position.

Even if the graph is simpler than the previous one, the winning strategy 
remains unobvious@footnote{However, with a little effort it is easy to get 
it!}.

@section Computing the winning strategy

To check the existence of the winning strategy we use @mecv{} specifications
(see @ref{Using the Mec 5 specifications}). The logic of @mecv{} permits to 
write easily formulas that talk about individual configurations and events 
rather than sets of configurations and transitions as in the @acheck{} language.

@mecv{} specifications are essentially a list of relations (or predicates) 
definitions. The first one we define is the unary relation that contains all
configurations that are winning for @emph{B}.
@smallexample
@i{arc>@t{eval
Win(s : Board!c) := 
   s.c[0][0] + s.c[1][0] + s.c[0][1] + s.c[1][1] = 0 or
   s.c[0][0] + s.c[1][0] + s.c[0][1] + s.c[1][1] = 4;
^D}
Win (s : Board!c) : 2 elements / 7 nodes
arc>}
@end smallexample

This declaration starts with the signature of the relation : its identifier
(@code{Win}) and the name and type of each columns (here @code{s} of type 
@code{Board!c}). @code{Board!c} is the type of configurations of the node 
@code{Board}. The prototype is then followed by a first order formula whose 
models are elements of the defined relation. The formula can refer to the 
relation itself (i.e. the relation is defined recursively) in which case its 
models are elements of the underlying fixed-point. We refer the reader to 
@ref{Using the Mec 5 specifications}, for details on the syntax and semantics 
of the @mecv{} logic.

If @arc{} has not been started in @i{quiet} mode (i.e. with the @option{-q} 
option) it displays the cardinality of the relation once its computation is 
done. To display the number of elements of a relation, use the @ref{cardcmd,,
@command{card} command}:
@smallexample
@i{arc>@t{card Win}
card (Win) = 2
arc>}
@end smallexample

@mecv{} specifications does not permit to talk about sequences of arbitrary 
length. To compute the result we enumerate possible lengths of strategies
until we found at least one. 

We first define a relation @var{WSeq}@ind{k} (@math{k > 0}) with @math{k+1}
arguments : a configuration @math{s} and @math{k} events @math{e_i} for 
@math{i=1, @dots{}, k}. A vector @math{@langle{}s, e_1, @dots{}, e_k@rangle{}} 
belongs to @var{WSeq}@ind{k} if and only if the sequence 
@math{e_1, @dots{}, e_k} is executed from the configuration @math{s} the game 
passes inevitably through a winning configuration:
@itemize
@item For @math{k=1}, the relation is simply:
@smallexample
WSeq1(s : Board!c, e1 : Board!ev) := 
 Win(s) or 
 [t : Board!c] (Board!t (s,e1,t) => Win (t));
@end smallexample
@item For any @math{k>1}, the relation is defined using @var{WSeq}@ind{k-1}:
@smallexample
WSeq@ind{k}(s : Board!c, e1 : Board!ev, @dots{}, e@ind{k} : Board!ev) := 
 Win(s) or 
 [t : Board!c] (Board!t (s, e1, t) => WSeq@ind{k-1} (t, e2, @dots{}, e@ind{k}));
@end smallexample
@end itemize

The relation @math{S_k} that contains winning strategy of length @math{k} is a 
@math{k}-ary relation whose argument are events @math{e_i} for @math{i = 1, 
@dots{}, k}. Its definition simply expresses that the sequence of events is 
winning from all configurations:
@smallexample
S@ind{k}(e1 : Board!ev, @dots{}, e@ind{k} : Board!ev) := 
 [s : Board!c] WSeq@ind{k} (s, e1, @dots{}, e@ind{k});
@end smallexample

These relations, @math{WSeq_k} and @math{S_k}, have been written until 
@math{S_k} becomes non-empty; we gathered them into a file @file{game.mec5}. 
The first non-empty relation is @math{S_7} and is a singleton:
@smallexample
@i{arc>@t{load game.mec5}
Loading file 'game.mec5'.
card (Win) = 2
card (S1) = 0
card (S2) = 0
card (S3) = 0
card (S4) = 0
card (S5) = 0
card (S6) = 0
card (S7) = 1
arc>@t{show S7}
e1. = diagonal, e2. = col_or_line, e3. = diagonal, e4. = one, e5. = diagonal, 
e6. = col_or_line, e7. = diagonal
arc>}
@end smallexample

The reader can use the @command{run} command (@xref{Graphical simulator}) to
try to win against the strategy given by the relation @var{S7} ...