Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

PROBPLUGIN - State View Expression does not allow Theory Plugin operators

Description

I was animating a model (ListTest1; cf below) which makes uses of the List Theory with the rev(.) operator.
I was not able to add an expression or predicate using the rev(.) operator in the State view (using the green + button).
The dialog box says:
[Unexpected sub-formula, expected: a predicate but was: an expression]

When I type rev(l)=nil (instead of rev(l)) I get the message:
Error in the underlying Rodin database.

Environment

None

Attachments

1

Gliffy Diagrams

Activity

Show:

Jenkins Build Server March 18, 2014 at 7:27 AM

FAILURE: Integrated in

ProB_eclipse_develop_Rodin3 #13

Jenkins Build Server January 31, 2014 at 11:55 AM

SUCCESS: Integrated in

ProB_eclipse_develop #1321
PROBPLUGIN-91: Bugfix, instead of default FormulaFactory, we now use the project's FormulaFactory (plagge: rev 631631ddb972cc121329d939731be2d5aa814969)

  • de.prob.core/src/de/prob/core/langdep/EventBAnimatorPart.java

Daniel Plagge January 31, 2014 at 11:17 AM

We are now using the project's FormulaFactory, not the default one.

Fixed

Details

Assignee

Reporter

Priority

Created January 14, 2014 at 9:24 PM
Updated March 18, 2014 at 7:27 AM
Resolved January 31, 2014 at 11:17 AM
Configure