Ecdar / Ecdar/j-Ecdar

CDD x>=0 and x<0

Open
#100 0 comments 0 reactions 0 assignees View on GitHub
bug
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["];
}
````
![x = 0](https://user-images.githubusercontent.com/58144556/224556710-a1312d5f-defb-4a99-bf0f-6a1185a5963c.png)

__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["];
}
````
![x 0](https://user-images.githubusercontent.com/58144556/224556132-1fd12efa-58c2-4b73-ba57-d29c2cac3a16.png)
__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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.