These exceptions are due to the new treatment of all formulas as TLA formulas. We should consider adding a method for internal evaluation in the ProB2 models (here for the classical B-translation instead of the TLA module in the context of operation parameters).
java.lang.NullPointerException: Cannot invoke "tla2sany.modanalyzer.ParseUnit.getParseTree()" because "p" is null
at de.tla2bAst.ExpressionTranslator.evalVariables(ExpressionTranslator.java:222)
at de.tla2bAst.ExpressionTranslator.parse(ExpressionTranslator.java:75)
at de.tla2bAst.Translator.translateExpressionIncludingModel(Translator.java:318)
at de.prob.animator.domainobjects.TLA.fromTLA(TLA.java:39)
at de.prob.animator.domainobjects.TLA.<init>(TLA.java:30)
at de.prob.model.representation.TLAModel.parseFormula(TLAModel.java:63)
at de.prob.model.representation.AbstractModel.parseFormula(AbstractModel.java:99)
at de.prob2.ui.operations.OperationItem.lambda$forTransitions$1(OperationItem.java:164)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.prob2.ui.operations.OperationItem.lambda$forTransitions$2(OperationItem.java:165)
at java.base/java.util.HashMap.forEach(HashMap.java:1429)
at de.prob2.ui.operations.OperationItem.forTransitions(OperationItem.java:136)
at de.prob2.ui.operations.OperationItem.forTransitionsFast(OperationItem.java:209)
at de.prob2.ui.history.HistoryItem.itemsForTrace(HistoryItem.java:21)
at de.prob2.ui.history.HistoryView.lambda$initialize$4(HistoryView.java:141)
at javafx.base@21.0.2/com.sun.javafx.binding.ExpressionHelper$Generic.fireValueChangedEvent(ExpressionHelper.java:372)
at javafx.base@21.0.2/com.sun.javafx.binding.ExpressionHelper.fireValueChangedEvent(ExpressionHelper.java:91)
at javafx.base@21.0.2/javafx.beans.property.ReadOnlyObjectPropertyBase.fireValueChangedEvent(ReadOnlyObjectPropertyBase.java:80)
at de.prob2.ui.prob2fx.CurrentTrace.access$000(CurrentTrace.java:39)
at de.prob2.ui.prob2fx.CurrentTrace$AnimationChangeListener.lambda$traceChange$0(CurrentTrace.java:51)
at javafx.graphics@21.0.2/com.sun.javafx.application.PlatformImpl.lambda$runLater$10(PlatformImpl.java:456)
at java.base/java.security.AccessController.doPrivileged(AccessController.java:400)
at javafx.graphics@21.0.2/com.sun.javafx.application.PlatformImpl.lambda$runLater$11(PlatformImpl.java:455)
at javafx.graphics@21.0.2/com.sun.glass.ui.InvokeLaterDispatcher$Future.run(InvokeLaterDispatcher.java:95)
tla2sany.configuration.TokenMgrError: Lexical error at line 1, column 1. Encountered: "" (0), after : ""
at tla2sany.configuration.ConfigurationTokenManager.getNextToken(ConfigurationTokenManager.java:1182)
at tla2sany.configuration.Configuration.jj_ntk(Configuration.java:390)
at tla2sany.configuration.Configuration.ConfigurationUnit(Configuration.java:79)
at tla2sany.configuration.Configuration.load(Configuration.java:62)
at tla2sany.drivers.SANY.frontEndInitialize(SANY.java:167)
at de.tla2bAst.ExpressionTranslator.parseModuleWithoutSemanticAnalyse(ExpressionTranslator.java:205)
at de.tla2bAst.ExpressionTranslator.parse(ExpressionTranslator.java:74)
at de.tla2bAst.Translator.translateExpressionIncludingModel(Translator.java:318)
at de.prob.animator.domainobjects.TLA.fromTLA(TLA.java:39)
at de.prob.animator.domainobjects.TLA.<init>(TLA.java:30)
at de.prob.model.representation.TLAModel.parseFormula(TLAModel.java:63)
at de.prob.model.representation.AbstractModel.parseFormula(AbstractModel.java:99)
at de.prob2.ui.operations.OperationItem.lambda$forTransitions$1(OperationItem.java:164)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.prob2.ui.operations.OperationItem.lambda$forTransitions$2(OperationItem.java:165)
at java.base/java.util.HashMap.forEach(HashMap.java:1429)
at de.prob2.ui.operations.OperationItem.forTransitions(OperationItem.java:136)
at de.prob2.ui.operations.OperationItem.forTransitions(OperationItem.java:205)
at de.prob2.ui.operations.OperationsView.updateBG(OperationsView.java:397)
at de.prob2.ui.operations.OperationsView.lambda$update$12(OperationsView.java:388)
at de.prob2.ui.internal.executor.BackgroundUpdater.lambda$execute$3(BackgroundUpdater.java:81)
at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:572)
at com.google.common.util.concurrent.TrustedListenableFutureTask$TrustedFutureInterruptibleTask.runInterruptibly(TrustedListenableFutureTask.java:131)
at com.google.common.util.concurrent.InterruptibleTask.run(InterruptibleTask.java:76)
at com.google.common.util.concurrent.TrustedListenableFutureTask.run(TrustedListenableFutureTask.java:82)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
at java.base/java.lang.Thread.run(Thread.java:1583)
These exceptions are due to the new treatment of all formulas as TLA formulas. We should consider adding a method for internal evaluation in the ProB2 models (here for the classical B-translation instead of the TLA module in the context of operation parameters).
(example used here: https://github.com/Apress/practical-tla-plus/blob/master/Chapter%201/wire.tla)