diff --git a/src/boolean_monitor.hh b/src/boolean_monitor.hh index 00da557..a8d26ef 100644 --- a/src/boolean_monitor.hh +++ b/src/boolean_monitor.hh @@ -20,6 +20,7 @@ namespace NonSymbolic { template class BooleanMonitor : public SingleSubject>, public Observer> { public: + static const constexpr std::size_t unobservableActionID = 127; BooleanMonitor(const NonParametricTA &automaton) : automaton(automaton) { configurations.clear(); // configurations.reserve(automaton.initialStates.size()); @@ -29,19 +30,28 @@ namespace NonSymbolic { // by default, initNEnv is unset (optional) NumberValuation initNEnv(automaton.numberVariableSize); for (const auto &initialState: automaton.initialStates) { - configurations.insert({initialState, initCVal, initSEnv, initNEnv}); + configurations.insert({initialState, initCVal, initSEnv, initNEnv, 0}); } } - virtual ~BooleanMonitor() = default; + virtual ~BooleanMonitor() { + epsilonTransition(configurations); + } void notify(const TimedWordEvent &event) { const Action actionId = event.actionId; const std::vector &strings = event.strings; const std::vector &numbers = event.numbers; const double timestamp = event.timestamp; + boost::unordered_set nextConfigurations; + configurations.merge(epsilonTransition(configurations)); + for (const Configuration &conf: configurations) { // make the current env auto clockValuation = std::get<1>(conf); // conf.clockValuation; + const auto absTime = std::get<4>(conf); + if (timestamp < absTime) { + continue; + } for (double &d: clockValuation) { d += timestamp - absTime; } @@ -68,14 +78,17 @@ namespace NonSymbolic { transition.update.execute(nextSEnv, nextNEnv); nextSEnv.resize(automaton.stringVariableSize); nextNEnv.resize(automaton.numberVariableSize); - nextConfigurations.insert({transition.target.lock(), std::move(nextCVal), nextSEnv, nextNEnv}); - if (transition.target.lock()->isMatch) { + auto target = transition.target.lock(); + if (!target) { + continue; + } + nextConfigurations.insert({target, std::move(nextCVal), nextSEnv, nextNEnv, timestamp}); + if (target->isMatch) { this->notifyObservers({index, timestamp, nextNEnv, nextSEnv}); } } } } - absTime = timestamp; index++; configurations = std::move(nextConfigurations); } @@ -83,7 +96,7 @@ namespace NonSymbolic { private: const NonParametricTA automaton; using Configuration = std::tuple>, std::vector, - StringValuation, NumberValuation>; + StringValuation, NumberValuation, double>; // struct Configuration { // std::shared_ptr> state; // std::vector clockValuation; @@ -95,7 +108,78 @@ namespace NonSymbolic { // } // }; boost::unordered_set configurations; - double absTime; std::size_t index = 0; + + /** + * Performs epsilon (unobservable) transitions starting from the given configurations. + * + * This method repeatedly explores transitions labeled with the unobservable action + * from all current configurations, advancing time according to clock guards, + * applying clock resets and symbolic updates, and collecting all reachable + * configurations. Exploration continues until no further epsilon transitions + * are possible. Whenever a target state marked as a match is reached, + * it notifies registered observers using the current index, absolute time, and valuations. + * + * @param currentConfigurations + * The initial set of configurations from which epsilon transitions + * are taken. The set is passed by value and moved into an internal + * worklist; it should not be used by the caller after this call. + * + * @return The set of configurations reachable via zero or more epsilon + * transitions that cannot be further extended by additional epsilon + * transitions. + * + */ + boost::unordered_set epsilonTransition(boost::unordered_set currentConfigurations) { + // the next configurations to explore + boost::unordered_set nextConfigurations; + // the configurations reachable via epsilon transitions + boost::unordered_set returnConfigurations; + + while (!currentConfigurations.empty()) { + nextConfigurations.clear(); + for (const Configuration &conf: currentConfigurations) { + auto transitionIt = std::get<0>(conf)->next.find(unobservableActionID); + if (transitionIt == std::get<0>(conf)->next.end()) { + continue; + } + // make the current env + const auto clockValuation = std::get<1>(conf); + const auto stringEnv = std::get<2>(conf); + const auto numberEnv = std::get<3>(conf); + for (const auto &transition: transitionIt->second) { + // evaluate the guards + auto nextCVal = clockValuation; + auto nextSEnv = stringEnv; + auto nextNEnv = numberEnv; + auto extendedGuard = transition.guard; + + auto absTime = std::get<4>(conf); + auto df = diff(nextCVal, extendedGuard); + if (!df) continue; + for (double &d: nextCVal) { + d += df.value(); + } + absTime += df.value(); + + if (eval(nextCVal, extendedGuard) && + eval(transition.stringConstraints, nextSEnv, transition.numConstraints, nextNEnv)) { + for (const VariableID resetVar: transition.resetVars) { + nextCVal[resetVar] = 0; + } + auto nextState = transition.target.lock(); + transition.update.execute(nextSEnv, nextNEnv); + nextConfigurations.insert({nextState, nextCVal, nextSEnv, nextNEnv, absTime}); + returnConfigurations.insert({nextState, nextCVal, nextSEnv, nextNEnv, absTime}); + if (nextState->isMatch) { + this->notifyObservers({index, absTime, nextNEnv, nextSEnv}); + } + } + } + } + std::swap(currentConfigurations, nextConfigurations); + } + return returnConfigurations; + } }; } // namespace NonSymbolic diff --git a/test/boolean_monitor_test.cc b/test/boolean_monitor_test.cc index ab5fda4..b42da39 100644 --- a/test/boolean_monitor_test.cc +++ b/test/boolean_monitor_test.cc @@ -1,121 +1,177 @@ #include "../src/boolean_monitor.hh" #include "../test/fixture/copy_automaton_fixture.hh" #include "../test/fixture/non_integer_timestamp_fixture.hh" +#include "../test/fixture/epsilon_transition_automaton_fixture.hh" #include "automaton.hh" #include "timed_word_parser.hh" #include #include +template +struct DummyTimedWordSubject : public SingleSubject { + DummyTimedWordSubject(std::vector &&vec) : vec(std::move(vec)) { + } + virtual ~DummyTimedWordSubject() { + } + void notifyAll() { + for (const auto &event: vec) { + this->notifyObservers(event); + } + vec.clear(); + } + std::vector vec; +}; + +template +struct DummyBooleanMonitorObserver : public Observer> { + DummyBooleanMonitorObserver() { + } + virtual ~DummyBooleanMonitorObserver() { + } + void notify(const BooleanMonitorResult &result) { + resultVec.push_back(result); + } + std::vector> resultVec; +}; + +template +struct BooleanMonitorFixture { + void feed(const NonParametricTA &automaton, std::vector &&vec) { + auto monitor = std::make_shared>(automaton); + std::shared_ptr> observer = std::make_shared>(); + monitor->addObserver(observer); + DummyTimedWordSubject subject{std::move(vec)}; + subject.addObserver(monitor); + subject.notifyAll(); + // Ensure the monitor's destructor runs now to emit epsilon-transition notifications + subject.addObserver(nullptr); // release subject's shared ownership + monitor.reset(); // release local ownership + resultVec = std::move(observer->resultVec); + } + std::vector> resultVec; +}; + namespace IntTest { using Number = int; using TimedWordEvent = TimedWordEvent; - - struct DummyTimedWordSubject : public SingleSubject { - DummyTimedWordSubject(std::vector &&vec) : vec(std::move(vec)) { - } - virtual ~DummyTimedWordSubject() { - } - void notifyAll() { - for (const auto &event: vec) { - notifyObservers(event); - } - vec.clear(); - } - std::vector vec; - }; - - struct DummyBooleanMonitorObserver : public Observer> { - DummyBooleanMonitorObserver() { - } - virtual ~DummyBooleanMonitorObserver() { - } - void notify(const BooleanMonitorResult &result) { - resultVec.push_back(result); - } - std::vector> resultVec; - }; - - struct CopyBooleanMonitorFixture : public CopyFixture { - void feed(std::vector &&vec) { - auto monitor = std::make_shared>(automaton); - std::shared_ptr observer = std::make_shared(); - monitor->addObserver(observer); - DummyTimedWordSubject subject{std::move(vec)}; - subject.addObserver(monitor); - subject.notifyAll(); - resultVec = std::move(observer->resultVec); - } - std::vector> resultVec; - }; + using BooleanMonitorFixture = BooleanMonitorFixture; BOOST_AUTO_TEST_SUITE(BooleanMonitorTest) - BOOST_FIXTURE_TEST_CASE(test1, CopyBooleanMonitorFixture) { + BOOST_FIXTURE_TEST_CASE(test1, BooleanMonitorFixture) + { std::vector dummyTimedWord(3); dummyTimedWord[0] = {0, {"x"}, {100}, 0.1}; dummyTimedWord[1] = {0, {"y"}, {200}, 10}; dummyTimedWord[2] = {0, {"x"}, {200}, 15}; - feed(std::move(dummyTimedWord)); + feed(CopyFixture().automaton, std::move(dummyTimedWord)); BOOST_TEST(resultVec.empty()); } - BOOST_FIXTURE_TEST_CASE(test2, CopyBooleanMonitorFixture) { + BOOST_FIXTURE_TEST_CASE(test2, BooleanMonitorFixture) + { std::vector dummyTimedWord(4); dummyTimedWord[0] = {0, {"x"}, {100}, 0.1}; dummyTimedWord[1] = {0, {"y"}, {200}, 10}; dummyTimedWord[2] = {0, {"x"}, {200}, 12}; dummyTimedWord[3] = {0, {"z"}, {200}, 15.5}; - feed(std::move(dummyTimedWord)); + feed(CopyFixture().automaton, std::move(dummyTimedWord)); BOOST_CHECK_EQUAL(resultVec.size(), 1); BOOST_CHECK_EQUAL(resultVec.front().index, 3); BOOST_CHECK_EQUAL(resultVec.front().timestamp, 15.5); } - BOOST_AUTO_TEST_SUITE_END() -} -namespace DoubleTest { - using Number = double; - using TimedWordEvent = TimedWordEvent; + BOOST_FIXTURE_TEST_CASE(epsilon_test1, BooleanMonitorFixture) + { + auto automaton = EpsilonTransitionAutomatonFixture::FIXTURE1.makeBooleanTA(); - struct DummyTimedWordSubject : public SingleSubject { - DummyTimedWordSubject(std::vector &&vec) : vec(std::move(vec)) { - } - virtual ~DummyTimedWordSubject() { - } - void notifyAll() { - for (const auto &event: vec) { - notifyObservers(event); - } - vec.clear(); - } - std::vector vec; - }; + std::vector timedWord{ + {0, {"c"}, {}, 1}, + {0, {"a"}, {}, 10}, + {0, {"b"}, {}, 12}, + {0, {"b"}, {}, 15}, + {0, {"c"}, {}, 20}, + {0, {"a"}, {}, 32}, + {0, {"b"}, {}, 40}, + {0, {"c"}, {}, 42}, + {0, {"a"}, {}, 51.5}, + {0, {"b"}, {}, 52}, + {0, {"a"}, {}, 53}, + {0, {"b"}, {}, 54}, + {0, {"c"}, {}, 55}, + }; + feed(automaton, std::move(timedWord)); - struct DummyBooleanMonitorObserver : public Observer> { - DummyBooleanMonitorObserver() { + BOOST_CHECK_EQUAL(resultVec.size(), 1); + BOOST_CHECK_EQUAL(resultVec.front().index, 6); + BOOST_CHECK_EQUAL(resultVec.front().timestamp, 40); } - virtual ~DummyBooleanMonitorObserver() { + + BOOST_FIXTURE_TEST_CASE(epsilon_test2, BooleanMonitorFixture) + { + auto automaton = EpsilonTransitionAutomatonFixture::FIXTURE2.makeBooleanTA(); + + std::vector timedWord{ + {0, {"a"}, {}, 0}, + {0, {"b"}, {}, 5}, + {0, {"a"}, {}, 10}, + {0, {"b"}, {}, 15}, + }; + feed(automaton, std::move(timedWord)); + + BOOST_CHECK_EQUAL(resultVec.size(), 2); + BOOST_CHECK_EQUAL(resultVec[0].index, 1); + BOOST_CHECK_EQUAL(resultVec[1].index, 3); } - void notify(const BooleanMonitorResult &result) { - resultVec.push_back(result); + + BOOST_FIXTURE_TEST_CASE(epsilon_test3, BooleanMonitorFixture) + { + auto automaton = EpsilonTransitionAutomatonFixture::FIXTURE3.makeBooleanTA(); + + std::vector timedWord{ + {0, {"a"}, {}, 0}, + {0, {"b"}, {}, 1}, + {0, {"c"}, {}, 7}, + {0, {"b"}, {}, 100}, + {0, {"a"}, {}, 101}, + {0, {"c"}, {}, 107}, + }; + feed(automaton, std::move(timedWord)); + + BOOST_CHECK_EQUAL(resultVec.size(), 1); + BOOST_CHECK_EQUAL(resultVec.front().index, 5); } - std::vector> resultVec; - }; - - struct NonIntegerTimestampBooleanMonitorFixture : public NonParametric::NonIntegerTimestampFixture { - void feed(std::vector &&vec) { - auto monitor = std::make_shared>(automaton); - std::shared_ptr observer = std::make_shared(); - monitor->addObserver(observer); - DummyTimedWordSubject subject{std::move(vec)}; - subject.addObserver(monitor); - subject.notifyAll(); - resultVec = std::move(observer->resultVec); + + BOOST_FIXTURE_TEST_CASE(epsilon_test4, BooleanMonitorFixture) + { + auto automaton = EpsilonTransitionAutomatonFixture::FIXTURE4.makeBooleanTA(); + + std::vector timedWord{ + {0, {"a"}, {}, 1.5}, + {0, {"b"}, {}, 2.5}, + {0, {"a"}, {}, 3.5}, + {0, {"b"}, {}, 4.5}, + }; + feed(automaton, std::move(timedWord)); + + BOOST_CHECK_EQUAL(resultVec.size(), 2); + BOOST_CHECK_EQUAL(resultVec[0].index, 2); + BOOST_CHECK_EQUAL(resultVec[0].timestamp, 5.5); + // The last index of timed word is 3, and it matches after the epsilon transition following the last event + BOOST_CHECK_EQUAL(resultVec[1].index, 4); + // The matched timestamp is 7.5 = 4.5 + 3 (the guard of epsilon transition is x0 == 3) + BOOST_CHECK_EQUAL(resultVec[1].timestamp, 7.5); } - std::vector> resultVec; - }; + + BOOST_AUTO_TEST_SUITE_END() +} + +namespace DoubleTest { + using Number = double; + using TimedWordEvent = TimedWordEvent; + using BooleanMonitorFixture = BooleanMonitorFixture; BOOST_AUTO_TEST_SUITE(BooleanMonitorTest) - BOOST_FIXTURE_TEST_CASE(non_integer_timestamp_test, NonIntegerTimestampBooleanMonitorFixture) { + BOOST_FIXTURE_TEST_CASE(non_integer_timestamp_test, BooleanMonitorFixture) { std::vector dummyTimedWord{ {0, {}, {0}, 0.}, {0, {}, {0}, 1.0}, @@ -123,7 +179,7 @@ namespace DoubleTest { {0, {}, {0}, 3.3}, {0, {}, {0}, 4.6} }; - feed(std::move(dummyTimedWord)); + feed(NonParametric::NonIntegerTimestampFixture().automaton, std::move(dummyTimedWord)); //NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched. //BOOST_CHECK_EQUAL(resultVec.size(), 1); BOOST_CHECK_EQUAL(resultVec.front().index, 2); diff --git a/test/data_parametric_monitor_test.cc b/test/data_parametric_monitor_test.cc index e9c60e5..cb60dab 100644 --- a/test/data_parametric_monitor_test.cc +++ b/test/data_parametric_monitor_test.cc @@ -2,7 +2,6 @@ #include #include "../src/data_parametric_monitor.hh" #include "../test/fixture/copy_automaton_fixture.hh" - #include "../test/fixture/non_integer_timestamp_fixture.hh" #include "../test/fixture/epsilon_transition_automaton_fixture.hh" @@ -73,7 +72,7 @@ BOOST_FIXTURE_TEST_CASE(test2, DataParametricMonitorFixture) BOOST_FIXTURE_TEST_CASE(epsilon_test1, DataParametricMonitorFixture) { - auto automaton = EpsilonTransitionAutomatonFixture::fixture1.makeDataParametricTA(); + auto automaton = EpsilonTransitionAutomatonFixture::FIXTURE1.makeDataParametricTA(); std::vector timedWord{ {0, {"c"}, {}, 1}, @@ -99,7 +98,7 @@ BOOST_FIXTURE_TEST_CASE(epsilon_test1, DataParametricMonitorFixture) BOOST_FIXTURE_TEST_CASE(epsilon_test2, DataParametricMonitorFixture) { - auto automaton = EpsilonTransitionAutomatonFixture::fixture2.makeDataParametricTA(); + auto automaton = EpsilonTransitionAutomatonFixture::FIXTURE2.makeDataParametricTA(); std::vector timedWord{ {0, {"a"}, {}, 0}, @@ -116,7 +115,7 @@ BOOST_FIXTURE_TEST_CASE(epsilon_test2, DataParametricMonitorFixture) BOOST_FIXTURE_TEST_CASE(epsilon_test3, DataParametricMonitorFixture) { - auto automaton = EpsilonTransitionAutomatonFixture::fixture3.makeDataParametricTA(); + auto automaton = EpsilonTransitionAutomatonFixture::FIXTURE3.makeDataParametricTA(); std::vector timedWord{ {0, {"a"}, {}, 0}, @@ -134,7 +133,7 @@ BOOST_FIXTURE_TEST_CASE(epsilon_test3, DataParametricMonitorFixture) BOOST_FIXTURE_TEST_CASE(epsilon_test4, DataParametricMonitorFixture) { - auto automaton = EpsilonTransitionAutomatonFixture::fixture4.makeDataParametricTA(); + auto automaton = EpsilonTransitionAutomatonFixture::FIXTURE4.makeDataParametricTA(); std::vector timedWord{ {0, {"a"}, {}, 1.5}, @@ -155,21 +154,8 @@ BOOST_FIXTURE_TEST_CASE(epsilon_test4, DataParametricMonitorFixture) BOOST_AUTO_TEST_SUITE_END() -struct NonIntegerTimestampDataParametricMonitorFixture : public Parametric::DataParametricNonIntegerTimestampFixture { - void feed(std::vector &&vec) { - auto monitor = std::make_shared(automaton); - std::shared_ptr observer = std::make_shared(); - monitor->addObserver(observer); - DummyDataTimedWordSubject subject{std::move(vec)}; - subject.addObserver(monitor); - subject.notifyAll(); - resultVec = std::move(observer->resultVec); - } - std::vector resultVec; -}; - BOOST_AUTO_TEST_SUITE(DataParametricNonIntegerTimestampMonitorTest) - BOOST_FIXTURE_TEST_CASE(non_integer_timestamp_test, NonIntegerTimestampDataParametricMonitorFixture) { + BOOST_FIXTURE_TEST_CASE(non_integer_timestamp_test, DataParametricMonitorFixture) { std::vector dummyTimedWord{ {0, {}, {0}, 0.}, {0, {}, {0}, 1.0}, @@ -177,7 +163,7 @@ BOOST_AUTO_TEST_SUITE(DataParametricNonIntegerTimestampMonitorTest) {0, {}, {0}, 3.3}, {0, {}, {0}, 4.6} }; - feed(std::move(dummyTimedWord)); + feed(Parametric::DataParametricNonIntegerTimestampFixture().automaton, std::move(dummyTimedWord)); //NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched. //BOOST_CHECK_EQUAL(resultVec.size(), 1); BOOST_CHECK_EQUAL(resultVec.front().index, 2); diff --git a/test/fixture/epsilon_transition_automaton_fixture.hh b/test/fixture/epsilon_transition_automaton_fixture.hh index e66c49f..4f5a82c 100644 --- a/test/fixture/epsilon_transition_automaton_fixture.hh +++ b/test/fixture/epsilon_transition_automaton_fixture.hh @@ -1,3 +1,5 @@ +#pragma once + #include #include #include @@ -21,7 +23,14 @@ class AutomatonFixture { public: AutomatonFixture(std::string dotStr):dotString(dotStr) {} - auto makeDataParametricTA() { + + auto makeBooleanTA() const { + using TAType = NonParametricTA; + using BoostTAType = NonParametricBoostTA; + return parseDotTA(dotString); + } + + auto makeDataParametricTA() const { using TAType = DataParametricTA; using BoostTAType = DataParametricBoostTA; return parseDotTA(dotString); @@ -29,7 +38,7 @@ class AutomatonFixture { }; namespace EpsilonTransitionAutomatonFixture { - const char dot_eps1[] = R"DOT(digraph G { + const char DOT_EPS1[] = R"DOT(digraph G { graph [ clock_variable_size = 1 string_variable_size = 1 @@ -48,10 +57,10 @@ namespace EpsilonTransitionAutomatonFixture { 3 -> 4 [label=0][s_constraints="{x1 == 'b'}"][guard="{x0 > 4}"] })DOT"; - auto fixture1 = AutomatonFixture(dot_eps1); + inline const AutomatonFixture FIXTURE1{DOT_EPS1}; //Epsilon transition with no guard - const char dot_eps2[] = R"DOT(digraph G { + const char DOT_EPS2[] = R"DOT(digraph G { graph [ clock_variable_size = 1 string_variable_size = 1 @@ -67,10 +76,10 @@ namespace EpsilonTransitionAutomatonFixture { 1 -> 2 [label=127][s_constraints="{x0 == 'z'}"] 2 -> 3 [label=0][s_constraints="{x1 == 'b', x0 == 'z'}"][guard="{x0 > 4}"] })DOT"; - auto fixture2 = AutomatonFixture(dot_eps2); + inline const AutomatonFixture FIXTURE2{DOT_EPS2}; // 2 clock variables - const char dot_eps3[] = R"DOT(digraph G { + const char DOT_EPS3[] = R"DOT(digraph G { graph [ clock_variable_size = 2 string_variable_size = 1 @@ -91,10 +100,10 @@ namespace EpsilonTransitionAutomatonFixture { 3 -> 4 [label=127][guard="{x0 == 2, x1 == 1}"] 4 -> 5 [label=0][s_constraints="{x1 == 'c'}"] })DOT"; - auto fixture3 = AutomatonFixture(dot_eps3); + inline const AutomatonFixture FIXTURE3{DOT_EPS3}; //Epsilon transition at last to accept state - const char dot_eps4[] = R"DOT(digraph G { + const char DOT_EPS4[] = R"DOT(digraph G { graph [ clock_variable_size = 1 string_variable_size = 1 @@ -109,6 +118,6 @@ namespace EpsilonTransitionAutomatonFixture { 1 -> 2 [label=127][guard="{x0 == 3}"] })DOT"; - auto fixture4 = AutomatonFixture(dot_eps4); + inline const AutomatonFixture FIXTURE4{DOT_EPS4}; } // namespace EpsilonTransitionAutomatonFixture