Resolve #11 by taiseiKMC · Pull Request #12 · MasWag/SyMon

taiseiKMC · 2025-12-07T17:28:07Z

Close #11.

Set double to Timestamp when using data_parametric_monitor and boolean_monitor, PPLRational when using parametric_monitor
Update parametric_timing_constraint_helper to handle PPLRational

…arison operators accordingly

calling is.peek twice at eof sometimes cause is.fail

MasWag

Please remove unnecessary comments.

MasWag · 2025-12-21T13:43:27Z

  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 ...)


This is likely an unnecessary comment.

Moved this line to the description part of this struct

MasWag · 2025-12-21T13:43:37Z

-  void toExpr(const std::size_t parameterSize, const atom_t &atom,
-              Parma_Polyhedra_Library::Linear_Expression &expr) const {
+  static auto toExpr(const std::size_t parameterSize, const atom_t &atom) {
+    // Coefficient は denominator


This is also likely an unnecessary comment.

MasWag · 2025-12-21T13:43:44Z

+    return expr;
  }

+  // constraint で ParametricTimingConstraint = Parma_Polyhedra_Library::NNC_Polyhedron の add_constraint する


This is also likely an unnecessary comment.

MasWag · 2025-12-21T13:43:49Z

  void extract(const std::size_t parameterSize, Parma_Polyhedra_Library::Constraint &constraint) const {
-    std::array<Parma_Polyhedra_Library::Linear_Expression, 2> expr;
+    std::array<std::pair<Parma_Polyhedra_Library::Linear_Expression, Parma_Polyhedra_Library::Coefficient>, 2> expr;
+    // head[i], tail[i] から expr[i] を生成


This is also likely an unnecessary comment.

Rewrote it more properly

…ional

…alComparison and add decimalCalculation cases

…raint structure and comparison details

Copilot

Pull request overview

This PR resolves issue #11 by adding support for decimal/non-integer timestamps and rational number constraints in parametric timing constraints. The main changes involve updating TimingConstraint to use double instead of int for timestamps, and migrating ParametricTimingConstraintHelper from using Parma_Polyhedra_Library::Coefficient to PPLRational for handling rational numbers in parametric constraints.

Key Changes:

Changed TimingConstraint to use double for timestamp values instead of int
Updated ParametricTimingConstraintHelper to use PPLRational for constants instead of Coefficient, with proper rational arithmetic operations
Added new equality operators to PPLRational class and improved decimal parsing

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
`src/timing_constraint.hh`	Changed timestamp type from `int` to `double` via `Timestamp` typedef
`src/ppl_rational.hh`	Fixed decimal parsing loop bug, added equality operators for `PPLRational`
`src/parametric_timing_constraint_helper.hh`	Migrated from `Coefficient` to `PPLRational` for constants, implemented rational arithmetic for expressions
`test/timing_constraint_test.cc`	Added test case for decimal timestamp constraints
`test/parametric_timing_constraint_helper_test.cc`	Updated assertions to use `PPLRational`, added comprehensive decimal parsing and calculation tests
`test/parametric_monitor_test.cc`	Added test for non-integer timestamps using `PPLRational`
`test/data_parametric_monitor_test.cc`	Added test fixture and test case for non-integer timestamps with data parametric monitors
`test/boolean_monitor_test.cc`	Refactored tests into namespaces, added non-integer timestamp test case
`test/fixture/non_integer_timestamp_fixture.hh`	New fixture file with three automaton variants for testing non-integer timestamps

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-01-02T09:23:46Z

+      //NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched.
+      //BOOST_CHECK_EQUAL(resultVec.size(), 1);


The commented-out assertion should either be uncommented with the correct expected value or removed entirely. Based on the NOTE comment, it appears the test expects 1 match but the floating-point precision issue causes 2 matches. Since the PR aims to fix decimal timestamp handling with PPLRational, if this test is using doubles (which still have floating-point precision issues), the comment should be clarified or the assertion should be updated to reflect the actual expected behavior.

Suggested change

//NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched.

//BOOST_CHECK_EQUAL(resultVec.size(), 1);

// NOTE: Due to double-precision rounding, 3.3 - 2.1 is evaluated as 1.1999999999999997 < 1.2,

// so both the third and fourth events are matched. This test documents that behavior for doubles.

BOOST_CHECK_EQUAL(resultVec.size(), 2);

I wanna keep it for comparison with the parametric_monitor_test

Copilot · 2026-01-02T09:23:46Z

+        {0, {}, {0}, {445, 100}}
+      };
+      feed(automaton, std::move(dummyTimedWord));
+      //NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched.


The comment is incorrect. It states "3.3 - 2.1 is 1.2" but the actual timestamp used in the test is 325/100 = 3.25, not 3.3. The calculation should be 3.25 - 2.1 = 1.15, which correctly falls within the guard range [1.1, 1.2). The comment should be updated to reflect the actual values used in the test.

Suggested change

//NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched.

// NOTE: The guard range is [1.1, 1.2). The difference 3.25 - 2.1 = 1.15 lies within this range, so the fourth event is also matched.

Deleted this line and modified the test case

Copilot · 2026-01-02T09:23:47Z

+}
+
+static inline bool operator==(const PPLRational &lhs, const int &rhs) {
+  return lhs.getNumerator() * rhs == lhs.getDenominator();


The equality operator implementation is incorrect. When comparing a rational number a/b with an integer c, it should check if a/b == c, which means a == c * b, not a * c == b. The current implementation lhs.getNumerator() * rhs == lhs.getDenominator() checks if numerator times the integer equals the denominator, which is wrong. For example, PPLRational(2, 1) == 2 would evaluate as 2 * 2 == 1 which is false, when it should be true.

Suggested change

return lhs.getNumerator() * rhs == lhs.getDenominator();

return lhs.getNumerator() == rhs * lhs.getDenominator();

Nice pick! Reflected

Copilot · 2026-01-02T09:23:47Z

+    //NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched.
+    //BOOST_CHECK_EQUAL(resultVec.size(), 1);


The commented-out assertion should either be uncommented with the correct expected value or removed entirely. Based on the NOTE comment, it appears the test expects 1 match but the floating-point precision issue causes 2 matches. Since the PR aims to fix decimal timestamp handling with PPLRational, if this test is using doubles (which still have floating-point precision issues), the comment should be clarified or the assertion should be updated to reflect the actual expected behavior.

Suggested change

//NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched.

//BOOST_CHECK_EQUAL(resultVec.size(), 1);

// NOTE: With double timestamps, 3.3 - 2.1 could be evaluated as 1.1999999999999997 < 1.2,

// which incorrectly matched the fourth event as well. Using PPLRational timestamps avoids

// this floating-point issue, so only the third event should match.

BOOST_CHECK_EQUAL(resultVec.size(), 1);

Same as boolean_monitor_test

MasWag

looks good to me

…ted index and timestamp for event matching

…nteger and add unit tests for rational comparisons

Copilot

Pull request overview

Copilot reviewed 10 out of 10 changed files in this pull request and generated 1 comment.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

operator==(PPLRational, int) has been given, but not the reversed Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

taiseiKMC force-pushed the hsaito/issue-11 branch 2 times, most recently from c9c62c0 to 138c8a9 Compare December 7, 2025 18:48

taiseiKMC added 2 commits December 17, 2025 23:19

Refactor TimingConstraint to use double for Timestamp and update comp…

af9ffa9

…arison operators accordingly

Fix ppl_rational.hh operator>>

e79ec98

calling is.peek twice at eof sometimes cause is.fail

taiseiKMC force-pushed the hsaito/issue-11 branch from 138c8a9 to 86cb8c2 Compare December 17, 2025 14:41

MasWag requested changes Dec 21, 2025

View reviewed changes

taiseiKMC added 8 commits January 2, 2026 16:57

Implement rational timing constraint for parametric

e446911

Enhance PPLRational equality operators and update tests to use PPLRat…

f4248a3

…ional

Fix test

af6715c

Update tests for ParametricTimingConstraintHelper: modify vectorDecim…

23adf13

…alComparison and add decimalCalculation cases

Add test case for decimal satisfaction in TimingConstraint

7ea8dca

Add non-integer timestamp fixtures and tests

6b768a0

Add documentation for ParametricTimingConstraintHelper: clarify const…

5ce6466

…raint structure and comparison details

Add data parametric test case with non-integer timestamp

2c2ebcf

taiseiKMC force-pushed the hsaito/issue-11 branch from 86cb8c2 to 2c2ebcf Compare January 2, 2026 09:11

taiseiKMC marked this pull request as ready for review January 2, 2026 09:19

MasWag requested a review from Copilot January 2, 2026 09:20

Copilot started reviewing on behalf of MasWag January 2, 2026 09:20 View session

Copilot AI reviewed Jan 2, 2026

View reviewed changes

MasWag approved these changes Jan 2, 2026

View reviewed changes

taiseiKMC added 2 commits January 6, 2026 16:21

Fix non_integer_timestamp_test in ParametricMonitorTest: adjust expec…

242a24b

…ted index and timestamp for event matching

Fix comparison operator for PPLRational: update equality check with i…

040e07f

…nteger and add unit tests for rational comparisons

MasWag requested review from MasWag and Copilot January 6, 2026 11:23

Copilot started reviewing on behalf of MasWag January 6, 2026 11:24 View session

MasWag approved these changes Jan 6, 2026

View reviewed changes

Copilot AI reviewed Jan 6, 2026

View reviewed changes

Comment thread src/ppl_rational.hh

taiseiKMC and others added 2 commits January 8, 2026 01:36

Update src/ppl_rational.hh: Add operator==(int, PPLRational)

5ea5f7d

operator==(PPLRational, int) has been given, but not the reversed Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Merge branch 'master' into hsaito/issue-11

21e043d

MasWag merged commit 1546906 into MasWag:master Jan 9, 2026
3 of 8 checks passed

		//NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched.
		//BOOST_CHECK_EQUAL(resultVec.size(), 1);

-      //NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched.
-      //BOOST_CHECK_EQUAL(resultVec.size(), 1);
+      // NOTE: Due to double-precision rounding, 3.3 - 2.1 is evaluated as 1.1999999999999997 < 1.2,
+      // so both the third and fourth events are matched. This test documents that behavior for doubles.
+      BOOST_CHECK_EQUAL(resultVec.size(), 2);

	//NOTE: 3.3 - 2.1 is 1.2, but this is evaluated as 1.1999999999999997 < 1.2, so the fourth event is also matched.
	// NOTE: The guard range is [1.1, 1.2). The difference 3.25 - 2.1 = 1.15 lies within this range, so the fourth event is also matched.

	return lhs.getNumerator() * rhs == lhs.getDenominator();
	return lhs.getNumerator() == rhs * lhs.getDenominator();

Conversation

taiseiKMC commented Dec 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MasWag left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Jan 2, 2026

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 2, 2026

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 2, 2026

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 2, 2026

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MasWag left a comment

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

taiseiKMC commented Dec 7, 2025 •

edited

Loading