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
|
class LEVEL
creation make
feature
count: INTEGER
-- Total count of occupied places.
free_count: INTEGER is
do
Result := park.count - count
end
capacity : INTEGER is
do
Result := count + free_count
end
full: BOOLEAN is
do
Result := count = capacity
end
feature -- Modifications:
make(max_cars: INTEGER) is
require
max_cars > 0
do
!!park.make(1,max_cars)
!!tickets.make(park.lower,park.upper)
count := 0
ensure
count = 0
end
arrival(car: INTEGER; arrival_time: DATE) is
require
not full
car > 0
local
i: INTEGER; stop: BOOLEAN; ticket: TICKET
do
from
i := park.lower
stop := false
until
stop
loop
if park.item(i) <= 0 then
stop := true
park.put(car,i)
!!ticket.make(arrival_time)
tickets.put(ticket,i)
count := count + 1
end
i := i + 1
end
ensure
count >= old count + 1
end
departure(car: INTEGER; departure_time: DATE; hour_price: REAL): REAL is
-- Gives price to pay or -1 when car is not at this level.
require
car > 0
local
i: INTEGER
do
i := park.index_of(car)
if i > park.upper then
Result := -1
else
Result := tickets.item(i).price(departure_time,hour_price)
tickets.put(Void,i)
park.put(0,i)
count := count - 1
end
end
feature {NONE}
park: ARRAY[INTEGER]
tickets: ARRAY[TICKET]
invariant
count >= 0
free_count >= 0
capacity = count + free_count
capacity >= 1
tickets.count = park.count
end -- LEVEL
|
