fixed a bug in tre2ta

MasWag · Feb 22, 2021 · 67d02c5 · 67d02c5
1 parent e2c70ce
commit 67d02c5
Show file tree

Hide file tree

Showing 6 changed files with 22 additions and 20 deletions.
diff --git a/libmonaa/timed_automaton.hh b/libmonaa/timed_automaton.hh
@@ -148,14 +148,14 @@ std::ostream& operator<<(std::ostream& os, const TimedAutomaton& TA) {
   os << "digraph G {\n";
 
   for (std::shared_ptr<TAState> state: TA.states) {
-    os << "        " << stateNumber.at(state.get()) << " [init=" << isInit.at(state.get()) << ", match=" << state->isMatch << "]\n";
+    os << "        loc" << stateNumber.at(state.get()) << " [init=" << isInit.at(state.get()) << ", match=" << state->isMatch << "]\n";
   }
 
   for (std::shared_ptr<TAState> source: TA.states) {
     for (auto edges: source->next) {
       for (TATransition edge: edges.second) {
         TAState* target = edge.target;
-        os << "        " << stateNumber.at(source.get()) << "->" << stateNumber.at(target) << " [label=\"" << edges.first << "\"";
+        os << "        loc" << stateNumber.at(source.get()) << "->loc" << stateNumber.at(target) << " [label=\"" << edges.first << "\"";
         if (!edge.guard.empty()) {
           os << ", guard=\"{";
           bool isFirst = true;
@@ -169,7 +169,7 @@ std::ostream& operator<<(std::ostream& os, const TimedAutomaton& TA) {
           os << "}\"";
         }
         if (!edge.resetVars.empty()) {
-          os << ", resets=\"{";
+          os << ", reset=\"{";
           bool isFirst = true;
           for (const ClockVariables var: edge.resetVars) {
             if (!isFirst) {

diff --git a/libmonaa/zone_automaton.hh b/libmonaa/zone_automaton.hh
@@ -133,7 +133,7 @@ struct ZoneAutomaton : public Automaton<ZAState> {
           return false;
         }
         for (const auto &edges: state->next) {
-          for (const auto edge: edges) {
+          for (const auto &edge: edges) {
             auto target = edge.lock();
             if (target && visited.find(target) == visited.end()) {
               // We have not visited the state

diff --git a/monaa/intermediate_tre.cc b/monaa/intermediate_tre.cc
@@ -70,8 +70,8 @@ DNFTRE::DNFTRE(const std::shared_ptr<const TRE> tre) {
     for (const auto& conjunctionsLeft: subfmlLeft->list) {
       for (const auto& conjunctionsRight: subfmlRight->list) {
         std::list<std::shared_ptr<AtomicTRE>> conjunctions;
-        for (const std::shared_ptr<AtomicTRE> left: conjunctionsLeft) {
-          for(const std::shared_ptr<AtomicTRE> right: conjunctionsRight) {
+        for (const std::shared_ptr<AtomicTRE> &left: conjunctionsLeft) {
+          for(const std::shared_ptr<AtomicTRE> &right: conjunctionsRight) {
             conjunctions.push_back(std::make_shared<AtomicTRE>(left, right));
           }
         }

diff --git a/monaa/tre.cc b/monaa/tre.cc
@@ -207,6 +207,9 @@ void TRE::toEventTA(TimedAutomaton &out) const {
               for (auto initState: out.initialStates) {
                 TATransition transition = edge;
                 transition.target = initState.get();
+                for (int clock = 0; clock < out.clockSize(); clock++) {
+                  transition.resetVars.push_back(clock);
+                }
                 edges.second.emplace_back(std::move(transition));
               }
             }
@@ -257,7 +260,6 @@ void TRE::toEventTA(TimedAutomaton &out) const {
           dummyInitialState->next[c].reserve(dummyInitialState->next[c].size() + initTransitionsPair.second.size());
           for (auto &edge: initTransitionsPair.second) {
             TATransition transition = edge;
-            transition.resetVars.push_back(out.clockSize());
             dummyInitialState->next[c].emplace_back(std::move(transition));
           }
         }

diff --git a/test/timed_automaton_test.cc b/test/timed_automaton_test.cc
@@ -77,14 +77,14 @@ BOOST_AUTO_TEST_CASE(small)
   TimedAutomaton small;
   std::stringstream stream;
   std::string expected = "digraph G {\n\
-        1 [init=1, match=0]\n\
-        2 [init=0, match=0]\n\
-        3 [init=0, match=0]\n\
-        4 [init=0, match=1]\n\
-        1->2 [label=\"l\", guard=\"{x0 < 1}\"]\n\
-        2->3 [label=\"h\", guard=\"{x0 < 1}\"]\n\
-        3->4 [label=\"$\", guard=\"{x0 < 1}\"]\n\
-        3->2 [label=\"l\", guard=\"{x0 < 1}\"]\n\
+        loc1 [init=1, match=0]\n\
+        loc2 [init=0, match=0]\n\
+        loc3 [init=0, match=0]\n\
+        loc4 [init=0, match=1]\n\
+        loc1->loc2 [label=\"l\", guard=\"{x0 < 1}\"]\n\
+        loc2->loc3 [label=\"h\", guard=\"{x0 < 1}\"]\n\
+        loc3->loc4 [label=\"$\", guard=\"{x0 < 1}\"]\n\
+        loc3->loc2 [label=\"l\", guard=\"{x0 < 1}\"]\n\
 }\n";
 
   // Input

diff --git a/test/tre_test.cc b/test/tre_test.cc
@@ -93,12 +93,12 @@ BOOST_AUTO_TEST_SUITE(treTest)
 
 
       BOOST_TEST(TA.isMember({}));
-      BOOST_TEST(TA.isMember({{'a', 1.2},
-                              {'b', 2.0},
-                              {'a', 3.0}}));
+      BOOST_TEST(TA.isMember({{'a', 0.2},
+                              {'b', 1.0},
+                              {'a', 1.9}}));
       BOOST_TEST(!TA.isMember({{'a', 1.2},
-                               {'b', 2.0},
-                               {'a', 3.3}}));
+                               {'b', 1.8},
+                               {'a', 2.0}}));
     }