16 Jun
2006
16 Jun
'06
3:09 p.m.
Benoît, ça :
for i from 0 to 1200 step 100 do
P=? [ true U (t <= i & (sensor[0][0]= 4 | sensor[0][1]= 4 | sensor[0][2]= 4
| sensor[0][3]= 4 | sensor[0][4]= 4 | sensor[0][5]= 4 | sensor[0][6]= 4 |
sensor[0][7]= 4 | sensor[0][8]= 4 | sensor[0][9]= 4 | sensor[9][0] = 4 |
sensor[9][1] = 4 | sensor[9][2] = 4 | sensor[9][3] = 4 | sensor[9][4] = 4 |
sensor[9][5] = 4 | sensor[9][6] = 4 | sensor[9][7] = 4 | sensor[9][8] = 4 |
sensor[9][9] = 4 | sensor[1][0] = 4 | sensor[2][0] = 4 | sensor[3][0] = 4 |
sensor[4][0] = 4 | sensor[5][0] = 4 | sensor[6][0] = 4 | sensor[7][0] = 4 |
sensor[8][0] = 4 | sensor[1][9] = 4 | sensor[2][9] = 4 | sensor[3][9] = 4 |
sensor[4][9] = 4 | sensor[5][9] = 4 | sensor[6][9] = 4 | sensor[7][9] = 4 |
sensor[8][9] = 4)) ]
end
c'est pas bon du tout. Il faut que tu me trouve un moyen de sucrer
cette horreur.
Est-ce que tu crois que tu saurais compiler ça par exemple :
formula north_receives =
for x = 0 .. X - 1 do
if sensor[x][0] = BROADCAST then return true end if
else
return false
(oui, le else est sur la boucle).
On peut-être faut-il faire une récursion ?
formula north_receives = line_receives (0, 0);
formula line_receives (int x, int y) =
x = X ? false : sensor[x][y] | line_receives (x + 1, y);
?
Je ne suis pas sur de vouloir écrire
formula north_receives = sensor[0..X-1][0] = BROADCAST;
C'est assez trompeur : ça semble vouloir que tous doivent être à BROADCAST.