suweining
commented
9 years ago 新的尝试： 需要明确的几点： 1）产生二义性的部分是关于InModes部分的 2）根据语法卡片，在SubCmpAssocDef 中，CmpInModes 出现在各个属性的后面 这样，我们可以把CmpInModes从各个属性的定义中独立出来，重新定义SubCmpAssocDef 。 SubCmpAssocDef原有的定义： syntax SubCmpAssocDef ::= SubCmpAssocDefElem | SubCmpAssocDefElem SubCmpAssocDef 重新定义为： syntax SubCmpAssocDef ::= SubCmpAssocDefMid // 这儿要对CmpInModes进行展开 | SubCmpAssocDefMid InModes | SubCmpAssocDefMid Min Mmodes MBracketLeft Id MRoughArrow Id MBracketRight | SubCmpAssocDefMid Min Mmodes MBracketLeft ModeName MComma ModeNameList MBracketRight
syntax SubCmpAssocDefMid ::= SubCmpAssocDefElem // Mid中并不包含CmpInModes
| SubCmpAssocDefElem SubCmpAssocDef
syntax SubCmpAssocDefElem ::= UniCmpClassifierRef | UniCmpClassifierRef ProtoTypeBindings | ArrayDimension | ArrayDimensions ArrayElementImplList // | CmpInModes // 将其独立出来单独存在 | MBraceLeft ContainedPpeAssoc MBraceRight | MBraceLeft PpeAssoc PpeContainedPpeAssocList MBraceRight | MBraceLeft ContainedPpeAssoc PpeContainedPpeAssocList MBraceRight | AmbBraceLeftPpeAssocBraceRight | AmbBracketLeftIdBracketRight 现在让我们看看ModalPpeValue 的定义： syntax ModalPpeValue ::= PpeValue InModes | PpeValue InModes MComma ModalPpeValue syntax PpeValue ::= SinglePpeValue | PpeListValue | Id 通过对SubCmpAssocDef 重新定义，可以更清晰的展示二义性的部分：
syntax SubCmpAssocDef ::=SubCmpAssocDefMid InModes 和 syntax ModalPpeValue ::= PpeValue InModes
解决方案：分别将SubCmpAssocDefElem和PpeValue展开，将相同的部分提取出来后重新定义
The last ambiguity appears when analyze the test tests/unit/ModesAndModeTransitions.aadl.The error message is the old one in the issue named "some internal errors while ' krun filename.k '".The main error message is: Exception in thread "main" java.lang.AssertionError: The greatest lower bound (GLB) of sorts [SubCmpAssocDef, ModalPpeValue]doesn't exist!
2.SubCmpAssocDef, ModalPpeValue in abstract syntax tree
First is about SubCmpAssocDef.
syntax SubCmp ::= Id Mcolon AbstractCmpCategory SubCmpAssocDef MSemicolon | ...... syntax SubCmpList ::= SubCmp | SubCmp SubCmpList syntax CmpImplAssocDefElem ::= Msubcomponents SubCmpList | .......
Second is about ModalPpeValue .
syntax PpeAssoc ::=UniPpeId MRoughArrow ModalPpeValue MSemicolon | ...... syntax ProtoTypePpeAssocList ::= PpeAssoc | PpeAssoc ProtoTypePpeAssocList syntax ProtoType ::= Id Mcolon ProtoTypeDef MBraceLeft ProtoTypePpeAssocList MBraceRight MSemicolon | ...... syntax ProtoTypeList ::= ProtoType | ProtoType ProtoTypeList syntax CmpImplAssocDefElem ::= Mprototypes ProtoTypeList
| ...... So CmpImplAssocDefElem is the least common ancestors in the abstract syntax tree. But ProtoTypeList begins with key word "prototypes" while SubCmpList begins with key word "subcomponents" and why they will overlap at the bottom of the abstract syntax tree.
3.reason of the last ambiguity
And we unfold the PpeValue :
It is clear that "InModes" may cause the overlap.
4 some try to eliminate the error
The defination of "SubCmpAssocDefElem SubCmpAssocDefElem" in SubCmpAssocDef is the position of the error.So we try to redefine the "SubCmpAssocDefElem SubCmpAssocDefElem".
step1) separate "SubCmpAssocDefElem SubCmpAssocDefElem" from the SubCmpAssocDef
syntax SubCmpAssocDef ::= SubCmpAssocDefElem // one SubCmpAssocDefElem
| SubCmpAssocDefElem SubCmpAssocDefElem // two SubCmpAssocDefElem
| SubCmpAssocDefElem SubCmpAssocDefElem SubCmpAssocDef // multy SubCmpAssocDefElem
redefine as below:
syntax SubCmpAssocDef ::= SubCmpAssocDefElem // one SubCmpAssocDefElem
| DoubleSubCmpAssocDefElemAdjust // two SubCmpAssocDefElem
| SubCmpAssocDefElem SubCmpAssocDefElem SubCmpAssocDef // multy SubCmpAssocDefElem
step2) define the "DoubleSubCmpAssocDefElemAdjust" We should pay more attention to CmpInModes and ArrayDimension because they can cause overlap. When we define the DoubleSubCmpAssocDefElemAdjust, we shall unfold "CmpInModes and ArrayDimension",thus remove the same syntax in PpeAssoc. Here is part of our defination about DoubleSubCmpAssocDefElemAdjust:
syntax DoubleSubCmpAssocDefElemAdjust ::= UniCmpClassifierRef Min Mmodes MBracketLeft Id MRoughArrow Id MBracketRight | UniCmpClassifierRef ProtoTypeBindings Min Mmodes MBracketLeft Id MRoughArrow Id MBracketRight | MLeftBracket ArrayDimensionSize MRightBracket Min Mmodes MBracketLeft Id MRoughArrow Id MBracketRight | ArrayDimensions ArrayElementImplList Min Mmodes MBracketLeft Id MRoughArrow Id MBracketRight | CmpInModes Min Mmodes MBracketLeft Id MRoughArrow Id MBracketRight | AmbBracketLeftIdBracketRight Min Mmodes MBracketLeft Id MRoughArrow Id MBracketRight | UniCmpClassifierRef Min Mmodes MBracketLeft ModeName MComma ModeNameList MBracketRight | UniCmpClassifierRef ProtoTypeBindings Min Mmodes MBracketLeft ModeName MComma ModeNameList MBracketRight | MLeftBracket ArrayDimensionSize MRightBracket Min Mmodes MBracketLeft ModeName MComma ModeNameList MBracketRight | ArrayDimensions ArrayElementImplList Min Mmodes MBracketLeft ModeName MComma ModeNameList MBracketRight | CmpInModes Min Mmodes MBracketLeft ModeName MComma ModeNameList MBracketRight | AmbBracketLeftIdBracketRight Min Mmodes MBracketLeft ModeName MComma ModeNameList MBracketRight
You can get the detal in Subcomponent.k
5 test
we krun the ModesAndModeTransitions.aadl and get the error message: [Error] Critical: Parse error: Syntax error near unexpected character '\n' File: ../tests/unit/ModesAndModeTransitions.aadl Location: (51,0,51,0) The position of the error is:
48: system implementation Gps.Secure extends Gps.Dual 49: subcomponents 50: Secure_Gps: process Gps_Sender.Secure in modes (Securemode); 51: connections .........
If we add "UniCmpClassifierRef AmbInModesBracketLeftIdBracketRight" in the DoubleSubCmpAssocDefElemAdjust ,the error will not appear,but this will cause the overlap error.