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 … reachable processes #69

Closed aubertc closed 1 year ago

aubertc commented 1 year ago

This is related to https://github.com/CinRC/IRDC-CCSK/issues/26 and possibly to https://github.com/CinRC/IRDC-CCSK/issues/66 .

The process a | a[k] is reachable and yet its parsing trigger an exception: 

java -jar target/IRDC-3.0.0.0-jar-with-dependencies.jar "a.0 | a[k]"
a[k]
Exception in thread "main" java.lang.IndexOutOfBoundsException: Index: 1, Size: 1
        at java.base/java.util.LinkedList.checkElementIndex(LinkedList.java:559)
        at java.base/java.util.LinkedList.remove(LinkedList.java:529)
        at org.cinrc.process.ProcessTemplate.initComplex(ProcessTemplate.java:54)
        at org.cinrc.process.ProcessTemplate.export(ProcessTemplate.java:78)
        at org.cinrc.IRDC.enumerate(IRDC.java:110)
        at org.cinrc.IRDC.main(IRDC.java:63)
peterbro1 commented 1 year ago

This was an error with implicit null processes. Fixed in latest commit

aubertc commented 1 year ago

This issue resurfaced…

java -jar target/IRDC-4.1.1.1-jar-with-dependencies.jar "a.0 | a[k]"
Exception in thread "main" org.cinrc.parser.CCSParserException: Attempted to parse a.0 | a[k] but was left with unrecognized characters: 
 [,],
        at org.cinrc.parser.ProcessBuilder.tokenize(ProcessBuilder.java:178)
        at org.cinrc.parser.ProcessBuilder.export(ProcessBuilder.java:86)
        at org.cinrc.parser.CCSParser.parseLine(CCSParser.java:46)
        at org.cinrc.IRDC.enumerate(IRDC.java:110)
        at org.cinrc.IRDC.main(IRDC.java:63)
aubertc commented 1 year ago

In the dev branch, I still have this issue:

java -jar target/IRDC-4.1.1.1-jar-with-dependencies.jar "a.0 | a[k]"
Exception in thread "main" org.cinrc.parser.CCSParserException: Attempted to parse a.0 | a[k] but was left with unrecognized characters: 
 [,],
aubertc commented 1 year ago

Ok, my mistake was to use k instead of kn for some n integer. That is,

java -jar target/IRDC-4.1.1.1-jar-with-dependencies.jar "a.0 | a[k1]"

works as intended.