enable TLC model check for models with classical B representation

- if not classical B, the internal representation is used
- the translation from B to TLA+ is limited

src/main/java/de/prob2/ui/menu/FileMenu.java

@@ -21,13 +21,13 @@
 import de.prob.model.representation.AbstractModel;
 import de.prob.model.representation.XTLModel;
 import de.prob.scripting.Api;
-import de.prob.scripting.ClassicalBFactory;
 import de.prob.statespace.FormalismType;
 import de.prob2.ui.beditor.BEditorView;
 import de.prob2.ui.config.FileChooserManager;
 import de.prob2.ui.documentation.SaveDocumentationStage;
 import de.prob2.ui.error.WarningAlert;
 import de.prob2.ui.internal.FXMLInjected;
+import de.prob2.ui.internal.I18n;
 import de.prob2.ui.internal.StageManager;
 import de.prob2.ui.preferences.PreferencesStage;
 import de.prob2.ui.prob2fx.CurrentProject;
@@ -36,7 +36,7 @@
 import de.prob2.ui.project.NewProjectStage;
 import de.prob2.ui.project.ProjectManager;
 
-import de.tlc4b.exceptions.TLC4BException;
+import de.prob2.ui.verifications.modelchecking.TLCModelCheckingTab;
 import javafx.beans.InvalidationListener;
 import javafx.event.ActionEvent;
 import javafx.fxml.FXML;
@@ -138,12 +138,10 @@ private void initialize() {
 				this.exportAsEventBProlog.setDisable(noEventBExport);
 			}
 		});
-		currentProject.currentMachineProperty().addListener((o, from, to) ->  {
-			if (to != null) {
-				// TLA Export, TODO: check if possible for Event-B (via pretty printing classical B)
-				this.exportAsTLAModule.setDisable(to.getModelFactoryClass() != ClassicalBFactory.class);
-			}
-		});
+
+		// TLA Export:
+		currentTrace.addListener((o, from, to) ->
+				this.exportAsTLAModule.setDisable(to != null && to.getModel().getFormalismType() != FormalismType.B));
 
 		MachineLoader machineLoader = injector.getInstance(MachineLoader.class);
 		this.reloadMachineItem.disableProperty().bind(currentProject.currentMachineProperty().isNull().or(machineLoader.loadingProperty()));
@@ -277,10 +275,10 @@ private void handleExportTLA() throws IOException, BCompoundException {
 		final Path outputDir = fileChooserManager.showDirectoryChooser(chooser, FileChooserManager.Kind.NEW_MACHINE, stageManager.getCurrent());
 
 		if (outputDir != null) {
-			Path bMachine = currentProject.getLocation().resolve(currentProject.getCurrentMachine().getLocation());
 			try {
+				Path bMachine = TLCModelCheckingTab.getClassicalBMachine(currentProject, currentTrace.getStateSpace(), injector.getInstance(I18n.class));
 				TLCModelChecker.generateTLAWithoutTLC(bMachine.toString(), outputDir.toString());
-			} catch (TLC4BException e) {
+			} catch (RuntimeException e) {
 				stageManager.makeAlert(Alert.AlertType.ERROR, "menu.file.items.exportEntireModelAs.tlaModule.exception.header",
 						"menu.file.items.exportEntireModelAs.tlaModule.exception.content", e.getMessage()).show();
 			}

src/main/java/de/prob2/ui/verifications/modelchecking/TLCModelCheckingItem.java

@@ -134,7 +134,7 @@ public void isFinished(String jobId, long timeElapsed, IModelCheckingResult resu
 		};
 
 		TLCModelChecker tlcModelChecker = new TLCModelChecker(
-			context.project().getLocation().resolve(context.machine().getLocation()).toString(),
+			TLCModelCheckingTab.getClassicalBMachine(context.project(), context.machine(), context.stateSpace(), context.i18n()).toString(),
 			stateSpace, listener,
 			new TLCModelCheckingOptions(getOptions()));
 		tlcModelChecker.call();

src/main/java/de/prob2/ui/verifications/modelchecking/TLCModelCheckingTab.java

@@ -1,21 +1,31 @@
 package de.prob2.ui.verifications.modelchecking;
 
+import java.io.IOException;
+import java.nio.file.Files;
 import java.nio.file.Path;
 import java.util.Map;
 
 import com.google.inject.Inject;
 
 import de.be4.classicalb.core.parser.exceptions.BCompoundException;
+import de.prob.animator.command.GetInternalRepresentationCommand;
+import de.prob.animator.domainobjects.FormulaTranslationMode;
 import de.prob.check.ModelCheckingSearchStrategy;
 import de.prob.check.TLCModelCheckingOptions;
-import de.prob.scripting.ClassicalBFactory;
+import de.prob.model.classicalb.ClassicalBModel;
+import de.prob.model.eventb.EventBModel;
+import de.prob.model.representation.AbstractModel;
+import de.prob.statespace.FormalismType;
+import de.prob.statespace.StateSpace;
 import de.prob2.ui.config.FileChooserManager;
 import de.prob2.ui.internal.FXMLInjected;
 import de.prob2.ui.internal.I18n;
 import de.prob2.ui.internal.StageManager;
 import de.prob2.ui.internal.TranslatableAdapter;
 import de.prob2.ui.prob2fx.CurrentProject;
 import de.prob2.ui.prob2fx.CurrentTrace;
+import de.prob2.ui.project.Project;
+import de.prob2.ui.project.machines.Machine;
 import de.tlc4b.TLC4B;
 import de.tlc4b.TLC4BOption;
 
@@ -225,27 +235,22 @@ void checkTlcApplicable() {
 
 		this.checkedTlcApplicable = true;
 
-		// TODO: support other languages by pretty printing internal representation (Event-B)?
-		//  (with current internal repr. not automatically possible)
-		if (currentProject.getCurrentMachine().getModelFactoryClass() == ClassicalBFactory.class) {
-			Path machinePath = currentProject.getLocation().resolve(currentProject.getCurrentMachine().getLocation());
-			Thread thread = new Thread(() -> {
-				try {
-					TLC4B.checkTLC4BIsApplicable(machinePath.toString());
-				} catch (BCompoundException | RuntimeException exc) {
-					LOGGER.warn("TLC4B is not applicable to this machine", exc);
-					Platform.runLater(() -> this.tlcApplicableError.set(exc.getMessage()));
-					return;
-				}
-
-				Platform.runLater(() -> this.tlcApplicableError.set(null));
-			}, "TLC4B applicability checker");
-			// Don't let this thread keep the JVM alive if it's still running when the UI exits.
-			thread.setDaemon(true);
-			thread.start();
-		} else {
-			this.tlcApplicableError.set(i18n.translate("verifications.modelchecking.modelcheckingStage.tlcTab.onlyClassicalB"));
-		}
+		Thread thread = new Thread(() -> {
+			try {
+				Path machinePath = getClassicalBMachine(currentProject, currentTrace.getStateSpace(), i18n);
+				// TODO: show info when internal representation is used
+				TLC4B.checkTLC4BIsApplicable(machinePath.toString());
+			} catch (BCompoundException | RuntimeException exc) {
+				LOGGER.warn("TLC4B is not applicable to this machine", exc);
+				Platform.runLater(() -> this.tlcApplicableError.set(exc.getMessage()));
+				return;
+			}
+
+			Platform.runLater(() -> this.tlcApplicableError.set(null));
+		}, "TLC4B applicability checker");
+		// Don't let this thread keep the JVM alive if it's still running when the UI exits.
+		thread.setDaemon(true);
+		thread.start();
 	}
 
 	public ModelCheckingItem getResult() {
@@ -286,5 +291,35 @@ private void setData(final Map<TLC4BOption, String> options) {
 			tfSaveLocation.setText(options.get(TLC4BOption.OUTPUT));
 		}
 	}
+
+	public static Path getClassicalBMachine(CurrentProject currentProject, StateSpace stateSpace, I18n i18n) {
+		return getClassicalBMachine(currentProject.get(), currentProject.getCurrentMachine(), stateSpace, i18n);
+	}
+
+	public static Path getClassicalBMachine(Project project, Machine machine, StateSpace stateSpace, I18n i18n) {
+		Path machinePath;
+		AbstractModel model = stateSpace.getModel();
+		if (model instanceof ClassicalBModel) {
+			machinePath = project.getLocation().resolve(machine.getLocation());
+		} else if (model.getFormalismType() == FormalismType.B) { // if not classical B: use internal representation
+			if (model instanceof EventBModel && !stateSpace.getCurrentPreference("NUMBER_OF_ANIMATED_ABSTRACTIONS").equals("0")) {
+				throw new RuntimeException(i18n.translate("verifications.modelchecking.modelcheckingStage.tlcTab.eventBAnimatedAbstractionsError"));
+			}
+			try { // translate Event-B/Alloy etc. to internal classical B representation
+				machinePath = Files.createTempFile("b_internal_rep_",".mch");
+				GetInternalRepresentationCommand cmd = new GetInternalRepresentationCommand();
+				cmd.setTranslationMode(FormulaTranslationMode.ATELIERB);
+				cmd.setTypeInfos(GetInternalRepresentationCommand.TypeInfos.NEEDED);
+				stateSpace.execute(cmd);
+				Files.writeString(machinePath, cmd.getPrettyPrint());
+				machinePath.toFile().deleteOnExit();
+			} catch (IOException e) {
+				throw new RuntimeException(e);
+			}
+		} else { // model has no classical B internal representation
+			throw new RuntimeException(i18n.translate("verifications.modelchecking.modelcheckingStage.tlcTab.onlyClassicalB"));
+		}
+		return machinePath;
+	}
 }
 

src/main/resources/de/prob2/ui/prob2.properties

@@ -1011,6 +1011,7 @@ verifications.modelchecking.modelcheckingStage.tlcTab.checkLTL = Check ASSERT_LT
 verifications.modelchecking.modelcheckingStage.tlcTab.checkLTLFormula = Check LTL formula
 verifications.modelchecking.modelcheckingStage.tlcTab.error.notApplicable = TLC Model Checking not applicable:
 verifications.modelchecking.modelcheckingStage.tlcTab.errors = Search for Errors and Properties:
+verifications.modelchecking.modelcheckingStage.tlcTab.eventBAnimatedAbstractionsError = For Event-B, you need to reload the model and set the preference NUMBER_OF_ANIMATED_ABSTRACTIONS to \u20180\u2019.
 verifications.modelchecking.modelcheckingStage.tlcTab.initialDepth = Initial Depth
 verifications.modelchecking.modelcheckingStage.tlcTab.LTLFormulaPrompt = LTL formula
 verifications.modelchecking.modelcheckingStage.tlcTab.nrWorkers = Number of workers

src/main/resources/de/prob2/ui/prob2_de.properties

@@ -978,6 +978,7 @@ verifications.modelchecking.modelcheckingStage.tlcTab.checkLTL = ASSERT_LTL Auss
 verifications.modelchecking.modelcheckingStage.tlcTab.checkLTLFormula = LTL Formel \u00FCberpr\u00FCfen
 verifications.modelchecking.modelcheckingStage.tlcTab.error.notApplicable = TLC Model Checking nicht anwendbar:
 verifications.modelchecking.modelcheckingStage.tlcTab.errors = Suche nach Fehlern und Eigenschaften:
+verifications.modelchecking.modelcheckingStage.tlcTab.eventBAnimatedAbstractionsError = F\u00FCr Event-B muss das Modell neu geladen und die Pr\u00E4ferenz NUMBER_OF_ANIMATED_ABSTRACTIONS auf '0' gesetzt werden.
 verifications.modelchecking.modelcheckingStage.tlcTab.initialDepth = Initiale Tiefe
 verifications.modelchecking.modelcheckingStage.tlcTab.LTLFormulaPrompt = LTL-Formel
 verifications.modelchecking.modelcheckingStage.tlcTab.nrWorkers = Anzahl der Worker

src/main/resources/de/prob2/ui/prob2_fr.properties

@@ -924,6 +924,7 @@ verifications.modelchecking.modelcheckingStage.tlcTab.checkLTL = V\u00E9rifier l
 verifications.modelchecking.modelcheckingStage.tlcTab.checkLTLFormula = V\u00E9rifier la formule LTL
 verifications.modelchecking.modelcheckingStage.tlcTab.error.notApplicable = TLC Model Checking non applicable :
 verifications.modelchecking.modelcheckingStage.tlcTab.errors = Recherche d'erreurs et de propri\u00E9t\u00E9s :
+verifications.modelchecking.modelcheckingStage.tlcTab.eventBAnimatedAbstractionsError = Pour Event-B, vous devez recharger le mod\u00E8le et d\u00E9finir la pr\u00E9f\u00E9rence NUMBER_OF_ANIMATED_ABSTRACTIONS \u00E0 \u00AB 0 \u00BB.
 verifications.modelchecking.modelcheckingStage.tlcTab.initialDepth = Profondeur initiale
 verifications.modelchecking.modelcheckingStage.tlcTab.LTLFormulaPrompt = Formule LTL
 verifications.modelchecking.modelcheckingStage.tlcTab.nrWorkers = Nombre de workers