CDD x>=0 and x<0
- Dominant language
- Java
- Stars
- 4
- Forks
- 9
- PR merge metrics
- No merged PRs in 30d
Description
## Clock guard ``x >= 0``
__Expected__
- The resulting pointer should point to a CDD node which is equivalent to ``true`` (In other words``isEquiv`` should return ``true``).
- The resulting pointer should preferably point to the terminal ``true`` node after reduction (In other words after calling ``reduce`` the CDD should have ``isTrue`` return ``True``).
- The resulting pointer should if ``isTrue`` returns ``True`` be a terminal node (In other words after reducing and ``isTrue`` returns ``true`` then ``isTerminal`` should return ``true``).
__Actual__
- ``isEquiv`` to ``true`` returns ``false``.
- ``isTrue`` returns ``false``.
- ``isTerminal`` returns ``false``.
- Interpretation of the CDD dot image below: Looks correct as the diagonal constraint on the global clock allows all valuations of ``x`` (``x1`` on the image) to be ``true``.
The dot output before and after reduction is the same ([preview](https://dreampuf.github.io/GraphvizOnline/#digraph%20G%20%7B%0A%220x7ff83c9826d1%22%20%5Bshape%3Dbox%2C%20label%3D%221%22%2C%20style%3Dfilled%2C%20height%3D0.3%2C%20width%3D0.3%5D%3B%0A%220x7ff83c9826d0%22%20%5Bshape%3Dbox%2C%20label%3D%220%22%2C%20style%3Dfilled%2C%20height%3D0.3%2C%20width%3D0.3%5D%3B%0A%220x7ff80c1b00400%22%20%5Bshape%3Doctagon%2C%20color%20%3D%20black%2C%20label%3D%22x1-x0%22%5D%3B%0A%220x7ff80c1b00400%22%20-%3E%20%220x7ff83c9826d1%22%20%5Bstyle%3Ddashed%2C%20label%3D%22%5B0%3BINF%5B%22%5D%3B%0A%7D)):
````
digraph G {
"0x7ff83c9826d1" [shape=box, label="1", style=filled, height=0.3, width=0.3];
"0x7ff83c9826d0" [shape=box, label="0", style=filled, height=0.3, width=0.3];
"0x7ff80c1b00400" [shape=octagon, color = black, label="x1-x0"];
"0x7ff80c1b00400" -> "0x7ff83c9826d1" [style=dashed, label="[0;INF["];
}
````

__Experimentation__
``True`` gives the same result (Here the ``x`` is added to the cdd. Without the clock we just get the terminal ``true`` node which is correct).
``x >= n`` gives the same result for a negative n value.
``x >= n || True`` gives the same result where n is 0 or negative.
``x < n || x >= n`` gives the same result even if n is negative.
## Clock guard ``x < 0``
__Expected__
- The resulting pointer should point to a CDD node which is equivalent to ``false`` (In other words``isEquiv`` should return ``false``).
- The resulting pointer should preferably point to the terminal ``false`` node after reduction (In other words after calling ``reduce`` the CDD should have ``isFalse`` return ``True``).
- The resulting pointer should if ``isFalse`` returns ``True`` be a terminal node (In other words after reducing and ``isFalse`` returns ``true`` then ``isTerminal`` should return ``true``).
__Actual__
- ``isEquiv`` to ``false`` returns ``false``.
- ``isFalse`` returns ``false``.
- ``isTerminal`` returns ``false``.
The dot output before and after reduction is the same ([preview](https://dreampuf.github.io/GraphvizOnline/#digraph%20G%20%7B%0A%220x7fb3c057d6d1%22%20%5Bshape%3Dbox%2C%20label%3D%221%22%2C%20style%3Dfilled%2C%20height%3D0.3%2C%20width%3D0.3%5D%3B%0A%220x7fb3c057d6d0%22%20%5Bshape%3Dbox%2C%20label%3D%220%22%2C%20style%3Dfilled%2C%20height%3D0.3%2C%20width%3D0.3%5D%3B%0A%220x7fb3901500500%22%20%5Bshape%3Doctagon%2C%20color%20%3D%20black%2C%20label%3D%22x1-x0%22%5D%3B%0A%220x7fb3901500500%22%20-%3E%20%220x7fb3c057d6d1%22%20%5Bstyle%3Ddashed%2C%20label%3D%22%5B0%3B0%5B%22%5D%3B%0A%7D)):
````
digraph G {
"0x7ff09e67f6d1" [shape=box, label="1", style=filled, height=0.3, width=0.3];
"0x7ff09e67f6d0" [shape=box, label="0", style=filled, height=0.3, width=0.3];
"0x7ff0701400500" [shape=octagon, color = black, label="x1-x0"];
"0x7ff0701400500" -> "0x7ff09e67f6d1" [style=dashed, label="[0;0["];
}
````

__Experimentation__
WIP
Contributor guide
No contributing guide indexed for this repository
Research direction
Start by reproducing the reported CDD results for the x >= 0 and x < 0 clock guards, then inspect the reduction and equivalence behavior behind reduce, isEquiv, isTrue, and isFalse. Done means the guards reduce to the expected terminal true or false nodes and isTerminal reports true.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- java
- Domain
- devtools
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 30/100