ProB Java API: Is it possible to dump model state after animation and load it to the model in the next run?

[Denis Efremov]

Hi,

as in de.prob2.kernel-3.11.0 version I can see Api.eventb_save method that saves Event-B model in prolog format, SerializeStateCommand and DeserializeStateCommand commands.

Can I save a model state after, let's say 5 animation steps, with SerializeStateCommand:

SerializeStateCommand cmd = new SerializeStateCommand(trace.getCurrentState().getId());
trace.getStateSpace().execute(cmd);
try (PrintWriter out = new PrintWriter("model.state")) {
   out.println(cmd.getState());
}


Next, load it somehow and start new animation from the loaded state?

DeserializeStateCommand cmd = new DeserializeStateCommand(new String(Files.readAllBytes(Paths.get("model.state"))));
stateSpace.execute(cmd);
Trace trace = new Trace(stateSpace.getState(cmd.getId())); // this doesn't work obviously

It looks like I need to call tcltk_save_state/tcltk_load_state predicates from src/state_space.pl but it's not possible from Java API because they are not whitelisted.

Thanks,
Denis

[Michael Leuschel]

Hi Denis,

in ProB2-UI it is possible to save a trace (as a JSON file) and replay it later.
This feature is also available within the JAVA API.
This may be the feature you need?

The tcltk_load_state predicates will only work in probcli and ProB Tcl/Tk, as ProB2-UI and the Java API have their own state (which is not saved by tcltk_save_state).

Greetings,
Michael

> --
> You received this message because you are subscribed to the Google Groups "ProB Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/prob-users/218f6c98-0629-4106-8488-463c8f26538ao%40googlegroups.com.

[Denis Efremov]

On Friday, July 3, 2020 at 5:57:17 PM UTC+3, Michael Leuschel wrote:

Hi Denis,

in ProB2-UI it is possible to save a trace (as a JSON file) and replay it later.
This feature is also available within the JAVA API.

Seems like it's not available. I can't find it in sources and in documentation to the Java API.

I tried to call print_trace_for_replay from src/b_trace_checking.pl directly. The error: "Call not on whitelist".

 

The tcltk_load_state predicates will only work in probcli and ProB Tcl/Tk, as ProB2-UI and the Java API have their own state (which is not saved by tcltk_save_state).

That's sad. Still, I don't understand what SerializeStateCommand/DeserializeStateCommand commands are for?

[Michael Leuschel]

Hi Denis,

the mechanism for saving a trace and replaying it are currently in the ProB2-UI codebase:

https://gitlab.cs.uni-duesseldorf.de/stups/prob/prob2_ui/-/blob/develop/src/main/java/de/prob2/ui/animation/tracereplay/TraceFileHandler.java
https://gitlab.cs.uni-duesseldorf.de/stups/prob/prob2_ui/-/blob/develop/src/main/java/de/prob2/ui/animation/tracereplay/TraceChecker.java

The Objects which are exported to JSON are in the ProB2 Java Kernel: https://gitlab.cs.uni-duesseldorf.de/stups/prob/prob2_kernel/-/tree/develop/de.prob2.kernel/src/main/java/de/prob/check/tracereplay


Maybe we can put all related functionality into the prob2 kernel.

Greetings,
Michael

> --
> You received this message because you are subscribed to the Google Groups "ProB Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/prob-users/864ff412-e4db-4932-8556-e8f83955ba8fo%40googlegroups.com.

[yefremo...@gmail.com]

This could be really helpful. I implement custom replay strategy based on data gathered from real system. When I detect model<->system behaviour divergence during animation it's really handy to dump the model state for further manual analysis and debugging in ProB UI. Unfortunately, I can't use probcli or ProB UI to implement my animation strategy.

Regards,

Denis

[Fabian Vu]

Hello Denis,

the mechanism for Trace Replay has been moved to the ProB2 Java API. You can invoke the functions

save(PersistentTrace trace, Path location)
load(Path path)

in TraceLoaderSaver to save and to load traces respectively. PersistentTrace can be created from an instance of the class Trace

https://github.com/hhu-stups/prob2_kernel/blob/develop/de.prob2.kernel/src/main/java/de/prob/check/tracereplay/TraceLoaderSaver.java

https://github.com/hhu-stups/prob2_kernel/blob/develop/de.prob2.kernel/src/main/java/de/prob/check/tracereplay/PersistentTrace.java


It is also possible to replay the loaded trace using replayTrace(PersistentTrace persistentTrace, StateSpace stateSpace) in ReplayTrace.

https://github.com/hhu-stups/prob2_kernel/blob/develop/de.prob2.kernel/src/main/java/de/prob/check/tracereplay/TraceReplay.java