libmonaa 0.5.2
Loading...
Searching...
No Matches
intermediate_zone.hh
1#pragma once
2
3#include <boost/variant.hpp>
4#include <iostream>
5
6#include "interval.hh"
7#include "zone.hh"
8
9class IntermediateZone : public Zone {
10private:
11 std::vector<bool> isAllocated;
12 static constexpr ClockVariables initialClock = 1;
13
14public:
15 ClockVariables newestClock;
16 // intervals]0]: t
17 // intervals]1]: t'
18 // intervals]2]: t' - t
19 // This is not an intervals but cells of DBMs
20 std::vector<Interval> intervals;
21 bool useInterval;
26 IntermediateZone(const Interval &interval)
27 : intervals({std::move(interval)}) {
28 useInterval = true;
29 intervals[0].lowerBound.first *= -1;
30 newestClock = 1;
31 }
32
39 IntermediateZone(Zone zone, std::size_t currentNewestClock = 0)
40 : Zone(std::move(zone)) {
41 useInterval = false;
42 // The zone must have at least one variable
43#ifdef DEBUG
44 assert(value.cols() == value.rows());
45 assert(value.cols() > 1);
46#endif
47 isAllocated.resize(value.cols(), false);
48 if (currentNewestClock) {
49 newestClock = currentNewestClock;
50 for (ClockVariables x = currentNewestClock + 1; x < value.cols(); x++) {
51 deallocate(x);
52 }
53 } else {
54 newestClock = value.cols() - 1;
55 }
56 isAllocated[0] = true;
57 isAllocated[initialClock] = true;
58 isAllocated[newestClock] = true;
59 }
60
62 ClockVariables alloc(const std::pair<double, bool> &upperBound,
63 const std::pair<double, bool> &lowerBound) {
64 static constexpr Bounds infinity =
65 Bounds(std::numeric_limits<double>::infinity(), false);
66 ClockVariables newClock;
67#define likely(x) __builtin_expect(!!(x), 1)
68#ifdef __GNUC__
69 if (likely(useInterval && intervals.size() == 1)) {
70#else
71 if (useInterval && intervals.size() == 1) {
72#endif
73 // use intervals
74 intervals.reserve(3);
75 intervals.emplace_back(std::move(lowerBound), std::move(upperBound));
76 // value(2, 1) <= value(2, 0) + value(0, 1)
77 // value(1, 2) <= value(1, 0) + value(0, 2)
78 intervals.emplace_back(
79 std::min(intervals[0].upperBound + intervals[1].lowerBound,
80 Bounds{0, true}),
81 intervals[1].upperBound + intervals[0].lowerBound);
82 return newestClock = 2;
83 } else if (useInterval) {
84 // convert intervals to a zone
85 useInterval = false;
86 isAllocated.resize(4, true);
87 value.resize(4, 4);
88 value.fill(Bounds(infinity));
89 for (int i = 0; i < 4; i++) {
90 value(i, i) = Bounds{0, true};
91 }
92 value(1, 0) = intervals[0].upperBound;
93 value(0, 1) = intervals[0].lowerBound;
94 value(2, 0) = intervals[1].upperBound;
95 value(0, 2) = intervals[1].lowerBound;
96 value(2, 1) = intervals[2].upperBound;
97 value(1, 2) = intervals[2].lowerBound;
98 value(2, 3) = Bounds{0, true};
99 value(3, 0) = std::move(upperBound);
100 value(0, 3) = std::move(lowerBound);
101 intervals.clear();
102 newClock = 3;
103 } else {
104 const auto newPos =
105 std::find(isAllocated.begin(), isAllocated.end(), false);
106#ifdef DEBUG
107 assert(value.cols() == value.rows());
108#endif
109
110 if (newPos != isAllocated.end()) {
111 // we do not have to alloc
112 newClock = newPos - isAllocated.begin();
113 } else {
114 // we have to alloc
116 // throw "monaa: Unexpected Variable Allocation";
118 value.conservativeResize(value.cols() + 1, value.cols() + 1);
119 newClock = value.cols() - 1;
120 isAllocated.resize(value.cols());
121 value.row(newClock).fill(infinity);
122 value.col(newClock).fill(infinity);
123 value(newClock, newClock) = Bounds(0, true);
124 }
125 isAllocated[newClock] = true;
126 value(newClock, 0) = std::move(upperBound);
127 value(0, newClock) = std::move(lowerBound);
128 value(newClock, newestClock) = Bounds(infinity);
129 value(newestClock, newClock) = {0, true};
130#ifdef DEBUG
131 assert(value.cols() == value.rows());
132#endif
133 }
134 for (int i = 0; i < value.rows(); i++) {
135 // for (int x = 0; x < value.cols(); x++) {
136 // value(i, newClock) = std::min(value(i, newClock), value(i, x) +
137 // value(x, newClock));
138 // }
139 value(i, newClock) =
140 std::min(value(i, newClock),
141 (value.row(i) + value.col(newClock).transpose()).minCoeff());
142 }
143 for (int x = 0; x < value.rows(); x++) {
144 for (int j = 0; j < value.cols(); j++) {
145 value(newClock, j) =
146 std::min(value(newClock, j), value(newClock, x) + value(x, j));
147 }
148 }
149 return newestClock = newClock;
150 }
151
152 void
153 update(const std::vector<boost::variant<double, ClockVariables>> &resetTime) {
154 if (useInterval) {
155 return;
156 }
157#ifdef DEBUG
158 assert(value.cols() == value.rows());
159#endif
160 std::fill(isAllocated.begin(), isAllocated.end(), false);
161 isAllocated[0] = true;
162 isAllocated[initialClock] = true;
163 isAllocated[newestClock] = true;
164 for (auto rtime : resetTime) {
165 const ClockVariables *p_x = boost::get<ClockVariables>(&rtime);
166 if (p_x) {
167 isAllocated[*p_x] = true;
168 }
169 }
170 for (ClockVariables x = 1; x < value.cols(); x++) {
171 if (!isAllocated[x]) {
172 deallocate(x);
173 }
174 }
175 }
176
177 void toAns(Zone &ansZone) const {
178 ansZone = Zone::zero(3);
179 if (useInterval) {
180 if (intervals.size() < 3) {
181 return;
182 }
183 ansZone.value(0, 1) = intervals[0].lowerBound;
184 ansZone.value(1, 0) = intervals[0].upperBound;
185 ansZone.value(0, 2) = intervals[1].lowerBound;
186 ansZone.value(2, 0) = intervals[1].upperBound;
187 ansZone.value(1, 2) = intervals[2].lowerBound;
188 ansZone.value(2, 1) = intervals[2].upperBound;
189 } else {
190 ansZone.value(0, 1) = value(0, 1);
191 ansZone.value(1, 0) = value(1, 0);
192 ansZone.value(0, 2) = value(0, newestClock);
193 ansZone.value(2, 0) = value(newestClock, 0);
194 ansZone.value(1, 2) = value(1, newestClock);
195 ansZone.value(2, 1) = value(newestClock, 1);
196 }
197 }
198
204 void tighten(const ClockVariables x, const ClockVariables y, Bounds c) {
205 if (useInterval) {
206 if (x == 0 && y == 1) {
207 intervals[0].lowerBound = std::min(intervals[0].lowerBound, c);
208 if (intervals.size() > 1) {
209 // value(0, 2) <= value(0, 1) + value(1, 2)
210 intervals[1].lowerBound =
211 std::min(intervals[1].lowerBound,
212 intervals[0].lowerBound + intervals[2].lowerBound);
213 // value(2, 1) <= value(2, 0) + value(0, 1)
214 intervals[2].upperBound =
215 std::min(intervals[2].upperBound,
216 intervals[1].upperBound + intervals[0].lowerBound);
217 }
218 } else if (x == 1 && y == 0) {
219 intervals[0].upperBound = std::min(intervals[0].upperBound, c);
220 if (intervals.size() > 1) {
221 // value(2, 0) <= value(2, 1) + value(1, 0)
222 intervals[1].upperBound =
223 std::min(intervals[1].upperBound,
224 intervals[2].upperBound + intervals[0].upperBound);
225 // value(1, 2) <= value(1, 0) + value(0, 2)
226 intervals[2].lowerBound =
227 std::min(intervals[2].lowerBound,
228 intervals[0].upperBound + intervals[1].lowerBound);
229 }
230 } else if (x == 0 && y == 2) {
231 intervals[1].lowerBound = std::min(intervals[1].lowerBound, c);
232 intervals[0].lowerBound =
233 std::min(intervals[0].lowerBound,
234 intervals[1].lowerBound + intervals[2].upperBound);
235 intervals[2].lowerBound =
236 std::min(intervals[2].lowerBound,
237 intervals[1].lowerBound + intervals[0].upperBound);
238 } else if (x == 2 && y == 0) {
239 intervals[1].upperBound = std::min(intervals[1].upperBound, c);
240 intervals[0].upperBound =
241 std::min(intervals[0].upperBound,
242 intervals[1].upperBound + intervals[2].lowerBound);
243 intervals[2].upperBound =
244 std::min(intervals[2].upperBound,
245 intervals[1].upperBound + intervals[0].lowerBound);
246 } else if (x == 1 && y == 2) {
247 intervals[2].lowerBound = std::min(intervals[2].lowerBound, c);
248 intervals[0].upperBound =
249 std::min(intervals[0].upperBound,
250 intervals[1].upperBound + intervals[2].lowerBound);
251 intervals[1].lowerBound =
252 std::min(intervals[1].lowerBound,
253 intervals[2].lowerBound + intervals[0].lowerBound);
254 } else if (x == 2 && y == 1) {
255 intervals[2].upperBound = std::min(intervals[2].upperBound, c);
256 intervals[1].upperBound =
257 std::min(intervals[1].upperBound,
258 intervals[2].upperBound + intervals[0].upperBound);
259 intervals[0].lowerBound =
260 std::min(intervals[0].lowerBound,
261 intervals[1].lowerBound + intervals[2].upperBound);
262 }
263 } else {
264 value(x, y) = std::min(value(x, y), c);
265 if (value(x, y) == c && newestClock != initialClock) {
266 close1(x);
267 close1(y);
268 }
269 }
270 }
271
272 void tighten(const ClockVariables x, const Constraint &c,
273 const ClockVariables reset = 0) {
274 switch (c.odr) {
275 case Constraint::Order::lt:
276 tighten(x, reset, Bounds{c.c, false});
277 break;
278 case Constraint::Order::le:
279 tighten(x, reset, Bounds{c.c, true});
280 break;
281 case Constraint::Order::gt:
282 tighten(reset, x, Bounds{-c.c, false});
283 break;
284 case Constraint::Order::ge:
285 tighten(reset, x, Bounds{-c.c, true});
286 break;
287 }
288 }
289
290 void tighten(const ClockVariables x, const Constraint &c, const double t) {
291 switch (c.odr) {
292 case Constraint::Order::lt:
293 tighten(x, 0, Bounds{c.c + t, false});
294 break;
295 case Constraint::Order::le:
296 tighten(x, 0, Bounds{c.c + t, true});
297 break;
298 case Constraint::Order::gt:
299 tighten(0, x, Bounds{-c.c - t, false});
300 break;
301 case Constraint::Order::ge:
302 tighten(0, x, Bounds{-c.c - t, true});
303 break;
304 }
305 }
306
307 void tighten(
308 const std::vector<Constraint> &constraints,
309 const std::vector<boost::variant<double, ClockVariables>> &resetTime) {
310 for (const Constraint &guard : constraints) {
311 const double *p_resetDouble = boost::get<double>(&resetTime[guard.x]);
312 const ClockVariables *p_resetClock =
313 boost::get<ClockVariables>(&resetTime[guard.x]);
314 if (p_resetDouble) {
315 tighten(newestClock, guard, *p_resetDouble);
316 } else {
317 tighten(newestClock, guard, *p_resetClock);
318 }
319 }
320 }
321
322 void
323 tighten(const std::vector<Constraint> &constraints,
324 const std::vector<boost::variant<double, ClockVariables>> &resetTime,
325 const double t) {
326 for (const Constraint &guard : constraints) {
327 const double *p_resetDouble = boost::get<double>(&resetTime[guard.x]);
328 const ClockVariables *p_resetClock =
329 boost::get<ClockVariables>(&resetTime[guard.x]);
330 if (p_resetDouble) {
331 // This constraint is unsatisfyable
332 if (!guard.satisfy(t - *p_resetDouble)) {
333 if (useInterval) {
334 static constexpr Bounds negInfinity =
335 Bounds(-std::numeric_limits<double>::infinity(), false);
336 intervals[0].lowerBound = negInfinity;
337 } else {
338 makeUnsat();
339 }
340 }
341 } else {
342 switch (guard.odr) {
343 case Constraint::Order::lt:
344 tighten(0, *p_resetClock, Bounds{guard.c - t, false});
345 break;
346 case Constraint::Order::le:
347 tighten(0, *p_resetClock, Bounds{guard.c - t, true});
348 break;
349 case Constraint::Order::gt:
350 tighten(*p_resetClock, 0, Bounds{t - guard.c, false});
351 break;
352 case Constraint::Order::ge:
353 tighten(*p_resetClock, 0, Bounds{t - guard.c, true});
354 break;
355 }
356 }
357 }
358 }
359
360 bool isSatisfiableCanonized() {
361 if (useInterval) {
362 return std::all_of(intervals.begin(), intervals.end(),
363 [](const Interval &interval) {
364 return interval.upperBound + interval.lowerBound >=
365 Bounds(0.0, true);
366 });
367 } else {
368 return (value + value.transpose()).minCoeff() >= Bounds(0.0, true);
369 }
370 }
371
372 void deallocate(const ClockVariables x) {
373 static constexpr Bounds infinity =
374 Bounds(std::numeric_limits<double>::infinity(), false);
375 static constexpr Bounds zero = Bounds(0, true);
376 value.col(x).fill(infinity);
377 value.row(x).fill(infinity);
378 value(x, x) = zero;
379 }
380};
IntermediateZone
Definition intermediate_zone.hh:9
IntermediateZone::alloc
ClockVariables alloc(const std::pair< double, bool > &upperBound, const std::pair< double, bool > &lowerBound)
Definition intermediate_zone.hh:62
IntermediateZone::tighten
void tighten(const ClockVariables x, const ClockVariables y, Bounds c)
add the constraint x - y \le (c,s)
Definition intermediate_zone.hh:204
IntermediateZone::IntermediateZone
IntermediateZone(Zone zone, std::size_t currentNewestClock=0)
construct an intermediate zone from a zone
Definition intermediate_zone.hh:39
IntermediateZone::IntermediateZone
IntermediateZone(const Interval &interval)
construct an intermediate zone from an interval
Definition intermediate_zone.hh:26
interval.hh
The implementation of the class Interval and related functions.
Constraint
A constraint in a guard of transitions.
Definition constraint.hh:16
Interval
Class for an interval.
Definition interval.hh:15
Zone
Implementation of a zone with DBM.
Definition zone.hh:43
Zone::makeUnsat
void makeUnsat()
make the zone unsatisfiable
Definition zone.hh:169
Generated by doxygen 1.9.8