libmonaa  0.5.2
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
65 struct 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 
85 struct 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 
100 inline bool isValidConstraint(const Bounds &upperConstraint,
101  const Bounds &lowerConstraint) {
102  return upperConstraint + lowerConstraint >= Bounds{0.0, true};
103 }
104 
108 inline 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 
150 template <class InputContainer, class OutputContainer>
151 void 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{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{-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 
701 template <class InputContainer, class OutputContainer>
702 void 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{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{-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{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{-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 
1168 template <class InputContainer, class OutputContainer>
1169 void 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{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{-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{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{-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:13
WordContainer::fetch
bool fetch(std::size_t n)
Fetch the timed words by n-th position.
Definition: word_container.hh:68
WordContainer::setFront
void setFront(std::size_t n)
Discard the elements before n-th position.
Definition: word_container.hh:61
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:14
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.1