Skip to content

Commit

Permalink
Feature/kleene star#1 (#4)
Browse files Browse the repository at this point in the history 
* ad hoc fix of Kleene star

* removed the note on Kleene star
  • Loading branch information
@MasWag
MasWag authored Jun 19, 2022
1 parent a369d8b commit 23b7ed0
Show file tree
Hide file tree
Showing 6 changed files with 78 additions and 36 deletions.
4 changes: 0 additions & 4 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
-------------

Expand Down
2 changes: 1 addition & 1 deletion doc/getting_started.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
56 changes: 28 additions & 28 deletions examples/integrated_test.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) - <<EOF
# 1.500000 <= t < 2.000000
# 3.200000 < t' <= 3.500000
# 1.200000 < t' - t <= 2.000000
# =============================
# 1.500000 <= t < 2.000000
# 4.600000 < t' <= inf
# 2.600000 < t' - t <= inf
# =============================
# 3.200000 <= t < 3.500000
# 4.600000 < t' <= inf
# 1.100000 < t' - t <= inf
# =============================
# EOF
diff <(../build/monaa -e '((A(B|C))*%(1,20))$' < ../examples/getting_started/timed_word.txt) - <<EOF
1.500000 <= t < 2.000000
3.200000 < t' <= 3.500000
1.200000 < t' - t <= 2.000000
=============================
1.500000 <= t < 2.000000
4.600000 < t' <= inf
2.600000 < t' - t <= inf
=============================
3.200000 <= t < 3.500000
4.600000 < t' <= inf
1.100000 < t' - t <= inf
=============================
EOF

# diff <(../build/monaa '((A(B|C))*%(1,20))$' < ../examples/getting_started/timed_word.txt) - <<EOF
# 1.500000 <= t < 2.000000
# 3.200000 < t' <= 3.500000
# 1.200000 < t' - t <= 2.000000
# =============================
# 1.500000 <= t < 2.000000
# 4.600000 < t' <= inf
# 2.600000 < t' - t <= inf
# =============================
# 3.200000 <= t < 3.500000
# 4.600000 < t' <= inf
# 1.100000 < t' - t <= inf
# =============================
# EOF
diff <(../build/monaa '((A(B|C))*%(1,20))$' < ../examples/getting_started/timed_word.txt) - <<EOF
1.500000 <= t < 2.000000
3.200000 < t' <= 3.500000
1.200000 < t' - t <= 2.000000
=============================
1.500000 <= t < 2.000000
4.600000 < t' <= inf
2.600000 < t' - t <= inf
=============================
3.200000 <= t < 3.500000
4.600000 < t' <= inf
1.100000 < t' - t <= inf
=============================
EOF
22 changes: 22 additions & 0 deletions libmonaa/intersection.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,12 @@ void intersectionTA(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<TAState>(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())]);
}
}
Expand All @@ -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())]);
}
}
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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())]);
}
Expand Down Expand Up @@ -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<TAState>(s1->isMatch && s2->isMatch);
out.states.push_back(toIState[std::make_pair(s1.get(), s2.get())]);
Expand All @@ -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())]);
}
}
Expand Down Expand Up @@ -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;
Expand Down
13 changes: 11 additions & 2 deletions libmonaa/timed_automaton.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -154,8 +160,11 @@ static inline std::ostream &operator<<(std::ostream &os,

for (std::shared_ptr<TAState> 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<TAState> source : TA.states) {
Expand Down
17 changes: 16 additions & 1 deletion monaa/tre.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
}
}
Expand Down Expand Up @@ -216,6 +217,7 @@ void TRE::toEventTA(TimedAutomaton &out) const {
out.states[0] = std::make_shared<TAState>();
out.initialStates = {out.states[0]};
out.states[0]->isMatch = true;
out.states[0]->zeroDuration = true;
out.maxConstraints.clear();
break;
}
Expand All @@ -226,10 +228,13 @@ void TRE::toEventTA(TimedAutomaton &out) const {
std::vector<TATransition> 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++) {
Expand Down Expand Up @@ -292,6 +297,16 @@ void TRE::toEventTA(TimedAutomaton &out) const {
bool isDummyUsed = false;
std::shared_ptr<TAState> dummyAcceptingState =
std::make_shared<TAState>(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) {
Expand Down

0 comments on commit 23b7ed0

Please sign in to comment.