You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to PRISM model checker
Hi, I am working on a program that makes use of an older version of Prism to check properties against states. I was wondering if Prism can be used concurrently in two or more threads with a different Prism instance being made in each thread? I have different folders for each thread to store the relevant files but I am occasionally having a sigsegv originating from inside prism when prism.modelCheck(PropertiesFile, Prop) is called by two threads at the same time. Otherwise it works fine for a single thread.
The Specific version I am using is based on https://github.com/kleinj/prism-svn/tree/proposed-global-sync as those changes were needed in our project. Is there any hard coded files in the prism library or other shared elements that would cause an issue?
Thanks,
Peter Aloisi
Dave Parker
unread,
Mar 31, 2022, 4:49:57 PM3/31/22
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to prismmod...@googlegroups.com, Peter Aloisi
Hi Peter,
PRISM was not built to be executed concurrently in this way I'm afraid,
so I'm not very surprised it crashes.
The main things that are static across Prism objects are the parser and
the native shared libraries (CUDD etc.). The segfault errror suggests it
could be a problem with the latter. So you _might_ have more luck
switching to the (pure Java) explicit engine (enabled with
prism.setEngine(Prism.EXPLICIT) from Java), but I wouldn't bank on it.