Errors in ProB2UI Execute by Predicate for Theory Operators

[leuschel]

For the model T_TemperatureMachinePrefix_mch.eventb in prob_examples/examples/EventBPrologPackages/Toulouse/Mendil the execute by predicate command does not work when providing values for the parameter. On the other hand, writing a predicate like unit(para)=Celsius works.

de.prob.animator.command.ExecuteOperationException: Formula must be a predicate, not ASSIGNMENT: newTemperature=newTemperatureT((1|->Kelvin))
    at de.prob.animator.command.GetOperationByPredicateCommand.<init>(GetOperationByPredicateCommand.java:78)
    at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:269)
    at de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:294)
    at de.prob2.ui.operations.ExecuteByPredicateStage.executeSync(ExecuteByPredicateStage.java:159)
    at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:539)
    at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
    at de.prob2.ui.internal.executor.CompletableFutureTask.run(CompletableFutureTask.java:40)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
    at java.base/java.lang.Thread.run(Thread.java:833)

[leuschel]

The error message with "not ASSIGNMENT" is also misleading. The error also appears when using just the predicate:

[leuschel]

In Tcl/Tk it works; maybe because it uses the B Parser and not the Event-B parser?? Also, in ProB2UI the expression newTemperatureT((21|->Kelvin)) does not work in the B Console.

[leuschel]

Actually, ProB2UI also works when we open the Rodin model via the .eventb file and not directly from Rodin.

[leuschel]

The archive is available at examples/EventBPrologPackages/Toulouse/Mendil/TemperatureAggregatorPrefix.zip

[leuschel]

In Console for model loaded directly from Rodin .bum file:

ProB B-Console
EventB> x=newTemperatureT((21|->Kelvin))
Could not parse formula:
Parsing predicate failed because: Preconditions for this extended operator are not fulfilled

Preconditions for this extended operator are not fulfilled
Parsing expression failed because: Preconditions for this extended operator are not fulfilled

Preconditions for this extended operator are not fulfilled
Parsing substitution failed because: Unknown operator:  (expected to find an assignment operator)

Unknown operator:  (expected to find an assignment operator)
Code: x=newTemperatureT((21|->Kelvin))
Unicode translation: x=newTemperatureT((21↦Kelvin))

After loading .eventb file:

Model loaded: T_TemperatureMachinePrefix_mch
EventB> x=newTemperatureT((21|->Kelvin))
TRUE (x = newTemperatureT((21↦Kelvin)))
EventB> 

[iTitus]

The console uses the current state space to execute expressions. It might not have been fully initialized?