search

CinRC / IRDC-CCSK

Java implementation of distributed reversible computation verification
https://spots.augusta.edu/caubert/cinrc/
GNU General Public License v3.0
4 stars 2 forks source link

Parsing unreachable processes #66

Closed aubertc closed 1 year ago

aubertc commented 1 year ago

The process "c.a[k].b.0" is not reachable, but the tool somehow makes it reachable by changing it to something actually meaningful:

java -jar target/IRDC-3.0.0.0-jar-with-dependencies.jar --interactive "c.a[k].b.0"
a[k]
------| Actionable Labels |------
[0] c
[1] [k1]
[q] Quit program
------------
a[k1].c.b

(with an additional weird bug that makes it display first a[k], then a[k1].c.b).

The expected behaviour (and this is related to https://github.com/CinRC/IRDC-CCSK/issues/22 ) would be to "reject" it.

aubertc commented 1 year ago

This issue resurfaced…

java -jar target/IRDC-4.1.1.1-jar-with-dependencies.jar "b.a[k1].0"
a[k0].b (Depth: 0), []
└─b─ a[k0].b[k1].0 (Depth: 1), [b]
aubertc commented 1 year ago

"b.a[k1].0"

I still get this issue?

peterbro1 commented 1 year ago

Fixed. That bug got reintroduced during parser v2 merge.