Connecting PRISM to Python

[Naz Alan]

Hello developers,

I am currently developing a program in Python and would like to fetch data from PRISM via an API. However, the PRISM API on GitHub seems to be written in Java, and since I don't have much knowledge in Java, I was wondering if anyone could give me some tips on how to connect Python program to my PRISM data.

Thank you in advance.

 Best Regards

[Dave Parker]

Hi Naz,

We don't yet have a good way to do this I'm afraid. It's on the todo
list. Others have had success with using py4j (https://www.py4j.org/) to
create a wrapper around the Java API accessible from PRISM, but it seems
likely that this does require a bit of Java knowledge too.

Best wishes,

Dave

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/c85a7ff9-3e02-4706-8b14-1627b4dff865n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/c85a7ff9-3e02-4706-8b14-1627b4dff865n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Naz Alan]

Hello Dave,

thank you very much for your response. I will try to look at that and will share my findings with you.

So, regarding the PRISM JAVA API. I have downloaded and successfully set up the source code using Cygwin on my windows and tested on Eclipse with no errors. But when I try to set-up the prism-api on my computer according to the instruction in documentation prismmodelchecker/prism-api: Example code for connecting to PRISM programmatically. (github.com) on github to build the examples (specifically, at ‘make’ after ‘cd prism-api’ part), I encountered this error on Cygwin:

User@DESKTOP-F***** /cygdrive/c/Users/user/Desktop/TAW/prism-api

$ make OSTYPE=cygwin JAVA_DIR="/cygdrive/c/Program Files/Java/jdk-18"

(javac -classpath "../prism/classes:../prism/lib/*:../prism/prism/classes:../prism/prism/lib/*" -d classes src/./demos/DTMCModelGenerator.java)

src\.\demos\DTMCModelGenerator.java:34: error: package parser does not exist

import parser.State;

             ^

src\.\demos\DTMCModelGenerator.java:35: error: package parser does not exist

import parser.VarList;

...

...

...

(Total of 67 errors)

make: *** [Makefile:23: classes/./demos/DTMCModelGenerator.class] Error 1

 

I have retried many times, but the same problem still occurs. Therefore, I would really appreciate any help or hints from you regarding this issue.

Thank you in advance.

 

Best Regards,

Naz 

[Dave Parker]

I guess that the Makefile has only been tested on Linux/Mac and not
Windows. Cygwin is happy to translate / to \ in the paths, but the
directory separator for the classpath should also change from : to ;
Try changing that in the definition of PRISM_CLASSPATH near the top of
the Makefile, and try again.

Best wishes,

Dave

On 01/04/2022 23:21, Naz Alan wrote:
> Hello Dave,
>
> thank you very much for your response. I will try to look at that and
> will share my findings with you.
>
> So, regarding the PRISM JAVA API. I have downloaded and successfully set
> up the source code using Cygwin on my windows and tested on Eclipse with
> no errors. But when I try to set-up the prism-api on my computer
> according to the instruction in documentation
> prismmodelchecker/prism-api: Example code for connecting to PRISM
> programmatically. (github.com)

> <https://github.com/prismmodelchecker/prism-api> on github to build the

> <https://www.py4j.org/>) to

> <https://groups.google.com/d/msgid/prismmodelchecker/c85a7ff9-3e02-4706-8b14-1627b4dff865n%40googlegroups.com?utm_medium=email&utm_source=footer
> <https://groups.google.com/d/msgid/prismmodelchecker/c85a7ff9-3e02-4706-8b14-1627b4dff865n%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit

> https://groups.google.com/d/msgid/prismmodelchecker/39781339-6efc-49ac-972d-a4976b33be88n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/39781339-6efc-49ac-972d-a4976b33be88n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Naz Alan]

Hi Dave,

i tried changing the directory separator for the classpath from : to ; , but unfortunately i received error in the make test.

Here is a screenshot of the results I get from performing make and make test on the prism-api:

Any help would be great.

Best Regards,

Naz

[Nasruddin]

Hi Dave,

i tried changing the directory separator for the classpath from : to ; , but unfortunately I received error in the 'make test'. Here is a screenshot of the results I get when performing make and make test on the prism-api:

Any help would be great.

Best Regards,

Naz

On Tuesday, April 26, 2022 at 8:30:20 PM UTC+2 d.a.parker wrote:

[Dave Parker]

OK, I'm glad that the compilation works now. You have the same issue in
the 'bin/run' script. Try changing PRISM_CLASSPATH (line 16) there in
the same way. I'm afraid I don't have a Windows install to hand to test
it, but I suspect you will also need to change the same thing (: -> ;)
in PRISM_LIB_PATH (line 20), and also change LD_LIBRARY_PATH (line 24)
to PATH.

Best wishes,

Dave

On 26/04/2022 19:57, Nasruddin wrote:
> Hi Dave,
>
> i tried changing the directory separator for the classpath from : to ; ,
> but unfortunately I received error in the 'make test'. Here is a
> screenshot of the results I get when performing make and make test on
> the prism-api:
>

> Screenshot 2022-04-26 205532.png
> Any help would be great.
>
> Best Regards,
> Naz
> On Tuesday, April 26, 2022 at 8:30:20 PM UTC+2 d.a.parker wrote:
>
> I guess that the Makefile has only been tested on Linux/Mac and not
> Windows. Cygwin is happy to translate / to \ in the paths, but the
> directory separator for the classpath should also change from : to ;
> Try changing that in the definition of PRISM_CLASSPATH near the top of
> the Makefile, and try again.
>
> Best wishes,
>
> Dave
>
> On 01/04/2022 23:21, Naz Alan wrote:
> > Hello Dave,
> >
> > thank you very much for your response. I will try to look at that
> and
> > will share my findings with you.
> >
> > So, regarding the PRISM JAVA API. I have downloaded and
> successfully set
> > up the source code using Cygwin on my windows and tested on
> Eclipse with
> > no errors. But when I try to set-up the prism-api on my computer
> > according to the instruction in documentation
> > prismmodelchecker/prism-api: Example code for connecting to PRISM

> > programmatically. (github.com <http://github.com>)
> > <https://github.com/prismmodelchecker/prism-api

> <https://groups.google.com/d/msgid/prismmodelchecker/39781339-6efc-49ac-972d-a4976b33be88n%40googlegroups.com?utm_medium=email&utm_source=footer
> <https://groups.google.com/d/msgid/prismmodelchecker/39781339-6efc-49ac-972d-a4976b33be88n%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit

> https://groups.google.com/d/msgid/prismmodelchecker/88e986a2-4eaf-4060-90b2-d97c39a29844n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/88e986a2-4eaf-4060-90b2-d97c39a29844n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Naz Alan]

Hi Dave,

thank you for your input. Now i have different error for 'make test' after changing the bin/run file (which looks like this):

btw, I use prism from source code as my prism folder, instead of cloning from git as suggested in the basic instructions in prismmodelchecker/prism-api: Example code for connecting to PRISM programmatically. (github.com), because I faced an error when performing 'make' by cloning from git.

Best Regards,

Naz

[Dave Parker]

Hi Naz,

Since we discussed this a bit further off-list, and it now seems to
work, I've added the Cygwin script to the prism-api repo:

https://github.com/prismmodelchecker/prism-api/blob/master/bin/run-cygwin

Best wishes,

Dave

On 26/04/2022 21:22, Naz Alan wrote:
> Hi Dave,
>
> thank you for your input. Now i have different error for 'make test'
> after changing the bin/run file (which looks like this):

> Screenshot 2022-04-26 221819.png
>
> btw, I use prism from source code as my prism folder, instead of cloning
> from git as suggested in the basic instructions in
> prismmodelchecker/prism-api: Example code for connecting to PRISM
> programmatically. (github.com)

> <https://github.com/prismmodelchecker/prism-api>, because I faced an

> <http://github.com <http://github.com>>)

> <https://groups.google.com/d/msgid/prismmodelchecker/88e986a2-4eaf-4060-90b2-d97c39a29844n%40googlegroups.com?utm_medium=email&utm_source=footer
> <https://groups.google.com/d/msgid/prismmodelchecker/88e986a2-4eaf-4060-90b2-d97c39a29844n%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit

> https://groups.google.com/d/msgid/prismmodelchecker/de4449a8-c707-44f2-a1ee-ce6b54a82eb3n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/de4449a8-c707-44f2-a1ee-ce6b54a82eb3n%40googlegroups.com?utm_medium=email&utm_source=footer>.