Issues
Cannot use Formal machine parameters with multiple instantiation
Description
Environment
Attachments
Gliffy Diagrams
Details
Details
Assignee
Reporter
Affects versions
Priority
Activity
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
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