We're updating the issue view to help you get more done. 

Unicode translator does not add space between identifier ending with non-letter and operator starting with letter

Description

When trying to load the third refinement of
git@github.com:heinzware/EventBPacman-Plugin.git ( https://github.com/heinzware/EventBPacman-Plugin/tree/master/eventb) Pacman_Machine_3.bum
ProB2 raises the following exception:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 de.prob.animator.domainobjects.EvaluationException: Could not parse formula: Parsing predicate failed because: Tokens have been ignored Parsing expression failed because: Unexpected sub-formula, expected: an expression but was: a predicate Parsing assignment failed because: Unknown operator: (expected to find an assignment operator) Unknown operator: (expected to find an assignment operator) Code: position=pos_geist_1or position=pos_geist_2or position=pos_geist_3or position=pos_geist_4 Unicode translation: position=pos_geist_1or position=pos_geist_2or position=pos_geist_3or position=pos_geist_4 at de.prob.animator.domainobjects.EventB.ensureParsed(EventB.java:106) at de.prob.animator.domainobjects.EventB.getAst(EventB.java:169) at de.prob.model.eventb.translate.EventBMachineTranslator.processEvents(EventBMachineTranslator.java:167) at de.prob.model.eventb.translate.EventBMachineTranslator.translateMachine(EventBMachineTranslator.java:75) at de.prob.model.eventb.translate.EventBModelTranslator.printProlog(EventBModelTranslator.java:121) at de.prob.animator.command.LoadEventBProjectCommand.writeCommand(LoadEventBProjectCommand.java:20) at de.prob.animator.CommandProcessor.sendCommand(CommandProcessor.java:44) at de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:68) at de.prob.statespace.StateSpace.execute(StateSpace.java:543) at de.prob.scripting.StateSpaceProvider.loadFromCommand(StateSpaceProvider.java:40) at de.prob.model.eventb.EventBModel.load(EventBModel.java:135) at de.prob.scripting.ExtractedModel.load(ExtractedModel.java:24) at de.prob.scripting.Api.eventb_load(Api.java:169) at de.prob2.ui.project.MachineLoader.load(MachineLoader.java:142) at de.prob2.ui.project.MachineLoader.lambda$loadAsync$2(MachineLoader.java:104) at java.base/java.lang.Thread.run(Thread.java:834)

Environment

None

Status

Assignee

dgelessus

Reporter

Michael Leuschel

Epic Name <span class="error">&#91;deprecated, this field is no longer being used&#93;</span>

None

Choose Group

None

Priority

Major