Skip to:

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

Java B Parser does not accept DEFINITIONS inside SETS clause

Description

The following works in Atelier-B but not in ProB:

/* TestSETDEF

  • Author:

  • Creation date: 27/03/2014
    */
    MACHINE
    TestSETDEF
    DEFINITIONS
    AA_els == {aa,bb}
    SETS
    AA = AA_els
    ASSERTIONS
    aa : AA
    END

Environment

None

Gliffy Diagrams

Activity

Show:

Jens Bendisposto March 11, 2015 at 1:31 AM

Should this be fixed?

Jens Bendisposto March 27, 2014 at 5:47 PM

Sets are not treated as Expressions in our parser because it is very limited what you can write. I am not sure, but I think we might end up in an very ugly special case.

Won't Fix

Details

Assignee

Reporter

Priority

More fields

Created March 27, 2014 at 4:17 PM
Updated June 29, 2015 at 9:47 AM
Resolved June 29, 2015 at 9:47 AM
Configure