session.texi 13.8 KB
Newer Older
point's avatar
point committed
1
2
@chapter @arc{} at a glance

point's avatar
point committed
3
In this chapter we present a small session with @arc{}. We do not present all
point's avatar
point committed
4
5
6
7
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.
point's avatar
point committed
8

point's avatar
point committed
9
10
@section The game 

point's avatar
point committed
11
We consider a game with two players, say @emph{A} and @emph{B}. Player @emph{A}
point's avatar
point committed
12
13
has four coins and each coin has two different sides. Player @emph{A} arranges 
 coins 
point's avatar
point committed
14
15
16
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
point's avatar
point committed
17
18
@itemize
@item one coin,
point's avatar
point committed
19
@item one column or one line of coins,
point's avatar
point committed
20
21
@item or one diagonal.
@end itemize
point's avatar
point committed
22
23
24
25
26
27
28
29
30
31
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. 
point's avatar
point committed
32
33
34

@section The model

point's avatar
point committed
35
The board game (i.e. the coins arranged as a square) is easily described with 
point's avatar
point committed
36
37
38
39
40
41
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:
point's avatar
point committed
42
43
44
 @itemize 
 @item the four coins are modeled with a two-dimensional array @code{c} 
       of values in @code{SIDE}.
point's avatar
point committed
45
 @item the three requests of the player @emph{B} are modeled with three 
point's avatar
point committed
46
47
       events called @code{one}, @code{col_or_line} and @code{diagonal}.
 @item the response of @emph{A} is modeled using transitions. The 
point's avatar
point committed
48
       non-deterministic choices made by @emph{A} is straitghforward since
point's avatar
point committed
49
       @altarica{} allows non-determinism on event occurrences.
point's avatar
point committed
50
 @end itemize
point's avatar
point committed
51
52
53
@end itemize

We store the @altarica{} model of the game into a file called @file{game.alt}.
point's avatar
point committed
54
55
The content of the file is given below. In the following lines @t{$} denotes 
the prompt of the shell program (e.g. @command{bash}).
point's avatar
point committed
56
57
58
59
60
61
62
63
64
65
66

@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
point's avatar
point committed
67
@code{@i{j}}. We come back on preprocessing in the next section.
point's avatar
point committed
68
69
70
71

@section Getting started with @arc{}

Now that we have written the model of the game we just have to start @arc{} and
point's avatar
point committed
72
load the file @file{game.alt}. @arc{} accepts several options followed by 
point's avatar
point committed
73
filenames (@pxref{The ARC command}, for details on options). 
point's avatar
point committed
74
We start the program with the file @file{game.alt} as argument (the ellipsis 
point's avatar
point committed
75
76
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}.
point's avatar
point committed
77
78
79

@smallexample
$ arc game.alt
point's avatar
point committed
80
@i{@dots{}
point's avatar
point committed
81
82
83
84
85
Loading file 'game.alt'.
game.alt:3: error: syntax error on symbol '#' (current parser is for any text syntax).
arc>}
@end smallexample

point's avatar
point committed
86
Things does not start very well because the @altarica{} parser founds an error
point's avatar
point committed
87
88
89
90
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
point's avatar
point committed
91
92
line 3. To enable it we use the @ref{setcmd,,@command{set} 
command}, to specify in the preference variable 
93
@code{arc.shell.preprocessor.default.command} which preprocessor we want to use by default (here @command{cpp}):
point's avatar
point committed
94
95

@smallexample
96
@i{arc>@t{set arc.shell.preprocessor.default.command "/usr/bin/cpp"}
point's avatar
point committed
97
98
99
100
101
102
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
point's avatar
point committed
103
104
@command{set} command. (@xref{User preferences}, for existing customization 
variables.)
point's avatar
point committed
105
106

Now we can reload @file{game.alt}. If we display the node @code{Board} (using 
point's avatar
point committed
107
the @ref{showcmd,,@command{show} command}) we can see substitutions realized
point's avatar
point committed
108
109
110
111
112
by the preprocessor:
@smallexample
@i{arc>@t{load game.alt}
Loading file 'game.alt'.
arc>@t{show Board}
point's avatar
point committed
113
@include Board.alt
point's avatar
point committed
114
115
116
arc>}
@end smallexample

point's avatar
point committed
117
One can notice the presence of an additional event @code{'$'} and a transition
point's avatar
point committed
118
119
120
121
122
@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

point's avatar
point committed
123
Our goal is to compute a strategy that is winning from all positions of coins. 
point's avatar
point committed
124
The size of the state-space of the game (16 configurations) is reasonable 
point's avatar
point committed
125
126
enough to be displayed. To do this we use @acheck{} commands (see @ref{Using 
the Acheck specifications}). Rather than 
point's avatar
point committed
127
128
129
130
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
point's avatar
point committed
131
generally @kbd{CTRL-D} on Unix-like systems.
point's avatar
point committed
132

point's avatar
point committed
133
134
135
136
137
138
139
140
141
142
@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 
point's avatar
point committed
143
144
commands listed between the @keyword{do} and @keyword{done} keywords to 
each nodes listed between @keyword{with} and @keyword{do}. Before executing
point's avatar
point committed
145
 commands @arc{} computes the semantics of the node and then applies 
point's avatar
point committed
146
147
148
149
150
151
152
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
point's avatar
point committed
153
restrict these two sets e.g. counterexamples).
point's avatar
point committed
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183

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;
point's avatar
point committed
184
@item @var{CL} is the set of states where coins form columns or lines;
point's avatar
point committed
185
186
187
188
189
190
@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{}
point's avatar
point committed
191
192
formula. In our example properties are related to values of coins. When we have
to talk about the
point's avatar
point committed
193
194
values of variables one writes the corresponding Boolean expression between
square-brackets. For instance, winning states (the set @var{W}) are those for 
point's avatar
point committed
195
which all coins display the side 0 or all display the side 1; the corresponding
point's avatar
point committed
196
197
198
199
200
201
202
203
204
205
206
207
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];

point's avatar
point committed
208
209
210
211
 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];
point's avatar
point committed
212
213
214
215
216
217
218
219

 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}
point's avatar
point committed
220
@include Board.props
point's avatar
point committed
221
222
223
224
225
226
227
228
229
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.

point's avatar
point committed
230
The reader can notice that some properties that was not specified have been 
point's avatar
point committed
231
232
233
234
235
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}}
point's avatar
point committed
236
This graph shows that the game would have been modeled with only four
point's avatar
point committed
237
238
239
240
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.

point's avatar
point committed
241
242
243
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!}.
point's avatar
point committed
244
245
246

@section Computing the winning strategy

point's avatar
point committed
247
248
249
250
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.
point's avatar
point committed
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265

@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
point's avatar
point committed
266
(@code{Win}) and the name and type of each columns (here @code{s} of type 
point's avatar
point committed
267
268
@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 
point's avatar
point committed
269
270
271
272
273
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.
point's avatar
point committed
274
275
276
277
278
279
280
281
282
283
284

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

point's avatar
point committed
285
286
287
288
289
290
@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 
point's avatar
point committed
291
292
@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 
point's avatar
point committed
293
294
295
296
297
298
299
300
301
302
303
304
305
@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 
point's avatar
point committed
306
 [t : Board!c] (Board!t (s, e1, t) => WSeq@ind{k-1} (t, e2, @dots{}, e@ind{k}));
point's avatar
point committed
307
308
309
310
311
312
@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 
point's avatar
point committed
313
winning from all configurations:
point's avatar
point committed
314
315
@smallexample
S@ind{k}(e1 : Board!ev, @dots{}, e@ind{k} : Board!ev) := 
point's avatar
point committed
316
 [s : Board!c] WSeq@ind{k} (s, e1, @dots{}, e@ind{k});
point's avatar
point committed
317
318
@end smallexample

point's avatar
point committed
319
320
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}. 
point's avatar
point committed
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
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

point's avatar
point committed
339
The reader can use the @command{run} command (@xref{Graphical simulator}) to
point's avatar
point committed
340
try to win against the strategy given by the relation @var{S7} ...