From 23b7ed0324c49b5516282166c5265ca1f1fa3131 Mon Sep 17 00:00:00 2001 From: Masaki Waga Date: Sun, 19 Jun 2022 09:47:55 +0900 Subject: [PATCH] Feature/kleene star#1 (#4) * ad hoc fix of Kleene star * removed the note on Kleene star --- README.md | 4 --- doc/getting_started.md | 2 +- examples/integrated_test.sh | 56 ++++++++++++++++++------------------- libmonaa/intersection.cc | 22 +++++++++++++++ libmonaa/timed_automaton.hh | 13 +++++++-- monaa/tre.cc | 17 ++++++++++- 6 files changed, 78 insertions(+), 36 deletions(-) diff --git a/README.md b/README.md index 5af3acd..6e0cc46 100644 --- a/README.md +++ b/README.md @@ -120,10 +120,6 @@ Syntax of Timed Regular Expressions | expr % (s,t) (Time Restriction) -### Note on time restriction of Kleene star - -Our TRE translation algorithm produces an incorrect TA for a time restriction of Kleene star. For example, `(A*)%(1,20)$` is not translated correctly, while `(AB*)%(1,20)$` is translated correctly. This is because such expression requires restriction of empty area, which requires an unobservable transition or TRE rewriting such as `(A*)%(1,2)$` into `((A+)%(1,2)$)|($%(>1))`. - References ------------- diff --git a/doc/getting_started.md b/doc/getting_started.md index 1a9e722..3389db1 100644 --- a/doc/getting_started.md +++ b/doc/getting_started.md @@ -129,7 +129,7 @@ We can use [Kleene plus](https://en.wikipedia.org/wiki/Kleene_star#Kleene_plus) ``` If you want match zero times repetition, i.e., empty events, you can use [Kleene star](https://en.wikipedia.org/wiki/Kleene_star). -We note that this does not change the result because in the log, we do not have any blank interval longer than 1. +We note that in the current example, this does not change the result because zero times repetition has zero duration, which is inconsistent with the constraint `%(1,20)`` ``` ../build/monaa -e '((A(B|C))*%(1,20))$' < ../examples/getting_started/timed_word.txt diff --git a/examples/integrated_test.sh b/examples/integrated_test.sh index 4ce808d..53630cc 100755 --- a/examples/integrated_test.sh +++ b/examples/integrated_test.sh @@ -112,32 +112,32 @@ diff <(../build/monaa '((A(B|C))+%(1,20))$' < ../examples/getting_started/timed_ ============================= EOF -# diff <(../build/monaa -e '((A(B|C))*%(1,20))$' < ../examples/getting_started/timed_word.txt) - <zeroDuration != s2->zeroDuration) { + continue; + } toIState[std::make_pair(s1.get(), s2.get())] = std::make_shared(s1->isMatch && s2->isMatch); + toIState[std::make_pair(s1.get(), s2.get())]->zeroDuration = s1->zeroDuration; out.states.push_back(toIState[std::make_pair(s1.get(), s2.get())]); } } @@ -29,6 +33,9 @@ void intersectionTA(const TimedAutomaton &in1, const TimedAutomaton &in2, in2.initialStates.size()); for (auto s1 : in1.initialStates) { for (auto s2 : in2.initialStates) { + if (s1->zeroDuration != s2->zeroDuration) { + continue; + } out.initialStates.push_back(toIState[std::make_pair(s1.get(), s2.get())]); } } @@ -77,6 +84,9 @@ void intersectionTA(const TimedAutomaton &in1, const TimedAutomaton &in2, // make edges for (auto s1 : in1.states) { for (auto s2 : in2.states) { + if (s1->zeroDuration != s2->zeroDuration) { + continue; + } // Epsilon transitions for (const auto &e1 : s1->next[0]) { auto nextS1 = e1.target; @@ -131,6 +141,9 @@ void updateInitAccepting(const TimedAutomaton &in1, const TimedAutomaton &in2, in2.initialStates.size()); for (auto init1 : in1.initialStates) { for (auto init2 : in2.initialStates) { + if (init1->zeroDuration != init2->zeroDuration) { + continue; + } out.initialStates.push_back( toIState[std::make_pair(init1.get(), init2.get())]); } @@ -160,6 +173,9 @@ void intersectionSignalTA(const TimedAutomaton &in1, const TimedAutomaton &in2, out.states.reserve(in1.stateSize() * in2.stateSize()); for (auto s1 : in1.states) { for (auto s2 : in2.states) { + if (s1->zeroDuration != s2->zeroDuration) { + continue; + } toIState[std::make_pair(s1.get(), s2.get())] = std::make_shared(s1->isMatch && s2->isMatch); out.states.push_back(toIState[std::make_pair(s1.get(), s2.get())]); @@ -172,6 +188,9 @@ void intersectionSignalTA(const TimedAutomaton &in1, const TimedAutomaton &in2, in2.initialStates.size()); for (auto s1 : in1.initialStates) { for (auto s2 : in2.initialStates) { + if (s1->zeroDuration != s2->zeroDuration) { + continue; + } out.initialStates.push_back(toIState[std::make_pair(s1.get(), s2.get())]); } } @@ -220,6 +239,9 @@ void intersectionSignalTA(const TimedAutomaton &in1, const TimedAutomaton &in2, // make edges for (auto s1 : in1.states) { for (auto s2 : in2.states) { + if (s1->zeroDuration != s2->zeroDuration) { + continue; + } // Epsilon transitions for (const auto &e1 : s1->next[0]) { auto nextS1 = e1.target; diff --git a/libmonaa/timed_automaton.hh b/libmonaa/timed_automaton.hh index c47993d..fb7662f 100644 --- a/libmonaa/timed_automaton.hh +++ b/libmonaa/timed_automaton.hh @@ -19,6 +19,12 @@ struct TATransition; struct TAState { //! @brief The value is true if and only if the state is an accepting state. bool isMatch; + /*! + * @brief The value is true if the duration to stay this state must be zero. + * + * Such state only exists during the translation from a TRE to a TA. + */ + bool zeroDuration = false; /*! @brief An mapping of a character to the transitions. @note Because of non-determinism, the second element is a vector. @@ -154,8 +160,11 @@ static inline std::ostream &operator<<(std::ostream &os, for (std::shared_ptr state : TA.states) { os << " loc" << stateNumber.at(state.get()) - << " [init=" << isInit.at(state.get()) << ", match=" << state->isMatch - << "]\n"; + << " [init=" << isInit.at(state.get()) << ", match=" << state->isMatch; + if (state->zeroDuration) { + os << ", zero_duration=" << state->zeroDuration; + } + os << "]\n"; } for (std::shared_ptr source : TA.states) { diff --git a/monaa/tre.cc b/monaa/tre.cc index 7410cf0..5614a20 100644 --- a/monaa/tre.cc +++ b/monaa/tre.cc @@ -56,6 +56,7 @@ void concat2(TimedAutomaton &left, const TimedAutomaton &right) { transition.target = initState.get(); transition.resetVars = rightClocks; newTransitions.emplace_back(std::move(transition)); + transition.target->zeroDuration = false; } } } @@ -216,6 +217,7 @@ void TRE::toEventTA(TimedAutomaton &out) const { out.states[0] = std::make_shared(); out.initialStates = {out.states[0]}; out.states[0]->isMatch = true; + out.states[0]->zeroDuration = true; out.maxConstraints.clear(); break; } @@ -226,10 +228,13 @@ void TRE::toEventTA(TimedAutomaton &out) const { std::vector newTransitions; for (TATransition edge : edges.second) { TAState *target = edge.target; - if (target && target->isMatch) { + if (target && target->isMatch && !target->zeroDuration) { newTransitions.reserve(newTransitions.size() + out.initialStates.size()); for (auto initState : out.initialStates) { + if (initState->zeroDuration) { + continue; + } TATransition transition = edge; transition.target = initState.get(); for (std::size_t clock = 0; clock < out.clockSize(); clock++) { @@ -292,6 +297,16 @@ void TRE::toEventTA(TimedAutomaton &out) const { bool isDummyUsed = false; std::shared_ptr dummyAcceptingState = std::make_shared(true); + // Make all the zero duration states non-initial + // Note: this would not work well if we allow constraints >= 0 + out.initialStates.erase(std::remove_if( + out.initialStates.begin(), out.initialStates.end(), + [](auto &state) {return state->zeroDuration;}), + out.initialStates.end()); + // Make all the state non-zero duration + for (auto state : out.states) { + state->zeroDuration = false; + } for (auto state : out.states) { for (auto &edges : state->next) { for (auto &edge : edges.second) {