Skip to:

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

Issues

Select view

Select search mode

 
1 of 1

Cannot use Formal machine parameters with multiple instantiation

Description

ProB fails to load B models where a machine with formal parameters is instantiatied twice.

Test case project :
https://github.com/vgheo/b-method-training/tree/2e3832cd4bed76962f836198adb73a54591a5779/tools-doc/ProB/samples/prob_include_prefix

Observed:

  • error "Cannot find CONSTANTS which satisfy...." :
    "The following properties directly led to an inconsistency:
    {0,1} = {2,3}
    == false
    0 = 2
    == false
    "

  • after "PARTIAL_SETUP_CONSTANTS" , the "State Properties" box contains:
    y1.Y1.T_ = {0,1}
    y1.Y1.init = 0
    x1.X1.T_ = {0,1}
    x1.X1.init = 0
    y1.Y1.T_ = {0,1}
    y1.Y1.init = 0
    x1.X1.T_ = {0,1}
    x1.X1.init = 0

NOTES:

  • The actual parameter names are missing defined prefixes a1 and b1, respectively.

  • The count and values for actual parameters are incorrect

Environment

None

Attachments

2

Gliffy Diagrams

Details

Assignee

Reporter

Affects versions

Priority

Created October 26, 2015 at 9:49 AM
Updated January 25, 2016 at 7:02 AM
Configure

Activity

Show:

Michael LeuschelJanuary 25, 2016 at 7:02 AM

I forgot to answer this question:
>>> The intermediate format uses "__" as a separator.
Actually, the . get translated into __ when pretty printing, so that it is in a form that can be read back in as a single machine.
So, internally there is no possibility of a clash, as users cannot use . within identifier names (only to separate identifiers).

[However, there could be a clash if you read the pretty-printed internal representation back in and you yourself use and identifier with __ in the middle. For this the pretty printer would need to use a table of symbols that appear in the B project.]

Michael LeuschelDecember 10, 2015 at 7:13 AM

Daniel and myself have discussed the issue.
Basically, we know how to fix it; but we haven't had the time to do it.
Michael

Vlad GheorgheDecember 8, 2015 at 8:32 PM

Hi there ! Are there any plans for this bug ?
Kind regards
Vlad Gheorghe

Vlad GheorgheOctober 27, 2015 at 6:48 PM

I have a question regarding the intermediate format (sample MM_Internal.mch).
The intermediate format uses "__" as a separator.

Does this translation properly handle user model identifiers that contain that sequence ("__") ?

Vlad GheorgheOctober 27, 2015 at 4:05 PM

Hi Michael,

I took the "B Language Reference" delivered with AtelierB 4.2.1 as a specification.
It also contains a grammar in the appendix.

I assume that there might be differences from the original B-Book (~1996).

Best regards
Vlad

Loading...