About using PRISM for validation in Python

[Serendipity953]

I am a graduate student who has just started researching the use of PRISM for some validation tasks. Instead of using a PRISM desktop application, I wanted to do this directly by building the PRISM model in Python and using the program interface.

I notice that your work uses PRISM through Py4j, for example "MDP = gateway.entry_point.getmdpsimple ()". I'm curious if "getMdpSimple()" is in a Java program you wrote yourself, and how can I use PRISM's Java API?

I would be honored if you could take note of my problem！

[phate09]

Hello Serendipity953 I'm currently using a fork of Prism to communicate with Python where I changed a couple of things such the use of Py4j. You can find the fork in the documentation in https://github.com/phate09/prism. The file is prism/prism/src/server/MdpAbstract.java Indeed there is no standard way of accessing PRISM from python so I built this interface for my project. Feel free to use it as a reference code

…

On Aug 23 2022, at 9:04 am, Serendipity953 ***@***.***> wrote: I am a graduate student who has just started researching the use of PRISM for some validation tasks. Instead of using a PRISM desktop application, I wanted to do this directly by building the PRISM model in Python and using the program interface. I notice that your work uses PRISM through Py4j, for example "MDP = gateway.entry_point.getmdpsimple ()". I'm curious if "getMdpSimple()" is in a Java program you wrote yourself, and how can I use PRISM's Java API? I would be honored if you could take note of my problem！ — Reply to this email directly, view it on GitHub (#3), or unsubscribe (https://github.com/notifications/unsubscribe-auth/ACWACB7BKWPTCPVW6WYXHMTV2SAYPANCNFSM57KNTCIQ). You are receiving this because you are subscribed to this thread.

[Serendipity953]

OK，thank you for your attention. I have found this file and I'm now reading it! It helps me a lot!

[Serendipity953]

Some errors have happened when I try to execute the runnables/symbolic/dqn/domain_analysis_sym.py follow the READEME.md.
The error looks like:

Traceback (most recent call last):
File "domain_analysis_sym.py", line 48, in
split_performed = unroll_methods.probability_iteration(storage, rtree, precision, rounding, env_class, n_workers, explorer, verification_model, state_size, horizon=horizon,
File "/root/SafeDRL/SafeDRL/symbolic/unroll_methods.py", line 602, in probability_iteration
leaves = storage.get_leaves(shortest_path, unsafe_threshold, horizon * 2)
File "/root/SafeDRL/SafeDRL/prism/state_storage.py", line 94, in get_leaves
leaves = [(interval, len(shortest_path[interval]) - 1, attributes.get('lb'), attributes.get('ub')) for interval, attributes in self.graph.nodes.data() if
File "/root/SafeDRL/SafeDRL/prism/state_storage.py", line 95, in
self.graph.out_degree(interval) == 0 and not attributes.get('half_fail') and not attributes.get('fail')and interval.action is None and not attributes.get(
AttributeError: 'tuple' object has no attribute 'action'

So I changed the node in the graph form :
storage.root = (HyperRectangle.round(current_interva, rounding), None)
storage.graph.add_node(storage.root)

to :
storage.root = HyperRectangle._action(HyperRectangle.round(current_interva, rounding), None) storage.graph.add_node(storage.root)

So that the interval in self.graph.nodes.data() can have attribute action and the program can be executed until another error occur:

Traceback (most recent call last):
File "domain_analysis_sym.py", line 48, in
split_performed = unroll_methods.probability_iteration(storage, rtree, precision, rounding, env_class, n_workers, explorer, verification_model, state_size, horizon=horizon,
File "/root/SafeDRL/SafeDRL/symbolic/unroll_methods.py", line 600, in probability_iteration
storage.recreate_prism(horizon * 2)
File "/root/SafeDRL/SafeDRL/prism/state_storage.py", line 151, in recreate_prism
solution_max = list(gateway.entry_point.check_state_list(half_terminal_states_java, False))
File "/root/miniconda3/envs/safedrl/lib/python3.8/site-packages/py4j/java_gateway.py", line 1309, in call
return_value = get_return_value(
File "/root/miniconda3/envs/safedrl/lib/python3.8/site-packages/py4j/protocol.py", line 326, in get_return_value
raise Py4JJavaError(
py4j.protocol.Py4JJavaError: An error occurred while calling t.check_state_list.
: java.lang.NullPointerException
at explicit.MDPModelChecker.doValueIterationReachProbs(MDPModelChecker.java:780)
at explicit.MDPModelChecker.computeReachProbsNumeric(MDPModelChecker.java:519)
at explicit.MDPModelChecker.computeReachProbs(MDPModelChecker.java:453)
at explicit.MDPModelChecker.computeReachProbs(MDPModelChecker.java:246)
at server.MdpAbstract.check_state_list(MdpAbstract.java:90)
at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base/java.lang.reflect.Method.invoke(Method.java:566)
at py4j.reflection.MethodInvoker.invoke(MethodInvoker.java:244)
at py4j.reflection.ReflectionEngine.invoke(ReflectionEngine.java:357)
at py4j.Gateway.invoke(Gateway.java:282)
at py4j.commands.AbstractCommand.invokeMethod(AbstractCommand.java:132)
at py4j.commands.CallCommand.execute(CallCommand.java:79)
at py4j.GatewayConnection.run(GatewayConnection.java:238)
at java.base/java.lang.Thread.run(Thread.java:834)

I‘m not sure whether the change I made is right and, if so, why the second error occurred. I'm sure that the gradle runs in the right way .

[Serendipity953]

maybe I found how to cope with this problem