libmonaa 0.5.2
Loading...
Searching...
No Matches
monaa.hh
Go to the documentation of this file.
1#pragma once
26#include <boost/variant.hpp>
27#include <chrono>
28#include <climits>
29#include <cmath>
30#include <iostream>
31#include <unordered_set>
32
33#include "ans_vec.hh"
34#include "intermediate_zone.hh"
35#include "intersection.hh"
36#include "kmp_skip_value.hh"
37#include "sunday_skip_value.hh"
38#include "ta2za.hh"
39#include "word_container.hh"
40
41#include "utils.hh"
64// Internal state of BFS
65struct InternalState {
66 const TAState *s;
67 // C -> (R or Z)
68 std::vector<boost::variant<double, ClockVariables>> resetTime;
69 IntermediateZone z;
70 InternalState(
71 const TAState *s,
72 const std::vector<boost::variant<double, ClockVariables>> &resetTime,
73 const IntermediateZone &z)
74 : s(std::move(s)), resetTime(std::move(resetTime)), z(std::move(z)) {}
75 InternalState(const std::size_t numOfVar, const TAState *s,
76 const Interval &interval)
77 : s(std::move(s)), z(std::move(interval)) {
78 static const std::vector<boost::variant<double, ClockVariables>>
79 zeroResetTime(numOfVar, ClockVariables(1));
80 // Every clock variables are reset at t1 ( = t)
81 resetTime = zeroResetTime;
82 }
83};
84
85struct IntervalInternalState {
86 using Variables = char;
87 const TAState *s;
88 std::vector<double> resetTime;
89 std::pair<double, bool> upperConstraint;
90 std::pair<double, bool> lowerConstraint;
91 IntervalInternalState(const TAState *s, const std::vector<double> &resetTime,
92 const std::pair<double, bool> &upperConstraint,
93 const std::pair<double, bool> &lowerConstraint)
94 : s(std::move(s)), resetTime(std::move(resetTime)),
95 upperConstraint(std::move(upperConstraint)),
96 lowerConstraint(std::move(lowerConstraint)) {}
97};
98
100inline bool isValidConstraint(const Bounds &upperConstraint,
101 const Bounds &lowerConstraint) {
102 return upperConstraint + lowerConstraint >= Bounds{0.0, true};
103}
104
108inline void updateConstraint(std::pair<double, bool> &upperConstraint,
109 std::pair<double, bool> &lowerConstraint,
110 const Constraint &delta,
111 const double comparedValue) {
112 switch (delta.odr) {
113 case Constraint::Order::gt:
114 if (lowerConstraint.first < comparedValue) {
115 lowerConstraint.first = comparedValue;
116 lowerConstraint.second = 0;
117 } else if (lowerConstraint.first == comparedValue) {
118 lowerConstraint.second = 0;
119 }
120 break;
121 case Constraint::Order::ge:
122 if (lowerConstraint.first < comparedValue) {
123 lowerConstraint.first = comparedValue;
124 lowerConstraint.second = 1;
125 }
126 break;
127 case Constraint::Order::lt:
128 if (upperConstraint.first > comparedValue) {
129 upperConstraint.first = comparedValue;
130 upperConstraint.second = 0;
131 } else if (upperConstraint.first == comparedValue) {
132 upperConstraint.second = 0;
133 }
134 break;
135 case Constraint::Order::le:
136 if (upperConstraint.first > comparedValue) {
137 upperConstraint.first = comparedValue;
138 upperConstraint.second = 1;
139 }
140 break;
141 }
142}
143
150template <class InputContainer, class OutputContainer>
151void monaa(WordContainer<InputContainer> word, TimedAutomaton A,
152 AnsContainer<OutputContainer> &ans) {
153 // Sunday's Skip value
154 // Char -> Skip Value
155 const SundaySkipValue delta = SundaySkipValue(A);
156 const int m = delta.getM();
157 std::unordered_set<Alphabet> endChars;
158 delta.getEndChars(endChars);
159
160 // KMP-Type Skip value
161 // A.State -> SkipValue
162 const KMPSkipValue beta(A, m);
163
164 // main computation
165 if (std::all_of(A.states.begin(), A.states.end(),
166 [](std::shared_ptr<TAState> s) {
167 return s->next.find(0) == s->next.end();
168 })) {
169 // When there is no epsilon transition
170 // auto start = std::chrono::system_clock::now();
171
172 std::size_t i = 0;
173 std::vector<std::pair<std::pair<double, bool>, std::pair<double, bool>>>
174 init;
175 std::vector<IntervalInternalState> CStates;
176 std::vector<IntervalInternalState> LastStates;
177 const Bounds zeroBounds = {0, true};
178
179 // When there can be immidiate accepting
180 // @todo This optimization is not yet when we have epsilon transitions
181#if 0
182 if (m == 1) {
183 for (const auto initState: A.initialStates) {
184 for (char c = 0; c < CHAR_MAX; c++) {
185 for (const auto &edge: initState->next[c]) {
186 if (edge.target.lock()->isMatch) {
187 // solve delta
188 IntermediateZone zone = Zone::zero(2);
189 for (const auto &constraint: edge.guard) {
190 zone.tighten(1, constraint);
191 }
192 if (zone.isSatisfiableCanonized()) {
193 init[c].push_back(std::move(zone));
194 }
195 }
196 }
197 }
198 }
199 }
200#endif
201
202 ans.clear();
203 std::size_t j;
204 while (word.fetch(i + m - 1)) {
205 bool tooLarge = false;
206 // Sunday Shift
207#if 0
208 if (m == 1 && init[word[i].first].size() > 0) {
209 // When there can be immidiate accepting
210 // @todo This optimization is not yet
211 ans.reserve(ans.size() + init[word[i].first].size());
212 if (i <= 0) {
213 for (auto zone: init[word[i].first]) {
214 Zone ansZone;
215 zone.value.col(0).fill({word[i].second, false});
216 if (zone.isSatisfiableCanonized()) {
217 zone.toAns(ansZone);
218 ans.push_back(std::move(ansZone));
219 }
220 }
221 } else {
222 for (auto zone: init[word[i].first]) {
223 Zone ansZone;
224 zone.value.col(0).fill({word[i].second, false});
225 zone.value.row(0).fill({-word[i-1].second, true});
226 if (zone.isSatisfiableCanonized()) {
227 zone.toAns(ansZone);
228 ans.push_back(std::move(ansZone));
229 }
230 }
231 }
232 } else
233#endif
234 if (m > 1 && word.fetch(i + m - 1)) {
235 while (endChars.find(word[i + m - 1].first) == endChars.end()) {
236 if (!word.fetch(i + m)) {
237 tooLarge = true;
238 break;
239 }
240 // increment i
241 i += delta[word[i + m].first];
242 word.setFront(i - 1);
243 if (!word.fetch(i + m - 1)) {
244 tooLarge = true;
245 break;
246 }
247 }
248 }
249
250 if (tooLarge)
251 break;
252
253 // KMP like Matching
254 CStates.clear();
255 CStates.reserve(A.initialStates.size());
256 std::vector<double> zeroResetTime(A.clockSize(), 0);
257 if (word.fetch(i)) {
258 IntervalInternalState istate = {
259 nullptr,
260 zeroResetTime,
261 {word[i].second, false},
262 ((i <= 0) ? zeroBounds : Bounds{-word[i - 1].second, true})};
263
264 CStates.resize(A.initialStates.size(), istate);
265 for (std::size_t k = 0; k < A.initialStates.size(); k++) {
266 CStates[k].s = A.initialStates[k].get();
267 }
268 } else {
269 break;
270 }
271 j = i;
272 while (!CStates.empty() && word.fetch(j)) {
273 const Alphabet c = word[j].first;
274 const double t = word[j].second;
275
276 // try to go to an accepting state
277 for (const auto &config : CStates) {
278 const TAState *s = config.s;
279 auto it = s->next.find(c);
280 if (it == s->next.end()) {
281 continue;
282 }
283 for (const auto &edge : it->second) {
284 auto target = edge.target;
285 if (!target || !target->isMatch) {
286 continue;
287 }
288 Bounds upperBeginConstraint = config.upperConstraint;
289 Bounds lowerBeginConstraint = config.lowerConstraint;
290 Bounds upperEndConstraint = {word[j].second, true};
291 Bounds lowerEndConstraint =
292 ((j > 0) ? Bounds{-word[j - 1].second, false} : zeroBounds);
293
294 // value(2, 1) <= value(2, 0) + value(0, 1)
295 Bounds upperDeltaConstraint =
296 upperEndConstraint + lowerBeginConstraint;
297 // value(1, 2) <= value(1, 0) + value(0, 2)
298 Bounds lowerDeltaConstraint =
299 std::min(lowerEndConstraint + upperBeginConstraint, zeroBounds);
300
301 auto tmpResetTime = config.resetTime;
302 // solve delta
303 for (const auto &delta : edge.guard) {
304 if (tmpResetTime[delta.x]) {
305 switch (delta.odr) {
306 case Constraint::Order::lt:
307 case Constraint::Order::le:
308 upperEndConstraint =
309 std::min(upperEndConstraint,
310 Bounds{delta.c + tmpResetTime[delta.x],
311 {delta.odr == Constraint::Order::le}});
312 // (2, 1) <= (2, 0) + (0, 1)
313 upperDeltaConstraint =
314 std::min(upperDeltaConstraint,
315 upperEndConstraint + lowerBeginConstraint);
316 // (1, 0) <= (1, 2) + (2, 0)
317 upperBeginConstraint =
318 std::min(upperBeginConstraint,
319 lowerDeltaConstraint + upperEndConstraint);
320 break;
321 case Constraint::Order::gt:
322 case Constraint::Order::ge:
323 lowerEndConstraint =
324 std::min(lowerEndConstraint,
325 Bounds{-delta.c - tmpResetTime[delta.x],
326 {delta.odr == Constraint::Order::ge}});
327 // (1, 2) <= (1, 0) + (0, 2)
328 lowerDeltaConstraint =
329 std::min(lowerDeltaConstraint,
330 upperBeginConstraint + lowerEndConstraint);
331 // (0, 1) <= (0, 2) + (2, 1)
332 lowerBeginConstraint =
333 std::min(lowerBeginConstraint,
334 lowerEndConstraint + upperDeltaConstraint);
335 break;
336 }
337 } else {
338 switch (delta.odr) {
339 case Constraint::Order::lt:
340 case Constraint::Order::le:
341 upperDeltaConstraint = std::min(
342 upperDeltaConstraint,
343 Bounds{static_cast<double>(delta.c), {delta.odr == Constraint::Order::le}});
344 // (2, 0) <= (2, 1) + (1, 0)
345 upperEndConstraint =
346 std::min(upperEndConstraint,
347 upperDeltaConstraint + upperBeginConstraint);
348 // (0, 1) <= (0, 2) + (2, 1)
349 lowerBeginConstraint =
350 std::min(lowerBeginConstraint,
351 lowerEndConstraint + upperDeltaConstraint);
352 break;
353 case Constraint::Order::gt:
354 case Constraint::Order::ge:
355 lowerDeltaConstraint = std::min(
356 lowerDeltaConstraint,
357 Bounds{static_cast<double>(-delta.c), {delta.odr == Constraint::Order::ge}});
358 // (1, 0) <= (1, 2) + (2, 0)
359 upperBeginConstraint =
360 std::min(upperBeginConstraint,
361 lowerDeltaConstraint + upperEndConstraint);
362 // (0, 2) <= (0, 1) + (1, 2)
363 lowerEndConstraint =
364 std::min(lowerEndConstraint,
365 lowerBeginConstraint + lowerDeltaConstraint);
366 break;
367 }
368 }
369 }
370
371 if (!isValidConstraint(upperBeginConstraint,
372 lowerBeginConstraint) ||
373 !isValidConstraint(upperEndConstraint, lowerEndConstraint) ||
374 !isValidConstraint(upperDeltaConstraint,
375 lowerDeltaConstraint)) {
376 continue;
377 }
378
379 Zone ansZone = Zone::zero(3);
380 ansZone.value(0, 1) = std::move(lowerBeginConstraint);
381 ansZone.value(1, 0) = std::move(upperBeginConstraint);
382 ansZone.value(0, 2) = std::move(lowerEndConstraint);
383 ansZone.value(2, 0) = std::move(upperEndConstraint);
384 ansZone.value(1, 2) = std::move(lowerDeltaConstraint);
385 ansZone.value(2, 1) = std::move(upperDeltaConstraint);
386
387 ans.push_back(std::move(ansZone));
388 }
389 }
390
391 // try observable transitios (usual)
392 LastStates = std::move(CStates);
393 for (const auto &config : LastStates) {
394 const TAState *s = config.s;
395 auto it = s->next.find(c);
396 if (it == s->next.end()) {
397 continue;
398 }
399 for (auto &edge : it->second) {
400 const auto target = edge.target;
401 if (!target) {
402 continue;
403 }
404
405 Bounds upperBeginConstraint = config.upperConstraint;
406 Bounds lowerBeginConstraint = config.lowerConstraint;
407 bool transitable = true;
408
409 for (const auto &delta : edge.guard) {
410 if (config.resetTime[delta.x]) {
411 if (!delta.satisfy(t - config.resetTime[delta.x])) {
412 transitable = false;
413 break;
414 }
415 } else {
416 switch (delta.odr) {
417 case Constraint::Order::lt:
418 case Constraint::Order::le:
419 lowerBeginConstraint =
420 std::min(lowerBeginConstraint,
421 Bounds{delta.c - t,
422 {delta.odr == Constraint::Order::le}});
423 break;
424 case Constraint::Order::gt:
425 case Constraint::Order::ge:
426 upperBeginConstraint =
427 std::min(upperBeginConstraint,
428 Bounds{t - delta.c,
429 {delta.odr == Constraint::Order::ge}});
430 break;
431 }
432 }
433 }
434
435 if (!transitable || !isValidConstraint(upperBeginConstraint,
436 lowerBeginConstraint)) {
437 continue;
438 }
439
440 auto tmpResetTime = config.resetTime;
441 for (auto i : edge.resetVars) {
442 tmpResetTime[i] = t;
443 }
444
445 CStates.emplace_back(edge.target, std::move(tmpResetTime),
446 std::move(upperBeginConstraint),
447 std::move(lowerBeginConstraint));
448 }
449 }
450 j++;
451 }
452 if (!word.fetch(j)) {
453 LastStates = std::move(CStates);
454 }
455 // KMP like skip value
456 int greatestN = 1;
457 for (const IntervalInternalState &istate : LastStates) {
458 greatestN = std::max(beta[istate.s], greatestN);
459 }
460 // increment i
461 i += greatestN;
462 word.setFront(i - 1);
463 }
464
465 // auto end = std::chrono::system_clock::now();
466 // auto dur = end - start;
467 // auto nsec =
468 // std::chrono::duration_cast<std::chrono::nanoseconds>(dur).count();
469 // std::cout << "main computation: " << nsec / 1000000.0 << " ms" <<
470 // std::endl;
471 } else {
472 // When there are some epsilon transitions
473 // auto start = std::chrono::system_clock::now();
474
475 std::size_t i = 0;
476 std::array<std::vector<IntermediateZone>, CHAR_MAX> init;
477 std::vector<InternalState> CStates;
478 std::vector<InternalState> LastStates;
479
480 // When there can be immidiate accepting
481 // @todo This optimization is not yet when we have epsilon transitions
482#if 0
483 if (m == 1) {
484 for (const auto initState: A.initialStates) {
485 for (char c = 0; c < CHAR_MAX; c++) {
486 for (const auto &edge: initState->next[c]) {
487 if (edge.target.lock()->isMatch) {
488 // solve delta
489 IntermediateZone zone = Zone::zero(2);
490 for (const auto &constraint: edge.guard) {
491 zone.tighten(1, constraint);
492 }
493 if (zone.isSatisfiableCanonized()) {
494 init[c].push_back(std::move(zone));
495 }
496 }
497 }
498 }
499 }
500 }
501#endif
502
503 ans.clear();
504 std::size_t j;
505 while (word.fetch(i + m - 1)) {
506 bool tooLarge = false;
507 // Sunday Shift
508#if 0
509 if (m == 1 && init[word[i].first].size() > 0) {
510 // When there can be immidiate accepting
511 // @todo This optimization is not yet
512 ans.reserve(ans.size() + init[word[i].first].size());
513 if (i <= 0) {
514 for (auto zone: init[word[i].first]) {
515 Zone ansZone;
516 zone.value.col(0).fill({word[i].second, false});
517 if (zone.isSatisfiableCanonized()) {
518 zone.toAns(ansZone);
519 ans.push_back(std::move(ansZone));
520 }
521 }
522 } else {
523 for (auto zone: init[word[i].first]) {
524 Zone ansZone;
525 zone.value.col(0).fill({word[i].second, false});
526 zone.value.row(0).fill({-word[i-1].second, true});
527 if (zone.isSatisfiableCanonized()) {
528 zone.toAns(ansZone);
529 ans.push_back(std::move(ansZone));
530 }
531 }
532 }
533 } else
534#endif
535 if (m > 1 && word.fetch(i + m - 1)) {
536 while (endChars.find(word[i + m - 1].first) == endChars.end()) {
537 if (!word.fetch(i + m)) {
538 tooLarge = true;
539 break;
540 }
541 // increment i
542 i += delta[word[i + m].first];
543 word.setFront(i - 1);
544 if (!word.fetch(i + m - 1)) {
545 tooLarge = true;
546 break;
547 }
548 }
549 }
550
551 if (tooLarge)
552 break;
553
554 // KMP like Matching
555 CStates.clear();
556 if (word.fetch(i)) {
557 InternalState istate = {
558 A.clockSize(), nullptr,
559 Interval{
560 ((i <= 0) ? Bounds{0, true} : Bounds{word[i - 1].second, true}),
561 {word[i].second, false}}};
562 CStates.resize(A.initialStates.size(), istate);
563 for (std::size_t k = 0; k < A.initialStates.size(); k++) {
564 CStates[k].s = A.initialStates[k].get();
565 }
566 } else {
567 break;
568 }
569 j = i;
570 while (!CStates.empty() && word.fetch(j)) {
571 // try unobservable transitions
572
573 // Correct the states have epsilon transitions
574 std::vector<InternalState> CurrEpsilonConf;
575 CurrEpsilonConf.reserve(CStates.size());
576 for (auto &istate : CStates) {
577 auto it = istate.s->next.find(0);
578 if (it != istate.s->next.end()) {
579 CurrEpsilonConf.push_back(istate);
580 }
581 }
582 while (!CurrEpsilonConf.empty()) {
583 std::vector<InternalState> PrevEpsilonConf =
584 std::move(CurrEpsilonConf);
585 CurrEpsilonConf.clear();
586 for (const auto &econfig : PrevEpsilonConf) {
587 auto it = econfig.s->next.find(0);
588 if (it == econfig.s->next.end()) {
589 continue;
590 }
591 for (const auto &edge : it->second) {
592 auto target = edge.target;
593 if (!target) {
594 continue;
595 }
596 IntermediateZone tmpZ = econfig.z;
597 ClockVariables newClock = 0;
598 tmpZ.alloc({word[j].second, true},
599 ((j > 0) ? Bounds{-word[j - 1].second, false}
600 : Bounds{0, true}));
601 tmpZ.tighten(edge.guard, econfig.resetTime);
602 if (tmpZ.isSatisfiableCanonized()) {
603 auto tmpResetTime = econfig.resetTime;
604 for (ClockVariables x : edge.resetVars) {
605 tmpResetTime[x] = newClock;
606 }
607 tmpZ.update(tmpResetTime);
608 CurrEpsilonConf.emplace_back(target, tmpResetTime, tmpZ);
609 }
610 }
611 }
612 CStates.insert(CStates.end(), CurrEpsilonConf.begin(),
613 CurrEpsilonConf.end());
614 }
615
616 const Alphabet c = word[j].first;
617 const double t = word[j].second;
618
619 // try to go to an accepting state
620 for (const auto &config : CStates) {
621 const TAState *s = config.s;
622 auto it = s->next.find(c);
623 if (it == s->next.end()) {
624 continue;
625 }
626 for (const auto &edge : it->second) {
627 auto target = edge.target;
628 if (!target || !target->isMatch) {
629 continue;
630 }
631 IntermediateZone tmpZ = config.z;
632 tmpZ.alloc({word[j].second, true},
633 ((j > 0) ? Bounds{-word[j - 1].second, false}
634 : Bounds{0, true}));
635 tmpZ.tighten(edge.guard, config.resetTime);
636 if (tmpZ.isSatisfiableCanonized()) {
637 Zone ansZone;
638 tmpZ.toAns(ansZone);
639 ans.push_back(std::move(ansZone));
640 }
641 }
642 }
643
644 // try observable transitios (usual)
645 LastStates = std::move(CStates);
646 for (const auto &config : LastStates) {
647 const TAState *s = config.s;
648 auto it = s->next.find(c);
649 if (it == s->next.end()) {
650 continue;
651 }
652 for (const auto &edge : it->second) {
653 auto target = edge.target;
654 if (!target) {
655 continue;
656 }
657 IntermediateZone tmpZ = config.z;
658 tmpZ.tighten(edge.guard, config.resetTime, t);
659 if (tmpZ.isSatisfiableCanonized()) {
660 auto tmpResetTime = config.resetTime;
661 for (ClockVariables x : edge.resetVars) {
662 tmpResetTime[x] = t;
663 }
664 tmpZ.update(tmpResetTime);
665 CStates.emplace_back(target, std::move(tmpResetTime),
666 std::move(tmpZ));
667 }
668 }
669 }
670 j++;
671 }
672 if (!word.fetch(j)) {
673 LastStates = std::move(CStates);
674 }
675 // KMP like skip value
676 int greatestN = 1;
677 for (const InternalState &istate : LastStates) {
678 greatestN = std::max(beta[istate.s], greatestN);
679 }
680 // increment i
681 i += greatestN;
682 word.setFront(i - 1);
683 }
684
685 // auto end = std::chrono::system_clock::now();
686 // auto dur = end - start;
687 // auto nsec =
688 // std::chrono::duration_cast<std::chrono::nanoseconds>(dur).count();
689 // std::cout << "main computation: " << nsec / 1000000.0 << " ms" <<
690 // std::endl;
691 }
692}
693
701template <class InputContainer, class OutputContainer>
702void monaaDollar(WordContainer<InputContainer> word, TimedAutomaton A,
703 AnsContainer<OutputContainer> &ans) {
704 TimedAutomaton Ap;
705 Ap.states.reserve(A.states.size());
706 Ap.initialStates.reserve(A.initialStates.size());
707 Ap.maxConstraints = A.maxConstraints;
708 std::unordered_map<const TAState *, std::shared_ptr<TAState>> ptrConv;
709 for (std::shared_ptr<TAState> s : A.states) {
710 ptrConv[s.get()] = std::make_shared<TAState>(*s);
711 Ap.states.push_back(ptrConv.at(s.get()));
712 if (std::binary_search(A.initialStates.begin(), A.initialStates.end(), s)) {
713 Ap.initialStates.push_back(ptrConv.at(s.get()));
714 }
715 }
716
717 for (std::shared_ptr<TAState> s : Ap.states) {
718 if (s->next.find('$') != s->next.end()) {
719 s->isMatch = true;
720 s->next['$'].clear();
721 s->next.erase('$');
722 }
723 for (auto &transitionsPair : s->next) {
724 for (auto &transition : transitionsPair.second) {
725 transition.target = ptrConv.at(transition.target).get();
726 }
727 }
728 }
729
730 // Sunday's Skip value
731 // Char -> Skip Value
732 const SundaySkipValue delta = SundaySkipValue(Ap);
733 const int m = delta.getM();
734 std::unordered_set<Alphabet> endChars;
735 delta.getEndChars(endChars);
736
737 // KMP-Type Skip value
738 // A.State -> SkipValue
739 const KMPSkipValue beta(Ap, m);
740
741 // main computation
742 if (std::all_of(A.states.begin(), A.states.end(),
743 [](std::shared_ptr<TAState> s) {
744 return s->next.find(0) == s->next.end();
745 })) {
746 // When there is no epsilon transition
747
748 std::size_t i = 0;
749 std::vector<std::pair<std::pair<double, bool>, std::pair<double, bool>>>
750 init;
751 std::vector<IntervalInternalState> CStates;
752 std::vector<IntervalInternalState> LastStates;
753 const Bounds zeroBounds = {0, true};
754
755 // When there can be immidiate accepting
756 // @todo This optimization is not yet when we have epsilon transitions
757#if 0
758 if (m == 1) {
759 for (const auto initState: A.initialStates) {
760 for (char c = 0; c < CHAR_MAX; c++) {
761 for (const auto &edge: initState->next[c]) {
762 if (edge.target.lock()->isMatch) {
763 // solve delta
764 IntermediateZone zone = Zone::zero(2);
765 for (const auto &constraint: edge.guard) {
766 zone.tighten(1, constraint);
767 }
768 if (zone.isSatisfiableCanonized()) {
769 init[c].push_back(std::move(zone));
770 }
771 }
772 }
773 }
774 }
775 }
776#endif
777
778 ans.clear();
779 std::size_t j;
780 while (word.fetch(i + m - 1)) {
781 bool tooLarge = false;
782 // Sunday Shift
783#if 0
784 if (m == 1 && init[word[i].first].size() > 0) {
785 // When there can be immidiate accepting
786 // @todo This optimization is not yet
787 ans.reserve(ans.size() + init[word[i].first].size());
788 if (i <= 0) {
789 for (auto zone: init[word[i].first]) {
790 Zone ansZone;
791 zone.value.col(0).fill({word[i].second, false});
792 if (zone.isSatisfiableCanonized()) {
793 zone.toAns(ansZone);
794 ans.push_back(std::move(ansZone));
795 }
796 }
797 } else {
798 for (auto zone: init[word[i].first]) {
799 Zone ansZone;
800 zone.value.col(0).fill({word[i].second, false});
801 zone.value.row(0).fill({-word[i-1].second, true});
802 if (zone.isSatisfiableCanonized()) {
803 zone.toAns(ansZone);
804 ans.push_back(std::move(ansZone));
805 }
806 }
807 }
808 } else
809#endif
810 if (m > 1 && word.fetch(i + m - 1)) {
811 while (endChars.find(word[i + m - 1].first) == endChars.end()) {
812 if (!word.fetch(i + m)) {
813 tooLarge = true;
814 break;
815 }
816 // increment i
817 i += delta[word[i + m].first];
818 word.setFront(i - 1);
819 if (!word.fetch(i + m - 1)) {
820 tooLarge = true;
821 break;
822 }
823 }
824 }
825
826 if (tooLarge)
827 break;
828
829 // KMP like Matching
830 CStates.clear();
831 CStates.reserve(A.initialStates.size());
832 std::vector<double> zeroResetTime(A.clockSize(), 0);
833 if (word.fetch(i)) {
834 IntervalInternalState istate = {
835 nullptr,
836 zeroResetTime,
837 {word[i].second, false},
838 ((i <= 0) ? zeroBounds : Bounds{-word[i - 1].second, true})};
839
840 CStates.resize(A.initialStates.size(), istate);
841 for (std::size_t k = 0; k < A.initialStates.size(); k++) {
842 CStates[k].s = A.initialStates[k].get();
843 }
844 } else {
845 break;
846 }
847 j = i;
848 while (!CStates.empty() && word.fetch(j)) {
849 const Alphabet c = word[j].first;
850 const double t = word[j].second;
851
852 // try to go to an accepting state
853 for (const auto &config : CStates) {
854 const TAState *s = config.s;
855 auto it = s->next.find('$');
856 if (it == s->next.end()) {
857 continue;
858 }
859 for (const auto &edge : it->second) {
860 auto target = edge.target;
861 if (!target || !target->isMatch) {
862 continue;
863 }
864 Bounds upperBeginConstraint = config.upperConstraint;
865 Bounds lowerBeginConstraint = config.lowerConstraint;
866 Bounds upperEndConstraint = {word[j].second, true};
867 Bounds lowerEndConstraint =
868 ((j > 0) ? Bounds{-word[j - 1].second, false} : zeroBounds);
869
870 // value(2, 1) <= value(2, 0) + value(0, 1)
871 Bounds upperDeltaConstraint =
872 upperEndConstraint + lowerBeginConstraint;
873 // value(1, 2) <= value(1, 0) + value(0, 2)
874 Bounds lowerDeltaConstraint =
875 std::min(lowerEndConstraint + upperBeginConstraint, zeroBounds);
876
877 auto tmpResetTime = config.resetTime;
878 // solve delta
879 for (const auto &delta : edge.guard) {
880 if (tmpResetTime[delta.x]) {
881 switch (delta.odr) {
882 case Constraint::Order::lt:
883 case Constraint::Order::le:
884 upperEndConstraint =
885 std::min(upperEndConstraint,
886 Bounds{delta.c + tmpResetTime[delta.x],
887 {delta.odr == Constraint::Order::le}});
888 // (2, 1) <= (2, 0) + (0, 1)
889 upperDeltaConstraint =
890 std::min(upperDeltaConstraint,
891 upperEndConstraint + lowerBeginConstraint);
892 // (1, 0) <= (1, 2) + (2, 0)
893 upperBeginConstraint =
894 std::min(upperBeginConstraint,
895 lowerDeltaConstraint + upperEndConstraint);
896 break;
897 case Constraint::Order::gt:
898 case Constraint::Order::ge:
899 lowerEndConstraint =
900 std::min(lowerEndConstraint,
901 Bounds{-delta.c - tmpResetTime[delta.x],
902 {delta.odr == Constraint::Order::ge}});
903 // (1, 2) <= (1, 0) + (0, 2)
904 lowerDeltaConstraint =
905 std::min(lowerDeltaConstraint,
906 upperBeginConstraint + lowerEndConstraint);
907 // (0, 1) <= (0, 2) + (2, 1)
908 lowerBeginConstraint =
909 std::min(lowerBeginConstraint,
910 lowerEndConstraint + upperDeltaConstraint);
911 break;
912 }
913 } else {
914 switch (delta.odr) {
915 case Constraint::Order::lt:
916 case Constraint::Order::le:
917 upperDeltaConstraint = std::min(
918 upperDeltaConstraint,
919 Bounds{static_cast<double>(delta.c), {delta.odr == Constraint::Order::le}});
920 // (2, 0) <= (2, 1) + (1, 0)
921 upperEndConstraint =
922 std::min(upperEndConstraint,
923 upperDeltaConstraint + upperBeginConstraint);
924 // (0, 1) <= (0, 2) + (2, 1)
925 lowerBeginConstraint =
926 std::min(lowerBeginConstraint,
927 lowerEndConstraint + upperDeltaConstraint);
928 break;
929 case Constraint::Order::gt:
930 case Constraint::Order::ge:
931 lowerDeltaConstraint = std::min(
932 lowerDeltaConstraint,
933 Bounds{static_cast<double>(-delta.c), {delta.odr == Constraint::Order::ge}});
934 // (1, 0) <= (1, 2) + (2, 0)
935 upperBeginConstraint =
936 std::min(upperBeginConstraint,
937 lowerDeltaConstraint + upperEndConstraint);
938 // (0, 2) <= (0, 1) + (1, 2)
939 lowerEndConstraint =
940 std::min(lowerEndConstraint,
941 lowerBeginConstraint + lowerDeltaConstraint);
942 break;
943 }
944 }
945 }
946
947 if (!isValidConstraint(upperBeginConstraint,
948 lowerBeginConstraint) ||
949 !isValidConstraint(upperEndConstraint, lowerEndConstraint) ||
950 !isValidConstraint(upperDeltaConstraint,
951 lowerDeltaConstraint)) {
952 continue;
953 }
954
955 Zone ansZone = Zone::zero(3);
956 ansZone.value(0, 1) = std::move(lowerBeginConstraint);
957 ansZone.value(1, 0) = std::move(upperBeginConstraint);
958 ansZone.value(0, 2) = std::move(lowerEndConstraint);
959 ansZone.value(2, 0) = std::move(upperEndConstraint);
960 ansZone.value(1, 2) = std::move(lowerDeltaConstraint);
961 ansZone.value(2, 1) = std::move(upperDeltaConstraint);
962
963 ans.push_back(std::move(ansZone));
964 }
965 }
966
967 // try observable transitios (usual)
968 LastStates = std::move(CStates);
969 for (const auto &config : LastStates) {
970 const TAState *s = config.s;
971 auto it = s->next.find(c);
972 if (it == s->next.end()) {
973 continue;
974 }
975 for (auto &edge : it->second) {
976 const auto target = edge.target;
977 if (!target) {
978 continue;
979 }
980
981 Bounds upperBeginConstraint = config.upperConstraint;
982 Bounds lowerBeginConstraint = config.lowerConstraint;
983 bool transitable = true;
984
985 for (const auto &delta : edge.guard) {
986 if (config.resetTime[delta.x]) {
987 if (!delta.satisfy(t - config.resetTime[delta.x])) {
988 transitable = false;
989 break;
990 }
991 } else {
992 switch (delta.odr) {
993 case Constraint::Order::lt:
994 case Constraint::Order::le:
995 lowerBeginConstraint =
996 std::min(lowerBeginConstraint,
997 Bounds{delta.c - t,
998 {delta.odr == Constraint::Order::le}});
999 break;
1000 case Constraint::Order::gt:
1001 case Constraint::Order::ge:
1002 upperBeginConstraint =
1003 std::min(upperBeginConstraint,
1004 Bounds{t - delta.c,
1005 {delta.odr == Constraint::Order::ge}});
1006 break;
1007 }
1008 }
1009 }
1010
1011 if (!transitable || !isValidConstraint(upperBeginConstraint,
1012 lowerBeginConstraint)) {
1013 continue;
1014 }
1015
1016 auto tmpResetTime = config.resetTime;
1017 for (auto i : edge.resetVars) {
1018 tmpResetTime[i] = t;
1019 }
1020
1021 CStates.emplace_back(edge.target, std::move(tmpResetTime),
1022 std::move(upperBeginConstraint),
1023 std::move(lowerBeginConstraint));
1024 }
1025 }
1026 j++;
1027 }
1028 if (!word.fetch(j)) {
1029 // try to go to an accepting state
1030 for (const auto &config : CStates) {
1031 const TAState *s = config.s;
1032 auto it = s->next.find('$');
1033 if (it == s->next.end()) {
1034 continue;
1035 }
1036 for (const auto &edge : it->second) {
1037 auto target = edge.target;
1038 if (!target || !target->isMatch) {
1039 continue;
1040 }
1041 Bounds upperBeginConstraint = config.upperConstraint;
1042 Bounds lowerBeginConstraint = config.lowerConstraint;
1043 Bounds upperEndConstraint = {
1044 std::numeric_limits<double>::infinity(), true};
1045 Bounds lowerEndConstraint =
1046 ((j > 0) ? Bounds{-word[j - 1].second, false} : zeroBounds);
1047
1048 // value(2, 1) <= value(2, 0) + value(0, 1)
1049 Bounds upperDeltaConstraint =
1050 upperEndConstraint + lowerBeginConstraint;
1051 // value(1, 2) <= value(1, 0) + value(0, 2)
1052 Bounds lowerDeltaConstraint =
1053 std::min(lowerEndConstraint + upperBeginConstraint, zeroBounds);
1054
1055 auto tmpResetTime = config.resetTime;
1056 // solve delta
1057 for (const auto &delta : edge.guard) {
1058 if (tmpResetTime[delta.x]) {
1059 switch (delta.odr) {
1060 case Constraint::Order::lt:
1061 case Constraint::Order::le:
1062 upperEndConstraint =
1063 std::min(upperEndConstraint,
1064 Bounds{delta.c + tmpResetTime[delta.x],
1065 {delta.odr == Constraint::Order::le}});
1066 // (2, 1) <= (2, 0) + (0, 1)
1067 upperDeltaConstraint =
1068 std::min(upperDeltaConstraint,
1069 upperEndConstraint + lowerBeginConstraint);
1070 // (1, 0) <= (1, 2) + (2, 0)
1071 upperBeginConstraint =
1072 std::min(upperBeginConstraint,
1073 lowerDeltaConstraint + upperEndConstraint);
1074 break;
1075 case Constraint::Order::gt:
1076 case Constraint::Order::ge:
1077 lowerEndConstraint =
1078 std::min(lowerEndConstraint,
1079 Bounds{-delta.c - tmpResetTime[delta.x],
1080 {delta.odr == Constraint::Order::ge}});
1081 // (1, 2) <= (1, 0) + (0, 2)
1082 lowerDeltaConstraint =
1083 std::min(lowerDeltaConstraint,
1084 upperBeginConstraint + lowerEndConstraint);
1085 // (0, 1) <= (0, 2) + (2, 1)
1086 lowerBeginConstraint =
1087 std::min(lowerBeginConstraint,
1088 lowerEndConstraint + upperDeltaConstraint);
1089 break;
1090 }
1091 } else {
1092 switch (delta.odr) {
1093 case Constraint::Order::lt:
1094 case Constraint::Order::le:
1095 upperDeltaConstraint = std::min(
1096 upperDeltaConstraint,
1097 Bounds{static_cast<double>(delta.c), {delta.odr == Constraint::Order::le}});
1098 // (2, 0) <= (2, 1) + (1, 0)
1099 upperEndConstraint =
1100 std::min(upperEndConstraint,
1101 upperDeltaConstraint + upperBeginConstraint);
1102 // (0, 1) <= (0, 2) + (2, 1)
1103 lowerBeginConstraint =
1104 std::min(lowerBeginConstraint,
1105 lowerEndConstraint + upperDeltaConstraint);
1106 break;
1107 case Constraint::Order::gt:
1108 case Constraint::Order::ge:
1109 lowerDeltaConstraint = std::min(
1110 lowerDeltaConstraint,
1111 Bounds{static_cast<double>(-delta.c), {delta.odr == Constraint::Order::ge}});
1112 // (1, 0) <= (1, 2) + (2, 0)
1113 upperBeginConstraint =
1114 std::min(upperBeginConstraint,
1115 lowerDeltaConstraint + upperEndConstraint);
1116 // (0, 2) <= (0, 1) + (1, 2)
1117 lowerEndConstraint =
1118 std::min(lowerEndConstraint,
1119 lowerBeginConstraint + lowerDeltaConstraint);
1120 break;
1121 }
1122 }
1123 }
1124
1125 if (!isValidConstraint(upperBeginConstraint,
1126 lowerBeginConstraint) ||
1127 !isValidConstraint(upperEndConstraint, lowerEndConstraint) ||
1128 !isValidConstraint(upperDeltaConstraint,
1129 lowerDeltaConstraint)) {
1130 continue;
1131 }
1132
1133 Zone ansZone = Zone::zero(3);
1134 ansZone.value(0, 1) = std::move(lowerBeginConstraint);
1135 ansZone.value(1, 0) = std::move(upperBeginConstraint);
1136 ansZone.value(0, 2) = std::move(lowerEndConstraint);
1137 ansZone.value(2, 0) = std::move(upperEndConstraint);
1138 ansZone.value(1, 2) = std::move(lowerDeltaConstraint);
1139 ansZone.value(2, 1) = std::move(upperDeltaConstraint);
1140
1141 ans.push_back(std::move(ansZone));
1142 }
1143 }
1144 LastStates = std::move(CStates);
1145 }
1146 // KMP like skip value
1147 int greatestN = 1;
1148 for (const IntervalInternalState &istate : LastStates) {
1149 greatestN = std::max(beta[ptrConv.at(istate.s).get()], greatestN);
1150 }
1151 // increment i
1152 i += greatestN;
1153 word.setFront(i - 1);
1154 }
1155 } else {
1156 }
1157}
1158
1168template <class InputContainer, class OutputContainer>
1169void monaaNotNecessaryDollar(WordContainer<InputContainer> word,
1170 TimedAutomaton A,
1171 AnsContainer<OutputContainer> &ans) {
1172 TimedAutomaton Ap;
1173 Ap.states.reserve(A.states.size());
1174 Ap.initialStates.reserve(A.initialStates.size());
1175 Ap.maxConstraints = A.maxConstraints;
1176 std::unordered_map<const TAState *, std::shared_ptr<TAState>> ptrConv;
1177 for (std::shared_ptr<TAState> s : A.states) {
1178 ptrConv[s.get()] = std::make_shared<TAState>(*s);
1179 Ap.states.push_back(ptrConv[s.get()]);
1180 if (std::binary_search(A.initialStates.begin(), A.initialStates.end(), s)) {
1181 Ap.initialStates.push_back(ptrConv[s.get()]);
1182 }
1183 }
1184
1185 for (std::shared_ptr<TAState> s : Ap.states) {
1186 if (s->next.find('$') != s->next.end()) {
1187 s->isMatch = true;
1188 s->next['$'].clear();
1189 s->next.erase('$');
1190 }
1191 for (auto &transitionsPair : s->next) {
1192 for (auto &transition : transitionsPair.second) {
1193 transition.target = ptrConv[transition.target].get();
1194 }
1195 }
1196 }
1197
1198 // Sunday's Skip value
1199 // Char -> Skip Value
1200 const SundaySkipValue delta = SundaySkipValue(Ap);
1201 const int m = delta.getM();
1202 std::unordered_set<Alphabet> endChars;
1203 delta.getEndChars(endChars);
1204
1205 // KMP-Type Skip value
1206 // A.State -> SkipValue
1207 const KMPSkipValue beta(Ap, m);
1208
1209 // main computation
1210 if (std::all_of(A.states.begin(), A.states.end(),
1211 [](std::shared_ptr<TAState> s) {
1212 return s->next.find(0) == s->next.end();
1213 })) {
1214 // When there is no epsilon transition
1215
1216 std::size_t i = 0;
1217 std::vector<std::pair<std::pair<double, bool>, std::pair<double, bool>>>
1218 init;
1219 std::vector<IntervalInternalState> CStates;
1220 std::vector<IntervalInternalState> LastStates;
1221 const Bounds zeroBounds = {0, true};
1222
1223 // When there can be immidiate accepting
1224 // @todo This optimization is not yet when we have epsilon transitions
1225#if 0
1226 if (m == 1) {
1227 for (const auto initState: A.initialStates) {
1228 for (char c = 0; c < CHAR_MAX; c++) {
1229 for (const auto &edge: initState->next[c]) {
1230 if (edge.target.lock()->isMatch) {
1231 // solve delta
1232 IntermediateZone zone = Zone::zero(2);
1233 for (const auto &constraint: edge.guard) {
1234 zone.tighten(1, constraint);
1235 }
1236 if (zone.isSatisfiableCanonized()) {
1237 init[c].push_back(std::move(zone));
1238 }
1239 }
1240 }
1241 }
1242 }
1243 }
1244#endif
1245
1246 ans.clear();
1247 std::size_t j;
1248 while (word.fetch(i + m - 1)) {
1249 bool tooLarge = false;
1250 // Sunday Shift
1251#if 0
1252 if (m == 1 && init[word[i].first].size() > 0) {
1253 // When there can be immidiate accepting
1254 // @todo This optimization is not yet
1255 ans.reserve(ans.size() + init[word[i].first].size());
1256 if (i <= 0) {
1257 for (auto zone: init[word[i].first]) {
1258 Zone ansZone;
1259 zone.value.col(0).fill({word[i].second, false});
1260 if (zone.isSatisfiableCanonized()) {
1261 zone.toAns(ansZone);
1262 ans.push_back(std::move(ansZone));
1263 }
1264 }
1265 } else {
1266 for (auto zone: init[word[i].first]) {
1267 Zone ansZone;
1268 zone.value.col(0).fill({word[i].second, false});
1269 zone.value.row(0).fill({-word[i-1].second, true});
1270 if (zone.isSatisfiableCanonized()) {
1271 zone.toAns(ansZone);
1272 ans.push_back(std::move(ansZone));
1273 }
1274 }
1275 }
1276 } else
1277#endif
1278 if (m > 1 && word.fetch(i + m - 1)) {
1279 while (endChars.find(word[i + m - 1].first) == endChars.end()) {
1280 if (!word.fetch(i + m)) {
1281 tooLarge = true;
1282 break;
1283 }
1284 // increment i
1285 i += delta[word[i + m].first];
1286 word.setFront(i - 1);
1287 if (!word.fetch(i + m - 1)) {
1288 tooLarge = true;
1289 break;
1290 }
1291 }
1292 }
1293
1294 if (tooLarge)
1295 break;
1296
1297 // KMP like Matching
1298 CStates.clear();
1299 CStates.reserve(A.initialStates.size());
1300 std::vector<double> zeroResetTime(A.clockSize(), 0);
1301 if (word.fetch(i)) {
1302 IntervalInternalState istate = {
1303 nullptr,
1304 zeroResetTime,
1305 {word[i].second, false},
1306 ((i <= 0) ? zeroBounds : Bounds{-word[i - 1].second, true})};
1307
1308 CStates.resize(A.initialStates.size(), istate);
1309 for (std::size_t k = 0; k < A.initialStates.size(); k++) {
1310 CStates[k].s = A.initialStates[k].get();
1311 }
1312 } else {
1313 break;
1314 }
1315 j = i;
1316 while (!CStates.empty() && word.fetch(j)) {
1317 const Alphabet c = word[j].first;
1318 const double t = word[j].second;
1319
1320 // try to go to an accepting state
1321 for (const auto &config : CStates) {
1322 const TAState *s = config.s;
1323 auto it = s->next.find('$');
1324 if (it == s->next.end()) {
1325 continue;
1326 }
1327 for (const auto &edge : it->second) {
1328 auto target = edge.target;
1329 if (!target || !target->isMatch) {
1330 continue;
1331 }
1332 Bounds upperBeginConstraint = config.upperConstraint;
1333 Bounds lowerBeginConstraint = config.lowerConstraint;
1334 Bounds upperEndConstraint = {word[j].second, true};
1335 Bounds lowerEndConstraint =
1336 ((j > 0) ? Bounds{-word[j - 1].second, false} : zeroBounds);
1337
1338 // value(2, 1) <= value(2, 0) + value(0, 1)
1339 Bounds upperDeltaConstraint =
1340 upperEndConstraint + lowerBeginConstraint;
1341 // value(1, 2) <= value(1, 0) + value(0, 2)
1342 Bounds lowerDeltaConstraint =
1343 std::min(lowerEndConstraint + upperBeginConstraint, zeroBounds);
1344
1345 auto tmpResetTime = config.resetTime;
1346 // solve delta
1347 for (const auto &delta : edge.guard) {
1348 if (tmpResetTime[delta.x]) {
1349 switch (delta.odr) {
1350 case Constraint::Order::lt:
1351 case Constraint::Order::le:
1352 upperEndConstraint =
1353 std::min(upperEndConstraint,
1354 Bounds{delta.c + tmpResetTime[delta.x],
1355 {delta.odr == Constraint::Order::le}});
1356 // (2, 1) <= (2, 0) + (0, 1)
1357 upperDeltaConstraint =
1358 std::min(upperDeltaConstraint,
1359 upperEndConstraint + lowerBeginConstraint);
1360 // (1, 0) <= (1, 2) + (2, 0)
1361 upperBeginConstraint =
1362 std::min(upperBeginConstraint,
1363 lowerDeltaConstraint + upperEndConstraint);
1364 break;
1365 case Constraint::Order::gt:
1366 case Constraint::Order::ge:
1367 lowerEndConstraint =
1368 std::min(lowerEndConstraint,
1369 Bounds{-delta.c - tmpResetTime[delta.x],
1370 {delta.odr == Constraint::Order::ge}});
1371 // (1, 2) <= (1, 0) + (0, 2)
1372 lowerDeltaConstraint =
1373 std::min(lowerDeltaConstraint,
1374 upperBeginConstraint + lowerEndConstraint);
1375 // (0, 1) <= (0, 2) + (2, 1)
1376 lowerBeginConstraint =
1377 std::min(lowerBeginConstraint,
1378 lowerEndConstraint + upperDeltaConstraint);
1379 break;
1380 }
1381 } else {
1382 switch (delta.odr) {
1383 case Constraint::Order::lt:
1384 case Constraint::Order::le:
1385 upperDeltaConstraint = std::min(
1386 upperDeltaConstraint,
1387 Bounds{static_cast<double>(delta.c), {delta.odr == Constraint::Order::le}});
1388 // (2, 0) <= (2, 1) + (1, 0)
1389 upperEndConstraint =
1390 std::min(upperEndConstraint,
1391 upperDeltaConstraint + upperBeginConstraint);
1392 // (0, 1) <= (0, 2) + (2, 1)
1393 lowerBeginConstraint =
1394 std::min(lowerBeginConstraint,
1395 lowerEndConstraint + upperDeltaConstraint);
1396 break;
1397 case Constraint::Order::gt:
1398 case Constraint::Order::ge:
1399 lowerDeltaConstraint = std::min(
1400 lowerDeltaConstraint,
1401 Bounds{static_cast<double>(-delta.c), {delta.odr == Constraint::Order::ge}});
1402 // (1, 0) <= (1, 2) + (2, 0)
1403 upperBeginConstraint =
1404 std::min(upperBeginConstraint,
1405 lowerDeltaConstraint + upperEndConstraint);
1406 // (0, 2) <= (0, 1) + (1, 2)
1407 lowerEndConstraint =
1408 std::min(lowerEndConstraint,
1409 lowerBeginConstraint + lowerDeltaConstraint);
1410 break;
1411 }
1412 }
1413 }
1414
1415 if (!isValidConstraint(upperBeginConstraint,
1416 lowerBeginConstraint) ||
1417 !isValidConstraint(upperEndConstraint, lowerEndConstraint) ||
1418 !isValidConstraint(upperDeltaConstraint,
1419 lowerDeltaConstraint)) {
1420 continue;
1421 }
1422
1423 Zone ansZone = Zone::zero(3);
1424 ansZone.value(0, 1) = std::move(lowerBeginConstraint);
1425 ansZone.value(1, 0) = std::move(upperBeginConstraint);
1426 ansZone.value(0, 2) = std::move(lowerEndConstraint);
1427 ansZone.value(2, 0) = std::move(upperEndConstraint);
1428 ansZone.value(1, 2) = std::move(lowerDeltaConstraint);
1429 ansZone.value(2, 1) = std::move(upperDeltaConstraint);
1430
1431 ans.push_back(std::move(ansZone));
1432 }
1433 }
1434
1435 // try observable transitios (usual)
1436 LastStates = std::move(CStates);
1437 for (const auto &config : LastStates) {
1438 const TAState *s = config.s;
1439 auto it = s->next.find(c);
1440 if (it == s->next.end()) {
1441 continue;
1442 }
1443 for (auto &edge : it->second) {
1444 const auto target = edge.target;
1445 if (!target) {
1446 continue;
1447 }
1448
1449 Bounds upperBeginConstraint = config.upperConstraint;
1450 Bounds lowerBeginConstraint = config.lowerConstraint;
1451 bool transitable = true;
1452
1453 for (const auto &delta : edge.guard) {
1454 if (config.resetTime[delta.x]) {
1455 if (!delta.satisfy(t - config.resetTime[delta.x])) {
1456 transitable = false;
1457 break;
1458 }
1459 } else {
1460 switch (delta.odr) {
1461 case Constraint::Order::lt:
1462 case Constraint::Order::le:
1463 lowerBeginConstraint =
1464 std::min(lowerBeginConstraint,
1465 Bounds{delta.c - t,
1466 {delta.odr == Constraint::Order::le}});
1467 break;
1468 case Constraint::Order::gt:
1469 case Constraint::Order::ge:
1470 upperBeginConstraint =
1471 std::min(upperBeginConstraint,
1472 Bounds{t - delta.c,
1473 {delta.odr == Constraint::Order::ge}});
1474 break;
1475 }
1476 }
1477 }
1478
1479 if (!transitable || !isValidConstraint(upperBeginConstraint,
1480 lowerBeginConstraint)) {
1481 continue;
1482 }
1483
1484 auto tmpResetTime = config.resetTime;
1485 for (auto i : edge.resetVars) {
1486 tmpResetTime[i] = t;
1487 }
1488
1489 if (edge.target->isMatch) {
1490 // If we reached an accepting state
1491 // CStates.emplace_back(edge.target,
1492 // std::move(tmpResetTime),
1493 // std::move(upperBeginConstraint),
1494 // std::move(lowerBeginConstraint));
1495
1496 const Bounds upperEndConstraint = {t, true};
1497 const Bounds lowerEndConstraint = {t, true};
1498
1499 // value(2, 1) <= value(2, 0) + value(0, 1)
1500 const Bounds upperDeltaConstraint =
1501 upperEndConstraint + lowerBeginConstraint;
1502 // value(1, 2) <= value(1, 0) + value(0, 2)
1503 const Bounds lowerDeltaConstraint = std::min(
1504 lowerEndConstraint + upperBeginConstraint, zeroBounds);
1505
1506 if (!isValidConstraint(upperBeginConstraint,
1507 lowerBeginConstraint) ||
1508 !isValidConstraint(upperEndConstraint, lowerEndConstraint) ||
1509 !isValidConstraint(upperDeltaConstraint,
1510 lowerDeltaConstraint)) {
1511 continue;
1512 }
1513
1514 Zone ansZone = Zone::zero(3);
1515 ansZone.value(0, 1) = lowerBeginConstraint;
1516 ansZone.value(1, 0) = upperBeginConstraint;
1517 ansZone.value(0, 2) = std::move(lowerEndConstraint);
1518 ansZone.value(2, 0) = std::move(upperEndConstraint);
1519 ansZone.value(1, 2) = std::move(lowerDeltaConstraint);
1520 ansZone.value(2, 1) = std::move(upperDeltaConstraint);
1521
1522 ans.push_back(std::move(ansZone));
1523 }
1524
1525 CStates.emplace_back(edge.target, std::move(tmpResetTime),
1526 std::move(upperBeginConstraint),
1527 std::move(lowerBeginConstraint));
1528 }
1529 }
1530 j++;
1531 }
1532 if (!word.fetch(j)) {
1533 // try to go to an accepting state
1534 for (const auto &config : CStates) {
1535 const TAState *s = config.s;
1536 auto it = s->next.find('$');
1537 if (it == s->next.end()) {
1538 continue;
1539 }
1540 for (const auto &edge : it->second) {
1541 auto target = edge.target;
1542 if (!target || !target->isMatch) {
1543 continue;
1544 }
1545 Bounds upperBeginConstraint = config.upperConstraint;
1546 Bounds lowerBeginConstraint = config.lowerConstraint;
1547 Bounds upperEndConstraint = {
1548 std::numeric_limits<double>::infinity(), true};
1549 Bounds lowerEndConstraint =
1550 ((j > 0) ? Bounds{-word[j - 1].second, false} : zeroBounds);
1551
1552 // value(2, 1) <= value(2, 0) + value(0, 1)
1553 Bounds upperDeltaConstraint =
1554 upperEndConstraint + lowerBeginConstraint;
1555 // value(1, 2) <= value(1, 0) + value(0, 2)
1556 Bounds lowerDeltaConstraint =
1557 std::min(lowerEndConstraint + upperBeginConstraint, zeroBounds);
1558
1559 auto tmpResetTime = config.resetTime;
1560 // solve delta
1561 for (const auto &delta : edge.guard) {
1562 if (tmpResetTime[delta.x]) {
1563 switch (delta.odr) {
1564 case Constraint::Order::lt:
1565 case Constraint::Order::le:
1566 upperEndConstraint =
1567 std::min(upperEndConstraint,
1568 Bounds{delta.c + tmpResetTime[delta.x],
1569 {delta.odr == Constraint::Order::le}});
1570 // (2, 1) <= (2, 0) + (0, 1)
1571 upperDeltaConstraint =
1572 std::min(upperDeltaConstraint,
1573 upperEndConstraint + lowerBeginConstraint);
1574 // (1, 0) <= (1, 2) + (2, 0)
1575 upperBeginConstraint =
1576 std::min(upperBeginConstraint,
1577 lowerDeltaConstraint + upperEndConstraint);
1578 break;
1579 case Constraint::Order::gt:
1580 case Constraint::Order::ge:
1581 lowerEndConstraint =
1582 std::min(lowerEndConstraint,
1583 Bounds{-delta.c - tmpResetTime[delta.x],
1584 {delta.odr == Constraint::Order::ge}});
1585 // (1, 2) <= (1, 0) + (0, 2)
1586 lowerDeltaConstraint =
1587 std::min(lowerDeltaConstraint,
1588 upperBeginConstraint + lowerEndConstraint);
1589 // (0, 1) <= (0, 2) + (2, 1)
1590 lowerBeginConstraint =
1591 std::min(lowerBeginConstraint,
1592 lowerEndConstraint + upperDeltaConstraint);
1593 break;
1594 }
1595 } else {
1596 switch (delta.odr) {
1597 case Constraint::Order::lt:
1598 case Constraint::Order::le:
1599 upperDeltaConstraint = std::min(
1600 upperDeltaConstraint,
1601 Bounds{static_cast<double>(delta.c), {delta.odr == Constraint::Order::le}});
1602 // (2, 0) <= (2, 1) + (1, 0)
1603 upperEndConstraint =
1604 std::min(upperEndConstraint,
1605 upperDeltaConstraint + upperBeginConstraint);
1606 // (0, 1) <= (0, 2) + (2, 1)
1607 lowerBeginConstraint =
1608 std::min(lowerBeginConstraint,
1609 lowerEndConstraint + upperDeltaConstraint);
1610 break;
1611 case Constraint::Order::gt:
1612 case Constraint::Order::ge:
1613 lowerDeltaConstraint = std::min(
1614 lowerDeltaConstraint,
1615 Bounds{static_cast<double>(-delta.c), {delta.odr == Constraint::Order::ge}});
1616 // (1, 0) <= (1, 2) + (2, 0)
1617 upperBeginConstraint =
1618 std::min(upperBeginConstraint,
1619 lowerDeltaConstraint + upperEndConstraint);
1620 // (0, 2) <= (0, 1) + (1, 2)
1621 lowerEndConstraint =
1622 std::min(lowerEndConstraint,
1623 lowerBeginConstraint + lowerDeltaConstraint);
1624 break;
1625 }
1626 }
1627 }
1628
1629 if (!isValidConstraint(upperBeginConstraint,
1630 lowerBeginConstraint) ||
1631 !isValidConstraint(upperEndConstraint, lowerEndConstraint) ||
1632 !isValidConstraint(upperDeltaConstraint,
1633 lowerDeltaConstraint)) {
1634 continue;
1635 }
1636
1637 Zone ansZone = Zone::zero(3);
1638 ansZone.value(0, 1) = std::move(lowerBeginConstraint);
1639 ansZone.value(1, 0) = std::move(upperBeginConstraint);
1640 ansZone.value(0, 2) = std::move(lowerEndConstraint);
1641 ansZone.value(2, 0) = std::move(upperEndConstraint);
1642 ansZone.value(1, 2) = std::move(lowerDeltaConstraint);
1643 ansZone.value(2, 1) = std::move(upperDeltaConstraint);
1644
1645 ans.push_back(std::move(ansZone));
1646 }
1647 }
1648 LastStates = std::move(CStates);
1649 }
1650 // KMP like skip value
1651 int greatestN = 1;
1652 for (const IntervalInternalState &istate : LastStates) {
1653 greatestN = std::max(beta[ptrConv[istate.s].get()], greatestN);
1654 }
1655 // increment i
1656 i += greatestN;
1657 word.setFront(i - 1);
1658 }
1659 } else {
1660 }
1661}
AnsContainer
Container class for the output zones.
Definition ans_vec.hh:17
AnsContainer::clear
void clear()
Remove all the contained zones.
Definition ans_vec.hh:42
AnsContainer::size
std::size_t size() const
Returns the number of the contained zones.
Definition ans_vec.hh:32
AnsContainer::reserve
void reserve(std::size_t n)
Reserve the space to contain zones.
Definition ans_vec.hh:50
AnsContainer::push_back
void push_back(typename Container::value_type in)
Append a zone to the container.
Definition ans_vec.hh:38
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
KMPSkipValue
The skip value function based on the KMP algorithm for string matching.
Definition kmp_skip_value.hh:17
SundaySkipValue
The skip value function based on Sunday's quick search.
Definition sunday_skip_value.hh:17
SundaySkipValue::getM
int getM() const
Minimum length of the recognized language.
Definition sunday_skip_value.hh:76
WordContainer
Container class for the input timed word.
Definition word_container.hh:14
WordContainer::fetch
bool fetch(std::size_t n)
Fetch the timed words by n-th position.
Definition word_container.hh:69
WordContainer::setFront
void setFront(std::size_t n)
Discard the elements before n-th position.
Definition word_container.hh:62
monaa
void monaa(WordContainer< InputContainer > word, TimedAutomaton A, AnsContainer< OutputContainer > &ans)
Execute the timed FJS algorithm.
Definition monaa.hh:151
monaaNotNecessaryDollar
void monaaNotNecessaryDollar(WordContainer< InputContainer > word, TimedAutomaton A, AnsContainer< OutputContainer > &ans)
Execute the timed FJS algorithm.
Definition monaa.hh:1169
updateConstraint
void updateConstraint(std::pair< double, bool > &upperConstraint, std::pair< double, bool > &lowerConstraint, const Constraint &delta, const double comparedValue)
update the assuming interval to satisfy the constraint
Definition monaa.hh:108
isValidConstraint
bool isValidConstraint(const Bounds &upperConstraint, const Bounds &lowerConstraint)
Check if the given constraint is non empty.
Definition monaa.hh:100
monaaDollar
void monaaDollar(WordContainer< InputContainer > word, TimedAutomaton A, AnsContainer< OutputContainer > &ans)
Execute the timed FJS algorithm. This is the original timed FJS algorithm.
Definition monaa.hh:702
Automaton::states
std::vector< std::shared_ptr< State > > states
The states of this automaton.
Definition common_types.hh:17
Automaton::initialStates
std::vector< std::shared_ptr< State > > initialStates
The initial states of this automaton.
Definition common_types.hh:19
Constraint
A constraint in a guard of transitions.
Definition constraint.hh:16
InternalState
Definition monaa.hh:65
IntervalInternalState
Definition monaa.hh:85
Interval
Class for an interval.
Definition interval.hh:15
TAState
A state of timed automata.
Definition timed_automaton.hh:19
TAState::next
std::unordered_map< Alphabet, std::vector< TATransition > > next
An mapping of a character to the transitions.
Definition timed_automaton.hh:32
TimedAutomaton
A timed automaton.
Definition timed_automaton.hh:54
TimedAutomaton::clockSize
size_t clockSize() const
Returns the number of clock variables used in the timed automaton.
Definition timed_automaton.hh:95
TimedAutomaton::maxConstraints
std::vector< int > maxConstraints
The maximum constraints for each clock variables.
Definition timed_automaton.hh:60
Zone
Implementation of a zone with DBM.
Definition zone.hh:43
Generated by doxygen 1.9.8