When I click on a formula (of a Rodin file) containing the inverse (with -1 Unicode exponent) and try to visualize the formula as a graph I get a list of lexer and parse errors:
ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: ProB Standalone: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Parsing expression failed because: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Unexpected sub-formula, expected: an expression but was: a predicate ProB Standalone: ProB Standalone: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Unexpected sub-formula, expected: an expression but was: a predicate ProB Standalone: Parsing substitution failed because: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Unknown operator: (expected to find an assignment operator) ProB Standalone: ProB Standalone: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Lexer error, character '⁻' has been ignored ProB Standalone: Lexer error, character '¹' has been ignored ProB Standalone: Unknown operator: (expected to find an assignment operator) ProB Standalone: Code: !r.(r : ROUTES => nxt(r) : (rtbl⁻¹)[{r}] \ {lst(r)} >->> (rtbl⁻¹)[{r}] \ {fst(r)}) ProB Standalone: Unicode translation: ∀r·(r ∈ ROUTES ⇒ nxt(r) ∈ (rtbl⁻¹)[{r}] ∖ {lst(r)} ⤖ (rtbl⁻¹)[{r}] ∖ {fst(r)}) ProB Standalone: at de.prob.animator.domainobjects.EventB.ensureParsed(EventB.java:127) ProB Standalone: at de.prob.animator.domainobjects.EventB.printProlog(EventB.java:173) ProB Standalone: at de.prob.animator.command.GetDotForVisualizationCommand.writeCommand(GetDotForVisualizationCommand.java:36) ProB Standalone: at de.prob.animator.command.ComposedCommand.writePrefixedCommand(ComposedCommand.java:57) ProB Standalone: at de.prob.animator.command.ComposedCommand.writeCommand(ComposedCommand.java:51) ProB Standalone: at de.prob.animator.CommandProcessor.sendCommand(CommandProcessor.java:44) ProB Standalone: at de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:62) ProB Standalone: at de.prob.statespace.StateSpace.execute(StateSpace.java:545) ProB Standalone: at de.prob2.ui.dynamic.dotty.DotView.getSvgForDotCommand(DotView.java:187) ProB Standalone: at de.prob2.ui.dynamic.dotty.DotView.lambda$visualize$6(DotView.java:151) ProB Standalone: at java.lang.Thread.run(Thread.java:748)
Major
When I click on a formula (of a Rodin file) containing the inverse (with -1 Unicode exponent) and try to visualize the formula as a graph I get a list of lexer and parse errors:
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone:
ProB Standalone: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Parsing expression failed because: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Unexpected sub-formula, expected: an expression but was: a predicate
ProB Standalone:
ProB Standalone: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Unexpected sub-formula, expected: an expression but was: a predicate
ProB Standalone: Parsing substitution failed because: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Unknown operator: (expected to find an assignment operator)
ProB Standalone:
ProB Standalone: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Lexer error, character '⁻' has been ignored
ProB Standalone: Lexer error, character '¹' has been ignored
ProB Standalone: Unknown operator: (expected to find an assignment operator)
ProB Standalone: Code: !r.(r : ROUTES => nxt(r) : (rtbl⁻¹)[{r}] \ {lst(r)} >->> (rtbl⁻¹)[{r}] \ {fst(r)})
ProB Standalone: Unicode translation: ∀r·(r ∈ ROUTES ⇒ nxt(r) ∈ (rtbl⁻¹)[{r}] ∖ {lst(r)} ⤖ (rtbl⁻¹)[{r}] ∖ {fst(r)})
ProB Standalone: at de.prob.animator.domainobjects.EventB.ensureParsed(EventB.java:127)
ProB Standalone: at de.prob.animator.domainobjects.EventB.printProlog(EventB.java:173)
ProB Standalone: at de.prob.animator.command.GetDotForVisualizationCommand.writeCommand(GetDotForVisualizationCommand.java:36)
ProB Standalone: at de.prob.animator.command.ComposedCommand.writePrefixedCommand(ComposedCommand.java:57)
ProB Standalone: at de.prob.animator.command.ComposedCommand.writeCommand(ComposedCommand.java:51)
ProB Standalone: at de.prob.animator.CommandProcessor.sendCommand(CommandProcessor.java:44)
ProB Standalone: at de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:62)
ProB Standalone: at de.prob.statespace.StateSpace.execute(StateSpace.java:545)
ProB Standalone: at de.prob2.ui.dynamic.dotty.DotView.getSvgForDotCommand(DotView.java:187)
ProB Standalone: at de.prob2.ui.dynamic.dotty.DotView.lambda$visualize$6(DotView.java:151)
ProB Standalone: at java.lang.Thread.run(Thread.java:748)