public class RulesTransformation extends DepthFirstAdapter
| Modifier and Type | Field and Description |
|---|---|
static java.lang.String |
COMPUTATION_DISABLED |
static java.lang.String |
COMPUTATION_EXECUTED |
static java.lang.String |
COMPUTATION_NOT_EXECUTED |
static java.lang.String |
RULE_COUNTER_EXAMPLE_VARIABLE_SUFFIX |
static java.lang.String |
RULE_COUNTEREXAMPLE_OUTPUT_PARAMETER_NAME |
static java.lang.String |
RULE_DISABLED |
static java.lang.String |
RULE_FAIL |
static java.lang.String |
RULE_NOT_CHECKED |
static java.lang.String |
RULE_RESULT_OUTPUT_PARAMETER_NAME |
static java.lang.String |
RULE_SUCCESS |
| Constructor and Description |
|---|
RulesTransformation(Start start,
BParser bParser,
RulesMachineChecker rulesMachineChecker,
java.util.Map<java.lang.String,AbstractOperation> allOperations) |
caseAAbstractConstantsContextClause, caseAAbstractConstantsMachineClause, caseAAbstractMachineParseUnit, caseAAddExpression, caseAAnticipatedEventstatus, caseAAnySubstitution, caseAArityExpression, caseAAssertionsMachineClause, caseAAssertionSubstitution, caseAAssignSubstitution, caseAAxiomsContextClause, caseABecomesElementOfSubstitution, caseABecomesSuchSubstitution, caseABinExpression, caseABlockSubstitution, caseABooleanFalseExpression, caseABooleanTrueExpression, caseABoolSetExpression, caseABtreeExpression, caseACardExpression, caseACartesianProductExpression, caseACaseOrSubstitution, caseACaseSubstitution, caseAChoiceOrSubstitution, caseAChoiceSubstitution, caseAClosureExpression, caseACompositionExpression, caseAComprehensionSetExpression, caseAConcatExpression, caseAConcreteVariablesMachineClause, caseAConjunctPredicate, caseAConstantsContextClause, caseAConstantsMachineClause, caseAConstExpression, caseAConstraintsMachineClause, caseAConstructorFreetypeConstructor, caseAConvergentEventstatus, caseAConversionDefinition, caseAConvertBoolExpression, caseACoupleExpression, caseADefArgpattern, caseADeferredSetSet, caseADefineSubstitution, caseADefinitionExpression, caseADefinitionFileParseUnit, caseADefinitionPredicate, caseADefinitionsMachineClause, caseADefinitionSubstitution, caseADescriptionExpression, caseADescriptionPredicate, caseADescriptionSet, caseADirectProductExpression, caseADisjunctPredicate, caseADivExpression, caseADomainExpression, caseADomainRestrictionExpression, caseADomainSubtractionExpression, caseAElementFreetypeConstructor, caseAEmptySequenceExpression, caseAEmptySetExpression, caseAEnumeratedSetSet, caseAEqualPredicate, caseAEquivalencePredicate, caseAEvent, caseAEventBComprehensionSetExpression, caseAEventBContextParseUnit, caseAEventBFirstProjectionExpression, caseAEventBFirstProjectionV2Expression, caseAEventBIdentityExpression, caseAEventBModelParseUnit, caseAEventBSecondProjectionExpression, caseAEventBSecondProjectionV2Expression, caseAEventsModelClause, caseAExistsPredicate, caseAExpressionDefinitionDefinition, caseAExpressionParseUnit, caseAExtendedExprExpression, caseAExtendedPredPredicate, caseAExtendsContextClause, caseAExtendsMachineClause, caseAFalsityPredicate, caseAFatherExpression, caseAFileDefinitionDefinition, caseAFileExpression, caseAFileMachineReference, caseAFin1SubsetExpression, caseAFinitePredicate, caseAFinSubsetExpression, caseAFirstExpression, caseAFirstProjectionExpression, caseAFlooredDivExpression, caseAForallPredicate, caseAForallSubMessageSubstitution, caseAForLoopSubstitution, caseAFreetype, caseAFreetypesMachineClause, caseAFrontExpression, caseAFuncOpSubstitution, caseAFunctionExpression, caseAFunctionOperation, caseAGeneralConcatExpression, caseAGeneralIntersectionExpression, caseAGeneralProductExpression, caseAGeneralSumExpression, caseAGeneralUnionExpression, caseAGeneratedParseUnit, caseAGreaterEqualPredicate, caseAGreaterPredicate, caseAIdentifierExpression, caseAIdentityExpression, caseAIfElsifSubstitution, caseAIfPredicatePredicate, caseAIfSubstitution, caseAIfThenElseExpression, caseAImageExpression, caseAImplementationMachineParseUnit, caseAImplicationPredicate, caseAImportPackage, caseAImportsMachineClause, caseAIncludesMachineClause, caseAInferredUnitExpression, caseAInfixExpression, caseAInitialisationMachineClause, caseAInsertFrontExpression, caseAInsertTailExpression, caseAIntegerExpression, caseAIntegerSetExpression, caseAIntersectionExpression, caseAIntervalExpression, caseAIntSetExpression, caseAInvalidOperationsClauseMachineClause, caseAInvalidSubstitution, caseAInvariantMachineClause, caseAInvariantModelClause, caseAIseq1Expression, caseAIseqExpression, caseAIterationExpression, caseALabelPredicate, caseALambdaExpression, caseALastExpression, caseALeftExpression, caseALessEqualPredicate, caseALessPredicate, caseALetExpressionExpression, caseALetPredicatePredicate, caseALetSubstitution, caseALocalOperationsMachineClause, caseAMachineClauseParseUnit, caseAMachineHeader, caseAMachineMachineVariant, caseAMachineReference, caseAMaxExpression, caseAMaxIntExpression, caseAMemberPredicate, caseAMinExpression, caseAMinIntExpression, caseAMinusExpression, caseAMinusOrSetSubtractExpression, caseAMirrorExpression, caseAMissingSemicolonOperation, caseAModelMachineVariant, caseAModuloExpression, caseAMultilineStringExpression, caseAMultiplicationExpression, caseAMultOrCartExpression, caseANat1SetExpression, caseANatSetExpression, caseANatural1SetExpression, caseANaturalSetExpression, caseANegationPredicate, caseANewUnitExpression, caseANotEqualPredicate, caseANotMemberPredicate, caseANotSubsetPredicate, caseANotSubsetStrictPredicate, caseAOperation, caseAOperationAttribute, caseAOperationCallExpression, caseAOperationCallSubstitution, caseAOperationsMachineClause, caseAOperatorExpression, caseAOperatorPredicate, caseAOperatorSubstitution, caseAOppatternParseUnit, caseAOpSubstitution, caseAOrdinaryEventstatus, caseAOverwriteExpression, caseAPackageParseUnit, caseAParallelProductExpression, caseAParallelSubstitution, caseAParseUnitDefinitionParseUnit, caseAPartialBijectionExpression, caseAPartialFunctionExpression, caseAPartialInjectionExpression, caseAPartialSurjectionExpression, caseAPartitionPredicate, caseAPermExpression, caseAPostfixExpression, caseAPow1SubsetExpression, caseAPowerOfExpression, caseAPowSubsetExpression, caseAPreconditionSubstitution, caseAPredecessorExpression, caseAPredicateAttributeOperationAttribute, caseAPredicateDefinitionDefinition, caseAPredicateFunctionPredicate, caseAPredicateIdentifierPredicate, caseAPredicateParseUnit, caseAPrefixExpression, caseAPrimedIdentifierExpression, caseAPromotesMachineClause, caseAPropertiesMachineClause, caseAProverComprehensionSetExpression, caseAQuantifiedIntersectionExpression, caseAQuantifiedUnionExpression, caseARangeExpression, caseARangeRestrictionExpression, caseARangeSubtractionExpression, caseARankExpression, caseARecEntry, caseARecExpression, caseARecordFieldExpression, caseAReferencesMachineClause, caseARefinementMachineParseUnit, caseARefinesModelClause, caseAReflexiveClosureExpression, caseARelationsExpression, caseARestrictFrontExpression, caseARestrictTailExpression, caseAReverseExpression, caseARevExpression, caseARightExpression, caseARingExpression, caseARuleFailSubSubstitution, caseASecondProjectionExpression, caseASeesMachineClause, caseASeesModelClause, caseASelectSubstitution, caseASelectWhenSubstitution, caseASeq1Expression, caseASeqExpression, caseASequenceExtensionExpression, caseASequenceSubstitution, caseASetExtensionExpression, caseASetsContextClause, caseASetsMachineClause, caseASetSubtractionExpression, caseASizeExpression, caseASizetExpression, caseASkipSubstitution, caseASonExpression, caseASonsExpression, caseAStringExpression, caseAStringSetExpression, caseAStructExpression, caseASubsetPredicate, caseASubsetStrictPredicate, caseASubstitutionDefinitionDefinition, caseASubstitutionParseUnit, caseASubstitutionPredicate, caseASubtreeExpression, caseASuccessorExpression, caseASurjectionRelationExpression, caseASymbolicComprehensionSetExpression, caseASymbolicLambdaExpression, caseASystemMachineVariant, caseATailExpression, caseATheoremsContextClause, caseATheoremsModelClause, caseATopExpression, caseATotalBijectionExpression, caseATotalFunctionExpression, caseATotalInjectionExpression, caseATotalRelationExpression, caseATotalSurjectionExpression, caseATotalSurjectionRelationExpression, caseATransFunctionExpression, caseATransRelationExpression, caseATreeExpression, caseATruthPredicate, caseATypeofExpression, caseAUnaryMinusExpression, caseAUndefArgpattern, caseAUnionExpression, caseAUnitAliasParseUnit, caseAUnitExpression, caseAUsesMachineClause, caseAValuesEntry, caseAValuesMachineClause, caseAVariablesMachineClause, caseAVariablesModelClause, caseAVariantModelClause, caseAVarSubstitution, caseAWhileSubstitution, caseAWitness, caseStart, defaultIn, defaultOut, inAAbstractConstantsContextClause, inAAbstractConstantsMachineClause, inAAbstractMachineParseUnit, inAAddExpression, inAAnticipatedEventstatus, inAAnySubstitution, inAArityExpression, inAAssertionsMachineClause, inAAssertionSubstitution, inAAssignSubstitution, inAAxiomsContextClause, inABecomesElementOfSubstitution, inABecomesSuchSubstitution, inABinExpression, inABlockSubstitution, inABooleanFalseExpression, inABooleanTrueExpression, inABoolSetExpression, inABtreeExpression, inACardExpression, inACartesianProductExpression, inACaseOrSubstitution, inACaseSubstitution, inAChoiceOrSubstitution, inAChoiceSubstitution, inAClosureExpression, inACompositionExpression, inAComprehensionSetExpression, inAComputationOperation, inAConcatExpression, inAConcreteVariablesMachineClause, inAConjunctPredicate, inAConstantsContextClause, inAConstantsMachineClause, inAConstExpression, inAConstraintsMachineClause, inAConstructorFreetypeConstructor, inAConvergentEventstatus, inAConversionDefinition, inAConvertBoolExpression, inACoupleExpression, inADefArgpattern, inADeferredSetSet, inADefineSubstitution, inADefinitionExpression, inADefinitionFileParseUnit, inADefinitionPredicate, inADefinitionsMachineClause, inADefinitionSubstitution, inADescriptionExpression, inADescriptionPredicate, inADescriptionSet, inADirectProductExpression, inADisjunctPredicate, inADivExpression, inADomainExpression, inADomainRestrictionExpression, inADomainSubtractionExpression, inAElementFreetypeConstructor, inAEmptySequenceExpression, inAEmptySetExpression, inAEnumeratedSetSet, inAEqualPredicate, inAEquivalencePredicate, inAEvent, inAEventBComprehensionSetExpression, inAEventBContextParseUnit, inAEventBFirstProjectionExpression, inAEventBFirstProjectionV2Expression, inAEventBIdentityExpression, inAEventBModelParseUnit, inAEventBSecondProjectionExpression, inAEventBSecondProjectionV2Expression, inAEventsModelClause, inAExistsPredicate, inAExpressionDefinitionDefinition, inAExpressionParseUnit, inAExtendedExprExpression, inAExtendedPredPredicate, inAExtendsContextClause, inAExtendsMachineClause, inAFalsityPredicate, inAFatherExpression, inAFileDefinitionDefinition, inAFileExpression, inAFileMachineReference, inAFin1SubsetExpression, inAFinitePredicate, inAFinSubsetExpression, inAFirstExpression, inAFirstProjectionExpression, inAFlooredDivExpression, inAForallPredicate, inAForallSubMessageSubstitution, inAFreetype, inAFreetypesMachineClause, inAFrontExpression, inAFuncOpSubstitution, inAFunctionExpression, inAFunctionOperation, inAGeneralConcatExpression, inAGeneralIntersectionExpression, inAGeneralProductExpression, inAGeneralSumExpression, inAGeneralUnionExpression, inAGeneratedParseUnit, inAGreaterEqualPredicate, inAGreaterPredicate, inAIdentifierExpression, inAIdentityExpression, inAIfElsifSubstitution, inAIfPredicatePredicate, inAIfSubstitution, inAIfThenElseExpression, inAImageExpression, inAImplementationMachineParseUnit, inAImplicationPredicate, inAImportPackage, inAImportsMachineClause, inAIncludesMachineClause, inAInferredUnitExpression, inAInfixExpression, inAInitialisationMachineClause, inAInsertFrontExpression, inAInsertTailExpression, inAIntegerExpression, inAIntegerSetExpression, inAIntersectionExpression, inAIntervalExpression, inAIntSetExpression, inAInvalidOperationsClauseMachineClause, inAInvalidSubstitution, inAInvariantMachineClause, inAInvariantModelClause, inAIseq1Expression, inAIseqExpression, inAIterationExpression, inALabelPredicate, inALambdaExpression, inALastExpression, inALeftExpression, inALessEqualPredicate, inALessPredicate, inALetExpressionExpression, inALetPredicatePredicate, inALetSubstitution, inALocalOperationsMachineClause, inAMachineClauseParseUnit, inAMachineHeader, inAMachineMachineVariant, inAMachineReference, inAMaxExpression, inAMaxIntExpression, inAMemberPredicate, inAMinExpression, inAMinIntExpression, inAMinusExpression, inAMinusOrSetSubtractExpression, inAMirrorExpression, inAMissingSemicolonOperation, inAModelMachineVariant, inAModuloExpression, inAMultilineStringExpression, inAMultiplicationExpression, inAMultOrCartExpression, inANat1SetExpression, inANatSetExpression, inANatural1SetExpression, inANaturalSetExpression, inANegationPredicate, inANewUnitExpression, inANotEqualPredicate, inANotMemberPredicate, inANotSubsetPredicate, inANotSubsetStrictPredicate, inAOperation, inAOperationAttribute, inAOperationCallExpression, inAOperationCallSubstitution, inAOperationsMachineClause, inAOperatorExpression, inAOperatorPredicate, inAOperatorSubstitution, inAOppatternParseUnit, inAOpSubstitution, inAOrdinaryEventstatus, inAOverwriteExpression, inAPackageParseUnit, inAParallelProductExpression, inAParallelSubstitution, inAParseUnitDefinitionParseUnit, inAPartialBijectionExpression, inAPartialFunctionExpression, inAPartialInjectionExpression, inAPartialSurjectionExpression, inAPartitionPredicate, inAPermExpression, inAPostfixExpression, inAPow1SubsetExpression, inAPowerOfExpression, inAPowSubsetExpression, inAPreconditionSubstitution, inAPredecessorExpression, inAPredicateAttributeOperationAttribute, inAPredicateDefinitionDefinition, inAPredicateFunctionPredicate, inAPredicateIdentifierPredicate, inAPredicateParseUnit, inAPrefixExpression, inAPrimedIdentifierExpression, inAPromotesMachineClause, inAPropertiesMachineClause, inAProverComprehensionSetExpression, inAQuantifiedIntersectionExpression, inAQuantifiedUnionExpression, inARangeExpression, inARangeRestrictionExpression, inARangeSubtractionExpression, inARankExpression, inARecEntry, inARecExpression, inARecordFieldExpression, inAReferencesMachineClause, inARefinementMachineParseUnit, inARefinesModelClause, inAReflexiveClosureExpression, inARelationsExpression, inARestrictFrontExpression, inARestrictTailExpression, inAReverseExpression, inARevExpression, inARightExpression, inARingExpression, inARuleFailSubSubstitution, inASecondProjectionExpression, inASeesMachineClause, inASeesModelClause, inASelectSubstitution, inASelectWhenSubstitution, inASeq1Expression, inASeqExpression, inASequenceExtensionExpression, inASequenceSubstitution, inASetExtensionExpression, inASetsContextClause, inASetsMachineClause, inASetSubtractionExpression, inASizeExpression, inASizetExpression, inASkipSubstitution, inASonExpression, inASonsExpression, inAStringExpression, inAStringSetExpression, inAStructExpression, inASubsetPredicate, inASubsetStrictPredicate, inASubstitutionDefinitionDefinition, inASubstitutionParseUnit, inASubstitutionPredicate, inASubtreeExpression, inASuccessorExpression, inASurjectionRelationExpression, inASymbolicComprehensionSetExpression, inASymbolicLambdaExpression, inASystemMachineVariant, inATailExpression, inATheoremsContextClause, inATheoremsModelClause, inATopExpression, inATotalBijectionExpression, inATotalFunctionExpression, inATotalInjectionExpression, inATotalRelationExpression, inATotalSurjectionExpression, inATotalSurjectionRelationExpression, inATransFunctionExpression, inATransRelationExpression, inATreeExpression, inATruthPredicate, inATypeofExpression, inAUnaryMinusExpression, inAUndefArgpattern, inAUnionExpression, inAUnitAliasParseUnit, inAUnitExpression, inAUsesMachineClause, inAValuesEntry, inAValuesMachineClause, inAVariablesMachineClause, inAVariablesModelClause, inAVariantModelClause, inAVarSubstitution, inAWhileSubstitution, inAWitness, inStart, outAAbstractConstantsContextClause, outAAbstractConstantsMachineClause, outAAbstractMachineParseUnit, outAAddExpression, outAAnticipatedEventstatus, outAAnySubstitution, outAArityExpression, outAAssertionsMachineClause, outAAssertionSubstitution, outAAssignSubstitution, outAAxiomsContextClause, outABecomesElementOfSubstitution, outABecomesSuchSubstitution, outABinExpression, outABlockSubstitution, outABooleanFalseExpression, outABooleanTrueExpression, outABoolSetExpression, outABtreeExpression, outACardExpression, outACartesianProductExpression, outACaseOrSubstitution, outACaseSubstitution, outAChoiceOrSubstitution, outAChoiceSubstitution, outAClosureExpression, outACompositionExpression, outAComprehensionSetExpression, outAConcatExpression, outAConcreteVariablesMachineClause, outAConjunctPredicate, outAConstantsContextClause, outAConstantsMachineClause, outAConstExpression, outAConstraintsMachineClause, outAConstructorFreetypeConstructor, outAConvergentEventstatus, outAConversionDefinition, outAConvertBoolExpression, outACoupleExpression, outADefArgpattern, outADeferredSetSet, outADefinitionExpression, outADefinitionFileParseUnit, outADefinitionPredicate, outADefinitionsMachineClause, outADefinitionSubstitution, outADescriptionExpression, outADescriptionPredicate, outADescriptionSet, outADirectProductExpression, outADisjunctPredicate, outADivExpression, outADomainExpression, outADomainRestrictionExpression, outADomainSubtractionExpression, outAElementFreetypeConstructor, outAEmptySequenceExpression, outAEmptySetExpression, outAEnumeratedSetSet, outAEqualPredicate, outAEquivalencePredicate, outAEvent, outAEventBComprehensionSetExpression, outAEventBContextParseUnit, outAEventBFirstProjectionExpression, outAEventBFirstProjectionV2Expression, outAEventBIdentityExpression, outAEventBModelParseUnit, outAEventBSecondProjectionExpression, outAEventBSecondProjectionV2Expression, outAEventsModelClause, outAExistsPredicate, outAExpressionDefinitionDefinition, outAExpressionParseUnit, outAExtendedExprExpression, outAExtendedPredPredicate, outAExtendsContextClause, outAExtendsMachineClause, outAFalsityPredicate, outAFatherExpression, outAFileDefinitionDefinition, outAFileExpression, outAFileMachineReference, outAFin1SubsetExpression, outAFinitePredicate, outAFinSubsetExpression, outAFirstExpression, outAFirstProjectionExpression, outAFlooredDivExpression, outAForallPredicate, outAFreetype, outAFreetypesMachineClause, outAFrontExpression, outAFuncOpSubstitution, outAFunctionExpression, outAGeneralConcatExpression, outAGeneralIntersectionExpression, outAGeneralProductExpression, outAGeneralSumExpression, outAGeneralUnionExpression, outAGeneratedParseUnit, outAGreaterEqualPredicate, outAGreaterPredicate, outAIdentifierExpression, outAIdentityExpression, outAIfElsifSubstitution, outAIfPredicatePredicate, outAIfSubstitution, outAIfThenElseExpression, outAImageExpression, outAImplementationMachineParseUnit, outAImplicationPredicate, outAImportPackage, outAImportsMachineClause, outAIncludesMachineClause, outAInferredUnitExpression, outAInfixExpression, outAInitialisationMachineClause, outAInsertFrontExpression, outAInsertTailExpression, outAIntegerExpression, outAIntegerSetExpression, outAIntersectionExpression, outAIntervalExpression, outAIntSetExpression, outAInvalidOperationsClauseMachineClause, outAInvalidSubstitution, outAInvariantMachineClause, outAInvariantModelClause, outAIseq1Expression, outAIseqExpression, outAIterationExpression, outALabelPredicate, outALambdaExpression, outALastExpression, outALeftExpression, outALessEqualPredicate, outALessPredicate, outALetExpressionExpression, outALetPredicatePredicate, outALetSubstitution, outALocalOperationsMachineClause, outAMachineClauseParseUnit, outAMachineHeader, outAMachineMachineVariant, outAMachineReference, outAMaxExpression, outAMaxIntExpression, outAMemberPredicate, outAMinExpression, outAMinIntExpression, outAMinusExpression, outAMinusOrSetSubtractExpression, outAMirrorExpression, outAMissingSemicolonOperation, outAModelMachineVariant, outAModuloExpression, outAMultilineStringExpression, outAMultiplicationExpression, outAMultOrCartExpression, outANat1SetExpression, outANatSetExpression, outANatural1SetExpression, outANaturalSetExpression, outANegationPredicate, outANewUnitExpression, outANotEqualPredicate, outANotMemberPredicate, outANotSubsetPredicate, outANotSubsetStrictPredicate, outAOperation, outAOperationAttribute, outAOperationCallExpression, outAOperationCallSubstitution, outAOperationsMachineClause, outAOperatorSubstitution, outAOppatternParseUnit, outAOpSubstitution, outAOrdinaryEventstatus, outAOverwriteExpression, outAPackageParseUnit, outAParallelProductExpression, outAParallelSubstitution, outAParseUnitDefinitionParseUnit, outAPartialBijectionExpression, outAPartialFunctionExpression, outAPartialInjectionExpression, outAPartialSurjectionExpression, outAPartitionPredicate, outAPermExpression, outAPostfixExpression, outAPow1SubsetExpression, outAPowerOfExpression, outAPowSubsetExpression, outAPreconditionSubstitution, outAPredecessorExpression, outAPredicateAttributeOperationAttribute, outAPredicateDefinitionDefinition, outAPredicateFunctionPredicate, outAPredicateIdentifierPredicate, outAPredicateParseUnit, outAPrefixExpression, outAPrimedIdentifierExpression, outAPromotesMachineClause, outAPropertiesMachineClause, outAProverComprehensionSetExpression, outAQuantifiedIntersectionExpression, outAQuantifiedUnionExpression, outARangeExpression, outARangeRestrictionExpression, outARangeSubtractionExpression, outARankExpression, outARecEntry, outARecExpression, outARecordFieldExpression, outAReferencesMachineClause, outARefinementMachineParseUnit, outARefinesModelClause, outAReflexiveClosureExpression, outARelationsExpression, outARestrictFrontExpression, outARestrictTailExpression, outAReverseExpression, outARevExpression, outARightExpression, outARingExpression, outASecondProjectionExpression, outASeesMachineClause, outASeesModelClause, outASelectSubstitution, outASelectWhenSubstitution, outASeq1Expression, outASeqExpression, outASequenceExtensionExpression, outASequenceSubstitution, outASetExtensionExpression, outASetsContextClause, outASetsMachineClause, outASetSubtractionExpression, outASizeExpression, outASizetExpression, outASkipSubstitution, outASonExpression, outASonsExpression, outAStringExpression, outAStringSetExpression, outAStructExpression, outASubsetPredicate, outASubsetStrictPredicate, outASubstitutionDefinitionDefinition, outASubstitutionParseUnit, outASubstitutionPredicate, outASubtreeExpression, outASuccessorExpression, outASurjectionRelationExpression, outASymbolicComprehensionSetExpression, outASymbolicLambdaExpression, outASystemMachineVariant, outATailExpression, outATheoremsContextClause, outATheoremsModelClause, outATopExpression, outATotalBijectionExpression, outATotalFunctionExpression, outATotalInjectionExpression, outATotalRelationExpression, outATotalSurjectionExpression, outATotalSurjectionRelationExpression, outATransFunctionExpression, outATransRelationExpression, outATreeExpression, outATruthPredicate, outATypeofExpression, outAUnaryMinusExpression, outAUndefArgpattern, outAUnionExpression, outAUnitAliasParseUnit, outAUnitExpression, outAUsesMachineClause, outAValuesEntry, outAValuesMachineClause, outAVariablesMachineClause, outAVariablesModelClause, outAVariantModelClause, outAVarSubstitution, outAWhileSubstitution, outAWitnesscaseEOF, caseTAbstractConstants, caseTAbstractVariables, caseTAny, caseTArity, caseTAssert, caseTAssertions, caseTAssign, caseTBe, caseTBegin, caseTBfalse, caseTBin, caseTBool, caseTBoolCast, caseTBtree, caseTCard, caseTCase, caseTChoice, caseTClosure, caseTClosure1, caseTComma, caseTComment, caseTCommentBody, caseTCommentEnd, caseTConc, caseTConcatSequence, caseTConcreteConstants, caseTConcreteVariables, caseTConjunction, caseTConst, caseTConstants, caseTConstraints, caseTDefinitions, caseTDefLiteralPredicate, caseTDefLiteralSubstitution, caseTDirectProduct, caseTDivision, caseTDo, caseTDollar, caseTDom, caseTDomainRestriction, caseTDomainSubtraction, caseTDot, caseTDoubleColon, caseTDoubleEqual, caseTDoubleVerticalBar, caseTEither, caseTElementOf, caseTElse, caseTElsif, caseTEmptySet, caseTEnd, caseTEqual, caseTEquivalence, caseTExists, caseTExtends, caseTFalse, caseTFather, caseTFin, caseTFin1, caseTFirst, caseTFnc, caseTForAny, caseTFront, caseTGeneralizedInter, caseTGeneralizedUnion, caseTGreater, caseTGreaterEqual, caseTHexLiteral, caseTId, caseTIdentifierLiteral, caseTIf, caseTImplementation, caseTImplies, caseTImports, caseTIn, caseTIncludes, caseTInclusion, caseTInfix, caseTInitialisation, caseTInsertEndSequence, caseTInsertStartSequence, caseTInt, caseTInteger, caseTIntegerLiteral, caseTIntersection, caseTInterval, caseTInvariant, caseTIpragmaUnit, caseTIseq, caseTIseq1, caseTIterate, caseTKwAbstractConstants, caseTKwAbstractVariables, caseTKwAssertions, caseTKwAttributeIdentifier, caseTKwBody, caseTKwComputation, caseTKwConcreteConstants, caseTKwConcreteVariables, caseTKwConstants, caseTKwConstraints, caseTKwCounterexample, caseTKwDefine, caseTKwDefinition, caseTKwDefinitions, caseTKwDummyValue, caseTKwExpect, caseTKwExpression, caseTKwExpressionOperator, caseTKwExtends, caseTKwFor, caseTKwFormula, caseTKwFreetypes, caseTKwFunction, caseTKwImports, caseTKwIncludes, caseTKwInitialisation, caseTKwInvariant, caseTKwLocalOperations, caseTKwMachineClause, caseTKwOperations, caseTKwOppattern, caseTKwPredicate, caseTKwPredicateAttribute, caseTKwPredicateOperator, caseTKwPromotes, caseTKwProperties, caseTKwReferences, caseTKwRule, caseTKwRuleErrorType, caseTKwRuleFail, caseTKwRuleForAll, caseTKwRulesMachine, caseTKwSees, caseTKwSets, caseTKwSubstitution, caseTKwSubstitutionOperator, caseTKwType, caseTKwUses, caseTKwValue, caseTKwValues, caseTKwVariables, caseTLambda, caseTLast, caseTLeft, caseTLeftBrace, caseTLeftBracket, caseTLeftPar, caseTLess, caseTLessEqual, caseTLet, caseTLineComment, caseTLocalOperations, caseTLogicalOr, caseTMachine, caseTMaplet, caseTMax, caseTMaxInt, caseTMin, caseTMinInt, caseTMinus, caseTMirror, caseTMod, caseTModel, caseTMultilineStringContent, caseTMultilineStringEnd, caseTMultilineStringStart, caseTNat, caseTNat1, caseTNatural, caseTNatural1, caseTNewPragmaUnit, caseTNonInclusion, caseTNot, caseTNotBelonging, caseTNotEqual, caseTOf, caseTOperations, caseTOr, caseTOutputParameters, caseTOverwriteRelation, caseTPartialBijection, caseTPartialFunction, caseTPartialInjection, caseTPartialSurjection, caseTPerm, caseTPi, caseTPlus, caseTPostfix, caseTPow, caseTPow1, caseTPowerOf, caseTPragmaConversion, caseTPragmaDescription, caseTPragmaEnd, caseTPragmaFile, caseTPragmaFreeText, caseTPragmaGenerated, caseTPragmaIdOrString, caseTPragmaImportPackage, caseTPragmaLabel, caseTPragmaPackage, caseTPragmaStart, caseTPragmaSymbolic, caseTPragmaUnit, caseTPragmaUnitAlias, caseTPre, caseTPred, caseTPredicateIdentifier, caseTPrefix, caseTPrj1, caseTPrj2, caseTProduct, caseTPromotes, caseTProperties, caseTQuantifiedInter, caseTQuantifiedSet, caseTQuantifiedUnion, caseTRan, caseTRangeRestriction, caseTRangeSubtraction, caseTRank, caseTRec, caseTRefinement, caseTRefines, caseTRel, caseTRestrictHeadSequence, caseTRestrictTailSequence, caseTRev, caseTRight, caseTRightBrace, caseTRightBracket, caseTRightPar, caseTSees, caseTSelect, caseTSemicolon, caseTSeq, caseTSeq1, caseTSetRelation, caseTSets, caseTSetSubtraction, caseTShebang, caseTShebangChar, caseTShebangEnd, caseTSigma, caseTSingleQuotation, caseTSize, caseTSizet, caseTSkip, caseTSlash, caseTSon, caseTSons, caseTStar, caseTStrictInclusion, caseTStrictNonInclusion, caseTString, caseTStringLiteral, caseTStruct, caseTSubtree, caseTSucc, caseTSurjectionRelation, caseTSystem, caseTTail, caseTThen, caseTTilde, caseTTop, caseTTotalBijection, caseTTotalFunction, caseTTotalInjection, caseTTotalRelation, caseTTotalSurjection, caseTTotalSurjectionRelation, caseTTree, caseTTrue, caseTTruthPredicate, caseTUnderscore, caseTUnion, caseTUnitContent, caseTUnitId, caseTUses, caseTValue, caseTVar, caseTVariables, caseTVariant, caseTVerticalBar, caseTWhen, caseTWhere, caseTWhile, caseTWhiteSpace, defaultCase, getIn, getOut, setIn, setOutpublic static final java.lang.String RULE_FAIL
public static final java.lang.String RULE_SUCCESS
public static final java.lang.String RULE_NOT_CHECKED
public static final java.lang.String RULE_DISABLED
public static final java.lang.String COMPUTATION_EXECUTED
public static final java.lang.String COMPUTATION_NOT_EXECUTED
public static final java.lang.String COMPUTATION_DISABLED
public static final java.lang.String RULE_RESULT_OUTPUT_PARAMETER_NAME
public static final java.lang.String RULE_COUNTEREXAMPLE_OUTPUT_PARAMETER_NAME
public static final java.lang.String RULE_COUNTER_EXAMPLE_VARIABLE_SUFFIX
public RulesTransformation(Start start, BParser bParser, RulesMachineChecker rulesMachineChecker, java.util.Map<java.lang.String,AbstractOperation> allOperations)
start - The root node of the abstract syntax tree.bParser - The parser of the rules machine.rulesMachineChecker - the rules machine checker which has already analyzed the rules
machineallOperations - The list of all operation in the project. This parameter is
needed in order to detect invalid reference to operations
which does not exist. Note, that such checks can not be done
by the RulesMachineChecker because they need more than
the machine scope. For example, it is checked that the first
argument of the GET_RULE_COUNTEREXAMPLES operator is an
existing rule operation which may be located in another rules
machine.public void runTransformation()
throws BCompoundException
BCompoundExceptionpublic java.util.List<AbstractOperation> getOperations()
public java.util.List<java.lang.String> getComputations()
public void outStart(Start node)
outStart in class DepthFirstAdapterpublic void caseAComputationOperation(AComputationOperation node)
caseAComputationOperation in interface AnalysiscaseAComputationOperation in class DepthFirstAdapterpublic java.util.List<PPredicate> getOperationDependenciesAsPredicateList(AbstractOperation operation)
public void outAComputationOperation(AComputationOperation node)
outAComputationOperation in class DepthFirstAdapterpublic void caseARuleOperation(ARuleOperation node)
caseARuleOperation in interface AnalysiscaseARuleOperation in class DepthFirstAdapterpublic void inARuleOperation(ARuleOperation node)
inARuleOperation in class DepthFirstAdapterpublic void outARuleOperation(ARuleOperation node)
outARuleOperation in class DepthFirstAdapterpublic void outAOperatorExpression(AOperatorExpression node)
outAOperatorExpression in class DepthFirstAdapterpublic void outADefineSubstitution(ADefineSubstitution node)
outADefineSubstitution in class DepthFirstAdapterpublic void outAFunctionOperation(AFunctionOperation node)
outAFunctionOperation in class DepthFirstAdapterpublic void outAOperatorPredicate(AOperatorPredicate node)
outAOperatorPredicate in class DepthFirstAdapterpublic void inAForLoopSubstitution(AForLoopSubstitution node)
inAForLoopSubstitution in class DepthFirstAdapterpublic void outAForLoopSubstitution(AForLoopSubstitution node)
outAForLoopSubstitution in class DepthFirstAdapterpublic void outARuleFailSubSubstitution(ARuleFailSubSubstitution node)
outARuleFailSubSubstitution in class DepthFirstAdapterpublic PSubstitution createCounterExampleSubstitutions(java.util.List<PExpression> identifiers, PPredicate wherePredicate, PPredicate expectPredicate, PExpression message, TIntegerLiteral errorTypeNode)
public void outAForallSubMessageSubstitution(AForallSubMessageSubstitution node)
outAForallSubMessageSubstitution in class DepthFirstAdapter