Exceptions when animating TLA modules in ProB2-UI

[cobizobi]

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 [email protected]/com.sun.javafx.binding.ExpressionHelper$Generic.fireValueChangedEvent(ExpressionHelper.java:372)
	at [email protected]/com.sun.javafx.binding.ExpressionHelper.fireValueChangedEvent(ExpressionHelper.java:91)
	at [email protected]/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 [email protected]/com.sun.javafx.application.PlatformImpl.lambda$runLater$10(PlatformImpl.java:456)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:400)
	at [email protected]/com.sun.javafx.application.PlatformImpl.lambda$runLater$11(PlatformImpl.java:455)
	at [email protected]/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)

(example used here: https://github.com/Apress/practical-tla-plus/blob/master/Chapter%201/wire.tla)