search

loonwerks / jkind

JKind - An infinite-state model checker for safety properties in Lustre
http://loonwerks.com/tools/jkind.html
Other
52 stars 32 forks source link

Fixes to allow '!' in identifiers #75

Closed mww-aws closed 1 year ago

mww-aws commented 1 year ago

Add an additional character to identifiers to make it easier to build translators.

agacek commented 1 year ago

Thanks Mike. Can you also add a test case to the testing folder? I know the general test set up isn't great anyway, but this will keep a record of intention.

mww-aws commented 1 year ago

I have added two test files to show how identifiers with '!' might look and I have also re-run 10 existing benchmarks to make sure that the parsing code did not break existing models. Since '!' is not a symbol used in Lustre, as expected, there were no issues.

agacek commented 1 year ago

Thanks Mike. I merged it.

mww-aws commented 1 year ago

Yes, absolutely, I will add a handful of tests and better document the outcome of adding support for ‘!’. I rushed that CR.

Mike

From: Andrew Gacek @.> Reply-To: loonwerks/jkind @.> Date: Thursday, September 29, 2022 at 9:05 PM To: loonwerks/jkind @.> Cc: "Whalen, Mike" @.>, Author @.***> Subject: Re: [loonwerks/jkind] Fixes to allow '!' in identifiers (PR #75)

Thanks Mike. Can you also add a test case to the testing folder? I know the general test set up isn't great anyway, but this will keep a record of intention.

— Reply to this email directly, view it on GitHubhttps://github.com/loonwerks/jkind/pull/75#issuecomment-1263017899, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ANIVFYGCT5JOSNC7JIDVB2LWAZDCBANCNFSM6AAAAAAQZJCDHU. You are receiving this because you authored the thread.Message ID: @.***>