From e59dff7b1a66405afeaa40a6ea6f1ea52d976e48 Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Wed, 19 Nov 2025 20:47:44 +0900
Subject: [PATCH 01/14] Experimental Implementation

---
 src/automata_operation.hh | 20 +++++++--------
 src/automaton.hh          |  8 +++---
 src/automaton_parser.hh   | 53 ++++++++++++++++++++++++++++-----------
 src/main.cc               | 20 +++++++--------
 src/symon_parser.hh       | 24 +++++++++---------
 src/timing_constraint.hh  | 45 ++++++++++++++++++++-------------
 6 files changed, 101 insertions(+), 69 deletions(-)

diff --git a/src/automata_operation.hh b/src/automata_operation.hh
index 2862afa..7c9d700 100644
--- a/src/automata_operation.hh
+++ b/src/automata_operation.hh
@@ -177,7 +177,7 @@ bool acceptsEmptyWord(const TimedAutomaton<StringConstraint, NumberConstraint, T
  * @param[in] right  The second (right-hand) timed automaton.
  * @return A TimedAutomaton representing the concatenation of two automata.
  */
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Time>
 TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update>
 concatenate(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &&left,
             TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &&right) {
@@ -261,7 +261,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 (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Time>>>) {
           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);
@@ -350,7 +350,7 @@ star(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update
  * @param[in] guard The timing constraint that restricts the time.
  * @return A TimedAutomaton with the new timing constraint on the total elapsed time.
  */
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Time>
 TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update>
 timeRestriction(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &&given,
                 TimingConstraint guard) {
@@ -358,8 +358,8 @@ 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 (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Time>>>) {
+    TimingValuation<Time> clockValuation(given.clockVariableSize, 0);
     acceptEmpty = acceptEmpty && eval(clockValuation, guard);
   }
   if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -375,7 +375,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 (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Time>>>) {
     guard = adjustDimension(guard, given.clockVariableSize); // Adjust the guard to include the new clock variable
   }
   if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -389,7 +389,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 (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Time>>>) {
           it->guard = adjustDimension(it->guard, given.clockVariableSize);
         }
         if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -473,14 +473,14 @@ ignoreActions(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstrain
  * @param[in] constraint The timing constraint to add to all transitions.
  * @return A reference to the modified automaton.
  */
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Time>
 TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &
 addConstraintToAllTransitions(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &automaton,
                               const TimingConstraint &constraint) {
 
   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 (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Time>>>) {
     adjustedConstraint = adjustDimension(constraint, automaton.clockVariableSize);
   } else if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
     adjustedConstraint = adjustDimension(constraint, automaton.parameterSize + automaton.clockVariableSize);
@@ -529,4 +529,4 @@ adjustAllDimensions(TimedAutomaton<StringConstraint, NumberConstraint, TimingCon
   }
 
   return automaton;
-}
\ No newline at end of file
+}
diff --git a/src/automaton.hh b/src/automaton.hh
index f350d51..2a6afe7 100644
--- a/src/automaton.hh
+++ b/src/automaton.hh
@@ -139,19 +139,19 @@ struct TimedAutomaton<StringConstraint, NumberConstraint, ParametricTimingConstr
 
 template <typename Number>
 using NonParametricTA = TimedAutomaton<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                                       std::vector<TimingConstraint>, NonSymbolic::Update<Number>>;
+                                       std::vector<TimingConstraint<Number>>, NonSymbolic::Update<Number>>;
 template <typename Number>
 using NonParametricTAState = AutomatonState<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                                            std::vector<TimingConstraint>, NonSymbolic::Update<Number>>;
+                                            std::vector<TimingConstraint<Number>>, NonSymbolic::Update<Number>>;
 
 #include "symbolic_number_constraint.hh"
 #include "symbolic_string_constraint.hh"
 #include "symbolic_update.hh"
 
 using DataParametricTA = TimedAutomaton<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                        std::vector<TimingConstraint>, Symbolic::Update>;
+                                        std::vector<TimingConstraint<double>>, Symbolic::Update>;
 using DataParametricTAState = AutomatonState<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                             std::vector<TimingConstraint>, Symbolic::Update>;
+                                             std::vector<TimingConstraint<double>>, Symbolic::Update>;
 
 #include "parametric_timing_constraint.hh"
 
diff --git a/src/automaton_parser.hh b/src/automaton_parser.hh
index d3507e0..5754adb 100644
--- a/src/automaton_parser.hh
+++ b/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,18 +56,19 @@ namespace boost {
   BOOST_INSTALL_PROPERTY(edge, guard);
 } // namespace boost
 
-static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint::Order &odr) {
+template <typename Time>
+static inline std::ostream &operator<<(std::ostream &os, const typename TimingConstraint<Time>::Order &odr) {
   switch (odr) {
-    case TimingConstraint::Order::lt:
+    case TimingConstraint<Time>::Order::lt:
       os << "<";
       break;
-    case TimingConstraint::Order::le:
+    case TimingConstraint<Time>::Order::le:
       os << "<=";
       break;
-    case TimingConstraint::Order::ge:
+    case TimingConstraint<Time>::Order::ge:
       os << ">=";
       break;
-    case TimingConstraint::Order::gt:
+    case TimingConstraint<Time>::Order::gt:
       os << ">";
       break;
     case TimingConstraint::Order::eq:
@@ -76,12 +78,32 @@ static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint:
   return os;
 }
 
-static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint &p) {
+static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint<double>::Order &odr) {
+  switch (odr) {
+    case TimingConstraint<double>::Order::lt:
+      os << "<";
+      break;
+    case TimingConstraint<double>::Order::le:
+      os << "<=";
+      break;
+    case TimingConstraint<double>::Order::ge:
+      os << ">=";
+      break;
+    case TimingConstraint<double>::Order::gt:
+      os << ">";
+      break;
+  }
+  return os;
+}
+
+template <typename Time>
+static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint<Time> &p) {
   os << "x" << int(p.x) << " " << p.odr << " " << p.c;
   return os;
 }
 
-static inline std::istream &operator>>(std::istream &is, TimingConstraint &p) {
+template <typename Time>
+static inline std::istream &operator>>(std::istream &is, TimingConstraint<Time> &p) {
   if (is.get() != 'x') {
     is.setstate(std::ios_base::failbit);
     return is;
@@ -105,13 +127,13 @@ static inline std::istream &operator>>(std::istream &is, TimingConstraint &p) {
   switch (odr[0]) {
     case '>':
       if (odr[1] == '=') {
-        p.odr = TimingConstraint::Order::ge;
+        p.odr = TimingConstraint<Time>::Order::ge;
         if (is.get() != ' ') {
           is.setstate(std::ios_base::failbit);
           return is;
         }
       } else if (odr[1] == ' ') {
-        p.odr = TimingConstraint::Order::gt;
+        p.odr = TimingConstraint<Time>::Order::gt;
       } else {
         is.setstate(std::ios_base::failbit);
         return is;
@@ -119,13 +141,13 @@ static inline std::istream &operator>>(std::istream &is, TimingConstraint &p) {
       break;
     case '<':
       if (odr[1] == '=') {
-        p.odr = TimingConstraint::Order::le;
+        p.odr = TimingConstraint<Time>::Order::le;
         if (is.get() != ' ') {
           is.setstate(std::ios_base::failbit);
           return is;
         }
       } else if (odr[1] == ' ') {
-        p.odr = TimingConstraint::Order::lt;
+        p.odr = TimingConstraint<Time>::Order::lt;
       } else {
         is.setstate(std::ios_base::failbit);
         return is;
@@ -299,11 +321,12 @@ 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>>;
-using DataParametricBoostTA =
-    BoostTimedAutomaton<Symbolic::StringConstraint, Symbolic::NumberConstraint, TimingConstraint, Symbolic::Update>;
+                                                 TimingConstraint<Timestamp>, NonSymbolic::Update<Number>>;
+template <typename Time>
+                                                 using DataParametricBoostTA =
+    BoostTimedAutomaton<Symbolic::StringConstraint, Symbolic::NumberConstraint, TimingConstraint<Time>, Symbolic::Update>;
 using BoostPTA = boost::adjacency_list<
     boost::listS, boost::vecS, boost::directedS, BoostTAState,
     BoostTATransition<Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraintHelper,
diff --git a/src/main.cc b/src/main.cc
index b3af369..0845f76 100644
--- a/src/main.cc
+++ b/src/main.cc
@@ -35,7 +35,7 @@ using ::operator<<;
  */
 template <typename TAType, typename BoostTAType, typename Number, typename Timestamp, typename Monitor,
           typename Printer, typename StringConstraint, typename NumberConstraint, typename TimingConstraintType,
-          typename UpdateType>
+          typename UpdateType, typename Time>
 int execute(const std::string &timedAutomatonFileName, const std::string &signatureFileName,
             const std::string &timedWordFileName, bool useNewSyntax = false) {
   TAType TA;
@@ -50,7 +50,7 @@ int execute(const std::string &timedAutomatonFileName, const std::string &signat
 
   if (useNewSyntax) {
     // Use the new syntax parser
-    SymonParser<StringConstraint, NumberConstraint, TimingConstraintType, UpdateType> parser;
+    SymonParser<StringConstraint, NumberConstraint, TimingConstraintType, UpdateType, Time> parser;
     try {
       parser.parse(taStream);
     } catch (const std::runtime_error &e) {
@@ -166,36 +166,36 @@ int main(int argc, char *argv[]) {
       // parametric with new syntax
       return execute<ParametricTA, BoostPTA, PPLRational, PPLRational, ParametricMonitor, ParametricPrinter,
                      Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
-                     Symbolic::Update>(timedAutomatonFileName, signatureFileName, timedWordFileName, true);
+                     Symbolic::Update, Parma_Polyhedra_Library::NNC_Polyhedron>(timedAutomatonFileName, signatureFileName, timedWordFileName, true);
     } else if (vm.count("dataparametric")) {
       // data parametric with new syntax
-      return execute<DataParametricTA, DataParametricBoostTA, PPLRational, double, DataParametricMonitor,
+      return execute<DataParametricTA, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor,
                      DataParametricPrinter, Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                     std::vector<TimingConstraint>, Symbolic::Update>(timedAutomatonFileName, signatureFileName,
+                     std::vector<TimingConstraint<Number>>, Symbolic::Update, Number>(timedAutomatonFileName, signatureFileName,
                                                                       timedWordFileName, true);
     } else {
       // boolean with new syntax
       return execute<NonParametricTA<Number>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number>,
                      BooleanPrinter<Number>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                     std::vector<TimingConstraint>, NonSymbolic::Update<Number>>(timedAutomatonFileName, signatureFileName,
+                     std::vector<TimingConstraint<Number>>, NonSymbolic::Update<Number>, Number>(timedAutomatonFileName, signatureFileName,
                                                                          timedWordFileName, true);
     }
   } else if (vm.count("parametric")) {
     // parametric
     return execute<ParametricTA, BoostPTA, PPLRational, PPLRational, ParametricMonitor, ParametricPrinter,
                    Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
-                   Symbolic::Update>(timedAutomatonFileName, signatureFileName, timedWordFileName, false);
+                   Symbolic::Update, Parma_Polyhedra_Library::NNC_Polyhedron>(timedAutomatonFileName, signatureFileName, timedWordFileName, false);
   } else if (vm.count("dataparametric")) {
     // data parametric
-    return execute<DataParametricTA, DataParametricBoostTA, PPLRational, double, DataParametricMonitor,
+    return execute<DataParametricTA, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor,
                    DataParametricPrinter, Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                   std::vector<TimingConstraint>, Symbolic::Update>(timedAutomatonFileName, signatureFileName,
+                   std::vector<TimingConstraint<Number>>, Symbolic::Update, Number>(timedAutomatonFileName, signatureFileName,
                                                                     timedWordFileName, false);
   } else {
     // boolean
     return execute<NonParametricTA<Number>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number>,
                    BooleanPrinter<Number>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                   std::vector<TimingConstraint>, NonSymbolic::Update<Number>>(timedAutomatonFileName, signatureFileName,
+                   std::vector<TimingConstraint<Number>>, NonSymbolic::Update<Number>, Number>(timedAutomatonFileName, signatureFileName,
                                                                        timedWordFileName, false);
   }
   return 0;
diff --git a/src/symon_parser.hh b/src/symon_parser.hh
index ec63c9e..e120f78 100644
--- a/src/symon_parser.hh
+++ b/src/symon_parser.hh
@@ -78,7 +78,7 @@ static inline TSNode nextNonCommentChild(const TSNode &parent, uint32_t &idx) {
   return std::nullopt;
 }
 
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Time>
 class SymonParser {
 public:
   using Automaton = TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update>;
@@ -196,13 +196,13 @@ public:
 
 public:
   // Helper function to extract the upper bound from a non-parametric timing constraint
-  static std::vector<::TimingConstraint> extractUpperBound(const std::vector<::TimingConstraint> &guard) {
-    std::vector<::TimingConstraint> upperBound;
+  static std::vector<::TimingConstraint<Time>> extractUpperBound(const std::vector<::TimingConstraint<Time>> &guard) {
+    std::vector<::TimingConstraint<Time>> upperBound;
 
     // Check each constraint in the guard
     for (const auto &constraint: guard) {
       // If the constraint is an upper bound (lt or le), add it to the result
-      if (constraint.odr == ::TimingConstraint::Order::lt || constraint.odr == ::TimingConstraint::Order::le) {
+      if (constraint.odr == ::TimingConstraint<Time>::Order::lt || constraint.odr == ::TimingConstraint<Time>::Order::le) {
         upperBound.push_back(constraint);
       }
     }
@@ -597,9 +597,9 @@ private:
           throw err;
         }
       } else {
-        return {boost::lexical_cast<::TimingConstraint>("x" + std::to_string(clockIndex) + " " +
+        return {boost::lexical_cast<::TimingConstraint<Time>>("x" + std::to_string(clockIndex) + " " +
                                                         (isLowerInclusive ? ">=" : ">") + " " + lowerBound),
-                boost::lexical_cast<::TimingConstraint>("x" + std::to_string(clockIndex) + " " +
+                boost::lexical_cast<::TimingConstraint<Time>>("x" + std::to_string(clockIndex) + " " +
                                                         (isUpperInclusive ? "<=" : "<") + " " + upperBound)};
       }
     }
@@ -629,7 +629,7 @@ private:
         return result;
       } else {
         return {
-            boost::lexical_cast<::TimingConstraint>("x" + std::to_string(clockIndex) + " " + comparator + " " + expr)};
+            boost::lexical_cast<::TimingConstraint<Time>>("x" + std::to_string(clockIndex) + " " + comparator + " " + expr)};
       }
     }
     throw std::runtime_error(makeErrorMessage(
@@ -837,7 +837,7 @@ private:
       TSNode rhsNode = nextNonCommentChild(child, p);
       Automaton lhs = this->parseExpr(content, lhsNode);
       Automaton rhs = this->parseExpr(content, rhsNode);
-      return concatenate(std::move(lhs), std::move(rhs));
+      return concatenate<StringConstraint, NumberConstraint, TimingConstraint, Update, Time>(std::move(lhs), std::move(rhs));
     } else if (kind == "conjunction") {
       uint32_t p = 0;
       TSNode lhsNode = nextNonCommentChild(child, p);
@@ -991,7 +991,7 @@ private:
       TimingConstraint guard = this->parseTimingConstraint(content, intervalNode, innerExpr.clockVariableSize);
 
       // Apply the time restriction operation
-      Automaton result = timeRestriction(std::move(innerExpr), guard);
+      Automaton result = timeRestriction<StringConstraint, NumberConstraint, TimingConstraint, Update, Time>(std::move(innerExpr), guard);
 
       if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
         assert(std::all_of(result.states.begin(), result.states.end(), [&](const auto &state) {
@@ -1005,17 +1005,17 @@ private:
       }
 
       // Extract the upper bound from the timing constraint and add it to all transitions
-      if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint>>) {
+      if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Time>>>) {
         // For non-parametric timing constraints
         auto upperBound = extractUpperBound(guard);
         if (!upperBound.empty()) {
           // It has an upper bound, add it to all transitions
-          addConstraintToAllTransitions(result, upperBound);
+          addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update, Time>(result, upperBound);
         }
       } else if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
         // For parametric timing constraints
         auto upperBound = extractUpperBound(guard, this->parameters.size() + innerExpr.clockVariableSize - 1);
-        addConstraintToAllTransitions(result, upperBound);
+        addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update, Time>(result, upperBound);
       }
 
       if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
diff --git a/src/timing_constraint.hh b/src/timing_constraint.hh
index 0d9dc90..a29d37f 100644
--- a/src/timing_constraint.hh
+++ b/src/timing_constraint.hh
@@ -16,6 +16,7 @@ inline bool toBool(Order odr) {
 }
 
 //! @brief A constraint in a guard of transitions
+template <typename Time>
 struct TimingConstraint {
   enum class Order { lt, le, ge, gt, eq };
   using Timestamp = double;
@@ -76,20 +77,24 @@ public:
   explicit ConstraintMaker(ClockVariables x) : x(x) {
   }
 
-  TimingConstraint operator<(Timestamp c) {
-    return TimingConstraint{x, TimingConstraint::Order::lt, c};
+  template<typename Time>
+  TimingConstraint<Time> operator<(Time c) {
+    return TimingConstraint{x, TimingConstraint<Time>::Order::lt, c};
   }
 
-  TimingConstraint operator<=(Timestamp c) {
-    return TimingConstraint{x, TimingConstraint::Order::le, c};
+  template<typename Time>
+  TimingConstraint<Time> operator<=(Time c) {
+    return TimingConstraint{x, TimingConstraint<Time>::Order::le, c};
   }
 
-  TimingConstraint operator>(Timestamp c) {
-    return TimingConstraint{x, TimingConstraint::Order::gt, c};
+  template<typename Time>
+  TimingConstraint<Time> operator>(Time c) {
+    return TimingConstraint<Time>{x, TimingConstraint<Time>::Order::gt, c};
   }
 
-  TimingConstraint operator>=(Timestamp c) {
-    return TimingConstraint{x, TimingConstraint::Order::ge, c};
+  template<typename Time>
+  TimingConstraint<Time> operator>=(Time c) {
+    return TimingConstraint<Time>{x, TimingConstraint<Time>::Order::ge, c};
   }
 
   TimingConstraint operator==(Timestamp c) {
@@ -105,12 +110,13 @@ public:
 //         return g.odr == TimingConstraint::Order::ge || g.odr == TimingConstraint::Order::gt;
 //     }), guard.end());
 // }
+template <typename Time>
+using TimingValuation = std::vector<Time>;
 
-using TimingValuation = std::vector<TimingConstraint::Timestamp>;
-
-static bool eval(const TimingValuation &clockValuation, const std::vector<TimingConstraint> &guard) {
+template<typename Time>
+static bool eval(const TimingValuation<Time> &clockValuation, const std::vector<TimingConstraint<Time>> &guard) {
   return std::all_of(guard.begin(), guard.end(),
-                     [&clockValuation](const TimingConstraint &g) { return g.satisfy(clockValuation.at(g.x)); });
+                     [&clockValuation](const TimingConstraint<Time> &g) { return g.satisfy(clockValuation.at(g.x)); });
 }
 
 /*!
@@ -148,8 +154,9 @@ static std::optional<double> diff(const TimingValuation &clockValuation, const s
  * @param width the width to shift the clock variable id
  * @return a new vector of TimingConstraint with the clock variables shifted
  */
-static std::vector<TimingConstraint> shift(const std::vector<TimingConstraint> &guard, const ClockVariables width) {
-  std::vector<TimingConstraint> shiftedGuard;
+template<typename Time>
+static std::vector<TimingConstraint<Time>> shift(const std::vector<TimingConstraint<Time>> &guard, const ClockVariables width) {
+  std::vector<TimingConstraint<Time>> shiftedGuard;
   shiftedGuard.reserve(guard.size());
   for (const auto &g: guard) {
     shiftedGuard.push_back(g.shift(width));
@@ -165,9 +172,10 @@ static std::vector<TimingConstraint> shift(const std::vector<TimingConstraint> &
  * @param right the second vector of TimingConstraint
  * @return a new vector containing all TimingConstraints from both vectors
  */
-static std::vector<TimingConstraint> operator&&(const std::vector<TimingConstraint> &left,
-                                                const std::vector<TimingConstraint> &right) {
-  std::vector<TimingConstraint> result = left;
+ template<typename Time>
+static std::vector<TimingConstraint<Time>> operator&&(const std::vector<TimingConstraint<Time>> &left,
+                                                const std::vector<TimingConstraint<Time>> &right) {
+  std::vector<TimingConstraint<Time>> result = left;
   result.reserve(left.size() + right.size());
   std::copy_if(right.begin(), right.end(), std::back_inserter(result),
                [&left](const auto &guard) { return std::find(left.begin(), left.end(), guard) == left.end(); });
@@ -181,7 +189,8 @@ static std::vector<TimingConstraint> operator&&(const std::vector<TimingConstrai
  * @param size the size to adjust the guard to
  * @return a new vector of TimingConstraint with the clock variables adjusted
  */
-static std::vector<TimingConstraint> adjustDimension(const std::vector<TimingConstraint> &guard,
+template<typename Time>
+static std::vector<TimingConstraint<Time>> adjustDimension(const std::vector<TimingConstraint<Time>> &guard,
                                                      const ClockVariables size) {
   return guard;
 }

From 69346f90f31795cb88fda85418902465b001a414 Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Tue, 25 Nov 2025 00:09:33 +0900
Subject: [PATCH 02/14] Update : add typename Time

Related #11
---
 src/automaton.hh               | 14 ++++++++------
 src/boolean_monitor.hh         | 11 ++++++-----
 src/data_parametric_monitor.hh | 10 ++++++----
 src/main.cc                    | 17 +++++++++--------
 4 files changed, 29 insertions(+), 23 deletions(-)

diff --git a/src/automaton.hh b/src/automaton.hh
index 2a6afe7..cc2f9de 100644
--- a/src/automaton.hh
+++ b/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 Time>
 using NonParametricTA = TimedAutomaton<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                                       std::vector<TimingConstraint<Number>>, NonSymbolic::Update<Number>>;
-template <typename Number>
+                                       std::vector<TimingConstraint<Time>>, NonSymbolic::Update<Number>>;
+template <typename Number, typename Time>
 using NonParametricTAState = AutomatonState<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                                            std::vector<TimingConstraint<Number>>, NonSymbolic::Update<Number>>;
+                                            std::vector<TimingConstraint<Time>>, NonSymbolic::Update<Number>>;
 
 #include "symbolic_number_constraint.hh"
 #include "symbolic_string_constraint.hh"
 #include "symbolic_update.hh"
 
+template<typename Time>
 using DataParametricTA = TimedAutomaton<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                        std::vector<TimingConstraint<double>>, Symbolic::Update>;
+                                        std::vector<TimingConstraint<Time>>, Symbolic::Update>;
+template<typename Time>
 using DataParametricTAState = AutomatonState<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                             std::vector<TimingConstraint<double>>, Symbolic::Update>;
+                                             std::vector<TimingConstraint<Time>>, Symbolic::Update>;
 
 #include "parametric_timing_constraint.hh"
 
diff --git a/src/boolean_monitor.hh b/src/boolean_monitor.hh
index a8d26ef..dfde345 100644
--- a/src/boolean_monitor.hh
+++ b/src/boolean_monitor.hh
@@ -17,11 +17,11 @@ template <class Number> struct BooleanMonitorResult {
 };
 
 namespace NonSymbolic {
-  template <typename Number>
+  template <typename Number, typename Time>
   class BooleanMonitor : public SingleSubject<BooleanMonitorResult<Number>>, public Observer<TimedWordEvent<Number>> {
   public:
     static const constexpr std::size_t unobservableActionID = 127;
-    BooleanMonitor(const NonParametricTA<Number> &automaton) : automaton(automaton) {
+    BooleanMonitor(const NonParametricTA<Number, Time> &automaton) : automaton(automaton) {
       configurations.clear();
       // configurations.reserve(automaton.initialStates.size());
       std::vector<double> initCVal(automaton.clockVariableSize);
@@ -94,9 +94,10 @@ namespace NonSymbolic {
     }
 
   private:
-    const NonParametricTA<Number> automaton;
-    using Configuration = std::tuple<std::shared_ptr<NonParametricTAState<Number>>, std::vector<double>,
-                                     StringValuation, NumberValuation<Number>, double>;
+
+    const NonParametricTA<Number, Time> automaton;
+    using Configuration = std::tuple<std::shared_ptr<NonParametricTAState<Number, Time>>, std::vector<double>,
+                                     StringValuation, NumberValuation<Number>, double>>;
     // struct Configuration {
     //   std::shared_ptr<AutomatonState<Number>> state;
     //   std::vector<double> clockValuation;
diff --git a/src/data_parametric_monitor.hh b/src/data_parametric_monitor.hh
index 79be6a2..bcc3384 100644
--- a/src/data_parametric_monitor.hh
+++ b/src/data_parametric_monitor.hh
@@ -24,11 +24,13 @@ struct DataParametricMonitorResult {
   Symbolic::StringValuation stringValuation;
 };
 
+template<typename Time>
 class DataParametricMonitor : public SingleSubject<DataParametricMonitorResult>,
                               public Observer<TimedWordEvent<PPLRational>> {
 public:
   static const constexpr std::size_t unobservableActionID = 127;
-  explicit DataParametricMonitor(const DataParametricTA &automaton) : automaton(automaton) {
+  explicit DataParametricMonitor(const DataParametricTA<Time> &automaton) : automaton(automaton) {
+    absTime = 0;
     configurations.clear();
     // configurations.reserve(automaton.initialStates.size());
     std::vector<double> initCVal(automaton.clockVariableSize);
@@ -103,9 +105,9 @@ public:
   }
 
 private:
-  const DataParametricTA automaton;
-  using Configuration = std::tuple<std::shared_ptr<DataParametricTAState>, std::vector<double>,
-                                   Symbolic::StringValuation, Symbolic::NumberValuation, double>;
+  const DataParametricTA<Time> automaton;
+  using Configuration = std::tuple<std::shared_ptr<DataParametricTAState<Time>>, std::vector<double>,
+                                   Symbolic::StringValuation, Symbolic::NumberValuation, double>>;
   // Symbolic::NumberValuation>;
   /*  struct Configuration {
       std::shared_ptr<DataParametricTAState> state;
diff --git a/src/main.cc b/src/main.cc
index 0845f76..9dc7781 100644
--- a/src/main.cc
+++ b/src/main.cc
@@ -109,6 +109,7 @@ int execute(const std::string &timedAutomatonFileName, const std::string &signat
 
 int main(int argc, char *argv[]) {
   using Number = double;
+  using Time = double;
 #ifdef NDEBUG
   const auto programName = "SyMon (relase build)";
 #else
@@ -169,15 +170,15 @@ int main(int argc, char *argv[]) {
                      Symbolic::Update, Parma_Polyhedra_Library::NNC_Polyhedron>(timedAutomatonFileName, signatureFileName, timedWordFileName, true);
     } else if (vm.count("dataparametric")) {
       // data parametric with new syntax
-      return execute<DataParametricTA, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor,
+      return execute<DataParametricTA<Time>, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor<Time>,
                      DataParametricPrinter, Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                     std::vector<TimingConstraint<Number>>, Symbolic::Update, Number>(timedAutomatonFileName, signatureFileName,
+                     std::vector<TimingConstraint<Time>>, Symbolic::Update, Time>(timedAutomatonFileName, signatureFileName,
                                                                       timedWordFileName, true);
     } else {
       // boolean with new syntax
-      return execute<NonParametricTA<Number>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number>,
+      return execute<NonParametricTA<Number, Time>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number, Time>,
                      BooleanPrinter<Number>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                     std::vector<TimingConstraint<Number>>, NonSymbolic::Update<Number>, Number>(timedAutomatonFileName, signatureFileName,
+                     std::vector<TimingConstraint<Time>>, NonSymbolic::Update<Number>, Time>(timedAutomatonFileName, signatureFileName,
                                                                          timedWordFileName, true);
     }
   } else if (vm.count("parametric")) {
@@ -187,15 +188,15 @@ int main(int argc, char *argv[]) {
                    Symbolic::Update, Parma_Polyhedra_Library::NNC_Polyhedron>(timedAutomatonFileName, signatureFileName, timedWordFileName, false);
   } else if (vm.count("dataparametric")) {
     // data parametric
-    return execute<DataParametricTA, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor,
+    return execute<DataParametricTA<Time>, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor<Time>,
                    DataParametricPrinter, Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                   std::vector<TimingConstraint<Number>>, Symbolic::Update, Number>(timedAutomatonFileName, signatureFileName,
+                   std::vector<TimingConstraint<Time>>, Symbolic::Update, Time>(timedAutomatonFileName, signatureFileName,
                                                                     timedWordFileName, false);
   } else {
     // boolean
-    return execute<NonParametricTA<Number>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number>,
+    return execute<NonParametricTA<Number, Time>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number, Time>,
                    BooleanPrinter<Number>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                   std::vector<TimingConstraint<Number>>, NonSymbolic::Update<Number>, Number>(timedAutomatonFileName, signatureFileName,
+                   std::vector<TimingConstraint<Time>>, NonSymbolic::Update<Number>, Time>(timedAutomatonFileName, signatureFileName,
                                                                        timedWordFileName, false);
   }
   return 0;

From 1d7dde3f095ade514787e93ce5c89110d74400a2 Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Tue, 25 Nov 2025 00:31:39 +0900
Subject: [PATCH 03/14] Rename typename Time to Timestamp

---
 src/automata_operation.hh      | 18 ++++++------
 src/automaton.hh               | 16 +++++-----
 src/automaton_parser.hh        | 35 +++++++++++-----------
 src/boolean_monitor.hh         |  9 +++---
 src/data_parametric_monitor.hh |  8 ++---
 src/main.cc                    | 26 ++++++++--------
 src/symon_parser.hh            | 24 +++++++--------
 src/timing_constraint.hh       | 54 +++++++++++++++++-----------------
 8 files changed, 95 insertions(+), 95 deletions(-)

diff --git a/src/automata_operation.hh b/src/automata_operation.hh
index 7c9d700..99727dc 100644
--- a/src/automata_operation.hh
+++ b/src/automata_operation.hh
@@ -177,7 +177,7 @@ bool acceptsEmptyWord(const TimedAutomaton<StringConstraint, NumberConstraint, T
  * @param[in] right  The second (right-hand) timed automaton.
  * @return A TimedAutomaton representing the concatenation of two automata.
  */
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Time>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Timestamp>
 TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update>
 concatenate(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &&left,
             TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &&right) {
@@ -261,7 +261,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<Time>>>) {
+        if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Timestamp>>>) {
           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);
@@ -350,7 +350,7 @@ star(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update
  * @param[in] guard The timing constraint that restricts the time.
  * @return A TimedAutomaton with the new timing constraint on the total elapsed time.
  */
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Time>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Timestamp>
 TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update>
 timeRestriction(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &&given,
                 TimingConstraint guard) {
@@ -358,8 +358,8 @@ timeRestriction(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstra
 
   bool acceptEmpty = acceptsEmptyWord(given);
 
-  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Time>>>) {
-    TimingValuation<Time> clockValuation(given.clockVariableSize, 0);
+  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Timestamp>>>) {
+    TimingValuation<Timestamp> clockValuation(given.clockVariableSize, 0);
     acceptEmpty = acceptEmpty && eval(clockValuation, guard);
   }
   if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -375,7 +375,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<Time>>>) {
+  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Timestamp>>>) {
     guard = adjustDimension(guard, given.clockVariableSize); // Adjust the guard to include the new clock variable
   }
   if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -389,7 +389,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<Time>>>) {
+        if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Timestamp>>>) {
           it->guard = adjustDimension(it->guard, given.clockVariableSize);
         }
         if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -473,14 +473,14 @@ ignoreActions(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstrain
  * @param[in] constraint The timing constraint to add to all transitions.
  * @return A reference to the modified automaton.
  */
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Time>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Timestamp>
 TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &
 addConstraintToAllTransitions(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &automaton,
                               const TimingConstraint &constraint) {
 
   TimingConstraint adjustedConstraint = constraint;
   // Ensure the constraint has the correct dimension for the automaton
-  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Time>>>) {
+  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Timestamp>>>) {
     adjustedConstraint = adjustDimension(constraint, automaton.clockVariableSize);
   } else if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
     adjustedConstraint = adjustDimension(constraint, automaton.parameterSize + automaton.clockVariableSize);
diff --git a/src/automaton.hh b/src/automaton.hh
index cc2f9de..1db254f 100644
--- a/src/automaton.hh
+++ b/src/automaton.hh
@@ -137,23 +137,23 @@ struct TimedAutomaton<StringConstraint, NumberConstraint, ParametricTimingConstr
 #include "non_symbolic_string_constraint.hh"
 #include "non_symbolic_update.hh"
 
-template <typename Number, typename Time>
+template <typename Number, typename Timestamp>
 using NonParametricTA = TimedAutomaton<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                                       std::vector<TimingConstraint<Time>>, NonSymbolic::Update<Number>>;
-template <typename Number, typename Time>
+                                       std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>>;
+template <typename Number, typename Timestamp>
 using NonParametricTAState = AutomatonState<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                                            std::vector<TimingConstraint<Time>>, 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 Time>
+template<typename Timestamp>
 using DataParametricTA = TimedAutomaton<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                        std::vector<TimingConstraint<Time>>, Symbolic::Update>;
-template<typename Time>
+                                        std::vector<TimingConstraint<Timestamp>>, Symbolic::Update>;
+template<typename Timestamp>
 using DataParametricTAState = AutomatonState<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                             std::vector<TimingConstraint<Time>>, Symbolic::Update>;
+                                             std::vector<TimingConstraint<Timestamp>>, Symbolic::Update>;
 
 #include "parametric_timing_constraint.hh"
 
diff --git a/src/automaton_parser.hh b/src/automaton_parser.hh
index 5754adb..3f6e375 100644
--- a/src/automaton_parser.hh
+++ b/src/automaton_parser.hh
@@ -56,19 +56,19 @@ namespace boost {
   BOOST_INSTALL_PROPERTY(edge, guard);
 } // namespace boost
 
-template <typename Time>
-static inline std::ostream &operator<<(std::ostream &os, const typename TimingConstraint<Time>::Order &odr) {
+template <typename Timestamp>
+static inline std::ostream &operator<<(std::ostream &os, const typename TimingConstraint<Timestamp>::Order &odr) {
   switch (odr) {
-    case TimingConstraint<Time>::Order::lt:
+    case TimingConstraint<Timestamp>::Order::lt:
       os << "<";
       break;
-    case TimingConstraint<Time>::Order::le:
+    case TimingConstraint<Timestamp>::Order::le:
       os << "<=";
       break;
-    case TimingConstraint<Time>::Order::ge:
+    case TimingConstraint<Timestamp>::Order::ge:
       os << ">=";
       break;
-    case TimingConstraint<Time>::Order::gt:
+    case TimingConstraint<Timestamp>::Order::gt:
       os << ">";
       break;
     case TimingConstraint::Order::eq:
@@ -96,14 +96,14 @@ static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint<
   return os;
 }
 
-template <typename Time>
-static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint<Time> &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;
 }
 
-template <typename Time>
-static inline std::istream &operator>>(std::istream &is, TimingConstraint<Time> &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;
@@ -127,13 +127,13 @@ static inline std::istream &operator>>(std::istream &is, TimingConstraint<Time>
   switch (odr[0]) {
     case '>':
       if (odr[1] == '=') {
-        p.odr = TimingConstraint<Time>::Order::ge;
+        p.odr = TimingConstraint<Timestamp>::Order::ge;
         if (is.get() != ' ') {
           is.setstate(std::ios_base::failbit);
           return is;
         }
       } else if (odr[1] == ' ') {
-        p.odr = TimingConstraint<Time>::Order::gt;
+        p.odr = TimingConstraint<Timestamp>::Order::gt;
       } else {
         is.setstate(std::ios_base::failbit);
         return is;
@@ -141,13 +141,13 @@ static inline std::istream &operator>>(std::istream &is, TimingConstraint<Time>
       break;
     case '<':
       if (odr[1] == '=') {
-        p.odr = TimingConstraint<Time>::Order::le;
+        p.odr = TimingConstraint<Timestamp>::Order::le;
         if (is.get() != ' ') {
           is.setstate(std::ios_base::failbit);
           return is;
         }
       } else if (odr[1] == ' ') {
-        p.odr = TimingConstraint<Time>::Order::lt;
+        p.odr = TimingConstraint<Timestamp>::Order::lt;
       } else {
         is.setstate(std::ios_base::failbit);
         return is;
@@ -324,9 +324,10 @@ using BoostTimedAutomaton = boost::adjacency_list<
 template <typename Number, typename Timestamp>
 using NonParametricBoostTA = BoostTimedAutomaton<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
                                                  TimingConstraint<Timestamp>, NonSymbolic::Update<Number>>;
-template <typename Time>
-                                                 using DataParametricBoostTA =
-    BoostTimedAutomaton<Symbolic::StringConstraint, Symbolic::NumberConstraint, TimingConstraint<Time>, Symbolic::Update>;
+
+template <typename Timestamp>
+using DataParametricBoostTA =
+    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,
diff --git a/src/boolean_monitor.hh b/src/boolean_monitor.hh
index dfde345..3aaa098 100644
--- a/src/boolean_monitor.hh
+++ b/src/boolean_monitor.hh
@@ -17,11 +17,11 @@ template <class Number> struct BooleanMonitorResult {
 };
 
 namespace NonSymbolic {
-  template <typename Number, typename Time>
+  template <typename Number, typename Timestamp>
   class BooleanMonitor : public SingleSubject<BooleanMonitorResult<Number>>, public Observer<TimedWordEvent<Number>> {
   public:
     static const constexpr std::size_t unobservableActionID = 127;
-    BooleanMonitor(const NonParametricTA<Number, Time> &automaton) : automaton(automaton) {
+    BooleanMonitor(const NonParametricTA<Number, Timestamp> &automaton) : automaton(automaton) {
       configurations.clear();
       // configurations.reserve(automaton.initialStates.size());
       std::vector<double> initCVal(automaton.clockVariableSize);
@@ -94,9 +94,8 @@ namespace NonSymbolic {
     }
 
   private:
-
-    const NonParametricTA<Number, Time> automaton;
-    using Configuration = std::tuple<std::shared_ptr<NonParametricTAState<Number, Time>>, std::vector<double>,
+    const NonParametricTA<Number, Timestamp> automaton;
+    using Configuration = std::tuple<std::shared_ptr<NonParametricTAState<Number, Timestamp>>, std::vector<double>,
                                      StringValuation, NumberValuation<Number>, double>>;
     // struct Configuration {
     //   std::shared_ptr<AutomatonState<Number>> state;
diff --git a/src/data_parametric_monitor.hh b/src/data_parametric_monitor.hh
index bcc3384..d562c7a 100644
--- a/src/data_parametric_monitor.hh
+++ b/src/data_parametric_monitor.hh
@@ -24,12 +24,12 @@ struct DataParametricMonitorResult {
   Symbolic::StringValuation stringValuation;
 };
 
-template<typename Time>
+template<typename Timestamp>
 class DataParametricMonitor : public SingleSubject<DataParametricMonitorResult>,
                               public Observer<TimedWordEvent<PPLRational>> {
 public:
   static const constexpr std::size_t unobservableActionID = 127;
-  explicit DataParametricMonitor(const DataParametricTA<Time> &automaton) : automaton(automaton) {
+  explicit DataParametricMonitor(const DataParametricTA<Timestamp> &automaton) : automaton(automaton) {
     absTime = 0;
     configurations.clear();
     // configurations.reserve(automaton.initialStates.size());
@@ -105,8 +105,8 @@ public:
   }
 
 private:
-  const DataParametricTA<Time> automaton;
-  using Configuration = std::tuple<std::shared_ptr<DataParametricTAState<Time>>, std::vector<double>,
+  const DataParametricTA<Timestamp> automaton;
+  using Configuration = std::tuple<std::shared_ptr<DataParametricTAState<Timestamp>>, std::vector<double>,
                                    Symbolic::StringValuation, Symbolic::NumberValuation, double>>;
   // Symbolic::NumberValuation>;
   /*  struct Configuration {
diff --git a/src/main.cc b/src/main.cc
index 9dc7781..a0fdad0 100644
--- a/src/main.cc
+++ b/src/main.cc
@@ -35,7 +35,7 @@ using ::operator<<;
  */
 template <typename TAType, typename BoostTAType, typename Number, typename Timestamp, typename Monitor,
           typename Printer, typename StringConstraint, typename NumberConstraint, typename TimingConstraintType,
-          typename UpdateType, typename Time>
+          typename UpdateType>
 int execute(const std::string &timedAutomatonFileName, const std::string &signatureFileName,
             const std::string &timedWordFileName, bool useNewSyntax = false) {
   TAType TA;
@@ -50,7 +50,7 @@ int execute(const std::string &timedAutomatonFileName, const std::string &signat
 
   if (useNewSyntax) {
     // Use the new syntax parser
-    SymonParser<StringConstraint, NumberConstraint, TimingConstraintType, UpdateType, Time> parser;
+    SymonParser<StringConstraint, NumberConstraint, TimingConstraintType, UpdateType, Timestamp> parser;
     try {
       parser.parse(taStream);
     } catch (const std::runtime_error &e) {
@@ -109,7 +109,7 @@ int execute(const std::string &timedAutomatonFileName, const std::string &signat
 
 int main(int argc, char *argv[]) {
   using Number = double;
-  using Time = double;
+  using Timestamp = double;
 #ifdef NDEBUG
   const auto programName = "SyMon (relase build)";
 #else
@@ -167,36 +167,36 @@ int main(int argc, char *argv[]) {
       // parametric with new syntax
       return execute<ParametricTA, BoostPTA, PPLRational, PPLRational, ParametricMonitor, ParametricPrinter,
                      Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
-                     Symbolic::Update, Parma_Polyhedra_Library::NNC_Polyhedron>(timedAutomatonFileName, signatureFileName, timedWordFileName, true);
+                     Symbolic::Update>(timedAutomatonFileName, signatureFileName, timedWordFileName, true);
     } else if (vm.count("dataparametric")) {
       // data parametric with new syntax
-      return execute<DataParametricTA<Time>, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor<Time>,
+      return execute<DataParametricTA<Timestamp>, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor<Timestamp>,
                      DataParametricPrinter, Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                     std::vector<TimingConstraint<Time>>, Symbolic::Update, Time>(timedAutomatonFileName, signatureFileName,
+                     std::vector<TimingConstraint<Timestamp>>, Symbolic::Update>(timedAutomatonFileName, signatureFileName,
                                                                       timedWordFileName, true);
     } else {
       // boolean with new syntax
-      return execute<NonParametricTA<Number, Time>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number, Time>,
+      return execute<NonParametricTA<Number, Timestamp>, NonParametricBoostTA<Number>, Number, Timestamp, BooleanMonitor<Number, Timestamp>,
                      BooleanPrinter<Number>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                     std::vector<TimingConstraint<Time>>, NonSymbolic::Update<Number>, Time>(timedAutomatonFileName, signatureFileName,
+                     std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>, Time<Timestamp>>(timedAutomatonFileName, signatureFileName,
                                                                          timedWordFileName, true);
     }
   } else if (vm.count("parametric")) {
     // parametric
     return execute<ParametricTA, BoostPTA, PPLRational, PPLRational, ParametricMonitor, ParametricPrinter,
                    Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
-                   Symbolic::Update, Parma_Polyhedra_Library::NNC_Polyhedron>(timedAutomatonFileName, signatureFileName, timedWordFileName, false);
+                   Symbolic::Update>(timedAutomatonFileName, signatureFileName, timedWordFileName, false);
   } else if (vm.count("dataparametric")) {
     // data parametric
-    return execute<DataParametricTA<Time>, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor<Time>,
+    return execute<DataParametricTA<Timestamp>, DataParametricBoostTA<Number>, PPLRational, Timestamp, DataParametricMonitor<Timestamp>,
                    DataParametricPrinter, Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                   std::vector<TimingConstraint<Time>>, Symbolic::Update, Time>(timedAutomatonFileName, signatureFileName,
+                   std::vector<TimingConstraint<Timestamp>>, Symbolic::Update>(timedAutomatonFileName, signatureFileName,
                                                                     timedWordFileName, false);
   } else {
     // boolean
-    return execute<NonParametricTA<Number, Time>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number, Time>,
+    return execute<NonParametricTA<Number, Timestamp>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number, Timestamp>,
                    BooleanPrinter<Number>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                   std::vector<TimingConstraint<Time>>, NonSymbolic::Update<Number>, Time>(timedAutomatonFileName, signatureFileName,
+                   std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>>(timedAutomatonFileName, signatureFileName,
                                                                        timedWordFileName, false);
   }
   return 0;
diff --git a/src/symon_parser.hh b/src/symon_parser.hh
index e120f78..69480ed 100644
--- a/src/symon_parser.hh
+++ b/src/symon_parser.hh
@@ -78,7 +78,7 @@ static inline TSNode nextNonCommentChild(const TSNode &parent, uint32_t &idx) {
   return std::nullopt;
 }
 
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Time>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Timestamp>
 class SymonParser {
 public:
   using Automaton = TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update>;
@@ -196,13 +196,13 @@ public:
 
 public:
   // Helper function to extract the upper bound from a non-parametric timing constraint
-  static std::vector<::TimingConstraint<Time>> extractUpperBound(const std::vector<::TimingConstraint<Time>> &guard) {
-    std::vector<::TimingConstraint<Time>> upperBound;
+  static std::vector<::TimingConstraint<Timestamp>> extractUpperBound(const std::vector<::TimingConstraint<Timestamp>> &guard) {
+    std::vector<::TimingConstraint<Timestamp>> upperBound;
 
     // Check each constraint in the guard
     for (const auto &constraint: guard) {
       // If the constraint is an upper bound (lt or le), add it to the result
-      if (constraint.odr == ::TimingConstraint<Time>::Order::lt || constraint.odr == ::TimingConstraint<Time>::Order::le) {
+      if (constraint.odr == ::TimingConstraint<Timestamp>::Order::lt || constraint.odr == ::TimingConstraint<Timestamp>::Order::le) {
         upperBound.push_back(constraint);
       }
     }
@@ -597,9 +597,9 @@ private:
           throw err;
         }
       } else {
-        return {boost::lexical_cast<::TimingConstraint<Time>>("x" + std::to_string(clockIndex) + " " +
+        return {boost::lexical_cast<::TimingConstraint<Timestamp>>("x" + std::to_string(clockIndex) + " " +
                                                         (isLowerInclusive ? ">=" : ">") + " " + lowerBound),
-                boost::lexical_cast<::TimingConstraint<Time>>("x" + std::to_string(clockIndex) + " " +
+                boost::lexical_cast<::TimingConstraint<Timestamp>>("x" + std::to_string(clockIndex) + " " +
                                                         (isUpperInclusive ? "<=" : "<") + " " + upperBound)};
       }
     }
@@ -629,7 +629,7 @@ private:
         return result;
       } else {
         return {
-            boost::lexical_cast<::TimingConstraint<Time>>("x" + std::to_string(clockIndex) + " " + comparator + " " + expr)};
+            boost::lexical_cast<::TimingConstraint<Timestamp>>("x" + std::to_string(clockIndex) + " " + comparator + " " + expr)};
       }
     }
     throw std::runtime_error(makeErrorMessage(
@@ -837,7 +837,7 @@ private:
       TSNode rhsNode = nextNonCommentChild(child, p);
       Automaton lhs = this->parseExpr(content, lhsNode);
       Automaton rhs = this->parseExpr(content, rhsNode);
-      return concatenate<StringConstraint, NumberConstraint, TimingConstraint, Update, Time>(std::move(lhs), std::move(rhs));
+      return concatenate<StringConstraint, NumberConstraint, TimingConstraint, Update, Timestamp>(std::move(lhs), std::move(rhs));
     } else if (kind == "conjunction") {
       uint32_t p = 0;
       TSNode lhsNode = nextNonCommentChild(child, p);
@@ -991,7 +991,7 @@ private:
       TimingConstraint guard = this->parseTimingConstraint(content, intervalNode, innerExpr.clockVariableSize);
 
       // Apply the time restriction operation
-      Automaton result = timeRestriction<StringConstraint, NumberConstraint, TimingConstraint, Update, Time>(std::move(innerExpr), guard);
+      Automaton result = timeRestriction<StringConstraint, NumberConstraint, TimingConstraint, Update, Timestamp>(std::move(innerExpr), guard);
 
       if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
         assert(std::all_of(result.states.begin(), result.states.end(), [&](const auto &state) {
@@ -1005,17 +1005,17 @@ private:
       }
 
       // Extract the upper bound from the timing constraint and add it to all transitions
-      if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Time>>>) {
+      if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Timestamp>>>) {
         // For non-parametric timing constraints
         auto upperBound = extractUpperBound(guard);
         if (!upperBound.empty()) {
           // It has an upper bound, add it to all transitions
-          addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update, Time>(result, upperBound);
+          addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update, Timestamp>(result, upperBound);
         }
       } else if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
         // For parametric timing constraints
         auto upperBound = extractUpperBound(guard, this->parameters.size() + innerExpr.clockVariableSize - 1);
-        addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update, Time>(result, upperBound);
+        addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update, Timestamp>(result, upperBound);
       }
 
       if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
diff --git a/src/timing_constraint.hh b/src/timing_constraint.hh
index a29d37f..bd65c4b 100644
--- a/src/timing_constraint.hh
+++ b/src/timing_constraint.hh
@@ -16,7 +16,7 @@ inline bool toBool(Order odr) {
 }
 
 //! @brief A constraint in a guard of transitions
-template <typename Time>
+template <typename Timestamp>
 struct TimingConstraint {
   enum class Order { lt, le, ge, gt, eq };
   using Timestamp = double;
@@ -77,24 +77,24 @@ public:
   explicit ConstraintMaker(ClockVariables x) : x(x) {
   }
 
-  template<typename Time>
-  TimingConstraint<Time> operator<(Time c) {
-    return TimingConstraint{x, TimingConstraint<Time>::Order::lt, c};
+  template<typename Timestamp>
+  TimingConstraint<Timestamp> operator<(Timestamp c) {
+    return TimingConstraint{x, TimingConstraint<Timestamp>::Order::lt, c};
   }
 
-  template<typename Time>
-  TimingConstraint<Time> operator<=(Time c) {
-    return TimingConstraint{x, TimingConstraint<Time>::Order::le, c};
+  template<typename Timestamp>
+  TimingConstraint<Timestamp> operator<=(Timestamp c) {
+    return TimingConstraint{x, TimingConstraint<Timestamp>::Order::le, c};
   }
 
-  template<typename Time>
-  TimingConstraint<Time> operator>(Time c) {
-    return TimingConstraint<Time>{x, TimingConstraint<Time>::Order::gt, c};
+  template<typename Timestamp>
+  TimingConstraint<Timestamp> operator>(Timestamp c) {
+    return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::gt, c};
   }
 
-  template<typename Time>
-  TimingConstraint<Time> operator>=(Time c) {
-    return TimingConstraint<Time>{x, TimingConstraint<Time>::Order::ge, c};
+  template<typename Timestamp>
+  TimingConstraint<Timestamp> operator>=(Timestamp c) {
+    return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::ge, c};
   }
 
   TimingConstraint operator==(Timestamp c) {
@@ -110,13 +110,13 @@ public:
 //         return g.odr == TimingConstraint::Order::ge || g.odr == TimingConstraint::Order::gt;
 //     }), guard.end());
 // }
-template <typename Time>
-using TimingValuation = std::vector<Time>;
+template <typename Timestamp>
+using TimingValuation = std::vector<Timestamp>;
 
-template<typename Time>
-static bool eval(const TimingValuation<Time> &clockValuation, const std::vector<TimingConstraint<Time>> &guard) {
+template<typename Timestamp>
+static bool eval(const TimingValuation<Timestamp> &clockValuation, const std::vector<TimingConstraint<Timestamp>> &guard) {
   return std::all_of(guard.begin(), guard.end(),
-                     [&clockValuation](const TimingConstraint<Time> &g) { return g.satisfy(clockValuation.at(g.x)); });
+                     [&clockValuation](const TimingConstraint<Timestamp> &g) { return g.satisfy(clockValuation.at(g.x)); });
 }
 
 /*!
@@ -154,9 +154,9 @@ static std::optional<double> diff(const TimingValuation &clockValuation, const s
  * @param width the width to shift the clock variable id
  * @return a new vector of TimingConstraint with the clock variables shifted
  */
-template<typename Time>
-static std::vector<TimingConstraint<Time>> shift(const std::vector<TimingConstraint<Time>> &guard, const ClockVariables width) {
-  std::vector<TimingConstraint<Time>> shiftedGuard;
+template<typename Timestamp>
+static std::vector<TimingConstraint<Timestamp>> shift(const std::vector<TimingConstraint<Timestamp>> &guard, const ClockVariables width) {
+  std::vector<TimingConstraint<Timestamp>> shiftedGuard;
   shiftedGuard.reserve(guard.size());
   for (const auto &g: guard) {
     shiftedGuard.push_back(g.shift(width));
@@ -172,10 +172,10 @@ static std::vector<TimingConstraint<Time>> shift(const std::vector<TimingConstra
  * @param right the second vector of TimingConstraint
  * @return a new vector containing all TimingConstraints from both vectors
  */
- template<typename Time>
-static std::vector<TimingConstraint<Time>> operator&&(const std::vector<TimingConstraint<Time>> &left,
-                                                const std::vector<TimingConstraint<Time>> &right) {
-  std::vector<TimingConstraint<Time>> result = left;
+ template<typename Timestamp>
+static std::vector<TimingConstraint<Timestamp>> operator&&(const std::vector<TimingConstraint<Timestamp>> &left,
+                                                const std::vector<TimingConstraint<Timestamp>> &right) {
+  std::vector<TimingConstraint<Timestamp>> result = left;
   result.reserve(left.size() + right.size());
   std::copy_if(right.begin(), right.end(), std::back_inserter(result),
                [&left](const auto &guard) { return std::find(left.begin(), left.end(), guard) == left.end(); });
@@ -189,8 +189,8 @@ static std::vector<TimingConstraint<Time>> operator&&(const std::vector<TimingCo
  * @param size the size to adjust the guard to
  * @return a new vector of TimingConstraint with the clock variables adjusted
  */
-template<typename Time>
-static std::vector<TimingConstraint<Time>> adjustDimension(const std::vector<TimingConstraint<Time>> &guard,
+template<typename Timestamp>
+static std::vector<TimingConstraint<Timestamp>> adjustDimension(const std::vector<TimingConstraint<Timestamp>> &guard,
                                                      const ClockVariables size) {
   return guard;
 }

From 6f85ff0cb5e5176aa6f057d2e38d5791e66d308b Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Tue, 25 Nov 2025 00:51:07 +0900
Subject: [PATCH 04/14] Refactor: Update BooleanMonitor and
 DataParametricMonitor to use Timestamp type for time-related variables

---
 src/boolean_monitor.hh         | 18 +++++++++---------
 src/data_parametric_monitor.hh | 24 +++++++++++++-----------
 src/main.cc                    | 14 +++++++-------
 src/printer.hh                 | 10 ++++++----
 4 files changed, 35 insertions(+), 31 deletions(-)

diff --git a/src/boolean_monitor.hh b/src/boolean_monitor.hh
index 3aaa098..00d3e81 100644
--- a/src/boolean_monitor.hh
+++ b/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, typename Timestamp>
-  class BooleanMonitor : public SingleSubject<BooleanMonitorResult<Number>>, public Observer<TimedWordEvent<Number>> {
+  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, 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;
@@ -95,11 +95,11 @@ namespace NonSymbolic {
 
   private:
     const NonParametricTA<Number, Timestamp> automaton;
-    using Configuration = std::tuple<std::shared_ptr<NonParametricTAState<Number, Timestamp>>, std::vector<double>,
+    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 {
diff --git a/src/data_parametric_monitor.hh b/src/data_parametric_monitor.hh
index d562c7a..cb6250a 100644
--- a/src/data_parametric_monitor.hh
+++ b/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,23 +18,24 @@ 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;
 };
 
 template<typename Timestamp>
-class DataParametricMonitor : public SingleSubject<DataParametricMonitorResult>,
-                              public Observer<TimedWordEvent<PPLRational>> {
+class DataParametricMonitor : public SingleSubject<DataParametricMonitorResult<Timestamp>>,
+                              public Observer<TimedWordEvent<PPLRational, Timestamp>> {
 public:
   static const constexpr std::size_t unobservableActionID = 127;
   explicit DataParametricMonitor(const DataParametricTA<Timestamp> &automaton) : automaton(automaton) {
     absTime = 0;
     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
@@ -47,12 +49,12 @@ 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));
 
@@ -63,7 +65,7 @@ public:
       if (timestamp < absTime) {
         continue;
       }
-      for (double &d: clockValuation) {
+      for (Timestamp &d: clockValuation) {
         d += timestamp - absTime;
       }
       auto stringEnv = std::get<2>(conf); //.stringEnv;
@@ -95,7 +97,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});
           }
         }
       }
@@ -106,12 +108,12 @@ public:
 
 private:
   const DataParametricTA<Timestamp> automaton;
-  using Configuration = std::tuple<std::shared_ptr<DataParametricTAState<Timestamp>>, std::vector<double>,
+  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;
     };*/
diff --git a/src/main.cc b/src/main.cc
index a0fdad0..5b6772b 100644
--- a/src/main.cc
+++ b/src/main.cc
@@ -170,15 +170,15 @@ int main(int argc, char *argv[]) {
                      Symbolic::Update>(timedAutomatonFileName, signatureFileName, timedWordFileName, true);
     } else if (vm.count("dataparametric")) {
       // data parametric with new syntax
-      return execute<DataParametricTA<Timestamp>, DataParametricBoostTA<Number>, PPLRational, double, DataParametricMonitor<Timestamp>,
-                     DataParametricPrinter, Symbolic::StringConstraint, Symbolic::NumberConstraint,
+      return execute<DataParametricTA<Timestamp>, DataParametricBoostTA<Number>, PPLRational, Timestamp, DataParametricMonitor<Timestamp>,
+                     DataParametricPrinter<Timestamp>, Symbolic::StringConstraint, Symbolic::NumberConstraint,
                      std::vector<TimingConstraint<Timestamp>>, Symbolic::Update>(timedAutomatonFileName, signatureFileName,
                                                                       timedWordFileName, true);
     } else {
       // boolean with new syntax
       return execute<NonParametricTA<Number, Timestamp>, NonParametricBoostTA<Number>, Number, Timestamp, BooleanMonitor<Number, Timestamp>,
-                     BooleanPrinter<Number>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
-                     std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>, Time<Timestamp>>(timedAutomatonFileName, signatureFileName,
+                     BooleanPrinter<Number, Timestamp>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
+                     std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>>(timedAutomatonFileName, signatureFileName,
                                                                          timedWordFileName, true);
     }
   } else if (vm.count("parametric")) {
@@ -189,13 +189,13 @@ int main(int argc, char *argv[]) {
   } else if (vm.count("dataparametric")) {
     // data parametric
     return execute<DataParametricTA<Timestamp>, DataParametricBoostTA<Number>, PPLRational, Timestamp, DataParametricMonitor<Timestamp>,
-                   DataParametricPrinter, Symbolic::StringConstraint, Symbolic::NumberConstraint,
+                   DataParametricPrinter<Timestamp>, Symbolic::StringConstraint, Symbolic::NumberConstraint,
                    std::vector<TimingConstraint<Timestamp>>, Symbolic::Update>(timedAutomatonFileName, signatureFileName,
                                                                     timedWordFileName, false);
   } else {
     // boolean
-    return execute<NonParametricTA<Number, Timestamp>, NonParametricBoostTA<Number>, Number, double, BooleanMonitor<Number, Timestamp>,
-                   BooleanPrinter<Number>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
+    return execute<NonParametricTA<Number, Timestamp>, NonParametricBoostTA<Number>, Number, Timestamp, BooleanMonitor<Number, Timestamp>,
+                   BooleanPrinter<Number, Timestamp>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
                    std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>>(timedAutomatonFileName, signatureFileName,
                                                                        timedWordFileName, false);
   }
diff --git a/src/printer.hh b/src/printer.hh
index beba899..0592dac 100644
--- a/src/printer.hh
+++ b/src/printer.hh
@@ -2,12 +2,13 @@
 
 #include "boolean_monitor.hh"
 
-template <class Number> struct BooleanPrinter : public Observer<BooleanMonitorResult<Number>> {
+template <class Number, typename Timestamp> struct BooleanPrinter
+    : public Observer<BooleanMonitorResult<Number, Timestamp>> {
   BooleanPrinter() = default;
 
   virtual ~BooleanPrinter() = default;
 
-  void notify(const BooleanMonitorResult<Number> &result) override {
+  void notify(const BooleanMonitorResult<Number, Timestamp> &result) override {
     std::cout << "@" << std::fixed << result.timestamp << std::defaultfloat << ".\t(time-point " << result.index << ")\t";
     for (std::size_t i = 0; i < result.stringValuation.size(); i++) {
       if (result.stringValuation[i]) {
@@ -24,12 +25,13 @@ template <class Number> struct BooleanPrinter : public Observer<BooleanMonitorRe
 
 #include "data_parametric_monitor.hh"
 
-struct DataParametricPrinter : public Observer<DataParametricMonitorResult> {
+template <typename Timestamp>
+struct DataParametricPrinter : public Observer<DataParametricMonitorResult<Timestamp>> {
   DataParametricPrinter() = default;
 
   virtual ~DataParametricPrinter() = default;
 
-  void notify(const DataParametricMonitorResult &result) override {
+  void notify(const DataParametricMonitorResult<Timestamp> &result) override {
     using Parma_Polyhedra_Library::IO_Operators::operator<<;
     std::cout << "@" << std::fixed << result.timestamp << ".\t(time-point " << result.index << ")\t";
     for (std::size_t i = 0; i < result.stringValuation.size(); i++) {

From 037908c53fcc94a02b60a8ce0995db50c6d77175 Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Tue, 25 Nov 2025 02:22:56 +0900
Subject: [PATCH 05/14] Update test

---
 src/timing_constraint.hh                      |  12 +-
 test/automaton_operation_test.cc              |  47 ++++---
 test/automaton_parser_test.cc                 |  26 ++--
 test/data_parametric_monitor_test.cc          |   8 +-
 test/fixture/copy_automaton_fixture.hh        |  72 +++++-----
 test/fixture/star_automaton_fixture.hh        |   8 +-
 .../time_restriction_automaton_fixture.hh     |   8 +-
 test/fixture/withdraw_automaton_fixture.hh    |  24 ++--
 test/symon_parser_test.cc                     | 126 +++++++++---------
 test/timing_constraint_test.cc                |   6 +-
 10 files changed, 173 insertions(+), 164 deletions(-)

diff --git a/src/timing_constraint.hh b/src/timing_constraint.hh
index bd65c4b..69e4e9c 100644
--- a/src/timing_constraint.hh
+++ b/src/timing_constraint.hh
@@ -77,22 +77,22 @@ public:
   explicit ConstraintMaker(ClockVariables x) : x(x) {
   }
 
-  template<typename Timestamp>
+  template<typename Timestamp = double>
   TimingConstraint<Timestamp> operator<(Timestamp c) {
-    return TimingConstraint{x, TimingConstraint<Timestamp>::Order::lt, c};
+    return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::lt, c};
   }
 
-  template<typename Timestamp>
+  template<typename Timestamp = double>
   TimingConstraint<Timestamp> operator<=(Timestamp c) {
-    return TimingConstraint{x, TimingConstraint<Timestamp>::Order::le, c};
+    return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::le, c};
   }
 
-  template<typename Timestamp>
+  template<typename Timestamp = double>
   TimingConstraint<Timestamp> operator>(Timestamp c) {
     return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::gt, c};
   }
 
-  template<typename Timestamp>
+  template<typename Timestamp = double>
   TimingConstraint<Timestamp> operator>=(Timestamp c) {
     return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::ge, c};
   }
diff --git a/test/automaton_operation_test.cc b/test/automaton_operation_test.cc
index 965d355..17705d9 100644
--- a/test/automaton_operation_test.cc
+++ b/test/automaton_operation_test.cc
@@ -72,7 +72,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             auto copyFinalState = copy.states[3];
             auto withdrawFinalState = withdraw.states[2];
 
-            auto result = concatenate(std::move(copy), std::move(withdraw));
+            auto result = concatenate<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<int>,
+                                       std::vector<TimingConstraint<double>>, NonSymbolic::Update<int>, double>(std::move(copy), std::move(withdraw));
 
             // Check the total number of states (should be the sum of both automata)
             BOOST_CHECK_EQUAL(result.states.size(), 6);
@@ -255,11 +256,12 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             auto originalFinalState = automaton_copy.states[1];
 
             // Create a timing constraint for the time restriction
-            std::vector<TimingConstraint> timeGuard;
-            timeGuard.push_back(ConstraintMaker(0) <= 10);
+            std::vector<TimingConstraint<double>> timeGuard;
+            timeGuard.push_back(ConstraintMaker(0) <= 10.);
 
             // Apply the time restriction operation
-            auto result = timeRestriction(std::move(automaton_copy), timeGuard);
+            auto result = timeRestriction<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<int>,
+                                       std::vector<TimingConstraint<double>>, NonSymbolic::Update<int>, double>(std::move(automaton_copy), timeGuard);
 
             // Check that the clock variable size is increased by 1
             BOOST_CHECK_EQUAL(result.clockVariableSize, 2);
@@ -353,8 +355,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             BOOST_CHECK_EQUAL(automaton_copy.states.size(), 4);
 
             // Create a timing constraint to add to all transitions
-            std::vector<TimingConstraint> constraint;
-            constraint.push_back(ConstraintMaker(0) <= 5);
+            std::vector<TimingConstraint<double>> constraint;
+            constraint.push_back(ConstraintMaker(0) <= 5.);
 
             // Count the number of transitions before adding the constraint
             size_t transitionCount = 0;
@@ -365,7 +367,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             }
 
             // Apply the constraint to all transitions
-            addConstraintToAllTransitions(automaton_copy, constraint);
+            addConstraintToAllTransitions<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<int>,
+                                       std::vector<TimingConstraint<double>>, NonSymbolic::Update<int>, double>(automaton_copy, constraint);
 
             // Verify that all transitions have the constraint applied
             size_t constrainedTransitionCount = 0;
@@ -375,7 +378,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
                         // Check that the constraint is applied to the transition
                         bool hasConstraint = false;
                         for (const auto &guard : transition.guard) {
-                            if (guard.x == 0 && guard.odr == TimingConstraint::Order::le && guard.c == 5) {
+                            if (guard.x == 0 && guard.odr == TimingConstraint<double>::Order::le && guard.c == 5) {
                                 hasConstraint = true;
                                 break;
                             }
@@ -455,7 +458,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             auto copyFinalState = copy.states[3];
             auto withdrawFinalState = withdraw.states[2];
 
-            auto result = concatenate(std::move(copy), std::move(withdraw));
+            auto result = concatenate<Symbolic::StringConstraint, Symbolic::NumberConstraint,
+                                        std::vector<TimingConstraint<double>>, Symbolic::Update, double>(std::move(copy), std::move(withdraw));
 
             // Check the total number of states (should be the sum of both automata)
             BOOST_CHECK_EQUAL(result.states.size(), 6);
@@ -640,11 +644,12 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             // Create a timing constraint for the time restriction
             using namespace Parma_Polyhedra_Library;
             using namespace Symbolic;
-            std::vector<TimingConstraint> timeGuard;
-            timeGuard.push_back(ConstraintMaker(0) <= 10);
+            std::vector<TimingConstraint<double>> timeGuard;
+            timeGuard.push_back(ConstraintMaker(0) <= 10.);
 
             // Apply the time restriction operation
-            auto result = timeRestriction(std::move(automaton_copy), timeGuard);
+            auto result = timeRestriction<Symbolic::StringConstraint, Symbolic::NumberConstraint,
+                                        std::vector<TimingConstraint<double>>, Symbolic::Update, double>(std::move(automaton_copy), timeGuard);
 
             // Check that the clock variable size is increased by 1
             BOOST_CHECK_EQUAL(result.clockVariableSize, 2);
@@ -738,8 +743,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             BOOST_CHECK_EQUAL(automaton_copy.states.size(), 4);
 
             // Create a timing constraint to add to all transitions
-            std::vector<TimingConstraint> constraint;
-            constraint.push_back(ConstraintMaker(0) <= 5);
+            std::vector<TimingConstraint<double>> constraint;
+            constraint.push_back(ConstraintMaker(0) <= 5.);
 
             // Count the number of transitions before adding the constraint
             size_t transitionCount = 0;
@@ -750,7 +755,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             }
 
             // Apply the constraint to all transitions
-            addConstraintToAllTransitions(automaton_copy, constraint);
+            addConstraintToAllTransitions<Symbolic::StringConstraint, Symbolic::NumberConstraint,
+                                        std::vector<TimingConstraint<double>>, Symbolic::Update, double>(automaton_copy, constraint);
 
             // Verify that all transitions have the constraint applied
             size_t constrainedTransitionCount = 0;
@@ -760,7 +766,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
                         // Check that the constraint is applied to the transition
                         bool hasConstraint = false;
                         for (const auto &guard : transition.guard) {
-                            if (guard.x == 0 && guard.odr == TimingConstraint::Order::le && guard.c == 5) {
+                            if (guard.x == 0 && guard.odr == TimingConstraint<double>::Order::le && guard.c == 5) {
                                 hasConstraint = true;
                                 break;
                             }
@@ -840,7 +846,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             auto copyFinalState = copy.states[3];
             auto withdrawFinalState = withdraw.states[2];
 
-            auto result = concatenate(std::move(copy), std::move(withdraw));
+            auto result = concatenate<Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
+                                    Symbolic::Update, ParametricTimingConstraint>(std::move(copy), std::move(withdraw));
 
             // Check the total number of states (should be the sum of both automata)
             BOOST_CHECK_EQUAL(result.states.size(), 6);
@@ -1029,7 +1036,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             timeGuard.add_constraint(Variable(1) <= 10);
 
             // Apply the time restriction operation
-            const auto result = timeRestriction(std::move(automaton_copy), timeGuard);
+            const auto result = timeRestriction<Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
+                                    Symbolic::Update, ParametricTimingConstraint>(std::move(automaton_copy), timeGuard);
 
             // Check that the clock variable size is increased by 1
             BOOST_CHECK_EQUAL(result.clockVariableSize, 2);
@@ -1136,7 +1144,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             }
 
             // Apply the constraint to all transitions
-            addConstraintToAllTransitions(automaton_copy, constraint);
+            addConstraintToAllTransitions<Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
+                                    Symbolic::Update, ParametricTimingConstraint>(automaton_copy, constraint);
 
             // Verify that all transitions have the constraint applied
             size_t constrainedTransitionCount = 0;
diff --git a/test/automaton_parser_test.cc b/test/automaton_parser_test.cc
index fdff97d..9d82905 100644
--- a/test/automaton_parser_test.cc
+++ b/test/automaton_parser_test.cc
@@ -178,7 +178,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
     BOOST_AUTO_TEST_SUITE(NonParametricTimedAutomaton)
 
       BOOST_AUTO_TEST_CASE(Copy) {
-        NonParametricBoostTA<int> BoostTA;
+        NonParametricBoostTA<int, double> BoostTA;
         std::ifstream file(PROJECT_ROOT "/example/copy/copy.dot");
         parseBoostTA(file, BoostTA);
 
@@ -214,7 +214,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
     BOOST_AUTO_TEST_SUITE(DataParametricTimedAutomaton)
 
       BOOST_AUTO_TEST_CASE(Copy) {
-        DataParametricBoostTA BoostTA;
+        DataParametricBoostTA<double> BoostTA;
         std::ifstream file(PROJECT_ROOT "/example/copy/copy_data_parametric.dot");
         parseBoostTA(file, BoostTA);
 
@@ -252,8 +252,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
     BOOST_AUTO_TEST_SUITE(NonParametricTimedAutomaton)
 
       BOOST_AUTO_TEST_CASE(Copy) {
-        NonParametricBoostTA<int> BoostTA;
-        NonParametricTA<int> TA;
+        NonParametricBoostTA<int, double> BoostTA;
+        NonParametricTA<int, double> TA;
         // NonParametricTA<int> TA;
         std::ifstream file(PROJECT_ROOT "/example/copy/copy.dot");
         parseBoostTA(file, BoostTA);
@@ -331,7 +331,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).update.numberUpdate.size(), 0);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, TimingConstraint::Order::lt);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, TimingConstraint<double>::Order::lt);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().c, 3);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).target.lock(), TA.states[1]);
 
@@ -355,8 +355,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
 
       BOOST_AUTO_TEST_CASE(Copy) {
         using namespace Parma_Polyhedra_Library;
-        DataParametricBoostTA BoostTA;
-        DataParametricTA TA;
+        DataParametricBoostTA<double> BoostTA;
+        DataParametricTA<double> TA;
         std::ifstream file(PROJECT_ROOT "/example/copy/copy_data_parametric.dot");
         parseBoostTA(file, BoostTA);
         convBoostTA(BoostTA, TA);
@@ -416,7 +416,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).update.numberUpdate.size(), 0);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, ::TimingConstraint::Order::lt);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, ::TimingConstraint<double>::Order::lt);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().c, 3);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).target.lock(), TA.states[1]);
 
@@ -441,8 +441,8 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
 
       BOOST_AUTO_TEST_CASE(withdraw) {
         using namespace Parma_Polyhedra_Library;
-        DataParametricBoostTA BoostTA;
-        DataParametricTA TA;
+        DataParametricBoostTA<double> BoostTA;
+        DataParametricTA<double> TA;
         std::ifstream file(PROJECT_ROOT "/example/withdraw/withdraw.dot");
         parseBoostTA(file, BoostTA);
         convBoostTA(BoostTA, TA);
@@ -495,7 +495,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).update.numberUpdate.size(), 0);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, ::TimingConstraint::Order::le);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, ::TimingConstraint<double>::Order::le);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().c, 30);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).target.lock(), TA.states[1]);
 
@@ -516,7 +516,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
                 Variable(0) + Variable(1)));
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.front().odr, ::TimingConstraint::Order::le);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.front().odr, ::TimingConstraint<double>::Order::le);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.front().c, 30);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).target.lock(), TA.states[1]);
 
@@ -528,7 +528,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).update.numberUpdate.size(), 0);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.front().odr, ::TimingConstraint::Order::gt);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.front().odr, ::TimingConstraint<double>::Order::gt);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.front().c, 30);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).target.lock(), TA.states[2]);
 
diff --git a/test/data_parametric_monitor_test.cc b/test/data_parametric_monitor_test.cc
index cb60dab..8ffd376 100644
--- a/test/data_parametric_monitor_test.cc
+++ b/test/data_parametric_monitor_test.cc
@@ -19,13 +19,13 @@ struct DummyDataTimedWordSubject : public SingleSubject<TWEvent> {
   std::vector<TWEvent> vec;
 };
 
-struct DummyDataParametricMonitorObserver : public Observer<DataParametricMonitorResult> {
+struct DummyDataParametricMonitorObserver : public Observer<DataParametricMonitorResult<double>> {
   DummyDataParametricMonitorObserver() {}
   virtual ~DummyDataParametricMonitorObserver() {}
-  void notify(const DataParametricMonitorResult& result) {
+  void notify(const DataParametricMonitorResult<double>& result) {
     resultVec.push_back(result);
   }
-  std::vector<DataParametricMonitorResult> resultVec;
+  std::vector<DataParametricMonitorResult<double>> resultVec;
 };
 
 struct DataParametricMonitorFixture {
@@ -41,7 +41,7 @@ struct DataParametricMonitorFixture {
     monitor.reset();            // release local ownership
     resultVec = std::move(observer->resultVec);
   }
-  std::vector<DataParametricMonitorResult> resultVec;
+  std::vector<DataParametricMonitorResult<double>> resultVec;
 };
 
 BOOST_AUTO_TEST_SUITE(DataParametricMonitorTest)
diff --git a/test/fixture/copy_automaton_fixture.hh b/test/fixture/copy_automaton_fixture.hh
index 46d7fd3..a5b89d9 100644
--- a/test/fixture/copy_automaton_fixture.hh
+++ b/test/fixture/copy_automaton_fixture.hh
@@ -18,7 +18,7 @@ struct CopyFixture {
         // Construct automaton
         automaton.states.resize(4);
         for (auto &state: automaton.states) {
-            state = std::make_shared<NonParametricTAState<int> >(false);
+            state = std::make_shared<NonParametricTAState<int, double> >(false);
         }
         automaton.initialStates = {automaton.states.front()};
         automaton.states[0]->isMatch = false;
@@ -86,8 +86,8 @@ struct CopyFixture {
             NonSymbolic::Update<int> update;
             std::vector<VariableID> resetVars;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[1]->next[0][0] = {
                 std::move(stringConstraints),
@@ -108,8 +108,8 @@ struct CopyFixture {
             NonSymbolic::Update<int> update;
             std::vector<VariableID> resetVars;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[1]->next[0][1] = {
                 std::move(stringConstraints),
@@ -132,8 +132,8 @@ struct CopyFixture {
             NonSymbolic::Update<int> update;
             std::vector<VariableID> resetVars;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[1]->next[0][2] = {
                 std::move(stringConstraints),
@@ -159,8 +159,8 @@ struct CopyFixture {
             NonSymbolic::Update<int> update;
             std::vector<VariableID> resetVars;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) <= 5);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) <= 5.);
 
             automaton.states[2]->next[0][0] = {
                 std::move(stringConstraints),
@@ -181,8 +181,8 @@ struct CopyFixture {
             NonSymbolic::Update<int> update;
             std::vector<VariableID> resetVars;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) <= 5);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) <= 5.);
 
             automaton.states[2]->next[0][1] = {
                 std::move(stringConstraints),
@@ -205,8 +205,8 @@ struct CopyFixture {
             NonSymbolic::Update<int> update;
             std::vector<VariableID> resetVars;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[2]->next[0][2] = {
                 std::move(stringConstraints),
@@ -225,8 +225,8 @@ struct CopyFixture {
             NonSymbolic::Update<int> update;
             std::vector<VariableID> resetVars;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) > 5);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) > 5.);
 
             automaton.states[2]->next[0][3] = {
                 std::move(stringConstraints),
@@ -239,13 +239,13 @@ struct CopyFixture {
         }
     }
 
-    NonParametricTA<int> automaton;
+    NonParametricTA<int, double> automaton;
     std::unique_ptr<Signature> signature;
 };
 
 
 struct DataParametricCopy {
-    DataParametricTA automaton;
+    DataParametricTA<double> automaton;
     std::unique_ptr<Signature> signature;
 
     DataParametricCopy() {
@@ -257,7 +257,7 @@ struct DataParametricCopy {
         // Construct automaton
         automaton.states.resize(4);
         for (auto &state: automaton.states) {
-            state = std::make_shared<DataParametricTAState>(false);
+            state = std::make_shared<DataParametricTAState<double>>(false);
         }
         automaton.initialStates = {automaton.states.front()};
         automaton.states[0]->isMatch = false;
@@ -312,8 +312,8 @@ struct DataParametricCopy {
             std::vector<NumberConstraint> numConstraints;
             numConstraints.push_back(Variable(0) > Variable(1));
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[1]->next[0][0] = {
                 std::move(stringConstraints),
@@ -336,8 +336,8 @@ struct DataParametricCopy {
             std::vector<NumberConstraint> numConstraints;
             numConstraints.push_back(Variable(0) < Variable(1));
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[1]->next[0][1] = {
                 std::move(stringConstraints),
@@ -358,8 +358,8 @@ struct DataParametricCopy {
 
             std::vector<NumberConstraint> numConstraints;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[1]->next[0][2] = {
                 std::move(stringConstraints),
@@ -382,8 +382,8 @@ struct DataParametricCopy {
             std::vector<NumberConstraint> numConstraints;
             numConstraints.push_back(Variable(0) == Variable(1));
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[1]->next[0][3] = {
                 std::move(stringConstraints),
@@ -409,8 +409,8 @@ struct DataParametricCopy {
             std::vector<NumberConstraint> numConstraints;
             numConstraints.push_back(Variable(0) == Variable(1));
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 5);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 5.);
 
             automaton.states[2]->next[0][0] = {
                 std::move(stringConstraints),
@@ -431,8 +431,8 @@ struct DataParametricCopy {
 
             std::vector<NumberConstraint> numConstraints;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 5);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 5.);
 
             automaton.states[2]->next[0][1] = {
                 std::move(stringConstraints),
@@ -455,8 +455,8 @@ struct DataParametricCopy {
             std::vector<NumberConstraint> numConstraints;
             numConstraints.push_back(Variable(0) > Variable(1));
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[2]->next[0][2] = {
                 std::move(stringConstraints),
@@ -479,8 +479,8 @@ struct DataParametricCopy {
             std::vector<NumberConstraint> numConstraints;
             numConstraints.push_back(Variable(0) < Variable(1));
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) < 3);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) < 3.);
 
             automaton.states[2]->next[0][3] = {
                 std::move(stringConstraints),
@@ -499,8 +499,8 @@ struct DataParametricCopy {
             std::vector<StringConstraint> stringConstraints;
             std::vector<NumberConstraint> numConstraints;
 
-            std::vector<TimingConstraint> guard;
-            guard.push_back(ConstraintMaker(0) > 5);
+            std::vector<TimingConstraint<double>> guard;
+            guard.push_back(ConstraintMaker(0) > 5.);
 
             automaton.states[2]->next[0][4] = {
                 std::move(stringConstraints),
diff --git a/test/fixture/star_automaton_fixture.hh b/test/fixture/star_automaton_fixture.hh
index b487c4d..d2c28a7 100644
--- a/test/fixture/star_automaton_fixture.hh
+++ b/test/fixture/star_automaton_fixture.hh
@@ -21,7 +21,7 @@ struct StarAutomatonFixture {
         // Construct automaton with 3 states
         automaton.states.resize(3);
         for (auto &state: automaton.states) {
-            state = std::make_shared<NonParametricTAState<int> >(false);
+            state = std::make_shared<NonParametricTAState<int, int> >(false);
         }
         automaton.initialStates = {automaton.states[0]};
         automaton.states[0]->isMatch = false;  // Initial state is not final
@@ -73,7 +73,7 @@ struct StarAutomatonFixture {
         }
     }
 
-    NonParametricTA<int> automaton;
+    NonParametricTA<int, int> automaton;
     std::unique_ptr<Signature> signature;
 };
 
@@ -96,7 +96,7 @@ struct DataParametricStarAutomaton {
         // Construct automaton with 3 states
         automaton.states.resize(3);
         for (auto &state: automaton.states) {
-            state = std::make_shared<DataParametricTAState>(false);
+            state = std::make_shared<DataParametricTAState<int>>(false);
         }
         automaton.initialStates = {automaton.states[0]};
         automaton.states[0]->isMatch = false;  // Initial state is not final
@@ -148,7 +148,7 @@ struct DataParametricStarAutomaton {
         }
     }
 
-    DataParametricTA automaton;
+    DataParametricTA<int> automaton;
     std::unique_ptr<Signature> signature;
 };
 
diff --git a/test/fixture/time_restriction_automaton_fixture.hh b/test/fixture/time_restriction_automaton_fixture.hh
index 66ee572..be213d0 100644
--- a/test/fixture/time_restriction_automaton_fixture.hh
+++ b/test/fixture/time_restriction_automaton_fixture.hh
@@ -21,7 +21,7 @@ struct TimeRestrictionFixture {
         // Construct automaton with 2 states
         automaton.states.resize(2);
         for (auto &state: automaton.states) {
-            state = std::make_shared<NonParametricTAState<int> >(false);
+            state = std::make_shared<NonParametricTAState<int, double> >(false);
         }
         automaton.initialStates = {automaton.states[0]};
         automaton.states[0]->isMatch = false;  // Initial state is not final
@@ -52,7 +52,7 @@ struct TimeRestrictionFixture {
         }
     }
 
-    NonParametricTA<int> automaton;
+    NonParametricTA<int, double> automaton;
     std::unique_ptr<Signature> signature;
 };
 
@@ -75,7 +75,7 @@ struct DataParametricTimeRestrictionFixture {
         // Construct automaton with 2 states
         automaton.states.resize(2);
         for (auto &state: automaton.states) {
-            state = std::make_shared<DataParametricTAState>(false);
+            state = std::make_shared<DataParametricTAState<double>>(false);
         }
         automaton.initialStates = {automaton.states[0]};
         automaton.states[0]->isMatch = false;  // Initial state is not final
@@ -106,7 +106,7 @@ struct DataParametricTimeRestrictionFixture {
         }
     }
 
-    DataParametricTA automaton;
+    DataParametricTA<double> automaton;
     std::unique_ptr<Signature> signature;
 };
 
diff --git a/test/fixture/withdraw_automaton_fixture.hh b/test/fixture/withdraw_automaton_fixture.hh
index 3b3f69e..bde4d79 100644
--- a/test/fixture/withdraw_automaton_fixture.hh
+++ b/test/fixture/withdraw_automaton_fixture.hh
@@ -22,7 +22,7 @@ struct WithdrawFixture {
         // Construct automaton
         automaton.states.resize(3);
         for (auto &state: automaton.states) {
-            state = std::make_shared<NonParametricTAState<int> >(false);
+            state = std::make_shared<NonParametricTAState<int, double> >(false);
         }
         automaton.initialStates = {automaton.states.front()};
         automaton.states[0]->isMatch = false;
@@ -34,11 +34,11 @@ struct WithdrawFixture {
         automaton.numberVariableSize = 1;
 
         // Create timing constraints
-        std::vector<TimingConstraint> lessThanEqual30;
-        lessThanEqual30.push_back(ConstraintMaker(0) <= 30);
+        std::vector<TimingConstraint<double>> lessThanEqual30;
+        lessThanEqual30.push_back(ConstraintMaker(0) <= 30.);
 
-        std::vector<TimingConstraint> greaterThan30;
-        greaterThan30.push_back(ConstraintMaker(0) > 30);
+        std::vector<TimingConstraint<double>> greaterThan30;
+        greaterThan30.push_back(ConstraintMaker(0) > 30.);
 
         // #### FROM STATE 0 ####
         automaton.states[0]->next[0].resize(2);
@@ -146,7 +146,7 @@ struct WithdrawFixture {
         }
     }
 
-    NonParametricTA<int> automaton;
+    NonParametricTA<int, double> automaton;
     std::unique_ptr<Signature> signature;
 };
 
@@ -164,7 +164,7 @@ struct DataParametricWithdrawFixture {
         // Construct automaton
         automaton.states.resize(3);
         for (auto &state: automaton.states) {
-            state = std::make_shared<DataParametricTAState>(false);
+            state = std::make_shared<DataParametricTAState<double>>(false);
         }
         automaton.initialStates = {automaton.states.front()};
         automaton.states[0]->isMatch = false;
@@ -176,11 +176,11 @@ struct DataParametricWithdrawFixture {
         automaton.numberVariableSize = 1;
 
         // Create timing constraints
-        std::vector<TimingConstraint> lessThanEqual30;
-        lessThanEqual30.push_back(ConstraintMaker(0) <= 30);
+        std::vector<TimingConstraint<double>> lessThanEqual30;
+        lessThanEqual30.push_back(ConstraintMaker(0) <= 30.);
 
-        std::vector<TimingConstraint> greaterThan30;
-        greaterThan30.push_back(ConstraintMaker(0) > 30);
+        std::vector<TimingConstraint<double>> greaterThan30;
+        greaterThan30.push_back(ConstraintMaker(0) > 30.);
 
         // #### FROM STATE 0 ####
         automaton.states[0]->next[0].resize(2);
@@ -288,7 +288,7 @@ struct DataParametricWithdrawFixture {
         }
     }
 
-    DataParametricTA automaton;
+    DataParametricTA<double> automaton;
     std::unique_ptr<Signature> signature;
 };
 
diff --git a/test/symon_parser_test.cc b/test/symon_parser_test.cc
index ea21f3e..f487057 100644
--- a/test/symon_parser_test.cc
+++ b/test/symon_parser_test.cc
@@ -26,7 +26,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
     using Update = Update<int>;
 
         struct CopyParserFixture {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string path = PROJECT_ROOT "/example/copy/copy.symon";
 
             CopyParserFixture() {
@@ -44,18 +44,18 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_FIXTURE_TEST_CASE(declarations, CopyParserFixture) {
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 1);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 1);
         }
 
         BOOST_AUTO_TEST_CASE(atomic) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value)";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 0);
@@ -81,11 +81,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(stringConstraint) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value | id == \"y\")";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 0);
@@ -114,11 +114,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(timingConstraint) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))%(< 5)";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 1);
@@ -139,18 +139,18 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().numConstraints.size(), 0);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint::Order::lt);
+            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::lt);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().c, 5);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().update.stringUpdate.size(), 0);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().update.numberUpdate.size(), 0);
         }
 
         BOOST_AUTO_TEST_CASE(concat) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value); update(id, value)";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 0);
@@ -194,11 +194,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(orEmpty) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))?";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 0);
@@ -234,11 +234,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(plus) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))+";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 0);
@@ -278,11 +278,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(one_or_more) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} one_or_more {update(id, value)}";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 0);
@@ -322,11 +322,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(star) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))*";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 0);
@@ -372,11 +372,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(zero_or_more) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} zero_or_more{update(id, value)}";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 0);
@@ -422,11 +422,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(orEmptyConcat) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))?;update(id, value)";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 0);
@@ -472,11 +472,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(timingConstraintConcat) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value); (update(id, value))%(> 5)";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 1);
@@ -513,7 +513,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().numConstraints.size(), 0);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().odr, TimingConstraint::Order::gt);
+            BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::gt);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().c, 5);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().update.stringUpdate.size(), 0);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().update.numberUpdate.size(), 0);
@@ -522,11 +522,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(optionalWithTimingConstraintLT) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value)?)%(< 3)";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 1);
@@ -558,7 +558,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have the timing constraint < 3
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint::Order::lt);
+            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::lt);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().c, 3);
             
             // The final states should have no transitions
@@ -567,11 +567,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(optionalWithTimingConstraintGT) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value)?)%(> 3)";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 1);
@@ -603,7 +603,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint > 3
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint::Order::gt);
+            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::gt);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().c, 3);
             
             // The intermediate state should have transitions for the update operation
@@ -611,11 +611,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(concatOptionalWithTimingConstraint) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value); (update(id, value)?)%(< 3)";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 1);
@@ -661,7 +661,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint < 3
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().odr, TimingConstraint::Order::lt);
+            BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::lt);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().c, 3);
             
             // The final state should have no transitions
@@ -673,7 +673,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // only the upper bound is added to all transitions
             
             // Create a parser
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             
             // Parse a simple automaton with a timing constraint that has both upper and lower bounds
             std::string content = R"(
@@ -706,10 +706,10 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             bool hasUpperBound = false;
             
             for (const auto& constraint : automaton.states[0]->next[0].front().guard) {
-                if (constraint.odr == ::TimingConstraint::Order::ge && constraint.c == 2) {
+                if (constraint.odr == ::TimingConstraint<double>::Order::ge && constraint.c == 2) {
                     // This is the original lower bound
                     hasLowerBound = true;
-                } else if (constraint.odr == ::TimingConstraint::Order::le && constraint.c == 5) {
+                } else if (constraint.odr == ::TimingConstraint<double>::Order::le && constraint.c == 5) {
                     // This is the original upper bound
                     hasUpperBound = true;
                 }
@@ -723,7 +723,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(inits) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             std::ifstream ifs(PROJECT_ROOT "/example/inits.symon");
             // This should throw an exception because initial constraints are not supported in non-symbolic automata
             BOOST_CHECK_THROW(parser.parse(ifs), std::runtime_error);
@@ -733,21 +733,21 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // Test that the extractUpperBound function correctly extracts the upper bound from a timing constraint
             
             // Create a timing constraint with both upper and lower bounds
-            std::vector<TimingConstraint> guard;
+            std::vector<TimingConstraint<double>> guard;
             
             // Add a lower bound: x >= 2
-            guard.push_back(TimingConstraint{VariableID{0}, TimingConstraint::Order::ge, 2});
+            guard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraint<double>::Order::ge, 2});
             
             // Add an upper bound: x <= 5
-            guard.push_back(TimingConstraint{VariableID{0}, TimingConstraint::Order::le, 5});
+            guard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraint<double>::Order::le, 5});
             
             // Extract the upper bound
-            auto upperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update>::extractUpperBound(guard);
+            auto upperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double>::extractUpperBound(guard);
             
             // Verify that only the upper bound was extracted
             BOOST_CHECK_EQUAL(upperBound.size(), 1);
             BOOST_CHECK_EQUAL(upperBound[0].x, VariableID{0});
-            BOOST_CHECK_EQUAL(upperBound[0].odr, TimingConstraint::Order::le);
+            BOOST_CHECK_EQUAL(upperBound[0].odr, TimingConstraint<double>::Order::le);
             BOOST_CHECK_EQUAL(upperBound[0].c, 5);
         }
         
@@ -755,21 +755,21 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // Test that extractUpperBound for parametric and non-parametric cases are equivalent
             
             // Create a non-parametric timing constraint with both upper and lower bounds
-            std::vector<TimingConstraint> nonParametricGuard;
+            std::vector<TimingConstraint<double>> nonParametricGuard;
             
             // Add a lower bound: x >= 2
-            nonParametricGuard.push_back(TimingConstraint{VariableID{0}, TimingConstraint::Order::ge, 2});
+            nonParametricGuard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraint<double>::Order::ge, 2});
             
             // Add an upper bound: x <= 5
-            nonParametricGuard.push_back(TimingConstraint{VariableID{0}, TimingConstraint::Order::le, 5});
+            nonParametricGuard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraint<double>::Order::le, 5});
             
             // Extract the upper bound from the non-parametric guard
-            auto nonParametricUpperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update>::extractUpperBound(nonParametricGuard);
+            auto nonParametricUpperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double>::extractUpperBound(nonParametricGuard);
             
             // Verify that only the upper bound was extracted
             BOOST_CHECK_EQUAL(nonParametricUpperBound.size(), 1);
             BOOST_CHECK_EQUAL(nonParametricUpperBound[0].x, VariableID{0});
-            BOOST_CHECK_EQUAL(nonParametricUpperBound[0].odr, TimingConstraint::Order::le);
+            BOOST_CHECK_EQUAL(nonParametricUpperBound[0].odr, TimingConstraint<double>::Order::le);
             BOOST_CHECK_EQUAL(nonParametricUpperBound[0].c, 5);
             
             // Create an equivalent parametric timing constraint
@@ -783,7 +783,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             parametricGuard.add_constraint(x <= 5);
             
             // Extract the upper bound from the parametric guard
-            auto parametricUpperBound = SymonParser<StringConstraint, NumberConstraint<int>, ParametricTimingConstraint, Update>::extractUpperBound(parametricGuard);
+            auto parametricUpperBound = SymonParser<StringConstraint, NumberConstraint<int>, ParametricTimingConstraint, Update, double>::extractUpperBound(parametricGuard);
             
             // Verify that the parametric upper bound contains only the upper bound constraint
             // We can't directly compare the constraints, but we can check that:
@@ -807,11 +807,11 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(case20250703_1) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint>, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
             const std::string content = "signature A {id: string;} signature B {id: string;} ((A( id | id != \"Bob\" ) || B( id | id != \"Bob\" ))%(<= 5);B (id | id == \"Bob\"))%(> 5)";
             parser.parse(content);
 
-            const NonParametricTA<int> automaton = parser.getAutomaton();
+            const NonParametricTA<int, double> automaton = parser.getAutomaton();
             BOOST_CHECK_EQUAL(automaton.numberVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.stringVariableSize, 0);
             BOOST_CHECK_EQUAL(automaton.clockVariableSize, 1);
@@ -841,7 +841,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint <= 5
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint::Order::le);
+            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::le);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().c, 5);
             
             // Transition for the first B
@@ -854,7 +854,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint <= 5
             BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.front().odr, TimingConstraint::Order::le);
+            BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.front().odr, TimingConstraint<double>::Order::le);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.front().c, 5);
 
             // Transition for the second B
@@ -867,7 +867,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint > 5
             BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.front().odr, TimingConstraint::Order::gt);
+            BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.front().odr, TimingConstraint<double>::Order::gt);
             BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.front().c, 5);
         }
 
@@ -877,7 +877,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         using namespace Symbolic;
 
         struct ParametricCopyParserFixture {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
             const std::string path = PROJECT_ROOT "/example/copy/copy.symon";
 
             ParametricCopyParserFixture() {
@@ -902,7 +902,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(inits) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
             std::ifstream ifs(PROJECT_ROOT "/example/inits.symon");
             parser.parse(ifs);
             const auto automaton = parser.getAutomaton();
@@ -918,8 +918,8 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(updates) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
-            const std::string content = "var {count: number; count2: number;} signature update {id: string;value: number;} update(id, value | | count := count + 1; count2 := count2 + 2 ; count := count + count2)";
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
+            const std::string content = "var {count: number; count2: number;} signature update {id: string;value: number;} update(id, value | | count := count + 1; count2 := count2 + 2 ; count := count + count 2)";
             parser.parse(content);
 
             const auto automaton = parser.getAutomaton();
@@ -948,7 +948,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(timingConstraintConcat) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value); (update(id, value))%(> 5)";
             parser.parse(content);
 
@@ -1005,7 +1005,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(parametricTimingConstraint) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
             const std::string content = "var {p: param;} signature A {} A()%(< p)";
             parser.parse(content);
 
@@ -1042,7 +1042,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(parametricTimingConstraintStar) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
             const std::string content = "var {p: param;} signature A {} (A()%(< p))*";
             parser.parse(content);
 
@@ -1095,7 +1095,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(parametricTimingConstraintStarConcat) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
             const std::string content = "var {p: param;} signature A {} A();(A()%(< p))*";
             parser.parse(content);
 
diff --git a/test/timing_constraint_test.cc b/test/timing_constraint_test.cc
index 3f62f9c..4c4debf 100644
--- a/test/timing_constraint_test.cc
+++ b/test/timing_constraint_test.cc
@@ -5,15 +5,15 @@
 
 BOOST_AUTO_TEST_SUITE(TimingConstraintTest)
     BOOST_AUTO_TEST_CASE(Shift) {
-        constexpr TimingConstraint constraint{0, TimingConstraint::Order::lt, 10};
+        constexpr TimingConstraint<double> constraint{0, TimingConstraint<double>::Order::lt, 10};
         auto [x, odr, c] = constraint.shift(1);
         BOOST_CHECK_EQUAL(x, 1);
-        BOOST_CHECK_EQUAL(odr, TimingConstraint::Order::lt);
+        BOOST_CHECK_EQUAL(odr, TimingConstraint<double>::Order::lt);
         BOOST_CHECK_EQUAL(c, 10);
     }
 
     BOOST_AUTO_TEST_CASE(Satisfy) {
-        constexpr TimingConstraint constraint{0, TimingConstraint::Order::lt, 10};
+        constexpr TimingConstraint<double> constraint{0, TimingConstraint<double>::Order::lt, 10};
         BOOST_CHECK(constraint.satisfy(5));
         BOOST_CHECK(!constraint.satisfy(10));
         BOOST_CHECK(!constraint.satisfy(15));

From afd7f09173efd757b03287982ec00fc85bb7eee9 Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Tue, 25 Nov 2025 02:41:19 +0900
Subject: [PATCH 06/14] Move TimingConstraint<Timestamp>::Order to
 TimingConstraintOrder

---
 src/automaton_parser.hh          | 28 ++++++++++++++--------------
 src/symon_parser.hh              |  2 +-
 src/timing_constraint.hh         | 25 ++++++++++++-------------
 test/automaton_operation_test.cc |  4 ++--
 test/automaton_parser_test.cc    | 10 +++++-----
 test/symon_parser_test.cc        | 32 ++++++++++++++++----------------
 test/timing_constraint_test.cc   |  6 +++---
 7 files changed, 53 insertions(+), 54 deletions(-)

diff --git a/src/automaton_parser.hh b/src/automaton_parser.hh
index 3f6e375..23e5906 100644
--- a/src/automaton_parser.hh
+++ b/src/automaton_parser.hh
@@ -57,18 +57,18 @@ namespace boost {
 } // namespace boost
 
 template <typename Timestamp>
-static inline std::ostream &operator<<(std::ostream &os, const typename TimingConstraint<Timestamp>::Order &odr) {
+static inline std::ostream &operator<<(std::ostream &os, const TimingConstraintOrder &odr) {
   switch (odr) {
-    case TimingConstraint<Timestamp>::Order::lt:
+    case TimingConstraintOrder::lt:
       os << "<";
       break;
-    case TimingConstraint<Timestamp>::Order::le:
+    case TimingConstraintOrder::le:
       os << "<=";
       break;
-    case TimingConstraint<Timestamp>::Order::ge:
+    case TimingConstraintOrder::ge:
       os << ">=";
       break;
-    case TimingConstraint<Timestamp>::Order::gt:
+    case TimingConstraintOrder::gt:
       os << ">";
       break;
     case TimingConstraint::Order::eq:
@@ -78,18 +78,18 @@ static inline std::ostream &operator<<(std::ostream &os, const typename TimingCo
   return os;
 }
 
-static inline std::ostream &operator<<(std::ostream &os, const TimingConstraint<double>::Order &odr) {
+static inline std::ostream &operator<<(std::ostream &os, const TimingConstraintOrder &odr) {
   switch (odr) {
-    case TimingConstraint<double>::Order::lt:
+    case TimingConstraintOrder::lt:
       os << "<";
       break;
-    case TimingConstraint<double>::Order::le:
+    case TimingConstraintOrder::le:
       os << "<=";
       break;
-    case TimingConstraint<double>::Order::ge:
+    case TimingConstraintOrder::ge:
       os << ">=";
       break;
-    case TimingConstraint<double>::Order::gt:
+    case TimingConstraintOrder::gt:
       os << ">";
       break;
   }
@@ -127,13 +127,13 @@ static inline std::istream &operator>>(std::istream &is, TimingConstraint<Timest
   switch (odr[0]) {
     case '>':
       if (odr[1] == '=') {
-        p.odr = TimingConstraint<Timestamp>::Order::ge;
+        p.odr = TimingConstraintOrder::ge;
         if (is.get() != ' ') {
           is.setstate(std::ios_base::failbit);
           return is;
         }
       } else if (odr[1] == ' ') {
-        p.odr = TimingConstraint<Timestamp>::Order::gt;
+        p.odr = TimingConstraintOrder::gt;
       } else {
         is.setstate(std::ios_base::failbit);
         return is;
@@ -141,13 +141,13 @@ static inline std::istream &operator>>(std::istream &is, TimingConstraint<Timest
       break;
     case '<':
       if (odr[1] == '=') {
-        p.odr = TimingConstraint<Timestamp>::Order::le;
+        p.odr = TimingConstraintOrder::le;
         if (is.get() != ' ') {
           is.setstate(std::ios_base::failbit);
           return is;
         }
       } else if (odr[1] == ' ') {
-        p.odr = TimingConstraint<Timestamp>::Order::lt;
+        p.odr = TimingConstraintOrder::lt;
       } else {
         is.setstate(std::ios_base::failbit);
         return is;
diff --git a/src/symon_parser.hh b/src/symon_parser.hh
index 69480ed..cbab594 100644
--- a/src/symon_parser.hh
+++ b/src/symon_parser.hh
@@ -202,7 +202,7 @@ public:
     // Check each constraint in the guard
     for (const auto &constraint: guard) {
       // If the constraint is an upper bound (lt or le), add it to the result
-      if (constraint.odr == ::TimingConstraint<Timestamp>::Order::lt || constraint.odr == ::TimingConstraint<Timestamp>::Order::le) {
+      if (constraint.odr == ::TimingConstraintOrder::le) {
         upperBound.push_back(constraint);
       }
     }
diff --git a/src/timing_constraint.hh b/src/timing_constraint.hh
index 69e4e9c..01f1ea6 100644
--- a/src/timing_constraint.hh
+++ b/src/timing_constraint.hh
@@ -15,25 +15,24 @@ inline bool toBool(Order odr) {
   return odr == Order::EQ;
 }
 
+enum class TimingConstraintOrder { lt, le, ge, gt };
+
 //! @brief A constraint in a guard of transitions
 template <typename Timestamp>
 struct TimingConstraint {
-  enum class Order { lt, le, ge, gt, eq };
-  using Timestamp = double;
-
   ClockVariables x;
-  Order odr;
+  TimingConstraintOrder odr;
   Timestamp c;
 
   [[nodiscard]] bool satisfy(Timestamp d) const {
     switch (odr) {
-      case Order::lt:
+      case TimingConstraintOrder::lt:
         return d < c;
-      case Order::le:
+      case TimingConstraintOrder::le:
         return d <= c;
-      case Order::gt:
+      case TimingConstraintOrder::gt:
         return d > c;
-      case Order::ge:
+      case TimingConstraintOrder::ge:
         return d >= c;
       case Order::eq:
         return d == c;
@@ -46,7 +45,7 @@ struct TimingConstraint {
   ::Order operator()(Interpretation val) const {
     if (satisfy(val.at(x))) {
       return ::Order::EQ;
-    } else if (odr == Order::lt || odr == Order::le) {
+    } else if (odr == TimingConstraintOrder::lt || odr == TimingConstraintOrder::le) {
       return ::Order::GT;
     } else {
       return ::Order::LT;
@@ -79,22 +78,22 @@ public:
 
   template<typename Timestamp = double>
   TimingConstraint<Timestamp> operator<(Timestamp c) {
-    return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::lt, c};
+    return TimingConstraint<Timestamp>{x, TimingConstraintOrder::lt, c};
   }
 
   template<typename Timestamp = double>
   TimingConstraint<Timestamp> operator<=(Timestamp c) {
-    return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::le, c};
+    return TimingConstraint<Timestamp>{x, TimingConstraintOrder::le, c};
   }
 
   template<typename Timestamp = double>
   TimingConstraint<Timestamp> operator>(Timestamp c) {
-    return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::gt, c};
+    return TimingConstraint<Timestamp>{x, TimingConstraintOrder::gt, c};
   }
 
   template<typename Timestamp = double>
   TimingConstraint<Timestamp> operator>=(Timestamp c) {
-    return TimingConstraint<Timestamp>{x, TimingConstraint<Timestamp>::Order::ge, c};
+    return TimingConstraint<Timestamp>{x, TimingConstraintOrder::ge, c};
   }
 
   TimingConstraint operator==(Timestamp c) {
diff --git a/test/automaton_operation_test.cc b/test/automaton_operation_test.cc
index 17705d9..4f545dd 100644
--- a/test/automaton_operation_test.cc
+++ b/test/automaton_operation_test.cc
@@ -378,7 +378,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
                         // Check that the constraint is applied to the transition
                         bool hasConstraint = false;
                         for (const auto &guard : transition.guard) {
-                            if (guard.x == 0 && guard.odr == TimingConstraint<double>::Order::le && guard.c == 5) {
+                            if (guard.x == 0 && guard.odr == TimingConstraintOrder::le && guard.c == 5) {
                                 hasConstraint = true;
                                 break;
                             }
@@ -766,7 +766,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
                         // Check that the constraint is applied to the transition
                         bool hasConstraint = false;
                         for (const auto &guard : transition.guard) {
-                            if (guard.x == 0 && guard.odr == TimingConstraint<double>::Order::le && guard.c == 5) {
+                            if (guard.x == 0 && guard.odr == TimingConstraintOrder::le && guard.c == 5) {
                                 hasConstraint = true;
                                 break;
                             }
diff --git a/test/automaton_parser_test.cc b/test/automaton_parser_test.cc
index 9d82905..7080eeb 100644
--- a/test/automaton_parser_test.cc
+++ b/test/automaton_parser_test.cc
@@ -331,7 +331,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).update.numberUpdate.size(), 0);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, TimingConstraint<double>::Order::lt);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, TimingConstraintOrder::lt);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().c, 3);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).target.lock(), TA.states[1]);
 
@@ -416,7 +416,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).update.numberUpdate.size(), 0);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, ::TimingConstraint<double>::Order::lt);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, ::TimingConstraintOrder::lt);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().c, 3);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).target.lock(), TA.states[1]);
 
@@ -495,7 +495,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).update.numberUpdate.size(), 0);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, ::TimingConstraint<double>::Order::le);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().odr, ::TimingConstraintOrder::le);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).guard.front().c, 30);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(0).target.lock(), TA.states[1]);
 
@@ -516,7 +516,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
                 Variable(0) + Variable(1)));
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.front().odr, ::TimingConstraint<double>::Order::le);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.front().odr, ::TimingConstraintOrder::le);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).guard.front().c, 30);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(1).target.lock(), TA.states[1]);
 
@@ -528,7 +528,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonParserTests)
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).update.numberUpdate.size(), 0);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.size(), 1);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.front().x, 0);
-        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.front().odr, ::TimingConstraint<double>::Order::gt);
+        BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.front().odr, ::TimingConstraintOrder::gt);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).guard.front().c, 30);
         BOOST_CHECK_EQUAL(TA.states[1]->next.at(0).at(2).target.lock(), TA.states[2]);
 
diff --git a/test/symon_parser_test.cc b/test/symon_parser_test.cc
index f487057..8c118a0 100644
--- a/test/symon_parser_test.cc
+++ b/test/symon_parser_test.cc
@@ -139,7 +139,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().numConstraints.size(), 0);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::lt);
+            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraintOrder::lt);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().c, 5);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().update.stringUpdate.size(), 0);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().update.numberUpdate.size(), 0);
@@ -513,7 +513,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().numConstraints.size(), 0);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::gt);
+            BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().odr, TimingConstraintOrder::gt);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().c, 5);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().update.stringUpdate.size(), 0);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().update.numberUpdate.size(), 0);
@@ -558,7 +558,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have the timing constraint < 3
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::lt);
+            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraintOrder::lt);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().c, 3);
             
             // The final states should have no transitions
@@ -603,7 +603,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint > 3
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::gt);
+            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraintOrder::gt);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().c, 3);
             
             // The intermediate state should have transitions for the update operation
@@ -661,7 +661,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint < 3
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::lt);
+            BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().odr, TimingConstraintOrder::lt);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[0].front().guard.front().c, 3);
             
             // The final state should have no transitions
@@ -706,10 +706,10 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             bool hasUpperBound = false;
             
             for (const auto& constraint : automaton.states[0]->next[0].front().guard) {
-                if (constraint.odr == ::TimingConstraint<double>::Order::ge && constraint.c == 2) {
+                if (constraint.odr == ::TimingConstraintOrder::ge && constraint.c == 2) {
                     // This is the original lower bound
                     hasLowerBound = true;
-                } else if (constraint.odr == ::TimingConstraint<double>::Order::le && constraint.c == 5) {
+                } else if (constraint.odr == ::TimingConstraintOrder::le && constraint.c == 5) {
                     // This is the original upper bound
                     hasUpperBound = true;
                 }
@@ -736,10 +736,10 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             std::vector<TimingConstraint<double>> guard;
             
             // Add a lower bound: x >= 2
-            guard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraint<double>::Order::ge, 2});
+            guard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraintOrder::ge, 2});
             
             // Add an upper bound: x <= 5
-            guard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraint<double>::Order::le, 5});
+            guard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraintOrder::le, 5});
             
             // Extract the upper bound
             auto upperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double>::extractUpperBound(guard);
@@ -747,7 +747,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // Verify that only the upper bound was extracted
             BOOST_CHECK_EQUAL(upperBound.size(), 1);
             BOOST_CHECK_EQUAL(upperBound[0].x, VariableID{0});
-            BOOST_CHECK_EQUAL(upperBound[0].odr, TimingConstraint<double>::Order::le);
+            BOOST_CHECK_EQUAL(upperBound[0].odr, TimingConstraintOrder::le);
             BOOST_CHECK_EQUAL(upperBound[0].c, 5);
         }
         
@@ -758,10 +758,10 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             std::vector<TimingConstraint<double>> nonParametricGuard;
             
             // Add a lower bound: x >= 2
-            nonParametricGuard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraint<double>::Order::ge, 2});
+            nonParametricGuard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraintOrder::ge, 2});
             
             // Add an upper bound: x <= 5
-            nonParametricGuard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraint<double>::Order::le, 5});
+            nonParametricGuard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraintOrder::le, 5});
             
             // Extract the upper bound from the non-parametric guard
             auto nonParametricUpperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double>::extractUpperBound(nonParametricGuard);
@@ -769,7 +769,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // Verify that only the upper bound was extracted
             BOOST_CHECK_EQUAL(nonParametricUpperBound.size(), 1);
             BOOST_CHECK_EQUAL(nonParametricUpperBound[0].x, VariableID{0});
-            BOOST_CHECK_EQUAL(nonParametricUpperBound[0].odr, TimingConstraint<double>::Order::le);
+            BOOST_CHECK_EQUAL(nonParametricUpperBound[0].odr, TimingConstraintOrder::le);
             BOOST_CHECK_EQUAL(nonParametricUpperBound[0].c, 5);
             
             // Create an equivalent parametric timing constraint
@@ -841,7 +841,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint <= 5
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraint<double>::Order::le);
+            BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().odr, TimingConstraintOrder::le);
             BOOST_CHECK_EQUAL(automaton.states[0]->next[0].front().guard.front().c, 5);
             
             // Transition for the first B
@@ -854,7 +854,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint <= 5
             BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.front().odr, TimingConstraint<double>::Order::le);
+            BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.front().odr, TimingConstraintOrder::le);
             BOOST_CHECK_EQUAL(automaton.states[1]->next[1].front().guard.front().c, 5);
 
             // Transition for the second B
@@ -867,7 +867,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // The transition should have timing constraint > 5
             BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.size(), 1);
             BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.front().x, VariableID{0});
-            BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.front().odr, TimingConstraint<double>::Order::gt);
+            BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.front().odr, TimingConstraintOrder::gt);
             BOOST_CHECK_EQUAL(automaton.states[2]->next[1].front().guard.front().c, 5);
         }
 
diff --git a/test/timing_constraint_test.cc b/test/timing_constraint_test.cc
index 4c4debf..64970c7 100644
--- a/test/timing_constraint_test.cc
+++ b/test/timing_constraint_test.cc
@@ -5,15 +5,15 @@
 
 BOOST_AUTO_TEST_SUITE(TimingConstraintTest)
     BOOST_AUTO_TEST_CASE(Shift) {
-        constexpr TimingConstraint<double> constraint{0, TimingConstraint<double>::Order::lt, 10};
+        constexpr TimingConstraint<double> constraint{0, TimingConstraintOrder::lt, 10};
         auto [x, odr, c] = constraint.shift(1);
         BOOST_CHECK_EQUAL(x, 1);
-        BOOST_CHECK_EQUAL(odr, TimingConstraint<double>::Order::lt);
+        BOOST_CHECK_EQUAL(odr, TimingConstraintOrder::lt);
         BOOST_CHECK_EQUAL(c, 10);
     }
 
     BOOST_AUTO_TEST_CASE(Satisfy) {
-        constexpr TimingConstraint<double> constraint{0, TimingConstraint<double>::Order::lt, 10};
+        constexpr TimingConstraint<double> constraint{0, TimingConstraintOrder::lt, 10};
         BOOST_CHECK(constraint.satisfy(5));
         BOOST_CHECK(!constraint.satisfy(10));
         BOOST_CHECK(!constraint.satisfy(15));

From 13c7bad91ae028ffd475ddb54edd9b48ac1aad25 Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Thu, 27 Nov 2025 00:18:55 +0900
Subject: [PATCH 07/14] Refactor: Remove Timestamp template parameter from
 various functions and update related code

---
 src/automata_operation.hh        | 20 +++++++-----
 src/automaton_parser.hh          | 22 -------------
 src/main.cc                      |  6 ++--
 src/symon_parser.hh              | 22 ++++++++-----
 src/timing_constraint.hh         | 34 +++++++++++++++++++
 test/automaton_operation_test.cc | 27 +++++----------
 test/symon_parser_test.cc        | 56 ++++++++++++++++----------------
 7 files changed, 98 insertions(+), 89 deletions(-)

diff --git a/src/automata_operation.hh b/src/automata_operation.hh
index 99727dc..f573196 100644
--- a/src/automata_operation.hh
+++ b/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>
 
@@ -177,7 +178,7 @@ bool acceptsEmptyWord(const TimedAutomaton<StringConstraint, NumberConstraint, T
  * @param[in] right  The second (right-hand) timed automaton.
  * @return A TimedAutomaton representing the concatenation of two automata.
  */
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Timestamp>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update>
 TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update>
 concatenate(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &&left,
             TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &&right) {
@@ -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<Timestamp>>>) {
+        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);
@@ -350,7 +351,7 @@ star(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update
  * @param[in] guard The timing constraint that restricts the time.
  * @return A TimedAutomaton with the new timing constraint on the total elapsed time.
  */
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Timestamp>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update>
 TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update>
 timeRestriction(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &&given,
                 TimingConstraint guard) {
@@ -358,8 +359,9 @@ timeRestriction(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstra
 
   bool acceptEmpty = acceptsEmptyWord(given);
 
-  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Timestamp>>>) {
-    TimingValuation<Timestamp> 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<Timestamp>>>) {
+  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<Timestamp>>>) {
+        if constexpr (is_vector_of_timingconstraint_v<TimingConstraint>) {
           it->guard = adjustDimension(it->guard, given.clockVariableSize);
         }
         if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
@@ -473,14 +475,14 @@ ignoreActions(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstrain
  * @param[in] constraint The timing constraint to add to all transitions.
  * @return A reference to the modified automaton.
  */
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Timestamp>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update>
 TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &
 addConstraintToAllTransitions(TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update> &automaton,
                               const TimingConstraint &constraint) {
 
   TimingConstraint adjustedConstraint = constraint;
   // Ensure the constraint has the correct dimension for the automaton
-  if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Timestamp>>>) {
+  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);
diff --git a/src/automaton_parser.hh b/src/automaton_parser.hh
index 23e5906..041e129 100644
--- a/src/automaton_parser.hh
+++ b/src/automaton_parser.hh
@@ -56,28 +56,6 @@ namespace boost {
   BOOST_INSTALL_PROPERTY(edge, guard);
 } // namespace boost
 
-template <typename Timestamp>
-static inline std::ostream &operator<<(std::ostream &os, const TimingConstraintOrder &odr) {
-  switch (odr) {
-    case TimingConstraintOrder::lt:
-      os << "<";
-      break;
-    case TimingConstraintOrder::le:
-      os << "<=";
-      break;
-    case TimingConstraintOrder::ge:
-      os << ">=";
-      break;
-    case TimingConstraintOrder::gt:
-      os << ">";
-      break;
-    case TimingConstraint::Order::eq:
-      os << "==";
-      break;
-  }
-  return os;
-}
-
 static inline std::ostream &operator<<(std::ostream &os, const TimingConstraintOrder &odr) {
   switch (odr) {
     case TimingConstraintOrder::lt:
diff --git a/src/main.cc b/src/main.cc
index 5b6772b..bb84b0f 100644
--- a/src/main.cc
+++ b/src/main.cc
@@ -50,7 +50,7 @@ int execute(const std::string &timedAutomatonFileName, const std::string &signat
 
   if (useNewSyntax) {
     // Use the new syntax parser
-    SymonParser<StringConstraint, NumberConstraint, TimingConstraintType, UpdateType, Timestamp> parser;
+    SymonParser<StringConstraint, NumberConstraint, TimingConstraintType, UpdateType> parser;
     try {
       parser.parse(taStream);
     } catch (const std::runtime_error &e) {
@@ -176,7 +176,7 @@ int main(int argc, char *argv[]) {
                                                                       timedWordFileName, true);
     } else {
       // boolean with new syntax
-      return execute<NonParametricTA<Number, Timestamp>, NonParametricBoostTA<Number>, Number, Timestamp, BooleanMonitor<Number, Timestamp>,
+      return execute<NonParametricTA<Number, Timestamp>, NonParametricBoostTA<Number, Timestamp>, Number, Timestamp, BooleanMonitor<Number, Timestamp>,
                      BooleanPrinter<Number, Timestamp>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
                      std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>>(timedAutomatonFileName, signatureFileName,
                                                                          timedWordFileName, true);
@@ -194,7 +194,7 @@ int main(int argc, char *argv[]) {
                                                                     timedWordFileName, false);
   } else {
     // boolean
-    return execute<NonParametricTA<Number, Timestamp>, NonParametricBoostTA<Number>, Number, Timestamp, BooleanMonitor<Number, Timestamp>,
+    return execute<NonParametricTA<Number, Timestamp>, NonParametricBoostTA<Number, Timestamp>, Number, Timestamp, BooleanMonitor<Number, Timestamp>,
                    BooleanPrinter<Number, Timestamp>, NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<Number>,
                    std::vector<TimingConstraint<Timestamp>>, NonSymbolic::Update<Number>>(timedAutomatonFileName, signatureFileName,
                                                                        timedWordFileName, false);
diff --git a/src/symon_parser.hh b/src/symon_parser.hh
index cbab594..1236e2e 100644
--- a/src/symon_parser.hh
+++ b/src/symon_parser.hh
@@ -78,7 +78,7 @@ static inline TSNode nextNonCommentChild(const TSNode &parent, uint32_t &idx) {
   return std::nullopt;
 }
 
-template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update, typename Timestamp>
+template <typename StringConstraint, typename NumberConstraint, typename TimingConstraint, typename Update>
 class SymonParser {
 public:
   using Automaton = TimedAutomaton<StringConstraint, NumberConstraint, TimingConstraint, Update>;
@@ -196,6 +196,7 @@ public:
 
 public:
   // Helper function to extract the upper bound from a non-parametric timing constraint
+  template <typename Timestamp>
   static std::vector<::TimingConstraint<Timestamp>> extractUpperBound(const std::vector<::TimingConstraint<Timestamp>> &guard) {
     std::vector<::TimingConstraint<Timestamp>> upperBound;
 
@@ -597,9 +598,11 @@ private:
           throw err;
         }
       } else {
-        return {boost::lexical_cast<::TimingConstraint<Timestamp>>("x" + std::to_string(clockIndex) + " " +
+        //TC = ::TimingConstraint<Timestamp>
+        using TC = timingconstraint_t<TimingConstraint>;
+        return {boost::lexical_cast<TC>("x" + std::to_string(clockIndex) + " " +
                                                         (isLowerInclusive ? ">=" : ">") + " " + lowerBound),
-                boost::lexical_cast<::TimingConstraint<Timestamp>>("x" + std::to_string(clockIndex) + " " +
+                boost::lexical_cast<TC>("x" + std::to_string(clockIndex) + " " +
                                                         (isUpperInclusive ? "<=" : "<") + " " + upperBound)};
       }
     }
@@ -628,8 +631,9 @@ private:
         result.add_constraint(constraint);
         return result;
       } else {
+        using TC = timingconstraint_t<TimingConstraint>;
         return {
-            boost::lexical_cast<::TimingConstraint<Timestamp>>("x" + std::to_string(clockIndex) + " " + comparator + " " + expr)};
+            boost::lexical_cast<TC>("x" + std::to_string(clockIndex) + " " + comparator + " " + expr)};
       }
     }
     throw std::runtime_error(makeErrorMessage(
@@ -837,7 +841,7 @@ private:
       TSNode rhsNode = nextNonCommentChild(child, p);
       Automaton lhs = this->parseExpr(content, lhsNode);
       Automaton rhs = this->parseExpr(content, rhsNode);
-      return concatenate<StringConstraint, NumberConstraint, TimingConstraint, Update, Timestamp>(std::move(lhs), std::move(rhs));
+      return concatenate<StringConstraint, NumberConstraint, TimingConstraint, Update>(std::move(lhs), std::move(rhs));
     } else if (kind == "conjunction") {
       uint32_t p = 0;
       TSNode lhsNode = nextNonCommentChild(child, p);
@@ -991,7 +995,7 @@ private:
       TimingConstraint guard = this->parseTimingConstraint(content, intervalNode, innerExpr.clockVariableSize);
 
       // Apply the time restriction operation
-      Automaton result = timeRestriction<StringConstraint, NumberConstraint, TimingConstraint, Update, Timestamp>(std::move(innerExpr), guard);
+      Automaton result = timeRestriction<StringConstraint, NumberConstraint, TimingConstraint, Update>(std::move(innerExpr), guard);
 
       if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
         assert(std::all_of(result.states.begin(), result.states.end(), [&](const auto &state) {
@@ -1005,17 +1009,17 @@ private:
       }
 
       // Extract the upper bound from the timing constraint and add it to all transitions
-      if constexpr (std::is_same_v<TimingConstraint, std::vector<::TimingConstraint<Timestamp>>>) {
+      if constexpr (is_vector_of_timingconstraint_v<TimingConstraint>) {
         // For non-parametric timing constraints
         auto upperBound = extractUpperBound(guard);
         if (!upperBound.empty()) {
           // It has an upper bound, add it to all transitions
-          addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update, Timestamp>(result, upperBound);
+          addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update>(result, upperBound);
         }
       } else if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
         // For parametric timing constraints
         auto upperBound = extractUpperBound(guard, this->parameters.size() + innerExpr.clockVariableSize - 1);
-        addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update, Timestamp>(result, upperBound);
+        addConstraintToAllTransitions<StringConstraint, NumberConstraint, TimingConstraint, Update>(result, upperBound);
       }
 
       if constexpr (std::is_same_v<TimingConstraint, ParametricTimingConstraint>) {
diff --git a/src/timing_constraint.hh b/src/timing_constraint.hh
index 01f1ea6..7113aa4 100644
--- a/src/timing_constraint.hh
+++ b/src/timing_constraint.hh
@@ -193,3 +193,37 @@ static std::vector<TimingConstraint<Timestamp>> adjustDimension(const std::vecto
                                                      const ClockVariables size) {
   return guard;
 }
+
+
+// T の参照/const/volatile を除去
+template<typename T>
+using remove_cvref_t = std::remove_cv_t<std::remove_reference_t<T>>;
+
+template<typename T>
+struct is_vector_of_timingconstraint_impl : std::false_type {};
+
+template<typename Timestamp>
+struct is_vector_of_timingconstraint_impl<std::vector<TimingConstraint<Timestamp>>> : std::true_type {};
+
+// T が std::vector<TimingConstraint<Timestamp>> の形かどうか
+template<typename T>
+constexpr bool is_vector_of_timingconstraint_v =
+    is_vector_of_timingconstraint_impl< remove_cvref_t<T> >::value;
+
+template<typename T>
+struct timingconstraint_timestamp_impl;
+
+template<typename Timestamp>
+struct timingconstraint_timestamp_impl<std::vector<TimingConstraint<Timestamp>>> {
+  using type = Timestamp;
+  using timingconstraint_type = TimingConstraint<Timestamp>;
+};
+
+// std::vector<TimingConstraint<Timestamp>> の Timestamp 型を取得
+template<typename T>
+using timingconstraint_timestamp_t =
+    typename timingconstraint_timestamp_impl< remove_cvref_t<T> >::type;
+
+template<typename T>
+using timingconstraint_t =
+    typename timingconstraint_timestamp_impl< remove_cvref_t<T> >::timingconstraint_type;
diff --git a/test/automaton_operation_test.cc b/test/automaton_operation_test.cc
index 4f545dd..4368f4a 100644
--- a/test/automaton_operation_test.cc
+++ b/test/automaton_operation_test.cc
@@ -72,8 +72,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             auto copyFinalState = copy.states[3];
             auto withdrawFinalState = withdraw.states[2];
 
-            auto result = concatenate<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<int>,
-                                       std::vector<TimingConstraint<double>>, NonSymbolic::Update<int>, double>(std::move(copy), std::move(withdraw));
+            auto result = concatenate(std::move(copy), std::move(withdraw));
 
             // Check the total number of states (should be the sum of both automata)
             BOOST_CHECK_EQUAL(result.states.size(), 6);
@@ -260,8 +259,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             timeGuard.push_back(ConstraintMaker(0) <= 10.);
 
             // Apply the time restriction operation
-            auto result = timeRestriction<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<int>,
-                                       std::vector<TimingConstraint<double>>, NonSymbolic::Update<int>, double>(std::move(automaton_copy), timeGuard);
+            auto result = timeRestriction(std::move(automaton_copy), timeGuard);
 
             // Check that the clock variable size is increased by 1
             BOOST_CHECK_EQUAL(result.clockVariableSize, 2);
@@ -367,8 +365,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             }
 
             // Apply the constraint to all transitions
-            addConstraintToAllTransitions<NonSymbolic::StringConstraint, NonSymbolic::NumberConstraint<int>,
-                                       std::vector<TimingConstraint<double>>, NonSymbolic::Update<int>, double>(automaton_copy, constraint);
+            addConstraintToAllTransitions(automaton_copy, constraint);
 
             // Verify that all transitions have the constraint applied
             size_t constrainedTransitionCount = 0;
@@ -458,8 +455,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             auto copyFinalState = copy.states[3];
             auto withdrawFinalState = withdraw.states[2];
 
-            auto result = concatenate<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                        std::vector<TimingConstraint<double>>, Symbolic::Update, double>(std::move(copy), std::move(withdraw));
+            auto result = concatenate(std::move(copy), std::move(withdraw));
 
             // Check the total number of states (should be the sum of both automata)
             BOOST_CHECK_EQUAL(result.states.size(), 6);
@@ -648,8 +644,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             timeGuard.push_back(ConstraintMaker(0) <= 10.);
 
             // Apply the time restriction operation
-            auto result = timeRestriction<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                        std::vector<TimingConstraint<double>>, Symbolic::Update, double>(std::move(automaton_copy), timeGuard);
+            auto result = timeRestriction(std::move(automaton_copy), timeGuard);
 
             // Check that the clock variable size is increased by 1
             BOOST_CHECK_EQUAL(result.clockVariableSize, 2);
@@ -755,8 +750,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             }
 
             // Apply the constraint to all transitions
-            addConstraintToAllTransitions<Symbolic::StringConstraint, Symbolic::NumberConstraint,
-                                        std::vector<TimingConstraint<double>>, Symbolic::Update, double>(automaton_copy, constraint);
+            addConstraintToAllTransitions(automaton_copy, constraint);
 
             // Verify that all transitions have the constraint applied
             size_t constrainedTransitionCount = 0;
@@ -846,8 +840,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             auto copyFinalState = copy.states[3];
             auto withdrawFinalState = withdraw.states[2];
 
-            auto result = concatenate<Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
-                                    Symbolic::Update, ParametricTimingConstraint>(std::move(copy), std::move(withdraw));
+            auto result = concatenate(std::move(copy), std::move(withdraw));
 
             // Check the total number of states (should be the sum of both automata)
             BOOST_CHECK_EQUAL(result.states.size(), 6);
@@ -1036,8 +1029,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             timeGuard.add_constraint(Variable(1) <= 10);
 
             // Apply the time restriction operation
-            const auto result = timeRestriction<Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
-                                    Symbolic::Update, ParametricTimingConstraint>(std::move(automaton_copy), timeGuard);
+            const auto result = timeRestriction(std::move(automaton_copy), timeGuard);
 
             // Check that the clock variable size is increased by 1
             BOOST_CHECK_EQUAL(result.clockVariableSize, 2);
@@ -1144,8 +1136,7 @@ BOOST_AUTO_TEST_SUITE(AutomatonOperationTest)
             }
 
             // Apply the constraint to all transitions
-            addConstraintToAllTransitions<Symbolic::StringConstraint, Symbolic::NumberConstraint, ParametricTimingConstraint,
-                                    Symbolic::Update, ParametricTimingConstraint>(automaton_copy, constraint);
+            addConstraintToAllTransitions(automaton_copy, constraint);
 
             // Verify that all transitions have the constraint applied
             size_t constrainedTransitionCount = 0;
diff --git a/test/symon_parser_test.cc b/test/symon_parser_test.cc
index 8c118a0..dd13ad7 100644
--- a/test/symon_parser_test.cc
+++ b/test/symon_parser_test.cc
@@ -26,7 +26,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
     using Update = Update<int>;
 
         struct CopyParserFixture {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string path = PROJECT_ROOT "/example/copy/copy.symon";
 
             CopyParserFixture() {
@@ -51,7 +51,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(atomic) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value)";
             parser.parse(content);
 
@@ -81,7 +81,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(stringConstraint) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value | id == \"y\")";
             parser.parse(content);
 
@@ -114,7 +114,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(timingConstraint) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))%(< 5)";
             parser.parse(content);
 
@@ -146,7 +146,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(concat) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value); update(id, value)";
             parser.parse(content);
 
@@ -194,7 +194,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(orEmpty) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))?";
             parser.parse(content);
 
@@ -234,7 +234,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(plus) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))+";
             parser.parse(content);
 
@@ -278,7 +278,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(one_or_more) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} one_or_more {update(id, value)}";
             parser.parse(content);
 
@@ -322,7 +322,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(star) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))*";
             parser.parse(content);
 
@@ -372,7 +372,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(zero_or_more) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} zero_or_more{update(id, value)}";
             parser.parse(content);
 
@@ -422,7 +422,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(orEmptyConcat) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value))?;update(id, value)";
             parser.parse(content);
 
@@ -472,7 +472,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(timingConstraintConcat) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value); (update(id, value))%(> 5)";
             parser.parse(content);
 
@@ -522,7 +522,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(optionalWithTimingConstraintLT) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value)?)%(< 3)";
             parser.parse(content);
 
@@ -567,7 +567,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(optionalWithTimingConstraintGT) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} (update(id, value)?)%(> 3)";
             parser.parse(content);
 
@@ -611,7 +611,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(concatOptionalWithTimingConstraint) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value); (update(id, value)?)%(< 3)";
             parser.parse(content);
 
@@ -673,7 +673,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             // only the upper bound is added to all transitions
             
             // Create a parser
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             
             // Parse a simple automaton with a timing constraint that has both upper and lower bounds
             std::string content = R"(
@@ -723,7 +723,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(inits) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             std::ifstream ifs(PROJECT_ROOT "/example/inits.symon");
             // This should throw an exception because initial constraints are not supported in non-symbolic automata
             BOOST_CHECK_THROW(parser.parse(ifs), std::runtime_error);
@@ -742,7 +742,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             guard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraintOrder::le, 5});
             
             // Extract the upper bound
-            auto upperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double>::extractUpperBound(guard);
+            auto upperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update>::extractUpperBound(guard);
             
             // Verify that only the upper bound was extracted
             BOOST_CHECK_EQUAL(upperBound.size(), 1);
@@ -764,7 +764,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             nonParametricGuard.push_back(TimingConstraint<double>{VariableID{0}, TimingConstraintOrder::le, 5});
             
             // Extract the upper bound from the non-parametric guard
-            auto nonParametricUpperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double>::extractUpperBound(nonParametricGuard);
+            auto nonParametricUpperBound = SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update>::extractUpperBound(nonParametricGuard);
             
             // Verify that only the upper bound was extracted
             BOOST_CHECK_EQUAL(nonParametricUpperBound.size(), 1);
@@ -783,7 +783,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
             parametricGuard.add_constraint(x <= 5);
             
             // Extract the upper bound from the parametric guard
-            auto parametricUpperBound = SymonParser<StringConstraint, NumberConstraint<int>, ParametricTimingConstraint, Update, double>::extractUpperBound(parametricGuard);
+            auto parametricUpperBound = SymonParser<StringConstraint, NumberConstraint<int>, ParametricTimingConstraint, Update>::extractUpperBound(parametricGuard);
             
             // Verify that the parametric upper bound contains only the upper bound constraint
             // We can't directly compare the constraints, but we can check that:
@@ -807,7 +807,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(case20250703_1) {
-            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint<int>, std::vector<TimingConstraint<double>>, Update> parser;
             const std::string content = "signature A {id: string;} signature B {id: string;} ((A( id | id != \"Bob\" ) || B( id | id != \"Bob\" ))%(<= 5);B (id | id == \"Bob\"))%(> 5)";
             parser.parse(content);
 
@@ -877,7 +877,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         using namespace Symbolic;
 
         struct ParametricCopyParserFixture {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
             const std::string path = PROJECT_ROOT "/example/copy/copy.symon";
 
             ParametricCopyParserFixture() {
@@ -902,7 +902,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(inits) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
             std::ifstream ifs(PROJECT_ROOT "/example/inits.symon");
             parser.parse(ifs);
             const auto automaton = parser.getAutomaton();
@@ -918,7 +918,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(updates) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
             const std::string content = "var {count: number; count2: number;} signature update {id: string;value: number;} update(id, value | | count := count + 1; count2 := count2 + 2 ; count := count + count 2)";
             parser.parse(content);
 
@@ -948,7 +948,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(timingConstraintConcat) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
             const std::string content = "signature update {id: string;value: number;} update(id, value); (update(id, value))%(> 5)";
             parser.parse(content);
 
@@ -1005,7 +1005,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(parametricTimingConstraint) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
             const std::string content = "var {p: param;} signature A {} A()%(< p)";
             parser.parse(content);
 
@@ -1042,7 +1042,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(parametricTimingConstraintStar) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
             const std::string content = "var {p: param;} signature A {} (A()%(< p))*";
             parser.parse(content);
 
@@ -1095,7 +1095,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
         }
 
         BOOST_AUTO_TEST_CASE(parametricTimingConstraintStarConcat) {
-            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update, double> parser;
+            SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
             const std::string content = "var {p: param;} signature A {} A();(A()%(< p))*";
             parser.parse(content);
 

From 54ff7e1c6cf5f008e66352259056a97090f9add1 Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Thu, 27 Nov 2025 01:02:11 +0900
Subject: [PATCH 08/14] Fix test

---
 src/parametric_timing_constraint_helper.hh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/parametric_timing_constraint_helper.hh b/src/parametric_timing_constraint_helper.hh
index b9cb4fb..e56fb7c 100644
--- a/src/parametric_timing_constraint_helper.hh
+++ b/src/parametric_timing_constraint_helper.hh
@@ -32,6 +32,7 @@ public:
   std::array<std::vector<std::pair<op_t, atom_t>>, 2> tail;
   //! @brief comparison in the constraint
   comparison_t comparison = comparison_t::EQ;
+  // (head[0] tail[0][0].first tail[0][0].second ...) comparison (head[1] tail[1][0].first tail[1][0].second ...)
 
   static auto toExpr(const std::size_t parameterSize, const atom_t &atom) {
     std::pair<Parma_Polyhedra_Library::Linear_Expression, Parma_Polyhedra_Library::Coefficient> expr;

From 2e74de74658b9786a460d62e745120bd49d40adf Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Tue, 2 Dec 2025 19:13:38 +0900
Subject: [PATCH 09/14] Add test case for decimal satisfaction in
 TimingConstraint

---
 test/timing_constraint_test.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/timing_constraint_test.cc b/test/timing_constraint_test.cc
index 64970c7..9b3a59a 100644
--- a/test/timing_constraint_test.cc
+++ b/test/timing_constraint_test.cc
@@ -20,7 +20,7 @@ BOOST_AUTO_TEST_SUITE(TimingConstraintTest)
     }
 
     BOOST_AUTO_TEST_CASE(Decimal) {
-        constexpr TimingConstraint constraint{1, TimingConstraint::Order::ge, 0.5};
+        constexpr TimingConstraint<double> constraint{1, TimingConstraintOrder::ge, 0.5};
         BOOST_CHECK(!constraint.satisfy(0.4));
         BOOST_CHECK(constraint.satisfy(0.5));
         BOOST_CHECK(constraint.satisfy(0.6));

From 5f59cfcaf94b6966fd4c10f32d7d502ab37731fe Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Fri, 6 Feb 2026 01:14:04 +0900
Subject: [PATCH 10/14] fixup booleanmonitor

---
 src/boolean_monitor.hh         | 2 +-
 src/data_parametric_monitor.hh | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/boolean_monitor.hh b/src/boolean_monitor.hh
index 00d3e81..6de634c 100644
--- a/src/boolean_monitor.hh
+++ b/src/boolean_monitor.hh
@@ -96,7 +96,7 @@ namespace NonSymbolic {
   private:
     const NonParametricTA<Number, Timestamp> automaton;
     using Configuration = std::tuple<std::shared_ptr<NonParametricTAState<Number, Timestamp>>, std::vector<Timestamp>,
-                                     StringValuation, NumberValuation<Number>, double>>;
+                                     StringValuation, NumberValuation<Number>, double>;
     // struct Configuration {
     //   std::shared_ptr<AutomatonState<Number>> state;
     //   std::vector<Timestamp> clockValuation;
diff --git a/src/data_parametric_monitor.hh b/src/data_parametric_monitor.hh
index cb6250a..e5563dd 100644
--- a/src/data_parametric_monitor.hh
+++ b/src/data_parametric_monitor.hh
@@ -32,7 +32,6 @@ class DataParametricMonitor : public SingleSubject<DataParametricMonitorResult<T
 public:
   static const constexpr std::size_t unobservableActionID = 127;
   explicit DataParametricMonitor(const DataParametricTA<Timestamp> &automaton) : automaton(automaton) {
-    absTime = 0;
     configurations.clear();
     // configurations.reserve(automaton.initialStates.size());
     std::vector<Timestamp> initCVal(automaton.clockVariableSize);
@@ -54,7 +53,7 @@ public:
     const std::vector<std::string> &strings = event.strings;
     const std::vector<PPLRational> &numbers = event.numbers;
     const Timestamp timestamp = event.timestamp;
-    
+
     boost::unordered_set<Configuration> nextConfigurations;
     configurations.merge(epsilonTransition(configurations));
 
@@ -109,7 +108,7 @@ public:
 private:
   const DataParametricTA<Timestamp> automaton;
   using Configuration = std::tuple<std::shared_ptr<DataParametricTAState<Timestamp>>, std::vector<Timestamp>,
-                                   Symbolic::StringValuation, Symbolic::NumberValuation, double>>;
+                                   Symbolic::StringValuation, Symbolic::NumberValuation, double>;
   // Symbolic::NumberValuation>;
   /*  struct Configuration {
       std::shared_ptr<DataParametricTAState> state;

From 126df603bf83642a1ba1dfb8fb76ef1fef91d11c Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Fri, 6 Feb 2026 01:14:28 +0900
Subject: [PATCH 11/14] fix timing_constraint

---
 src/timing_constraint.hh | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/timing_constraint.hh b/src/timing_constraint.hh
index 7113aa4..6804ff9 100644
--- a/src/timing_constraint.hh
+++ b/src/timing_constraint.hh
@@ -15,7 +15,7 @@ inline bool toBool(Order odr) {
   return odr == Order::EQ;
 }
 
-enum class TimingConstraintOrder { lt, le, ge, gt };
+enum class TimingConstraintOrder { lt, le, ge, gt, eq };
 
 //! @brief A constraint in a guard of transitions
 template <typename Timestamp>
@@ -34,7 +34,7 @@ struct TimingConstraint {
         return d > c;
       case TimingConstraintOrder::ge:
         return d >= c;
-      case Order::eq:
+      case TimingConstraintOrder::eq:
         return d == c;
     }
     return false;
@@ -69,7 +69,6 @@ struct TimingConstraint {
 
 // An interface to write an inequality constrait easily
 class ConstraintMaker {
-  using Timestamp = TimingConstraint::Timestamp;
   ClockVariables x;
 
 public:
@@ -96,8 +95,9 @@ public:
     return TimingConstraint<Timestamp>{x, TimingConstraintOrder::ge, c};
   }
 
-  TimingConstraint operator==(Timestamp c) {
-    return TimingConstraint{x, TimingConstraint::Order::eq, c};
+  template<typename Timestamp = double>
+  TimingConstraint<Timestamp> operator==(Timestamp c) {
+    return TimingConstraint<Timestamp>{x, TimingConstraintOrder::eq, c};
   }
 };
 
@@ -127,10 +127,11 @@ static bool eval(const TimingValuation<Timestamp> &clockValuation, const std::ve
   and throws if any non-equality constraint is present.
 
 */
-static std::optional<double> diff(const TimingValuation &clockValuation, const std::vector<TimingConstraint> &guard) {
+template<typename Timestamp>
+static std::optional<double> diff(const TimingValuation<Timestamp> &clockValuation, const std::vector<TimingConstraint<Timestamp>> &guard) {
   std::optional<double> result = std::nullopt;
   for (auto&& g: guard) {
-    if(g.odr != TimingConstraint::Order::eq) {
+    if(g.odr != TimingConstraintOrder::eq) {
       throw std::runtime_error("TimingConstraint: unsupported guard with inequality constraints on unobservable transition");
     }
     auto timeDiff = g.c - clockValuation.at(g.x);

From f840c9673004ed628cfe484275bcfb9190d39a7d Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Fri, 6 Feb 2026 01:14:41 +0900
Subject: [PATCH 12/14] fix automaton_parser

---
 src/automaton_parser.hh | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/automaton_parser.hh b/src/automaton_parser.hh
index 041e129..c60eb05 100644
--- a/src/automaton_parser.hh
+++ b/src/automaton_parser.hh
@@ -70,6 +70,9 @@ static inline std::ostream &operator<<(std::ostream &os, const TimingConstraintO
     case TimingConstraintOrder::gt:
       os << ">";
       break;
+    case TimingConstraintOrder::eq:
+      os << "==";
+      break;
   }
   return os;
 }
@@ -133,7 +136,7 @@ static inline std::istream &operator>>(std::istream &is, TimingConstraint<Timest
       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;

From 0c8e7b58a9e8809c8667374f6dc86c2a218c7e40 Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Fri, 6 Feb 2026 01:14:53 +0900
Subject: [PATCH 13/14] fixup symon_parser

---
 test/symon_parser_test.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/symon_parser_test.cc b/test/symon_parser_test.cc
index dd13ad7..a0afced 100644
--- a/test/symon_parser_test.cc
+++ b/test/symon_parser_test.cc
@@ -919,7 +919,7 @@ BOOST_AUTO_TEST_SUITE(SymonParserTests)
 
         BOOST_AUTO_TEST_CASE(updates) {
             SymonParser<StringConstraint, NumberConstraint, ParametricTimingConstraint, Update> parser;
-            const std::string content = "var {count: number; count2: number;} signature update {id: string;value: number;} update(id, value | | count := count + 1; count2 := count2 + 2 ; count := count + count 2)";
+            const std::string content = "var {count: number; count2: number;} signature update {id: string;value: number;} update(id, value | | count := count + 1; count2 := count2 + 2 ; count := count + count2)";
             parser.parse(content);
 
             const auto automaton = parser.getAutomaton();

From 5f5c25f8eb4fa1de51be591c9acb5157ad21263c Mon Sep 17 00:00:00 2001
From: taiseiKMC <taisei@kmc.gr.jp>
Date: Fri, 6 Feb 2026 01:15:08 +0900
Subject: [PATCH 14/14] fix booleanmonitortest

---
 test/boolean_monitor_test.cc                  | 28 ++++++++++---------
 test/data_parametric_monitor_test.cc          |  5 ++--
 .../epsilon_transition_automaton_fixture.hh   |  8 +++---
 test/fixture/non_integer_timestamp_fixture.hh | 12 ++++----
 4 files changed, 28 insertions(+), 25 deletions(-)

diff --git a/test/boolean_monitor_test.cc b/test/boolean_monitor_test.cc
index b42da39..97ddf2a 100644
--- a/test/boolean_monitor_test.cc
+++ b/test/boolean_monitor_test.cc
@@ -22,23 +22,23 @@ struct DummyTimedWordSubject : public SingleSubject<TimedWordEvent> {
   std::vector<TimedWordEvent> vec;
 };
 
-template<typename Number>
-struct DummyBooleanMonitorObserver : public Observer<BooleanMonitorResult<Number>> {
+template<typename Number, typename Timestamp>
+struct DummyBooleanMonitorObserver : public Observer<BooleanMonitorResult<Number, Timestamp>> {
   DummyBooleanMonitorObserver() {
   }
   virtual ~DummyBooleanMonitorObserver() {
   }
-  void notify(const BooleanMonitorResult<Number> &result) {
+  void notify(const BooleanMonitorResult<Number, Timestamp> &result) {
     resultVec.push_back(result);
   }
-  std::vector<BooleanMonitorResult<Number>> resultVec;
+  std::vector<BooleanMonitorResult<Number, Timestamp>> resultVec;
 };
 
-template<typename Number, typename TimedWordEvent>
+template<typename Number, typename Timestamp, typename TimedWordEvent>
 struct BooleanMonitorFixture {
-  void feed(const NonParametricTA<Number> &automaton, std::vector<TimedWordEvent> &&vec) {
-    auto monitor = std::make_shared<NonSymbolic::BooleanMonitor<Number>>(automaton);
-    std::shared_ptr<DummyBooleanMonitorObserver<Number>> observer = std::make_shared<DummyBooleanMonitorObserver<Number>>();
+  void feed(const NonParametricTA<Number, Timestamp> &automaton, std::vector<TimedWordEvent> &&vec) {
+    auto monitor = std::make_shared<NonSymbolic::BooleanMonitor<Number, Timestamp>>(automaton);
+    std::shared_ptr<DummyBooleanMonitorObserver<Number, Timestamp>> observer = std::make_shared<DummyBooleanMonitorObserver<Number, Timestamp>>();
     monitor->addObserver(observer);
     DummyTimedWordSubject<TimedWordEvent> subject{std::move(vec)};
     subject.addObserver(monitor);
@@ -48,13 +48,14 @@ struct BooleanMonitorFixture {
     monitor.reset();            // release local ownership
     resultVec = std::move(observer->resultVec);
   }
-  std::vector<BooleanMonitorResult<Number>> resultVec;
+  std::vector<BooleanMonitorResult<Number, Timestamp>> resultVec;
 };
 
 namespace IntTest {
   using Number = int;
-  using TimedWordEvent = TimedWordEvent<Number, double>;
-  using BooleanMonitorFixture = BooleanMonitorFixture<Number, TimedWordEvent>;
+  using Timestamp = double;
+  using TimedWordEvent = TimedWordEvent<Number, Timestamp>;
+  using BooleanMonitorFixture = BooleanMonitorFixture<Number, Timestamp, TimedWordEvent>;
 
   BOOST_AUTO_TEST_SUITE(BooleanMonitorTest)
     BOOST_FIXTURE_TEST_CASE(test1, BooleanMonitorFixture)
@@ -167,8 +168,9 @@ namespace IntTest {
 
 namespace DoubleTest {
   using Number = double;
-  using TimedWordEvent = TimedWordEvent<Number, double>;
-  using BooleanMonitorFixture = BooleanMonitorFixture<Number, TimedWordEvent>;
+  using Timestamp = double;
+  using TimedWordEvent = TimedWordEvent<Number, Timestamp>;
+  using BooleanMonitorFixture = BooleanMonitorFixture<Number, Timestamp, TimedWordEvent>;
 
   BOOST_AUTO_TEST_SUITE(BooleanMonitorTest)
     BOOST_FIXTURE_TEST_CASE(non_integer_timestamp_test, BooleanMonitorFixture) {
diff --git a/test/data_parametric_monitor_test.cc b/test/data_parametric_monitor_test.cc
index 8ffd376..5387747 100644
--- a/test/data_parametric_monitor_test.cc
+++ b/test/data_parametric_monitor_test.cc
@@ -6,6 +6,7 @@
 #include "../test/fixture/epsilon_transition_automaton_fixture.hh"
 
 using TWEvent = TimedWordEvent<PPLRational>;
+using Timestamp = double;
 
 struct DummyDataTimedWordSubject : public SingleSubject<TWEvent> {
   DummyDataTimedWordSubject(std::vector<TWEvent> &&vec) :vec(std::move(vec)) {}
@@ -29,8 +30,8 @@ struct DummyDataParametricMonitorObserver : public Observer<DataParametricMonito
 };
 
 struct DataParametricMonitorFixture {
-  void feed(DataParametricTA automaton, std::vector<TWEvent> &&vec) {
-    auto monitor = std::make_shared<DataParametricMonitor>(automaton);
+  void feed(DataParametricTA<Timestamp> automaton, std::vector<TWEvent> &&vec) {
+    auto monitor = std::make_shared<DataParametricMonitor<Timestamp>>(automaton);
     std::shared_ptr<DummyDataParametricMonitorObserver> observer = std::make_shared<DummyDataParametricMonitorObserver>();
     monitor->addObserver(observer);
     DummyDataTimedWordSubject subject{std::move(vec)};
diff --git a/test/fixture/epsilon_transition_automaton_fixture.hh b/test/fixture/epsilon_transition_automaton_fixture.hh
index 4f5a82c..9c205c3 100644
--- a/test/fixture/epsilon_transition_automaton_fixture.hh
+++ b/test/fixture/epsilon_transition_automaton_fixture.hh
@@ -25,14 +25,14 @@ class AutomatonFixture {
         AutomatonFixture(std::string dotStr):dotString(dotStr) {}
 
         auto makeBooleanTA() const {
-            using TAType = NonParametricTA<int>;
-            using BoostTAType = NonParametricBoostTA<int>;
+            using TAType = NonParametricTA<int, double>;
+            using BoostTAType = NonParametricBoostTA<int, double>;
             return parseDotTA<TAType, BoostTAType>(dotString);
         }
 
         auto makeDataParametricTA() const {
-            using TAType = DataParametricTA;
-            using BoostTAType = DataParametricBoostTA;
+            using TAType = DataParametricTA<double>;
+            using BoostTAType = DataParametricBoostTA<double>;
             return parseDotTA<TAType, BoostTAType>(dotString);
         }
 };
diff --git a/test/fixture/non_integer_timestamp_fixture.hh b/test/fixture/non_integer_timestamp_fixture.hh
index 973d0ca..fd31e06 100644
--- a/test/fixture/non_integer_timestamp_fixture.hh
+++ b/test/fixture/non_integer_timestamp_fixture.hh
@@ -12,7 +12,7 @@ namespace NonParametric {
     @brief Automaton with a guard restricting time to non-integer values.
     */
     struct NonIntegerTimestampFixture {
-        NonParametricTA<double> automaton;
+        NonParametricTA<double, double> automaton;
         std::unique_ptr<Signature> signature;
         NonIntegerTimestampFixture() {
             // Construct signature
@@ -23,7 +23,7 @@ namespace NonParametric {
             // Construct automaton with 2 states
             automaton.states.resize(2);
             for (auto &state: automaton.states) {
-                state = std::make_shared<NonParametricTAState<double> >(false);
+                state = std::make_shared<NonParametricTAState<double, double> >(false);
             }
             automaton.initialStates = {automaton.states[0]};
             automaton.states[0]->isMatch = false;  // Initial state is not final
@@ -56,7 +56,7 @@ namespace NonParametric {
                 std::vector<NonSymbolic::NumberConstraint<double> > numConstraints;
                 NonSymbolic::Update<double> update;
                 std::vector<VariableID> resetVars;
-                std::vector<TimingConstraint> guard;
+                std::vector<TimingConstraint<double>> guard;
                 guard.push_back(ConstraintMaker(0) >= 1.1);
                 guard.push_back(ConstraintMaker(0) < 1.2);
                 
@@ -79,7 +79,7 @@ namespace Parametric {
     @brief Data parametric version of the non-integer timestamp automaton fixture.
     */
     struct DataParametricNonIntegerTimestampFixture {
-        DataParametricTA automaton;
+        DataParametricTA<double> automaton;
         std::unique_ptr<Signature> signature;
         DataParametricNonIntegerTimestampFixture() {
             using namespace Symbolic;
@@ -93,7 +93,7 @@ namespace Parametric {
             // Construct automaton with 2 states
             automaton.states.resize(2);
             for (auto &state: automaton.states) {
-                state = std::make_shared<DataParametricTAState>(false);
+                state = std::make_shared<DataParametricTAState<double>>(false);
             }
             automaton.initialStates = {automaton.states[0]};
             automaton.states[0]->isMatch = false;  // Initial state is not final
@@ -126,7 +126,7 @@ namespace Parametric {
                 std::vector<NumberConstraint> numConstraints;
                 Update update;
                 std::vector<VariableID> resetVars;
-                std::vector<TimingConstraint> guard;
+                std::vector<TimingConstraint<double>> guard;
                 guard.push_back(ConstraintMaker(0) >= 1.1);
                 guard.push_back(ConstraintMaker(0) < 1.2);