1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
class PARKING
creation make
feature
lower_level: INTEGER is
do
Result := level_list.lower
end
upper_level: INTEGER is
do
Result := level_list.upper
end
hour_price: REAL
default_hour_price: REAL is 1.50
count: INTEGER is
local
i: INTEGER
do
from
i := lower_level
until
i > upper_level
loop
Result := Result + level_count(i)
i := i + 1
end
end
clock: DATE
level_count(number: INTEGER): INTEGER is
require
number <= upper_level
lower_level <= number
do
Result := level_list.item(number).count
ensure
Result >= 0
end
feature -- Modifications:
make(ll: like level_list) is
require
ll /= Void
do
!!clock.make(0,360)
hour_price := default_hour_price
level_list := ll
last_car := 0
ensure
hour_price = default_hour_price
level_list = ll
last_car = 0
end
arrival: INTEGER is
-- Gives 0 when no more place.
local
i: INTEGER
do
from
i := lower_level
until
(i > upper_level) or else
(not level_list.item(i).full)
loop
i := i + 1
end
if (i > upper_level) or else
(level_list.item(i).full)
then
Result := 0
else
last_car := last_car + 1
level_list.item(i).arrival(last_car,clock.twin)
Result := last_car
end
ensure
Result >= 0
end
departure(car: INTEGER): REAL is
-- Gives the price to pay or -1 when car has already leaved.
require
car > 0
local
i: INTEGER; stop: BOOLEAN; c: like clock
do
from
i := lower_level
stop := level_list.count <= 0
Result := -1
c := clock.twin
until
stop
loop
Result := level_list.item(i).departure(car,c,hour_price)
i := i + 1
stop := (Result >= 0) or (i > upper_level)
end
end
add_time(incr: INTEGER) is
do
clock.add_time(incr)
end
set_hour_price(hp: REAL) is
require
hp >= 0
do
hour_price := hp
ensure
hour_price = hp
end
feature {NONE}
level_list: ARRAY[LEVEL]
last_car: INTEGER
invariant
valid_price: hour_price >= 0
clock /= Void
last_car >= 0
level_list /= Void
end -- PARKING
|
