template timestamp

src/automata_operation.hh

@@ -3,6 +3,7 @@
 #include "automaton.hh"
 #include "common_types.hh"
 #include "parametric_timing_constraint.hh"
+#include "timing_constraint.hh"
 #include <ostream>
 #include <ppl.hh>
 
@@ -261,7 +262,7 @@ concatenate(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint,
     for (auto &[label, transitions]: sourceState->next) {
       for (auto &transition: transitions) {
         // Update the guard to include the new clock variable
-        if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint>>) {
+        if constexpr (is_vector_of_timingconstraint_v<TimingConstraint>) {
           transition.guard = adjustDimension(transition.guard, left.clockVariableSize);
         } else if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
           transition.guard = adjustDimension(transition.guard, left.clockVariableSize + left.parameterSize);
@@ -358,8 +359,9 @@ timeRestriction(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstra
 
   bool acceptEmpty = acceptsEmptyWord(given);
 
-  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint>>) {
-    TimingValuation clockValuation(given.clockVariableSize, 0);
+  if constexpr (is_vector_of_timingconstraint_v<TimingConstraint>) {
+    using TimeStamp = timingconstraint_timestamp_t<TimingConstraint>;
+    TimingValuation<TimeStamp> clockValuation(given.clockVariableSize, 0);
     acceptEmpty = acceptEmpty && eval(clockValuation, guard);
   }
   if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -375,7 +377,7 @@ timeRestriction(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstra
   auto newFinalState =
       std::make_shared<AutomatonState<StringConstraint, NumberConstraint, TimingConstraint, Update>>(true);
   given.states.push_back(newFinalState);
-  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint>>) {
+  if constexpr (is_vector_of_timingconstraint_v<TimingConstraint>) {
     guard = adjustDimension(guard, given.clockVariableSize); // Adjust the guard to include the new clock variable
   }
   if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -389,7 +391,7 @@ timeRestriction(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstra
       std::vector<AutomatonTransition<StringConstraint, NumberConstraint, TimingConstraint, Update>> newTransitions;
       for (auto it = transitions.begin(); it != transitions.end();) {
         // Update the guard to include the new clock variable
-        if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint>>) {
+        if constexpr (is_vector_of_timingconstraint_v<TimingConstraint>) {
           it->guard = adjustDimension(it->guard, given.clockVariableSize);
         }
         if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -480,7 +482,7 @@ addConstraintToAllTransitions(TimedAutomaton<StringConstraint, NumberConstraint,
 
   TimingConstraint adjustedConstraint = constraint;
   // Ensure the constraint has the correct dimension for the automaton
-  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint>>) {
+  if constexpr (is_vector_of_timingconstraint_v<TimingConstraint>) {
     adjustedConstraint = adjustDimension(constraint, automaton.clockVariableSize);
   } else if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
     adjustedConstraint = adjustDimension(constraint, automaton.parameterSize + automaton.clockVariableSize);
@@ -529,4 +531,4 @@ adjustAllDimensions(TimedAutomaton<StringConstraint, NumberConstraint, TimingCon
   }
 
   return automaton;
-}
+}

src/automaton.hh

@@ -137,21 +137,23 @@ struct TimedAutomaton<StringConstraint, NumberConstraint, ParametricTimingConstr
 #include "non_symbolic_string_constraint.hh"
 #include "non_symbolic_update.hh"
 
-template <typename Number>
+template <typename Number, typename Timestamp>
 using NonParametricTA = TimedAutomaton<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                                       std::vector<TimingConstraint>, NonSymbolic::Update<Number>>;
-template <typename Number>
+                                       std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>>;
+template <typename Number, typename Timestamp>
 using NonParametricTAState = AutomatonState<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                                            std::vector<TimingConstraint>, NonSymbolic::Update<Number>>;
+                                            std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>>;
 
 #include "symbolic_number_constraint.hh"
 #include "symbolic_string_constraint.hh"
 #include "symbolic_update.hh"
 
+template<typename Timestamp>
 using DataParametricTA = TimedAutomaton<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                        std::vector<TimingConstraint>, Symbolic::Update>;
+                                        std::vector<TimingConstraint<Timestamp>>, Symbolic::Update>;
+template<typename Timestamp>
 using DataParametricTAState = AutomatonState<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                             std::vector<TimingConstraint>, Symbolic::Update>;
+                                             std::vector<TimingConstraint<Timestamp>>, Symbolic::Update>;
 
 #include "parametric_timing_constraint.hh"
 

src/automaton_parser.hh

@@ -9,6 +9,7 @@
 #include "io_operators.hh"
 
 #include "parametric_timing_constraint_helper.hh"
+#include "timing_constraint.hh"
 
 namespace boost {
   using ::operator>>;
@@ -55,33 +56,35 @@ namespace boost {
   BOOST_INSTALL_PROPERTY(edge, guard);
 } // namespace boost
 
-static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint::Order &odr) {
+static inline std::ostream &operator<<(std::ostream &os, const TimingConstraintOrder &odr) {
   switch (odr) {
-    case TimingConstraint::Order::lt:
+    case TimingConstraintOrder::lt:
       os << "<";
       break;
-    case TimingConstraint::Order::le:
+    case TimingConstraintOrder::le:
       os << "<=";
       break;
-    case TimingConstraint::Order::ge:
+    case TimingConstraintOrder::ge:
       os << ">=";
       break;
-    case TimingConstraint::Order::gt:
+    case TimingConstraintOrder::gt:
       os << ">";
       break;
-    case TimingConstraint::Order::eq:
+    case TimingConstraintOrder::eq:
       os << "==";
       break;
   }
   return os;
 }
 
-static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint &p) {
+template <typename Timestamp>
+static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint<Timestamp> &p) {
   os << "x" << int(p.x) << " " << p.odr << " " << p.c;
   return os;
 }
 
-static inline std::istream &operator>>(std::istream &is, TimingConstraint &p) {
+template <typename Timestamp>
+static inline std::istream &operator>>(std::istream &is, TimingConstraint<Timestamp> &p) {
   if (is.get() != 'x') {
     is.setstate(std::ios_base::failbit);
     return is;
@@ -105,35 +108,35 @@ static inline std::istream &operator>>(std::istream &is, TimingConstraint &p) {
   switch (odr[0]) {
     case '>':
       if (odr[1] == '=') {
-        p.odr = TimingConstraint::Order::ge;
+        p.odr = TimingConstraintOrder::ge;
         if (is.get() != ' ') {
           is.setstate(std::ios_base::failbit);
           return is;
         }
       } else if (odr[1] == ' ') {
-        p.odr = TimingConstraint::Order::gt;
+        p.odr = TimingConstraintOrder::gt;
       } else {
         is.setstate(std::ios_base::failbit);
         return is;
       }
       break;
     case '<':
       if (odr[1] == '=') {
-        p.odr = TimingConstraint::Order::le;
+        p.odr = TimingConstraintOrder::le;
         if (is.get() != ' ') {
           is.setstate(std::ios_base::failbit);
           return is;
         }
       } else if (odr[1] == ' ') {
-        p.odr = TimingConstraint::Order::lt;
+        p.odr = TimingConstraintOrder::lt;
       } else {
         is.setstate(std::ios_base::failbit);
         return is;
       }
       break;
     case '=':
       if (odr[1] == '=') {
-        p.odr = TimingConstraint::Order::eq;
+        p.odr = TimingConstraintOrder::eq;
         if (is.get() != ' ') {
           is.setstate(std::ios_base::failbit);
           return is;
@@ -299,11 +302,13 @@ using BoostTimedAutomaton = boost::adjacency_list<
                     boost::property<boost::graph_string_variable_size_t, std::size_t,
                                     boost::property<boost::graph_number_variable_size_t, std::size_t>>>>;
 
-template <typename Number>
+template <typename Number, typename Timestamp>
 using NonParametricBoostTA = BoostTimedAutomaton<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                                                 TimingConstraint, NonSymbolic::Update<Number>>;
+                                                 TimingConstraint<Timestamp>, NonSymbolic::Update<Number>>;
+
+template <typename Timestamp>
 using DataParametricBoostTA =
-    BoostTimedAutomaton<Symbolic::StringConstraint, Symbolic::NumberConstraint, TimingConstraint, Symbolic::Update>;
+    BoostTimedAutomaton<Symbolic::StringConstraint, Symbolic::NumberConstraint, TimingConstraint<Timestamp>, Symbolic::Update>;
 using BoostPTA = boost::adjacency_list<
     boost::listS, boost::vecS, boost::directedS, BoostTAState,
     BoostTATransition<Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraintHelper,

src/boolean_monitor.hh

@@ -9,22 +9,22 @@
 #include "timed_word_subject.hh"
 #include <boost/unordered_set.hpp>
 
-template <class Number> struct BooleanMonitorResult {
+template <class Number, typename Timestamp> struct BooleanMonitorResult {
   std::size_t index;
-  double timestamp;
+  Timestamp timestamp;
   NonSymbolic::NumberValuation<Number> numberValuation;
   NonSymbolic::StringValuation stringValuation;
 };
 
 namespace NonSymbolic {
-  template <typename Number>
-  class BooleanMonitor : public SingleSubject<BooleanMonitorResult<Number>>, public Observer<TimedWordEvent<Number>> {
+  template <typename Number, typename Timestamp>
+  class BooleanMonitor : public SingleSubject<BooleanMonitorResult<Number, Timestamp>>, public Observer<TimedWordEvent<Number, Timestamp>> {
   public:
     static const constexpr std::size_t unobservableActionID = 127;
-    BooleanMonitor(const NonParametricTA<Number> &automaton) : automaton(automaton) {
+    BooleanMonitor(const NonParametricTA<Number, Timestamp> &automaton) : automaton(automaton) {
       configurations.clear();
       // configurations.reserve(automaton.initialStates.size());
-      std::vector<double> initCVal(automaton.clockVariableSize);
+      std::vector<Timestamp> initCVal(automaton.clockVariableSize);
       // by default, initSEnv is no violating set (variant)
       StringValuation initSEnv(automaton.stringVariableSize);
       // by default, initNEnv is unset (optional)
@@ -36,11 +36,11 @@ namespace NonSymbolic {
     virtual ~BooleanMonitor() {
       epsilonTransition(configurations);
     }
-    void notify(const TimedWordEvent<Number> &event) {
+    void notify(const TimedWordEvent<Number, Timestamp> &event) {
       const Action actionId = event.actionId;
       const std::vector<std::string> &strings = event.strings;
       const std::vector<Number> &numbers = event.numbers;
-      const double timestamp = event.timestamp;
+      const Timestamp timestamp = event.timestamp;
 
       boost::unordered_set<Configuration> nextConfigurations;
       configurations.merge(epsilonTransition(configurations));
@@ -52,7 +52,7 @@ namespace NonSymbolic {
         if (timestamp < absTime) {
           continue;
         }
-        for (double &d: clockValuation) {
+        for (Timestamp &d: clockValuation) {
           d += timestamp - absTime;
         }
         auto stringEnv = std::get<2>(conf); // conf.stringEnv;
@@ -94,12 +94,12 @@ namespace NonSymbolic {
     }
 
   private:
-    const NonParametricTA<Number> automaton;
-    using Configuration = std::tuple<std::shared_ptr<NonParametricTAState<Number>>, std::vector<double>,
+    const NonParametricTA<Number, Timestamp> automaton;
+    using Configuration = std::tuple<std::shared_ptr<NonParametricTAState<Number, Timestamp>>, std::vector<Timestamp>,
                                      StringValuation, NumberValuation<Number>, double>;
     // struct Configuration {
     //   std::shared_ptr<AutomatonState<Number>> state;
-    //   std::vector<double> clockValuation;
+    //   std::vector<Timestamp> clockValuation;
     //   StringValuation stringEnv;
     //   NumberValuation<Number> numberEnv;
     //   bool operator==(const Configuration x) const {

src/data_parametric_monitor.hh

@@ -7,6 +7,7 @@
 #include "symbolic_number_constraint.hh"
 #include "symbolic_string_constraint.hh"
 #include "symbolic_update.hh"
+#include "timed_word_parser.hh"
 #include "timed_word_subject.hh"
 
 namespace Parma_Polyhedra_Library {
@@ -17,21 +18,23 @@ namespace Parma_Polyhedra_Library {
 
 #include <boost/unordered_set.hpp>
 
+template <typename Timestamp>
 struct DataParametricMonitorResult {
   std::size_t index;
-  double timestamp;
+  Timestamp timestamp;
   Symbolic::NumberValuation numberValuation;
   Symbolic::StringValuation stringValuation;
 };
 
-class DataParametricMonitor : public SingleSubject<DataParametricMonitorResult>,
-                              public Observer<TimedWordEvent<PPLRational>> {
+template<typename Timestamp>
+class DataParametricMonitor : public SingleSubject<DataParametricMonitorResult<Timestamp>>,
+                              public Observer<TimedWordEvent<PPLRational, Timestamp>> {
 public:
   static const constexpr std::size_t unobservableActionID = 127;
-  explicit DataParametricMonitor(const DataParametricTA &automaton) : automaton(automaton) {
+  explicit DataParametricMonitor(const DataParametricTA<Timestamp> &automaton) : automaton(automaton) {
     configurations.clear();
     // configurations.reserve(automaton.initialStates.size());
-    std::vector<double> initCVal(automaton.clockVariableSize);
+    std::vector<Timestamp> initCVal(automaton.clockVariableSize);
     // by default, initSEnv is no violating set (variant)
     Symbolic::StringValuation initSEnv(automaton.stringVariableSize);
     // by default, initNEnv is the universe of dimension automaton.numberVariableSize
@@ -45,11 +48,11 @@ public:
     epsilonTransition(configurations);
   }
 
-  void notify(const TimedWordEvent<PPLRational> &event) override {
+  void notify(const TimedWordEvent<PPLRational, Timestamp> &event) override {
     const Action actionId = event.actionId;
     const std::vector<std::string> &strings = event.strings;
     const std::vector<PPLRational> &numbers = event.numbers;
-    const double timestamp = event.timestamp;
+    const Timestamp timestamp = event.timestamp;
 
     boost::unordered_set<Configuration> nextConfigurations;
     configurations.merge(epsilonTransition(configurations));
@@ -61,7 +64,7 @@ public:
       if (timestamp < absTime) {
         continue;
       }
-      for (double &d: clockValuation) {
+      for (Timestamp &d: clockValuation) {
         d += timestamp - absTime;
       }
       auto stringEnv = std::get<2>(conf); //.stringEnv;
@@ -93,7 +96,7 @@ public:
           nextNEnv.remove_higher_space_dimensions(automaton.numberVariableSize);
           nextConfigurations.insert({transition.target.lock(), std::move(nextCVal), nextSEnv, nextNEnv, timestamp});
           if (transition.target.lock()->isMatch) {
-            notifyObservers({index, timestamp, nextNEnv, nextSEnv});
+            this->notifyObservers({index, timestamp, nextNEnv, nextSEnv});
           }
         }
       }
@@ -103,13 +106,13 @@ public:
   }
 
 private:
-  const DataParametricTA automaton;
-  using Configuration = std::tuple<std::shared_ptr<DataParametricTAState>, std::vector<double>,
+  const DataParametricTA<Timestamp> automaton;
+  using Configuration = std::tuple<std::shared_ptr<DataParametricTAState<Timestamp>>, std::vector<Timestamp>,
                                    Symbolic::StringValuation, Symbolic::NumberValuation, double>;
   // Symbolic::NumberValuation>;
   /*  struct Configuration {
       std::shared_ptr<DataParametricTAState> state;
-      std::vector<double> clockValuation;
+      std::vector<Timestamp> clockValuation;
       NonSymbolic::StringValuation stringEnv;
       Symbolic::NumberValuation numberEnv;
     };*/