Use the same probcli instance to load all machines

This significantly improves the performance of loading new machines.

CHANGELOG.md

@@ -2,6 +2,8 @@
 
 ## [(next version)](./README.md#for-developers)
 
+* Updated ProB 2 to version 4.0.0-SNAPSHOT.
+* Improved the performance of loading machines by reusing the existing instance of ProB instead of starting a new one for each machine.
 * Significantly refactored the logic for parsing commands and their arguments.
 	* This is an internal change and should not affect any user-visible behavior. That is, all inputs that were accepted by previous versions should still be accepted - if any previously valid inputs are no longer accepted, this is a bug.
 	* As a side effect, the inspection and code completion features now work better in a few edge cases.

build.gradle

@@ -39,7 +39,7 @@ configurations.all {
 dependencies {
 	implementation(group: "com.google.code.gson", name: "gson", version: "2.8.6")
 	implementation(group: "com.google.guava", name: "guava", version: "28.2-jre")
-	implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "3.11.0")
+	implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "4.0.0-SNAPSHOT")
 	implementation(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.3.0")
 	implementation(group: "org.jetbrains", name: "annotations", version: "18.0.0")
 	implementation(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")

src/main/java/de/prob2/jupyter/ProBKernel.java

@@ -16,6 +16,7 @@ import java.util.Map;
 import java.util.Optional;
 import java.util.Properties;
 import java.util.concurrent.atomic.AtomicReference;
+import java.util.function.Function;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 import java.util.stream.Collectors;
@@ -25,10 +26,12 @@ import com.google.inject.Inject;
 import com.google.inject.Injector;
 import com.google.inject.Singleton;
 
+import de.prob.animator.ReusableAnimator;
 import de.prob.animator.domainobjects.ErrorItem;
 import de.prob.exception.ProBError;
 import de.prob.scripting.ClassicalBFactory;
 import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.StateSpace;
 import de.prob.statespace.Trace;
 import de.prob2.jupyter.commands.AssertCommand;
 import de.prob2.jupyter.commands.BrowseCommand;
@@ -218,6 +221,7 @@ public final class ProBKernel extends BaseKernel {
 	}
 	
 	private final @NotNull AnimationSelector animationSelector;
+	private final @NotNull ReusableAnimator animator;
 	
 	private final @NotNull Map<@NotNull String, @NotNull Command> commands;
 	private final @NotNull AtomicReference<@Nullable Thread> currentEvalThread;
@@ -226,12 +230,13 @@ public final class ProBKernel extends BaseKernel {
 	private @NotNull Path currentMachineDirectory;
 	
 	@Inject
-	private ProBKernel(final @NotNull Injector injector, final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector) {
+	private ProBKernel(final @NotNull Injector injector, final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector, final @NotNull ReusableAnimator animator) {
 		super();
 		
 		this.setShouldReplaceStdStreams(false);
 		
 		this.animationSelector = animationSelector;
+		this.animator = animator;
 		
 		this.commands = COMMAND_CLASSES.stream()
 			.map(injector::getInstance)
@@ -240,7 +245,10 @@ public final class ProBKernel extends BaseKernel {
 		this.currentEvalThread = new AtomicReference<>(null);
 		this.variables = new HashMap<>();
 		
-		this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").load()));
+		this.switchMachine(Paths.get(""), stateSpace -> {
+			classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").loadIntoStateSpace(stateSpace);
+			return new Trace(stateSpace);
+		});
 		this.currentMachineDirectory = Paths.get("");
 	}
 	
@@ -272,6 +280,28 @@ public final class ProBKernel extends BaseKernel {
 		this.currentMachineDirectory = currentMachineDirectory;
 	}
 	
+	public void unloadMachine() {
+		final Trace oldTrace = this.animationSelector.getCurrentTrace();
+		if (oldTrace != null) {
+			assert oldTrace.getStateSpace() == this.animator.getCurrentStateSpace();
+			this.animationSelector.changeCurrentAnimation(null);
+			oldTrace.getStateSpace().kill();
+		}
+		this.setCurrentMachineDirectory(Paths.get(""));
+	}
+	
+	public void switchMachine(final @NotNull Path machineDirectory, final @NotNull Function<@NotNull StateSpace, @NotNull Trace> newTraceCreator) {
+		this.unloadMachine();
+		final StateSpace newStateSpace = this.animator.createStateSpace();
+		try {
+			this.animationSelector.changeCurrentAnimation(newTraceCreator.apply(newStateSpace));
+		} catch (final RuntimeException e) {
+			newStateSpace.kill();
+			throw e;
+		}
+		this.setCurrentMachineDirectory(machineDirectory);
+	}
+	
 	@Override
 	public @NotNull String getBanner() {
 		return "ProB Interactive Expression and Predicate Evaluator (on Jupyter)\nType \":help\" for more information.";

src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java

@@ -77,10 +77,13 @@ public final class LoadCellCommand implements Command {
 		final String body = args.get(CODE_PARAM);
 		final Map<String, String> preferences = CommandUtils.parsePreferences(args.get(PREFS_PARAM));
 		
-		this.animationSelector.changeCurrentAnimation(new Trace(CommandUtils.withSourceCode(body, () ->
-			this.classicalBFactory.create("(machine from Jupyter cell)", body).load(preferences)
-		)));
-		this.proBKernelProvider.get().setCurrentMachineDirectory(Paths.get(""));
+		this.proBKernelProvider.get().switchMachine(Paths.get(""), stateSpace -> {
+			stateSpace.changePreferences(preferences);
+			CommandUtils.withSourceCode(body, () ->
+				this.classicalBFactory.create("(machine from Jupyter cell)", body).loadIntoStateSpace(stateSpace)
+			);
+			return new Trace(stateSpace);
+		});
 		return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getStateSpace().getMainComponent());
 	}
 	

src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java

@@ -101,13 +101,16 @@ public final class LoadFileCommand implements Command {
 		}
 		final Map<String, String> preferences = CommandUtils.parsePreferences(args.get(PREFS_PARAM));
 		
-		try {
 		final ModelFactory<?> factory = this.injector.getInstance(FactoryProvider.factoryClassFromExtension(extension));
-			this.animationSelector.changeCurrentAnimation(new Trace(factory.extract(machineFilePath.toString()).load(preferences)));
-			this.proBKernelProvider.get().setCurrentMachineDirectory(machineFileDirectory);
-		} catch (IOException | ModelTranslationError e) {
+		this.proBKernelProvider.get().switchMachine(machineFileDirectory, stateSpace -> {
+			stateSpace.changePreferences(preferences);
+			try {
+				factory.extract(machineFilePath.toString()).loadIntoStateSpace(stateSpace);
+			} catch (final IOException | ModelTranslationError e) {
 				throw new RuntimeException(e);
 			}
+			return new Trace(stateSpace);
+		});
 		return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getStateSpace().getMainComponent());
 	}