java.lang.UnsatisfiedLinkError: ..\lib\jdd.dll: Can't find dependent libraries

[John Smith]

Hi All,

I am trying to run PRISM programmatically (using Eclipse IDE), however, when I run my checker class I get exactly this output:

java.lang.UnsatisfiedLinkError: ..\prism-4.3.beta\lib\jdd.dll: Can't find dependent libraries
PRISM
=====

Version: 4.3.beta
Date: Tue Aug 11 19:29:21 BST 2015
Hostname: (my computer)
Memory limits: cudd=1g, java(heap)=247.5m

It should then commence with a verification, although nothing happens.

Sorry that I am unable to give much detail on the problem as I really don't know what would be helpful to include. All I can say is that in Eclipse, I right click on JRE System Library (in my project) -> Build Path -> Configure Build Path -> Add External JARs... and then navigate to prism.jar - is this incorrect?

Note: I have triple checked I am using the same bit version of PRISM and Java. Also, I have coded my class to that which is practically identical to how it is shown in PrismTest.java, so I am positive that the issue is not coding error.

Many thanks for any help you can give.
John.

[Dave Parker]

Hi John,

There are some Eclipse+PRISM instructions here:

http://www.prismmodelchecker.org/wiki/Developers/SettingUpEclipse

It looks like your problem is that you have not set up the environment
variables to allow the native libraries (DLLs) to be found. On Windows,
this means setting the "PATH" environment variable to ";lib". That
assumes that your Eclipse project is the PRISM directory, which includes
the lib directory.

Best wishes,

Dave.

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecke...@googlegroups.com
> <mailto:prismmodelchecke...@googlegroups.com>.
> To post to this group, send email to
> prismmodel...@googlegroups.com
> <mailto:prismmodel...@googlegroups.com>.
> Visit this group at http://groups.google.com/group/prismmodelchecker-dev.

[John Smith]

Hi Dave,

Thanks a lot, PRISM is now working, adding "lib" to the windows Path solved it. A couple of final questions:

When performing prism.closeDown() I get the following error (note: this ONLY occurs when closing down prism, otherwise it runs fine):

Exception in thread "main" java.lang.NoClassDefFoundError: edu/jas/kern/ComputerThreads
    at param.ParamModelChecker.closeDown(ParamModelChecker.java:1176)
    at prism.Prism.closeDown(Prism.java:3535)
    at prism.Prism.closeDown(Prism.java:3519)
    at Checker.verify(Checker.java:51)
    at Checker.main(Checker.java:25)
Caused by: java.lang.ClassNotFoundException: edu.jas.kern.ComputerThreads
    at java.net.URLClassLoader.findClass(Unknown Source)
    at java.lang.ClassLoader.loadClass(Unknown Source)
    at sun.misc.Launcher$AppClassLoader.loadClass(Unknown Source)
    at java.lang.ClassLoader.loadClass(Unknown Source)
    ... 5 more

Also, is there any way to surpress the output from PRISM? I only require the result from Result.getResult() - a lot of other information is printed out that is essentially flooding the console.

Regards,
John.

[Dave Parker]

> Thanks a lot, PRISM is now working, adding "lib" to the windows Path
> solved it. A couple of final questions:

Great.

> When performing prism.closeDown() I get the following error (note: this
> ONLY occurs when closing down prism, otherwise it runs fine):
>
> Exception in thread "main" java.lang.NoClassDefFoundError:
> edu/jas/kern/ComputerThreads

That is a class in colt.jar, which is the lib directory. You need to add
all jar files in that directory to the "Libraries" section when you
configure the build path in Eclipse.

> Also, is there any way to surpress the output from PRISM? I only require
> the result from Result.getResult() - a lot of other information is
> printed out that is essentially flooding the console.

Use new PrismDevNullLog() instead of new PrismFileLog("stdout") when you
create the Prism object.

Best wishes,

Dave.

[John Smith]

Perfect, that's solved everything now, much appreciated.

Kind regards,
John.