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

Jkind 2.1 requires Java 8 #21

Closed lwrage closed 9 years ago

lwrage commented 9 years ago

Version 2.1 seems to be built with Java 8 (classfile version 52.0). Is it possible to provide a build for Java 7?

agacek commented 9 years ago

I think it would be difficult at this point to provide a Java 7 build. We use various Java 8 features (lambdas, optional, streams, ...). It would take a long time to remove these.

Is there a pressing motivation for wanting a Java 7 version?

lwrage commented 9 years ago

It's not really a problem. OSATE runs on Java 7 and I had to update jkind to version 2.1 to run Agree. It's mostly a matter of documenting this on our end. Currently the Agree plugin doesn't report any error if it tries to run jkind on Java 7, it just doesn't do anything.

agacek commented 9 years ago

Yes, that is unfortunate. If you go to Window > Preferences > AGREE > Analysis and click on the "Check if available" button does it give an error message there? I know we were trying to add some more diagnostics there.

On Tue, Feb 24, 2015 at 8:00 AM, Lutz Wrage notifications@github.com wrote:

It's not really a problem. OSATE runs on Java 7 and I had to update jkind to version 2.1 to run Agree. It's mostly a matter of documenting this on our end. Currently the Agree plugin doesn't report any error if it tries to run jkind on Java 7, it just doesn't do anything.

— Reply to this email directly or view it on GitHub https://github.com/agacek/jkind/issues/21#issuecomment-75760456.

lwrage commented 9 years ago

The diagnostics don't work for me. No success message, no error message, nothing in the error log. We're about 2 weeks behind the smaccm develop branch, could there be a later commit that we need?

agacek commented 9 years ago

Yes, it's a fairly recent addition I think.

On Tue, Feb 24, 2015 at 8:33 AM, Lutz Wrage notifications@github.com wrote:

The diagnostics don't work for me. No success message, no error message, nothing in the error log. We're about 2 weeks behind the smaccm develop branch, could there be a later commit that we need?

— Reply to this email directly or view it on GitHub https://github.com/agacek/jkind/issues/21#issuecomment-75766529.

lwrage commented 9 years ago

Actually, there's a stack trace in the error log. And the fix is to catch Throwable instead of Exception in AgreePreferencePage.checkAvailable(). The same probably applies when jkind is called to get an error message when you try to run it. I don't have write permission so I can't fix it myself.

agacek commented 9 years ago

Ok, I've updated the develop branch of AGREE with that fix. Thanks!

On Tue, Feb 24, 2015 at 8:54 AM, Lutz Wrage notifications@github.com wrote:

Actually, there's a stack trace in the error log. And the fix is to catch Throwable instead of Exception in AgreePreferencePage.checkAvailable(). The same probably applies when jkind is called to get an error message when you try to run it. I don't have write permission so I can't fix it myself.

— Reply to this email directly or view it on GitHub https://github.com/agacek/jkind/issues/21#issuecomment-75770589.